Abstract: This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably provide ETR-completeness results for distinct variants of this problem. Furthermore, we provide insights in the functions describing the induced reachability probabilities, and how pMDPs generalise concurrent stochastic reachability games.

DOI: 10.4230/LIPIcs.CONCUR.2019.14

Abstract: The decidability and complexity of reachability problems and model-checking for flat counter systems have been explored in detail. However, only few results are known for flat FIFO systems, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO systems, generalizing similar existing results for flat counter systems. We construct a trace-flattable counter system that is bisimilar to a given flat FIFO system, which allows to model-check the original flat FIFO system. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO systems based on analysis of flat subsystems.

DOI: 10.4230/LIPIcs.CONCUR.2019.12

Abstract: Limit-average automata are weighted automata on infinite words that use average to aggregate the weights seen in infinite runs. We study approximate learning problems for limit-average automata in two settings: passive and active. In the passive learning case, we show that limit-average automata are not PAC-learnable as samples must be of exponential-size to provide (with good probability) enough details to learn an automaton. We also show that the problem of finding an automaton that fits a given sample is NP-complete.

In the active learning case, we show that limit-average automata can be learned almost-exactly, i.e., we can learn in polynomial time an automaton that is consistent with the target automaton on almost all words. On the other hand, we show that the problem of learning an automaton that approximates the target automaton (with perhaps fewer states) is NP-complete. The abovementioned results are shown for the uniform distribution on words. We briefly discuss learning over different distributions.

DOI: 10.4230/LIPIcs.CONCUR.2019.17

Abstract: The window mechanism was introduced by Chatterjee et al. [1] to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games, thanks to the ability to reason about such time bounds in system specifications, but also the increased tractability that it usually yields.
In this work, we extend the window framework to stochastic environments by considering the fundamental threshold probability problem in Markov decision processes for window objectives. That is, given such an objective, we want to synthesize strategies that guarantee satisfying runs with a given probability. We solve this problem for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.
[1] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at mean-payoff and total-payoff through windows. Inf. Comput., 242:25-52, 2015.

DOI: 10.4230/LIPIcs.CONCUR.2019.8

Abstract: In this paper we consider the reachability problem for bounded branching VASS. Bounded VASS are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the input. This model gained a lot of attention in 2012 when Haase et al. showed its connections with timed automata. Later in 2013 Fearnley and Jurdziński proved that the reachability problem in this model is PSPACE-complete even in dimension 1. Here, we investigate the complexity of the reachability problem when the model is extended with branching transitions, and we prove that the problem is EXPTIME-complete when the dimension is 2 or larger.

DOI: 10.4230/LIPIcs.CONCUR.2019.28

Abstract: A vector addition system with states (VASS) consists of a finite set of states and counters.
A configuration is a state and a value for each counter;
a transition changes the state and each counter is incremented, decremented, or left unchanged.
While qualitative properties such as state and configuration reachability have been studied for VASS,
we consider the long-run average cost of infinite computations of VASS.
The cost of a configuration is for each state, a linear combination of the counter values.
In the special case of uniform cost functions, the linear combination is the same for all states.
The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value,
if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold.
For uniform cost functions, we show that the regular long-run emptiness problem is
(a)~decidable in polynomial time for integer-valued VASS, and
(b)~decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters) and non-zero cost functions.
For general cost functions, we show that the problem is
(c)~NP-complete for integer-valued VASS, and
(d)~undecidable for natural-valued VASS.
Our most interesting result is for (c) integer-valued VASS with general cost functions,
where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities.
The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c),
where it remains open.

DOI: 10.4230/LIPIcs.CONCUR.2019.27

Abstract: In distributed synthesis, we generate a set of process implementations that, together, accomplish an objective against all possible behaviors of the environment. A lot of recent work has focussed on systems with causal memory, i.e., sets of asynchronous processes that exchange their causal histories upon synchronization. Decidability results for this problem have been stated either in terms of control games, which extend Zielonka's asynchronous automata by partitioning the actions into controllable and uncontrollable, or in terms of Petri games, which extend Petri nets by partitioning the tokens into system and environment players. The precise connection between these two models was so far, however, an open question.

