CONCUR 2019
The 30th International Conference on Concurrency Theory
Amsterdam, the Netherlands, August 26-31, 2019
KEYNOTE SPEAKERS and CONFERENCE TECHNICAL PROGRAM
KEYNOTE SPEAKERS
- Marta Kwiatkowska - University of Oxford (UK)
- Kim G. Larsen - Aalborg University (Denmark)
- Joël Ouaknine - Max Planck Institute for Software Systems (Germany)
- Jaco van de Pol - Aarhus University (Denmark)
OUTLINE OF PROGRAM
- August 26: workshops
- August 27-30: CONCUR
- August 27-29: FORMATS
- August 31: workshops
| Monday August 26 |
Tuesday August 27 |
Wednesday August 28 |
Thursday August 29 |
Friday August 30 |
Saturday August 31 |
| EXPRESS/SOS | CONCUR | YR-CONCUR | |||
| DHS | FORMATS | TIPS | |||
| RADICAL | FMICS | ||||
| TRENDS | |||||
KEYNOTE DETAILS
Prof. Marta Kwiatkowska: Safety verification for deep neural networks with provable guarantees
Abstract: Computing systems are becoming ever more complex, with decisions increasingly often based on deep learning components. A wide variety of applications are being developed, many of them safety-critical, such as self-driving cars and medical diagnosis. Since deep learning is unstable with respect to adversarial perturbations, there is a need for rigorous software development methodologies that encompass machine learning components. This lecture will describe progress with developing automated verification techniques for deep neural networks to ensure safety and robustness of their decisions with respect to input perturbations. The techniques exploit Lipschitz continuity of the networks and aim to approximate, for a given set of inputs, the reachable set of network outputs in terms of lower and upper bounds, in anytime manner, with provable guarantees. We develop novel algorithms based on feature-guided search, games, global optimisation and Bayesian methods, and evaluate them on state-of-the-art networks. The lecture will conclude with an overview of the challenges in this field.
DOI: 10.4230/LIPIcs.CONCUR.2019.1
Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She is known for fundamental contributions to the theory and practice of model checking for probabilistic systems, focusing on automated techniques for verification and synthesis from quantitative specifications. She led the development of the PRISM model checker (www.prismmodelchecker.org), the leading software tool in the area and winner of the HVC Award 2016. Probabilistic model checking has been adopted in diverse fields, including distributed computing, wireless networks, security, robotics, healthcare, systems biology, DNA computing and nanotechnology, with genuine flaws found and corrected in real-world protocols. Kwiatkowska is the first female winner of the Royal Society Milner Award and was awarded an honorary doctorate from KTH Royal Institute of Technology in Stockholm. She won two ERC Advanced Grants, VERIWARE and FUN2MODEL, and is a coinvestigator of the EPSRC Programme Grant on Mobile Autonomy. Kwiatkowska is a Fellow of the Royal Society, Fellow of ACM and Member of Academia Europea.
Prof. Kim G. Larsen: Synthesis of Safe, Optimal and Compact Strategies for Stochastic Hybrid Games
Abstract: 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.
DOI: 10.4230/LIPIcs.CONCUR.2019.2
Kim G. Larsen is professor in the Department of Computer Science at Aalborg University within the Distributed and Embedded Systems Unit and director of the ICT-competence center CISS, Center for Embedded Software Systems.
In 2015 he won an ERC Advanced Grant with the project LASSO for learning, analysis, synthesis and optimization of cyber-physical systems.
He is director of the Sino-Danish Basic Research Center IDEA4CPS, the Danish Innovation Network InfinIT, as well as the innovation research center DiCyPS: Data Intensive Cyber Physical Systems.
His research interests include modeling, verification, performance analysis of real-time and embedded systems with applications to concurrency theory and model checking. In particular he is prime investigator of the real-time verification UPPAAL as well as the various new branches of the tool targeted towards planning, optimization, testing, synthesis and compositional analysis.
Prof. Joël Ouaknine: Program Invariants
Abstract: 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.
DOI: 10.4230/LIPIcs.CONCUR.2019.3
Joël Ouaknine is a Scientific Director at the Max Planck Institute for Software Systems in Saarbrücken, Germany, where he leads the Foundations of Algorithmic Verification group. He also holds secondary appointments at Oxford University and Saarland University. His research interests span a range of topics broadly connected to algorithmic verification and theoretical computer science. His group's recent focus has been on decision, control, and synthesis problems for linear dynamical systems (both continuous and discrete), making use among others of tools from number theory, Diophantine geometry, and algebraic geometry. Other interests include the algorithmic analysis of real-time, probabilistic, and infinite-state systems (e.g. model-checking algorithms, synthesis problems, complexity), logic and applications to verification, automated software analysis, and concurrency.
Prior to joining MPI-SWS, Joël worked as an academic in the Computer Science Department at Oxford University from 2004 to 2016, becoming Full Professor in 2010. He earned a BSc and MSc in Mathematics from McGill University, and received his PhD in Computer Science from Oxford in 2001. He held postdoc positions at Tulane University and Carnegie Mellon University, and served twice as visiting professor at the Ecole Normale Supérieure de Cachan, France. In both 2007 and 2008 he received an Outstanding Teaching Award from Oxford University, and the following year he was awarded an EPSRC Leadership Fellowship, enabling him to focus (almost) exclusively on research for a period of five years. He is the recipient of the 2010 Roger Needham Award, given annually "for a distinguished research contribution in Computer Science by a UK-based researcher within ten years of his or her PhD", and in 2015 was awarded an ERC Consolidator Grant to carry out research in dynamical systems.
Prof. Jaco van de Pol: Concurrent Algorithms and Data Structures for Model Checking
Abstract: 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 the 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 a brute force approach with clever algorithms: 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: 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 will present some of the solutions found over the last 10 years, leading to the high-performance model checker LTSmin. These include parallel NDFS (based on the PhD thesis of Alfons Laarman), the parallel detection of SCCs with concurrent Union-Find (based on the PhD thesis of Vincent Bloemen), and concurrent BDDs and other decision diagrams (based on the PhD thesis of Tom van Dijk). This functionality is provided in a specification-language agnostic manner, while exploiting the locality typical for a-synchronous distributed systems (based on the PhD thesis of Jeroen Meijer).
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.
DOI: 10.4230/LIPIcs.CONCUR.2019.4
Jaco van de Pol received his PhD on termination of higher-order rewriting in 1996 from Utrecht University.
After positions at LMU Münich and TU Eindhoven, he became senior researcher at CWI (2000-2007).
He was full professor, heading the chair in formal methods and tools at the University of Twente (2007-2018),
where he was head of department from 2014-2017. He was invited professor in Paris (2016-2019).
Since 2018, he is full professor in Computer Science at Aarhus University.
Van de Pol publishes regularly in conferences like TACAS, CAV and CONCUR. He is member of the steering
committees of SPIN and FMICS, and in the editorial boards for the journals SCP and STTT.
His research interests are in distributed concurrent systems and automated reasoning. In particular, he investigated
parallel and symbolic algorithms for efficient model checking. He and his team built the award-winning toolset
LTSmin for high-performance model checking. Application domains include safety and performance of embedded
and distributed systems, security protocols and risk analysis, and signaling pathways in biological systems.
CONFERENCE TECHNICAL PROGRAM
| Tuesday, 27 August, 2019 | CONCUR, Turing Room |
|---|---|
| 08:30–09:00 | Opening |
| 09:00–10:00 |
Keynote: Marta Kwiatkovska DOI: 10.4230/LIPIcs.CONCUR.2019.1 |
| 10:00–10:30 | Coffee break |
| 10:30–12:30 | Markov Decision Processes |
| 10:30–11:00 |
Of Cores: A Partial-Exploration Framework for Markov Decision Processes
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.
|
| 11:00–11:30 |
Combinations of Qualitative Winning for Stochastic Parity Games
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.
|
| 11:30–12:00 |
Near-linear time algorithms for Streett objectives in Graphs and MDPs
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.
|
| 12:00–12:30 |
Life is Random, Time is Not: Markov Decision Processes with Window Objectives
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. |
| 12:30–13:30 | Lunch break |
| 13:30–15:00 | Probabilistic systems |
| 13:30–14:00 |
Computing Probabilistic Bisimilarity Distances for Probabilistic Automata
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.
|
| 14:00–14:30 |
Asymmetric Distances for Approximate Differential Privacy
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.
|
| 14:30–15:00 |
Event structures for mixed choice
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.
|
| 15:00–15:30 | Coffee break |
| 15:30–17:30 | Reachability |
| 15:30–16:00 |
Verification of Flat FIFO System
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.
|
| 16:00–16:30 |
The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games
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.
|
| 16:30–17:00 |
On the Complexity of Reachability in Parametric Markov Decision Processes
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.
|
| 17:00–17:30 |
Timed Basic Parallel Processes
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.
|
| 17:30–19:00 | Drinks |
| Wednesday, 28 August, 2019 | CONCUR, Turing Room |
| 08:30–09:00 | Opening |
| 09:00–10:00 |
Keynote: Joël Ouaknine DOI: 10.4230/LIPIcs.CONCUR.2019.3 |
| 10:00–10:30 | Coffee break |
| 10:30–12:30 | Automata |
| 10:30–11:00 |
Revisiting local time semantics for networks of timed automata
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. |
| 11:00–11:30 |
Approximate Learning of Limit-Average Automata
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. |
| 11:30–12:00 |
Good for Games Automata: From Nondeterminism to Alternation
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. |
| 12:00–12:30 |
Alternating Weak Automata from Universal Trees
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\'nski and Lazi\'c, 2017; and Fearnley, Jain, Schewe, Stephan, and Wojtczak, 2017), and hence it would yield a significant breakthrough.
|
| 12:30–13:15 | Lunch break |
| 13:15–21:00 | Social Activity |
| Thursday, 29 August, 2019 | CONCUR, Turing Room |
| 08:30–09:00 | Opening |
| 09:00–10:00 |
Keynote: Kim G. Larsen DOI: 10.4230/LIPIcs.CONCUR.2019.2 |
| 10:00–10:30 | Coffee break |
| 10:30–12:30 | Games |
| 10:30–11:00 |
Determinacy in Discrete-Bidding Infinite-Duration Games
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.
|
| 11:00–11:30 |
Energy mean-payoff games
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.
|
| 11:30–12:00 |
Equilibrium Design for Concurrent Games
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.
|
| 12:00–12:30 |
Partial Order Reduction for Reachability Games
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.
|
| 12:30–13:30 | Lunch break |
| 13:30–15:00 | Synthesis |
| 13:30–14:00 |
Synthesis of Data Word Transducers
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. |
| 14:00–14:30 |
Register-Bounded Synthesis
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. |
| 14:30–15:00 |
Translating Asynchronous Games for Distributed Synthesis
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. |
| 15:00–15:30 | Coffee break |
| 15:30–17:30 | VASS and concurrent programming |
| 15:30–16:00 |
Reachability for Bounded Branching VASS
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.
|
| 16:00–16:30 |
Long-Run Average Behavior of Vector Addition Systems with States
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.
|
| 16:30–17:00 |
Reasoning about Distributed Knowledge of Groups with Infinitely Many Agents
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. |
| 17:00–17:30 |
Robustness Against Transactional Causal Consistency
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. |
| Friday, 30 August, 2019 | CONCUR, Turing Room |
| 08:30–09:00 | Opening |
| 09:00–10:00 |
Keynote: Jaco van de Pol DOI: 10.4230/LIPIcs.CONCUR.2019.4 |
| 10:00–10:30 | Coffee break |
| 10:30–12:30 | Broadcast and fault-tolerance |
| 10:30–11:00 |
Expressive Power of Broadcast Consensus Protocols
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.
|
| 11:00–11:30 |
Reconfiguration and message losses in parameterized broadcast networks
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.
|
| 11:30–12:00 |
Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries
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.
|
| 12:00–12:30 |
A sound foundation for the topological approach to task solvability
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.
|
| 12:30–13:30 | Lunch break |
| 13:30–15:00 | Coalgebra and model checking |
| 13:30–14:00 |
Game-Based Local Model Checking for the Coalgebraic mu-Calculus
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.
|
| 14:00–14:30 |
Graded Monads and Graded Logics for the Linear Time -- Branching Time Spectrum
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.
|
| 14:30–15:00 |
Bialgebraic Semantics for String Diagrams
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. |
| 15:00–15:30 | Coffee break |
| 15:30–17:30 | Session types and Kleene algebra |
| 15:30–16:00 |
A sound algorithm for asynchronous session subtyping
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.
|
| 16:00–16:30 |
Domain-Aware Session Types
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. |
| 16:30–17:00 |
Derivatives of Trace Closures of Regular Languages
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.
|
| 17:00–17:30 |
Kleene Algebra with Observations
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.
|
TECHNICAL PROGRAM (EXTERNAL LINKS)
Last updated: August 20, 2019
