eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
0
0
10.4230/LIPIcs.CONCUR.2019
article
LIPIcs, Volume 140, CONCUR'19, Complete Volume
Fokkink, Wan
1
van Glabbeek, Rob
2
Vrije Universiteit Amsterdam, the Netherlands
Data61, CSIRO, Sydney, Australia
LIPIcs, Volume 140, CONCUR'19, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019/LIPIcs.CONCUR.2019.pdf
Theory of computation, Concurrency
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
0:i
0:xiv
10.4230/LIPIcs.CONCUR.2019.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Fokkink, Wan
1
van Glabbeek, Rob
2
Vrije Universiteit Amsterdam, the Netherlands
Data61, CSIRO, Sydney, Australia
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.0/LIPIcs.CONCUR.2019.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
1:1
1:5
10.4230/LIPIcs.CONCUR.2019.1
article
Safety Verification for Deep Neural Networks with Provable Guarantees (Invited Paper)
Kwiatkowska, Marta Z.
1
https://orcid.org/0000-0001-9022-7599
Department of Computer Science, University of Oxford, UK
Computing systems are becoming ever more complex, increasingly often incorporating deep learning components. Since deep learning is unstable with respect to adversarial perturbations, there is a need for rigorous software development methodologies that encompass machine learning. This paper describes progress with developing automated verification techniques for deep neural networks to ensure safety and robustness of their decisions with respect to input perturbations. This includes novel algorithms based on feature-guided search, games, global optimisation and Bayesian methods.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.1/LIPIcs.CONCUR.2019.1.pdf
Neural networks
robustness
formal verification
Bayesian neural networks
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
2:1
2:5
10.4230/LIPIcs.CONCUR.2019.2
article
Synthesis of Safe, Optimal and Compact Strategies for Stochastic Hybrid Games (Invited Paper)
Larsen, Kim G.
1
Department of Computer Science, Aalborg University, DK
UPPAAL-Stratego is a recent branch of the verification tool UPPAAL allowing for synthesis of safe and optimal strategies for stochastic timed (hybrid) games. We describe newly developed learning methods, allowing for synthesis of significantly better strategies and with much improved convergence behaviour. Also, we describe novel use of decision trees for learning orders-of-magnitude more compact strategy representation. In both cases, the seek for optimality does not compromise safety.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.2/LIPIcs.CONCUR.2019.2.pdf
Timed automata
Stochastic hybrid grame
Symbolic synthesis
Reinforcement learning
Q-learning
M-learning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
3:1
3:1
10.4230/LIPIcs.CONCUR.2019.3
article
Program Invariants (Invited Talk)
Ouaknine, Joël
1
2
Max Planck Institute for Software Systems, Saarbrücken, Germany
Oxford University, UK
Automated invariant generation is a fundamental challenge in program analysis and verification, going back many decades, and remains a topic of active research. In this talk I'll present a select overview and survey of work on this problem, and discuss unexpected connections to other fields including algebraic geometry, group theory, and quantum computing. (No previous knowledge of these topics will be assumed.)
This is joint work with Ehud Hrushovski, Amaury Pouly, and James Worrell.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.3/LIPIcs.CONCUR.2019.3.pdf
Automated invariant generation
program analysis and verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
4:1
4:1
10.4230/LIPIcs.CONCUR.2019.4
article
Concurrent Algorithms and Data Structures for Model Checking (Invited Talk)
van de Pol, Jaco
1
2
https://orcid.org/0000-0003-4305-0625
Aarhus University, Denmark
University of Twente, The Netherlands
Model checking is a successful method for checking properties on the state space of concurrent, reactive systems. Since it is based on exhaustive search, scaling this method to industrial systems has been a challenge since its conception. Research has focused on clever data structures and algorithms, to reduce the size of the state space or its representation; smart search heuristics, to reveal potential bugs and counterexamples early; and high-performance computing, to deploy the brute force processing power of clusters of compute-servers. The main challenge is to combine these approaches - brute-force alone (when implemented carefully) can bring a linear speedup in the number of processors. This is great, since it reduces model-checking times from days to minutes. On the other hand, proper algorithms and data structures can lead to exponential gains. Therefore, the parallelization bonus is only real if we manage to speedup clever algorithms.
There are some obstacles though: many linear-time graph algorithms depend on a depth-first exploration order, which is hard to parallelize. Examples include the detection of strongly connected components (SCC) and the nested depth-first-search (NDFS) algorithm. Both are used in model checking LTL properties. Symbolic representations, like binary decision diagrams (BDDs), reduce model checking to "pointer-chasing", leading to irregular memory-access patterns. This poses severe challenges on achieving actual speedup in (clusters of) modern multi-core computer architectures.
This talk presents some of the solutions found over the last 10 years, which led to the high-performance model checker LTSmin [Gijs Kant et al., 2015]. These include parallel NDFS (based on the PhD thesis of Alfons Laarman [Alfons Laarman, 2014]), the parallel detection of SCCs with concurrent Union-Find (based on the PhD thesis of Vincent Bloemen [Vincent Bloemen, 2019]), and concurrent BDDs (based on the PhD thesis of Tom van Dijk [Tom van Dijk, 2016]).
Finally, I will sketch a perspective on moving forward from high-performance model checking to high-performance synthesis algorithms. Examples include parameter synthesis for stochastic and timed systems, and strategy synthesis for (stochastic and timed) games.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.4/LIPIcs.CONCUR.2019.4.pdf
model checking
parallel algorithms
concurrent datastructures
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
5:1
5:17
10.4230/LIPIcs.CONCUR.2019.5
article
Of Cores: A Partial-Exploration Framework for Markov Decision Processes
Křetínský, Jan
1
https://orcid.org/0000-0002-8122-2881
Meggendorfer, Tobias
1
https://orcid.org/0000-0002-1712-2165
Technical University of Munich, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.5/LIPIcs.CONCUR.2019.5.pdf
Markov Decision Processes
Reachability
Approximation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
6:1
6:17
10.4230/LIPIcs.CONCUR.2019.6
article
Combinations of Qualitative Winning for Stochastic Parity Games
Chatterjee, Krishnendu
1
Piterman, Nir
2
3
IST Austria, Klosterneuburg, Austria
University of Gothenburg, Sweden
University of Leicester, UK
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 cap 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 cap 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 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.6/LIPIcs.CONCUR.2019.6.pdf
Two Player Games
Stochastic Games
Parity Winning Conditions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
7:1
7:16
10.4230/LIPIcs.CONCUR.2019.7
article
Near-Linear Time Algorithms for Streett Objectives in Graphs and MDPs
Chatterjee, Krishnendu
1
Dvořák, Wolfgang
2
Henzinger, Monika
3
Svozil, Alexander
3
IST Austria, Klosterneuburg, Austria
Institute of Logic and Computation, TU Wien, Austria
Theory and Application of Algorithms, University of Vienna, Austria
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 the 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 objectives 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 O~(m + b), where the 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.7/LIPIcs.CONCUR.2019.7.pdf
model checking
graph games
Streett games
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
8:1
8:18
10.4230/LIPIcs.CONCUR.2019.8
article
Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives
Brihaye, Thomas
1
Delgrange, Florent
1
2
Oualhadj, Youssouf
3
Randour, Mickael
4
UMONS - Université de Mons, Belgium
RWTH Aachen, Germany
LACL - UPEC, Paris, France
F.R.S.-FNRS & UMONS - Université de Mons, Belgium
The window mechanism was introduced by Chatterjee et al. [Krishnendu Chatterjee et al., 2015] 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.8/LIPIcs.CONCUR.2019.8.pdf
Markov decision processes
window mean-payoff
window parity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
9:1
9:17
10.4230/LIPIcs.CONCUR.2019.9
article
Computing Probabilistic Bisimilarity Distances for Probabilistic Automata
Bacci, Giorgio
1
Bacci, Giovanni
1
Larsen, Kim G.
1
Mardare, Radu
1
Tang, Qiyi
2
van Breugel, Franck
3
Department of Computer Science, Aalborg University, DK
Department of Computing, Imperial College, London, UK
DisCoVeri Group, Dept. of Electrical Engineering and Computer Science, York University, Canada
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 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. In the proofs of all the above-mentioned results, an alternative presentation of the Hausdorff distance due to Mémoli plays a central rôle.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.9/LIPIcs.CONCUR.2019.9.pdf
Probabilistic automata
Behavioural metrics
Simple stochastic games
Simple policy iteration algorithm
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
10:1
10:17
10.4230/LIPIcs.CONCUR.2019.10
article
Asymmetric Distances for Approximate Differential Privacy
Chistikov, Dmitry
1
Murawski, Andrzej S.
2
Purser, David
1
Centre for Discrete Mathematics and its Applications (DIMAP) & Department of Computer Science, University of Warwick, UK
Department of Computer Science, University of Oxford, UK
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. For a given epsilon, the parameter delta can be captured by a variant of the total variation distance, which we call lv_{alpha} (where alpha = e^{epsilon}).
First we study lv_{alpha} 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_{alpha} from above, which provides a tighter bound than previously known 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. Finally, we illustrate the distances on case studies.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.10/LIPIcs.CONCUR.2019.10.pdf
Bisimilarity distances
Differential privacy
Labelled Markov chains
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
11:1
11:16
10.4230/LIPIcs.CONCUR.2019.11
article
Event Structures for Mixed Choice
de Visme, Marc
1
Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France
In the context of models with mixed nondeterministic and probabilistic choice, we present a concurrent model based on partial orders, 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 on CCS, event structures and labelled transition systems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.11/LIPIcs.CONCUR.2019.11.pdf
probability
nondeterminism
concurrency
event structures
CCS
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
12:1
12:17
10.4230/LIPIcs.CONCUR.2019.12
article
Verification of Flat FIFO Systems
Finkel, Alain
1
2
Praveen, M.
3
2
LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
UMI ReLaX, French-Indian research laboratory in computer sciences, Chennaï, India
Chennai Mathematical Institute, India
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.12/LIPIcs.CONCUR.2019.12.pdf
Infinite state systems
FIFO
counters
flat systems
reachability
termination
complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
13:1
13:16
10.4230/LIPIcs.CONCUR.2019.13
article
The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games
Brihaye, Thomas
1
Bruyère, Véronique
1
Goeminne, Aline
1
2
Raskin, Jean-François
2
van den Bogaard, Marie
2
Université de Mons (UMONS), Belgium
Université libre de Bruxelles (ULB), Belgium
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.13/LIPIcs.CONCUR.2019.13.pdf
multiplayer non-zero-sum games played on graphs
quantitative reachability objectives
subgame perfect equilibria
constrained existence problem
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
14:1
14:17
10.4230/LIPIcs.CONCUR.2019.14
article
On the Complexity of Reachability in Parametric Markov Decision Processes
Winkler, Tobias
1
Junges, Sebastian
1
https://orcid.org/0000-0003-0978-8466
Pérez, Guillermo A.
2
https://orcid.org/0000-0002-1200-4952
Katoen, Joost-Pieter
1
https://orcid.org/0000-0002-6143-1926
RWTH Aachen University, Germany
University of Antwerp, Belgium
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.14/LIPIcs.CONCUR.2019.14.pdf
Parametric Markov decision processes
Formal verification
ETR
Complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
15:1
15:16
10.4230/LIPIcs.CONCUR.2019.15
article
Timed Basic Parallel Processes
Clemente, Lorenzo
1
https://orcid.org/0000-0003-0578-9103
Hofman, Piotr
1
https://orcid.org/0000-0001-9866-3723
Totzke, Patrick
2
https://orcid.org/0000-0001-5274-8190
University of Warsaw, Poland
University of Liverpool, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.15/LIPIcs.CONCUR.2019.15.pdf
Timed Automata
Petri Nets
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
16:1
16:15
10.4230/LIPIcs.CONCUR.2019.16
article
Revisiting Local Time Semantics for Networks of Timed Automata
Govind, R.
1
2
Herbreteau, Frédéric
2
Srivathsan, B.
1
Walukiewicz, Igor
2
Chennai Mathematical Institute, India
Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks of timed automata working in parallel. In the timed setting this explosion is particularly visible as even different interleavings of local actions of processes may lead to different zones. Salah et al. in 2006 have shown that the union of all these different zones is also a zone. This observation was used in an algorithm which from time to time detects and aggregates these zones into a single zone.
We show that such aggregated zones can be calculated more efficiently using the local time semantics and the related notion of local zones proposed by Bengtsson et al. in 1998. Next, we point out a flaw in the existing method to ensure termination of the local zone graph computation. We fix this with a new algorithm that builds the local zone graph and uses abstraction techniques over (standard) zones for termination. 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, the algorithm performs like the standard zone algorithm.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.16/LIPIcs.CONCUR.2019.16.pdf
Timed automata
verification
local-time semantics
abstraction
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
17:1
17:16
10.4230/LIPIcs.CONCUR.2019.17
article
Approximate Learning of Limit-Average Automata
Michaliszyn, Jakub
1
https://orcid.org/0000-0002-5053-0347
Otop, Jan
1
https://orcid.org/0000-0002-8804-8011
University of Wrocław, Poland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.17/LIPIcs.CONCUR.2019.17.pdf
weighted automata
learning
expected value
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
18:1
18:14
10.4230/LIPIcs.CONCUR.2019.18
article
Alternating Weak Automata from Universal Trees
Daviaud, Laure
1
Jurdziński, Marcin
2
Lehtinen, Karoliina
3
City, University of London, UK
University of Warwick, UK
University of Liverpool, UK
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 it is polynomial if the asymptotic number of priorities is at most 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ć, 2017; and Fearnley, Jain, Schewe, Stephan, and Wojtczak, 2017), and hence it would yield a significant breakthrough.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.18/LIPIcs.CONCUR.2019.18.pdf
alternating automata
weak automata
Büchi automata
parity automata
parity games
universal trees
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
19:1
19:16
10.4230/LIPIcs.CONCUR.2019.19
article
Good for Games Automata: From Nondeterminism to Alternation
Boker, Udi
1
Lehtinen, Karoliina
2
https://orcid.org/0000-0003-1171-8790
Interdisciplinary Center (IDC) Herzliya, Israel
University of Liverpool, United Kingdom
A word automaton recognizing a language L is good for games (GFG) if its composition with any game with winning condition L preserves the game’s winner. While all deterministic automata are GFG, some nondeterministic automata are 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". The equivalence of these properties has not been formally shown.
We generalize all of these definitions to alternating automata and show their equivalence. We further show that alternating GFG automata are as expressive as deterministic automata with the same acceptance conditions and indices. We then show that alternating GFG automata over finite words, and weak automata over infinite words, are not more succinct than deterministic automata, and that determinizing Büchi and co-Büchi 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.19/LIPIcs.CONCUR.2019.19.pdf
Good for games
history-determinism
alternation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
20:1
20:17
10.4230/LIPIcs.CONCUR.2019.20
article
Determinacy in Discrete-Bidding Infinite-Duration Games
Aghajohari, Milad
1
Avni, Guy
2
Henzinger, Thomas A.
2
Sharif University of Technology, Iran
IST Austria, Klosterneuburg, Austria
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 discrete-bidding and infinite-duration games. Our most important result proves that these games form a large determined subclass of concurrent games, where 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.20/LIPIcs.CONCUR.2019.20.pdf
Bidding games
Richman games
determinacy
concurrent games
discrete bidding
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
21:1
21:17
10.4230/LIPIcs.CONCUR.2019.21
article
Energy Mean-Payoff Games
Bruyère, Véronique
1
Hautem, Quentin
1
Randour, Mickael
2
Raskin, Jean-François
3
Université de Mons (UMONS), Belgium
Université de Mons (F.R.S.-FNRS & UMONS), Belgium
Université libre de Bruxelles (ULB), Belgium
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.21/LIPIcs.CONCUR.2019.21.pdf
two-player zero-sum games played on graphs
energy and mean-payoff objectives
complexity study and construction of optimal strategies
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
22:1
22:16
10.4230/LIPIcs.CONCUR.2019.22
article
Equilibrium Design for Concurrent Games
Gutierrez, Julian
1
Najib, Muhammad
1
Perelli, Giuseppe
2
Wooldridge, Michael
1
Department of Computer Science, University of Oxford, UK
Department of Computer Science, University of Göteborg, Sweden
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 solution 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.22/LIPIcs.CONCUR.2019.22.pdf
Games
Temporal logic
Synthesis
Model checking
Nash equilibrium
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
23:1
23:15
10.4230/LIPIcs.CONCUR.2019.23
article
Partial Order Reduction for Reachability Games
Bønneland, Frederik Meyer
1
Jensen, Peter Gjøl
1
https://orcid.org/0000-0002-9320-9991
Larsen, Kim G.
1
Muñiz, Marco
1
https://orcid.org/0000-0003-2357-0375
Srba, Jiří
1
Department of Computer Science, Aalborg University, Denmark
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/p023-B-nneland/LIPIcs.CONCUR.2019.23/LIPIcs.CONCUR.2019.23.pdf
Petri nets
games
synthesis
partial order reduction
stubborn sets
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
24:1
24:15
10.4230/LIPIcs.CONCUR.2019.24
article
Synthesis of Data Word Transducers
Exibard, Léo
1
2
Filiot, Emmanuel
2
Reynier, Pierre-Alain
1
Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
Université libre de Bruxelles, Brussels, Belgium
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 (omega-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite. In this paper, we consider data omega-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 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.24/LIPIcs.CONCUR.2019.24.pdf
Register Automata
Synthesis
Data words
Transducers
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
25:1
25:16
10.4230/LIPIcs.CONCUR.2019.25
article
Register-Bounded Synthesis
Khalimov, Ayrat
1
Kupferman, Orna
1
School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel
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 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. The bounded setting captures better real-life scenarios where bounds on the systems and/or its environment are known. In addition, the bounds are the key to new synthesis algorithms, and, as recently shown in [A. Khalimov et al., 2018], they lead to decidability. Our contributions include a stronger specification formalism (universal register parity automata), simpler algorithms, which enable 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 among a fixed, finite, and infinite number of registers, and the determinacy of the corresponding games.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.25/LIPIcs.CONCUR.2019.25.pdf
Synthesis
Register Automata
Register Transducers
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
26:1
26:16
10.4230/LIPIcs.CONCUR.2019.26
article
Translating Asynchronous Games for Distributed Synthesis
Beutner, Raven
1
Finkbeiner, Bernd
1
Hecking-Harbusch, Jesko
1
Saarland University, Saarbrücken, Germany
In distributed synthesis, a set of process implementations is generated, which 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 the two game types 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 allow 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.26/LIPIcs.CONCUR.2019.26.pdf
synthesis
distributed systems
causal memory
Petri games
control games
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
27:1
27:16
10.4230/LIPIcs.CONCUR.2019.27
article
Long-Run Average Behavior of Vector Addition Systems with States
Chatterjee, Krishnendu
1
https://orcid.org/0000-0002-4561-241X
Henzinger, Thomas A.
1
Otop, Jan
2
https://orcid.org/0000-0002-8804-8011
IST Austria, Klosterneuburg, Austria
University of Wrocław, Poland
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). 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.27/LIPIcs.CONCUR.2019.27.pdf
vector addition systems
mean-payoff
Diophantine inequalities
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
28:1
28:13
10.4230/LIPIcs.CONCUR.2019.28
article
Reachability for Bounded Branching VASS
Mazowiecki, Filip
1
Pilipczuk, Michał
2
LaBRI, Université de Bordeaux, France
University of Warsaw, Poland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.28/LIPIcs.CONCUR.2019.28.pdf
Branching VASS
counter machines
reachability problem
bobrvass
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
29:1
29:15
10.4230/LIPIcs.CONCUR.2019.29
article
Reasoning About Distributed Knowledge of Groups with Infinitely Many Agents
Guzmán, Michell
1
Knight, Sophia
2
Quintero, Santiago
3
Ramírez, Sergio
4
Rueda, Camilo
4
Valencia, Frank
5
4
University of Milano-Bicocca, Italy
University of Minnesota Duluth, MN, USA
LIX École Polytechnique de Paris, France
Pontificia Universidad Javeriana de Cali, Colombia
CNRS, LIX École Polytechnique de Paris, France
Spatial constraint systems (scs) are semantic structures for reasoning about spatial and epistemic information in concurrent systems. We develop the theory of scs to reason about the distributed information of potentially infinite groups. We characterize the notion of distributed 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 provide an alternative characterization of this notion as the greatest family of join-preserving functions that satisfy certain basic properties. We show compositionality results for these characterizations and conditions under which information that can be obtained by an infinite group can also be obtained by a finite group. Finally, we provide algorithms that compute the distributive group information of finite groups.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.29/LIPIcs.CONCUR.2019.29.pdf
Reasoning about Groups
Distributed Knowledge
Infinitely Many Agents
Reasoning about Space
Algebraic Modeling
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
30:1
30:18
10.4230/LIPIcs.CONCUR.2019.30
article
Robustness Against Transactional Causal Consistency
Beillahi, Sidi Mohamed
1
Bouajjani, Ahmed
1
Enea, Constantin
1
Université de Paris, IRIF, CNRS, F-75013 Paris, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.30/LIPIcs.CONCUR.2019.30.pdf
Distributed Databases
Causal Consistency
Model Checking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
31:1
31:16
10.4230/LIPIcs.CONCUR.2019.31
article
Expressive Power of Broadcast Consensus Protocols
Blondin, Michael
1
Esparza, Javier
2
Jaax, Stefan
2
Département d'informatique, Université de Sherbrooke, Sherbrooke, Canada
Fakultät für Informatik, Technische Universität München, Garching bei München, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.31/LIPIcs.CONCUR.2019.31.pdf
population protocols
complexity theory
counter machines
distributed computing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
32:1
32:15
10.4230/LIPIcs.CONCUR.2019.32
article
Reconfiguration and Message Losses in Parameterized Broadcast Networks
Bertrand, Nathalie
1
https://orcid.org/0000-0002-9957-5394
Bouyer, Patricia
2
https://orcid.org/0000-0002-2823-0911
Majumdar, Anirban
1
2
Univ. Rennes, Inria, CNRS, IRISA - Rennes, France
LSV, CNRS & ENS Paris-Saclay, Univ. Paris-Saclay - Cachan, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.32/LIPIcs.CONCUR.2019.32.pdf
model checking
parameterized verification
broadcast networks
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
33:1
33:15
10.4230/LIPIcs.CONCUR.2019.33
article
Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries
Bertrand, Nathalie
1
https://orcid.org/0000-0002-9957-5394
Konnov, Igor
2
https://orcid.org/0000-0001-6629-3377
Lazić, Marijana
3
https://orcid.org/0000-0002-9222-6191
Widder, Josef
4
5
https://orcid.org/0000-0003-2795-611X
Univ. Rennes, Inria, CNRS, IRISA, Rennes, France
University of Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
TU München, 85748 Garching bei München, Germany
TU Wien, 1040 Vienna, Austria
Interchain Foundation, 6340 Baar, Switzerland
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 consensus 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 processes enter round r only after all 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.33/LIPIcs.CONCUR.2019.33.pdf
threshold automata
counter systems
parameterized verification
randomized distributed algorithms
Byzantine faults
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
34:1
34:15
10.4230/LIPIcs.CONCUR.2019.34
article
A Sound Foundation for the Topological Approach to Task Solvability
Ledent, Jérémy
1
Mimram, Samuel
1
École Polytechnique, Palaiseau, France
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 it 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.34/LIPIcs.CONCUR.2019.34.pdf
Fault-tolerant protocols
Asynchronous computability
Combinatorial topology
Protocol complex
Distributed task
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
35:1
35:16
10.4230/LIPIcs.CONCUR.2019.35
article
Game-Based Local Model Checking for the Coalgebraic mu-Calculus
Hausmann, Daniel
1
Schröder, Lutz
1
Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
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 in both 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 quasi-polynomial 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.35/LIPIcs.CONCUR.2019.35.pdf
Model checking
mu-calculus
coalgebraic logic
graded mu-calculus
probabilistic mu-calculus
parity games
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
36:1
36:16
10.4230/LIPIcs.CONCUR.2019.36
article
Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum
Dorsch, Ulrich
1
Milius, Stefan
1
Schröder, Lutz
1
Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the 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 exemplary proofs of their expressiveness based on our generic criterion.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.36/LIPIcs.CONCUR.2019.36.pdf
Linear Time
Branching Time
Monads
System Equivalences
Modal Logics
Expressiveness
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
37:1
37:17
10.4230/LIPIcs.CONCUR.2019.37
article
Bialgebraic Semantics for String Diagrams
Bonchi, Filippo
1
Piedeleu, Robin
2
Sobocinski, Pawel
3
Zanasi, Fabio
2
University of Pisa, Italy
University College London, UK
University of Southampton, UK
Turi and Plotkin’s bialgebraic semantics 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 (an endofunctor). This setup is instrumental in showing that a semantic specification (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 string diagrams, a graphical syntax that is increasingly used in the study of interacting systems across different disciplines. Our analysis relies on representing the two-dimensional operations underlying string diagrams in various categories as a monad, and their bialgebraic semantics in terms of a distributive law for that monad.
As a proof of concept, we provide bialgebraic 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.37/LIPIcs.CONCUR.2019.37.pdf
String Diagram
Structural Operational Semantics
Bialgebraic semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
38:1
38:16
10.4230/LIPIcs.CONCUR.2019.38
article
A Sound Algorithm for Asynchronous Session Subtyping
Bravetti, Mario
1
2
https://orcid.org/0000-0001-5193-2914
Carbone, Marco
3
https://orcid.org/0000-0001-9479-2632
Lange, Julien
4
https://orcid.org/0000-0001-9697-1378
Yoshida, Nobuko
5
https://orcid.org/0000-0002-3925-8557
Zavattaro, Gianluigi
1
2
https://orcid.org/0000-0003-3313-6409
University of Bologna, Italy
INRIA FoCUS Team
IT University of Copenhagen, Denmark
University of Kent, UK
Imperial College London, UK
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 this 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; this 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.38/LIPIcs.CONCUR.2019.38.pdf
Session types
Concurrency
Subtyping
Algorithm
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
39:1
39:17
10.4230/LIPIcs.CONCUR.2019.39
article
Domain-Aware Session Types
Caires, Luís
1
https://orcid.org/0000-0002-3215-6734
Pérez, Jorge A.
2
https://orcid.org/0000-0002-1452-6180
Pfenning, Frank
3
Toninho, Bernardo
1
https://orcid.org/0000-0002-0746-7514
Universidade Nova de Lisboa, Portugal
University of Groningen, The Netherlands
Carnegie Mellon University, Pittsburgh, PA, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.39/LIPIcs.CONCUR.2019.39.pdf
Session Types
Linear Logic
Process Calculi
Hybrid Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
40:1
40:16
10.4230/LIPIcs.CONCUR.2019.40
article
Reordering Derivatives of Trace Closures of Regular Languages
Maarand, Hendrik
1
https://orcid.org/0000-0002-1967-4297
Uustalu, Tarmo
2
1
https://orcid.org/0000-0002-1297-0579
Department of Software Science, Tallinn University of Technology, Estonia
School of Computer Science, Reykjavik University, Iceland
We provide syntactic derivative-like 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 syntactic reordering derivative operations yield deterministic and nondeterministic automata respectively. But trace closures of regular languages are in general not regular, hence these automata cannot generally be finite. Still, as we show, for star-connected expressions, the Antimirov and Brzozowski automata, suitably quotiented, are finite. We also define a refined version of the Antimirov reordering derivative operation where parts-of-derivatives (states of the automaton) are nonempty lists of regular expressions rather than single regular expressions. We define the uniform scattering rank of a language and show that, for a regexp whose language has finite uniform scattering rank, the truncation of the (generally infinite) refined Antimirov automaton, obtained by removing long states, is finite without any quotienting, but still accepts the trace closure. We also show that star-connected languages have finite uniform scattering rank.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.40/LIPIcs.CONCUR.2019.40.pdf
Mazurkiewicz traces
trace closure
regular languages
finite automata
language derivatives
scattering rank
star-connected expressions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
140
41:1
41:16
10.4230/LIPIcs.CONCUR.2019.41
article
Kleene Algebra with Observations
Kappé, Tobias
1
https://orcid.org/0000-0002-6068-880X
Brunet, Paul
1
https://orcid.org/0000-0002-9762-6872
Rot, Jurriaan
1
2
Silva, Alexandra
1
https://orcid.org/0000-0001-5014-9784
Wagemaker, Jana
1
Zanasi, Fabio
1
University College London, UK
Radboud University, Nijmegen, The Netherlands
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Generalising KAT to reason about concurrent programs is not straightforward, because axioms native to KAT in conjunction with expected axioms for concurrency lead to an anomalous 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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol140-concur2019/LIPIcs.CONCUR.2019.41/LIPIcs.CONCUR.2019.41.pdf
Concurrent Kleene algebra
Kleene algebra with tests
free model
axiomatisation
decision procedure