In this paper, we provide the first formal connection between control games and Petri games. We establish the equivalence of two games based on weak bisimulations between their strategies. For both directions, we show that a game of one type can be translated into an equivalent game of the other type. We provide exponential upper and lower bounds for the translations. Our translations make it possible to transfer and combine decidability results between the two types of games. Exemplarily, we translate decidability in acyclic communication architectures, originally obtained for control games, to Petri games, and decidability in single-process systems, originally obtained for Petri games, to control games.

DOI: 10.4230/LIPIcs.CONCUR.2019.26

Abstract: Population protocols are a formal model of computation by identical, anonymous mobile agents interacting in pairs. Their computational power is rather limited: Angluin et al. have shown that they can only compute the predicates over N^k expressible in Presburger arithmetic. For this reason, several extensions of the model have been proposed, including the addition of devices called cover-time services, absence detectors, and clocks. All these extensions increase the expressive power to the class of predicates over N^k lying in the complexity class NL when the input is given in unary. However, these devices are difficult to implement, since they require that an agent atomically receives messages from all other agents in a population of unknown size; moreover, the agent must know that they have all been received. Inspired by the work of the verification community on Emerson and Namjoshi's broadcast protocols, we show that NL-power is also achieved by extending population protocols with reliable broadcasts, a simpler, standard communication primitive.

DOI: 10.4230/LIPIcs.CONCUR.2019.31

Abstract: Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. However, when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with expected axioms for reasoning about concurrency lead to an unexpected equation. In this paper, we propose Kleene algebra with observations (KAO), a variant of KAT, as an alternative foundation for extending KAT to a concurrent setting. We characterise the free model of KAO, and establish a decision procedure w.r.t. its equational theory.

DOI: 10.4230/LIPIcs.CONCUR.2019.41

Abstract: In this paper, we study one-player and two-player energy mean-payoff games. Energy mean-payoff games are games of infinite duration played on a finite graph with edges labeled by 2-dimensional weight vectors. The objective of the first player (the protagonist) is to satisfy an energy objective on the first dimension and a mean-payoff objective on the second dimension. We show that optimal strategies for the first player may require infinite memory while optimal strategies for the second player (the antagonist) do not require memory. In the one-player case (where only the first player has choices), the problem of deciding who is the winner can be solved in polynomial time while for the two-player case we show co-NP membership and we give effective constructions for the infinite-memory optimal strategies of the protagonist.

DOI: 10.4230/LIPIcs.CONCUR.2019.21

Abstract: In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent, for example, the monetary value expressed in cents. We study, for the first time, the combination of {\em discrete-bidding} and {\em infinite-duration} games. Our most important result proves that these games form a large determined subclass of concurrent games, where {\em determinacy} is the strong property that there always exists exactly one player who can guarantee winning the game. In particular, we show that, in contrast to non-discrete bidding games, the mechanism with which tied bids are resolved plays an important role in discrete-bidding games. We study several natural tie-breaking mechanisms and show that, while some do not admit determinacy, most natural mechanisms imply determinacy for every pair of initial budgets.

DOI: 10.4230/LIPIcs.CONCUR.2019.20

Abstract: We study multiplayer quantitative reachability games played on a finite directed graph, where the objective of each player is to reach his target set of vertices as quickly as possible. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. It is known that there always exists an SPE in quantitative reachability games and that the constrained existence problem is decidable. We here prove that this problem is PSPACE-complete. To obtain this result, we propose a new algorithm that iteratively builds a set of constraints characterizing the set of SPE outcomes in quantitative reachability games. This set of constraints is obtained by iterating an operator that reinforces the constraints up to obtaining a fixpoint. With this fixpoint, the set of SPE outcomes can be represented by a finite graph of size at most exponential. A careful inspection of the computation allows us to establish PSPACE membership.

DOI: 10.4230/LIPIcs.CONCUR.2019.13

Abstract: Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behavior but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with such a negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; such a tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm and we apply it to many examples that cannot be managed with the previous approaches.

DOI: 10.4230/LIPIcs.CONCUR.2019.38

Abstract: Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (iii) an unbounded number of asynchronous rounds. This combination makes verification hard. Challenge (i) was recently addressed in the framework of threshold automata. We extend threshold automata to model randomized algorithms that perform an unbounded number of asynchronous rounds. For non-probabilistic properties, we show that it is necessary and sufficient to verify these properties under round-rigid schedules, that is, schedules where no process enters round r before all other processes finished round r-1. For almost-sure termination, we analyze these algorithms under round-rigid adversaries, that is, fair adversaries that only generate round-rigid schedules. This allows us to do compositional and inductive reasoning that reduces verification of the asynchronous multi-round algorithms to model checking of a one-round threshold automaton. We apply this framework and automatically verify the following classic algorithms: Ben-Or's and Bracha's seminal consensus algorithms for crashes and Byzantine faults, 2-set agreement for crash faults, and RS-Bosco for the Byzantine case.

DOI: 10.4230/LIPIcs.CONCUR.2019.33

Abstract: The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often.
All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification.
Consider graphs/MDPs with n vertices, m edges, and a Streett objective with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants.
The current best-known algorithm for the problem requires time O(min(n^2, m sqrt(m log n)) + b log n).
In this work, we present randomized near-linear time algorithms, with expected running time \widetilde{O}(m + b), where the \widetilde{O} notation hides poly-log factors.
Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors.

DOI: 10.4230/LIPIcs.CONCUR.2019.7

Abstract: State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the particular case of labelled transition systems, these equivalences range from trace equivalence to (strong) bisimilarity, and are organized in what is known as the linear time - branching time spectrum. A combination of universal coalgebra and graded monads provides a generic framework in which the semantics of concurrency can be parametrized both over the branching type of the underlying transition systems and over the granularity of process equivalence. We show in the present paper that this framework of graded semantics does subsume the most important equivalences from the linear time - branching time spectrum. An important feature of graded semantics is that it allows for the principled extraction of characteristic modal logics. We have established invariance of these graded logics under the given graded semantics in earlier work; in the present paper, we extend the logical framework with an explicit propositional layer and provide a generic expressiveness criterion that generalizes the classical Hennessy-Milner theorem to coarser notions of process equivalence. We extract graded logics for a range of graded semantics on labelled transition systems and probabilistic systems, and give exemplaric proofs of their expressiveness based on our generic criterion.

DOI: 10.4230/LIPIcs.CONCUR.2019.36

Abstract: In the context of models with mixed nondeterministic and probabilistic choice, we present a concurrent model based on partial orders, or more precisely Winskel's event structures. We study its relationship with the interleaving based model of Segala's probabilistic automata. Lastly, we use this model to give a truly concurrent semantics to an extension of CCS with probabilistic choice, and relate this concurrent semantics to the usual interleaving semantics, thus generalising existing results with CCS, event structures and labelled transition systems.

DOI: 10.4230/LIPIcs.CONCUR.2019.11

Abstract: In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals (ω-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite. In this paper, we do not make such an assumption and consider data ω-words instead, i.e., words over an infinite alphabet. In this context, we study specifications and implementations respectively given as automata and transducers extended with a finite set of registers. We consider different instances, depending on whether the specification is nondeterministic, universal or deterministic, and depending on whether the number of registers of the implementation is given (bounded synthesis) or not.

In the unbounded setting, we show undecidability for both universal and non-deterministic specifications, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but can be recovered by disallowing tests over input data. The generic technique we use to show the latter result allows us to reprove some known result, namely decidability of bounded synthesis for universal specifications.

DOI: 10.4230/LIPIcs.CONCUR.2019.24

Abstract: Distributed storage systems and databases are widely used by various types of applications. Transactional access to these storage systems is an important abstraction allowing application programmers to consider blocks of actions (i.e., transactions) as executing atomically. For performance reasons, the consistency models implemented by modern databases are weaker than the standard serializability model, which corresponds to the atomicity abstraction of transactions executing over a sequentially consistent memory. Causal consistency for instance is one such model that is widely used in practice.

In this paper, we investigate application-specific relationships between several variations of causal consistency and we address the issue of verifying automatically if a given transactional program is robust against causal consistency, i.e., all its behaviors when executed over an arbitrary causally consistent database are serializable. We show that programs without write-write races have the same set of behaviors under all these variations, and we show that checking robustness is polynomial time reducible to a state reachability problem in transactional programs over a sequentially consistent shared memory. A surprising corollary of the latter result is that causal consistency variations which admit incomparable sets of behaviors admit comparable sets of robust programs. This reduction also opens the door to leveraging existing methods and tools for the verification of concurrent programs (assuming sequential consistency) for reasoning about programs running over causally consistent databases. Furthermore, it allows to establish that the problem of checking robustness is decidable when the programs executed at different sites are finite-state.

DOI: 10.4230/LIPIcs.CONCUR.2019.30

Abstract: Broadcast networks allow one to model networks of identical nodes communicating through message broadcasts. Their parameterized verification aims at proving a property holds for any number of nodes, under any communication topology, and on all possible executions. We focus on the coverability problem which dually asks whether there exists an execution that visits a configuration exhibiting some given state of the broadcast protocol. Coverability is known to be undecidable for static networks, i.e. when the number of nodes and communication topology is fixed along executions. In contrast, it is decidable in PTIME when the communication topology may change arbitrarily along executions, that is for reconfigurable networks. Surprisingly, no lower nor upper bounds on the minimal number of nodes, or the minimal length of covering execution in reconfigurable networks, appear in the literature. In this paper we show tight bounds for cutoff and length, which happen to be linear and quadratic, respectively, in the number of states of the protocol. We also introduce an intermediary model with static communication topology and non-deterministic message losses upon sending. We show that the same tight bounds apply to lossy networks, although, reconfigurable executions may be linearly more succinct than lossy executions. Finally, we show NP-completeness for the natural optimisation problem associated with the cutoff.

DOI: 10.4230/LIPIcs.CONCUR.2019.32

Abstract: Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with (context-free) branching rules, and as such may be used to model networks of independent timed automata with process creation. We show that the coverability and reachability problems (with unary encoded target multiplicities) are PSPACE-complete and EXPTIME-complete, respectively. For the special case of 1-clock TBPP, both are NP-complete and hence not more complex than for untimed BPP. This contrasts with known super-Ackermannian-completeness and undecidability results for general timed Petri nets. As a result of independent interest, and basis for our NP upper bounds, we show that the reachability relation of 1-clock TA can be expressed by a formula of polynomial size in the existential fragment of linear arithmetic, which improves on recent results from the literature.

DOI: 10.4230/LIPIcs.CONCUR.2019.15

Abstract: A word automaton recognizing a language L is good for games (GFG) if its composition with any game whose winning condition is L preserves the game's winner. Deterministic automata are GFG, while nondeterministic automata are generally not. There are various other properties that are used in the literature for defining that a nondeterministic automaton is GFG, including ``history deterministic'', ``compliant with some letter game'', ``good for trees'', and ``good for composition with other automata''. Yet, it is not formally shown that all of these properties are equivalent.

We clarify the different definitions of GFG automata and prove that they are all indeed equivalent. In the setting of alternating automata, so far only some of the above definitions have been considered. We generalize the other definitions and prove that they all remain equivalent.

We further look into alternating GFG automata, showing that they are as expressive as deterministic automata with the same acceptance conditions and indices. Considering their succinctness, we show that alternating GFG automata over finite words, as well as weak automata over infinite words, are not more succinct than deterministic automata, and that determinizing Buchi and co-Buchi alternating GFG automata involves a 2^\Theta(n) state blow-up. We leave open the question of whether alternating GFG automata of stronger acceptance conditions allow for doubly-exponential succinctness compared to deterministic automata.

DOI: 10.4230/LIPIcs.CONCUR.2019.19

Abstract: In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we study the design of incentives so that a desirable equilibrium is obtained, for instance, an equilibrium satisfying a given temporal logic property -- a problem that we call equilibrium design. We base our study on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players' goals as mean-payoff objectives. In particular, we consider system specifications given by LTL and GR(1) formulae, and show that implementing a mechanism to ensure that a given temporal logic property is satisfied on some/every Nash equilibrium of the game, whenever such a mechanism exists, can be done in PSPACE for LTL properties and in NP / Sigma^P_2 for GR(1) specifications. We also study the complexity of various related decision and optimisation problems, such as optimality and uniqueness of solutions, and show that the complexities of all such problems lie within the polynomial hierarchy. As an application, equilibrium design can be used as an alternative answer to the rational synthesis and verification problems for concurrent games with mean-payoff objectives whenever no solution exists, or as a technique to repair, whenever possible, concurrent games with undesirable rational outcomes (Nash equilibria) in an optimal way.

DOI: 10.4230/LIPIcs.CONCUR.2019.22

Abstract: Traditional synthesis algorithms return, given a specification over finite sets of input and output Boolean variables, a finite-state transducer all whose computations satisfy the specification. Many real-life systems have an infinite state space. In particular, behaviors of systems with a finite control yet variables that range over infinite domains, are specified by automata with infinite alphabets. A register automaton has a finite set of registers, and its transitions are based on a comparison of the letters in the input with these stored in its registers. Unfortunately, reasoning about register automata is complex. In particular, the synthesis problem for specifications given by register automata, where the goal is to generate correct register transducers, is undecidable.
We study of the synthesis problem for systems with a bounded number of registers. Formally, the register- bounded realizability problem is to decide, given a specification register automaton A over infinite input and output alphabets and numbers k_s and k_e of registers, whether there is a system transducer T with at most k_s registers such that for all environment transducers T' with at most k_e registers, the computation T || T', generated by the interaction of T with T', satisfies the specification A. The register-bounded synthesis problem is to construct such a transducer T, if exists. As has been the case with bounded synthesis in the finite-state setting, the motivation for the study is both conceptual and computational: First, the bounded setting captures better scenarios where bounds on the the systems and/or its environment are known. Second, the bounds are the key to new synthesis algorithms, and, as recently shown in [18], in the case of systems with an infinite data domain, they lead to decidability. Our main contributions include simpler algorithms, which enables a clean complexity analysis, a study of settings in which both the system and the environment are bounded, and a study of the theoretical aspects of the setting, in particular the differences between infinitely many registers and finitely yet unboundedly many ones, and the determinacy of the corresponding games.

DOI: 10.4230/LIPIcs.CONCUR.2019.25

Abstract: An improved translation from alternating parity automata on infinite words to alternating weak automata is given. The blow-up of the number of states is related to the size of the smallest universal ordered trees and hence it is quasi-polynomial, and only polynomial if the asymptotic number of priorities is logarithmic in the number of states. This is an exponential improvement on the translation of Kupferman and Vardi (2001) and a quasi-polynomial improvement on the translation of Boker and Lehtinen (2018). Any slightly better such translation would (if---like all presently known such translations---it is efficiently constructive) lead to algorithms for solving parity games that are asymptotically faster in the worst case than the current state of the art (Calude, Jain, Khoussainov, Li, and Stephan, 2017; Jurdziński and Lazi\'c, 2017; and Fearnley, Jain, Schewe, Stephan, and Wojtczak, 2017), and hence it would yield a significant breakthrough.

DOI: 10.4230/LIPIcs.CONCUR.2019.18

Abstract: We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains.

These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Typing also ensures that processes only communicate with accessible domains and so respect the accessibility relation.

Remarkably, our domain-aware framework can specify scenarios in which domain information is available only at runtime; flexible accessibility relations can be cleanly defined and statically enforced.

As a specific application, we introduce domain-aware multiparty session types, in which global protocols can express arbitrarily nested sub-protocols via domain migration. We develop a precise analysis of these multiparty protocols by reduction to our binary domain-aware framework: complex domain-aware protocols can be reasoned about at the right level of abstraction, ensuring also the principled transfer of key correctness properties from the binary to the multiparty setting.

DOI: 10.4230/LIPIcs.CONCUR.2019.39

Abstract: Spatial constraint systems (scs) are semantic structures from concurrent constraint programming (ccp). They are used in the operational semantics of ccp to represent the spatial distribution of information, i.e., the spatial memory (or store), at each step of a program run. Their underlying theory and properties have also been used for reasoning about spatial information, belief, knowledge in concurrent systems.

Nevertheless, scs are confined to a finite number of agents and to reasoning about agents individually rather than as a group. Reasoning about groups includes fundamental issues such as being able to predict that the members of a group may reach information, potentially inconsistent or unwanted, collectively rather than individually. Allowing infinite agents is particularly important when reasoning about groups in situations where the number of agents in a group is unbounded or not known a priori (e.g., social networks).

In this paper we shall develop a scs-based semantic structure, to reason about the distributed information of potentially \emph{infinite groups}. In particular, we will characterize the information of a group of agents as the infimum of the set of join-preserving functions that represent the spaces of the agents in the group. We will also provide an alternative characterization of group information as greatest family of join preserving functions that satisfy certain basic properties. We will also show compositionally results for group information. We will exploit these compositionality results to produce algorithms to compute group information. Finally we will show that some existing formalisms for distributed reasoning in economy and epistemic logic are instances of our semantic structure.

DOI: 10.4230/LIPIcs.CONCUR.2019.29

Abstract: The bialgebraic semantics of Turi and Plotkin is an abstract approach to specifying the operational semantics of a system, by means of a distributive law between its syntax (encoded as a monad) and its dynamics (encoded as an endofunctor). This setup is instrumental in showing that a semantic specification (encoded as a coalgebra) satisfies desirable properties: in particular, that it is compositional.

In this work, we use the bialgebraic approach to derive well-behaved structural operational semantics of \emph{string diagrams}, a graphical syntax that is increasingly used in the study of interacting systems across different disciplines. Our analysis relies on the formal theory of monads by Street and Lack to represent the two-dimensional operations underlying string diagrams as a monad in a certain bicategory, and their bialgebraic semantics in terms of a distributive law internal to that bicategory.

As a proof of concept, we provide biaglebraic compositional semantics for a versatile string diagrammatic language which has been used to model both signal flow graphs (control theory) and Petri nets (concurrency theory). Moreover, our approach reveals a correspondence between two different interpretations of the Frobenius equations on string diagrams and two synchronisation mechanisms for processes, à la Hoare and à la Milner.

DOI: 10.4230/LIPIcs.CONCUR.2019.37

Abstract: We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability~1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP and in co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP and in co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to the combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games.

DOI: 10.4230/LIPIcs.CONCUR.2019.6

Abstract: The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata.
In this paper, we present a novel characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condon's simple policy iteration on these games. The correctness of Condon's approach, however, relies on the assumption that the games are \emph{stopping}. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in UP \cap coUP and PPAD. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution.
Finally, we show that the bisimilarity distances can be used to bound the difference between two states w.r.t. their maximal (or minimal) probability of satisfying arbitrary omega-regular specifications, expressed, eg., as LTL formulas. In the proofs of all the above-mentioned results, an alternative presentation of the Hausdorff distance due to Mémoli plays a central role.

DOI: 10.4230/LIPIcs.CONCUR.2019.9

Abstract: Differential privacy is a widely studied notion of privacy for various models of computation, based on measuring differences between probability distributions. We consider (epsilon,delta)-differential privacy in the setting of labelled Markov chains. The parameter delta can be captured by a variant of the total variation distance, which we call \lv. First we study \lv directly, showing that it cannot be computed exactly. However, the associated approximation problem turns out to be in PSPACE and #P-hard. Next we introduce a new bisimilarity distance for bounding \lv, which provides a tighter bound than previous distances while remaining computable with the same complexity (polynomial time with an NP oracle). We also propose an alternative bound that can be computed in polynomial time. We illustrate the distances on several case studies.

DOI: 10.4230/LIPIcs.CONCUR.2019.10

Abstract: The coalgebraic mu-calculus is a generic framework for fixpoint logics with varying branching types that subsumes, besides the standard relational mu-calculus, such diverse logics as the graded mu-calculus, the monotone mu-calculus, the probabilistic mu-calculus, and the alternating-time mu-calculus. In the present work, we give a local model checking algorithm for the coalgebraic mu-calculus using a coalgebraic variant of parity games that runs, under mild assumptions on the complexity of the so-called one-step satisfaction problem, in time p^k where p is a polynomial in the formula and model size and where k is the alternation depth of the formula. We show moreover that under the same assumptions, the model checking problem is contained in the intersection of NP and coNP, improving the complexity in all mentioned non-relational cases. If one-step satisfaction can be solved by means of small finite games, we moreover obtain standard parity games, ensuring quasipolynomial run time. This applies in particular to the monotone mu-calculus, the alternating-time mu-calculus, and the graded mu-calculus with grades coded in unary.

DOI: 10.4230/LIPIcs.CONCUR.2019.35

Abstract: The area of fault-tolerant distributed computability is concerned with the solvability of decision tasks in various computational models where the processes might crash. A very successful approach to prove impossibility results in this context is that of combinatorial topology, started by Herlihy and Shavit's paper in 1999. They proved that, for wait-free protocols where the processes communicate through read/write registers, a task is solvable if and only if there exists some map between simplicial complexes satisfying some properties.
This approach was then extended to many different contexts, where the processes have access to various synchronization and communication primitives. Usually, in those cases, the existence of a simplicial map from the protocol complex
to the output complex is taken as the definition of what it means to solve a task. In particular, no proof is provided of the fact that this abstract topological definition agrees with a more concrete operational definition of task solvability.
In this paper, we bridge this gap by proving a version of Herlihy and Shavit's theorem that applies to any kind of object. First, we start with a very general way of specifying concurrent objects, and we define what is means to implement an object B in a computational model where the processes are allowed to communicate through shared objects A_1,..., A_k. Then, we derive the notion of a decision task as a special case of concurrent object. Finally, we prove an analogue of Herlihy and Shavit's theorem in this context. In particular, our version of the theorem subsumes all the uses of the combinatorial topology approach that we are aware of.

DOI: 10.4230/LIPIcs.CONCUR.2019.34

Abstract: We provide syntactic derivative operations, defined by recursion on regular expressions, in the styles of both Brzozowski and Antimirov, for trace closures of regular languages. Just as the Brzozowski and Antimirov derivative operations for regular languages, these operations yield deterministic and nondeterministic automata respectively. But trace closures of regular languages are in general not recognizable, hence these automata cannot generally be finite, not even with quotienting. Still, as we show, for a star-connected expression, the Antimirov and Brzozowski automata, quotiented by the Kleene algebra equations, are finite. We also define a refined version of the Antimirov derivative operation where parts-of-derivatives (states of the automaton) are not regular expressions, but nonempty lists of regular expressions. We define the uniform scattering rank of a language and show that, for a regular expression whose language has finite uniform rank $N$, the truncation of the (generally infinite) refined Antimirov automaton, obtained by removing states longer than $N$, is finite without any quotienting, but still accepts the trace closure. We also show that star-connected languages have finite uniform rank.

DOI: 10.4230/LIPIcs.CONCUR.2019.40

Abstract: Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability/safety objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn reduction on several case studies and demonstrate its efficiency.

DOI: 10.4230/LIPIcs.CONCUR.2019.23

Abstract: The reachability problem for timed automata is generally solved using a zone graph approach. When the timed automaton is a network of timed automata working in parallel, there is a combinatorial explosion occurring due to interleavings of the same sequence of actions, as different interleavings potentially lead to different zones. Salah et al. in 2006 have shown that the union of all these different zones is also a zone, and have used this observation in an algorithm which aggregates these zones from time to time. A limitation of this approach is that it works only for acyclic timed automata. Bengtsson et al. in 1998 have proposed a local time semantics, where time is allowed to progress independently in each process of a network, and local times synchronize during joint actions. An analogous notion of local zone graphs was proposed where, in contrast, different interleavings lead to the same local zone.

We first show a connection between the two approaches, which provides a more direct and efficient method than Salah et al. and extends it to timed automata with cycles. Next, we point out a flaw in the existing method to compute finite local zone graphs. We then propose a new algorithm for reachability in networks of timed automata that builds the local zone graph and uses abstraction techniques over (standard) zones for termination. This benefits from the efficient handling of interleavings due to local zones and efficient abstraction techniques over standard zones. Moreover, the algorithm is a relatively simple extension of the standard zone algorithm. We evaluate our algorithm on standard examples. On various examples, we observe an order of magnitude decrease in the search space. On the other examples, it performs like the standard zone algorithm.

DOI: 10.4230/LIPIcs.CONCUR.2019.16

Abstract: We introduce a framework for approximate analysis of Markov decision processes (MDP) with bounded-, unbounded-, and infinite-horizon properties. The main idea is to identify a "core" of an MDP, i.e., a subsystem where we provably remain with high probability, and to avoid computation on the less relevant rest of the state space. Although we identify the core using simulations and statistical techniques, it allows for rigorous error bounds in the analysis. Consequently, we obtain efficient analysis algorithms based on partial exploration for various settings, including the challenging case of strongly connected systems.

DOI: 10.4230/LIPIcs.CONCUR.2019.5