Volume
LIPIcs, Volume 203
32nd International Conference on Concurrency Theory (CONCUR 2021)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Event
CONCUR 2021, August 24-27, 2021, Virtual ConferenceEditors
Publication Details
- published at: 2021-08-13
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-203-7
- DBLP: db/conf/concur/concur2021
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 203, CONCUR 2021, Complete Volume
Abstract
LIPIcs, Volume 203, CONCUR 2021, Complete Volume
Cite as
32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 1-672, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@Proceedings{haddad_et_al:LIPIcs.CONCUR.2021,
title = {{LIPIcs, Volume 203, CONCUR 2021, Complete Volume}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {1--672},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021},
URN = {urn:nbn:de:0030-drops-143766},
doi = {10.4230/LIPIcs.CONCUR.2021},
annote = {Keywords: LIPIcs, Volume 203, CONCUR 2021, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{haddad_et_al:LIPIcs.CONCUR.2021.0,
author = {Haddad, Serge and Varacca, Daniele},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.0},
URN = {urn:nbn:de:0030-drops-143779},
doi = {10.4230/LIPIcs.CONCUR.2021.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
CONCUR Test-Of-Time Award 2021 (Invited Paper)
Abstract
This short article announces the recipients of the CONCUR Test-of-Time Award 2021.
Cite as
Nathalie Bertrand, Luca de Alfaro, Rob van Glabbeek, Catuscia Palamidessi, and Nobuko Yoshida. CONCUR Test-Of-Time Award 2021 (Invited Paper). In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 1:1-1:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2021.1,
author = {Bertrand, Nathalie and de Alfaro, Luca and van Glabbeek, Rob and Palamidessi, Catuscia and Yoshida, Nobuko},
title = {{CONCUR Test-Of-Time Award 2021}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {1:1--1:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.1},
URN = {urn:nbn:de:0030-drops-143786},
doi = {10.4230/LIPIcs.CONCUR.2021.1},
annote = {Keywords: Concurrency, CONCUR Test-of-Time Award}
}
Document
Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation
Abstract
This paper provides several optimizations of the rank-based approach for complementing Büchi automata. We start with Schewe’s theoretically optimal construction and develop a set of techniques for pruning its state space that are key to obtaining small complement automata in practice. In particular, the reductions (except one) have the property that they preserve (at least some) so-called super-tight runs, which are runs whose ranking is as tight as possible. Our evaluation on a large benchmark shows that the optimizations indeed significantly help the rank-based approach and that, in a large number of cases, the obtained complement is the smallest from those produced by state-of-the-art tools for Büchi complementation.
Cite as
Vojtěch Havlena and Ondřej Lengál. Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 2:1-2:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{havlena_et_al:LIPIcs.CONCUR.2021.2,
author = {Havlena, Vojt\v{e}ch and Leng\'{a}l, Ond\v{r}ej},
title = {{Reducing (To) the Ranks: Efficient Rank-Based B\"{u}chi Automata Complementation}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {2:1--2:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.2},
URN = {urn:nbn:de:0030-drops-143799},
doi = {10.4230/LIPIcs.CONCUR.2021.2},
annote = {Keywords: B\"{u}chi automata, rank-based complementation, super-tight runs}
}
Document
Inclusion Testing of Büchi Automata Based on Well-Quasiorders
Abstract
We introduce an algorithmic framework to decide whether inclusion holds between languages of infinite words over a finite alphabet. Our approach falls within the class of Ramsey-based methods and relies on a least fixpoint characterization of ω-languages leveraging ultimately periodic infinite words of type uv^ω, with u a finite prefix and v a finite period of an infinite word. We put forward an inclusion checking algorithm between Büchi automata, called BAInc, designed as a complete abstract interpretation using a pair of well-quasiorders on finite words. BAInc is quite simple: it consists of two least fixpoint computations (one for prefixes and the other for periods) manipulating finite sets (of pairs) of states compared by set inclusion, so that language inclusion holds when the sets (of pairs) of states of the fixpoints satisfy some basic conditions. We implemented BAInc in a tool called BAIT that we experimentally evaluated against the state-of-the-art. We gathered, in addition to existing benchmarks, a large number of new case studies stemming from program verification and word combinatorics, thereby significantly expanding both the scope and size of the available benchmark set. Our experimental results show that BAIT advances the state-of-the-art on an overwhelming majority of these benchmarks. Finally, we demonstrate the generality of our algorithmic framework by instantiating it to the inclusion problem of Büchi pushdown automata into Büchi automata.
Cite as
Kyveli Doveri, Pierre Ganty, Francesco Parolini, and Francesco Ranzato. Inclusion Testing of Büchi Automata Based on Well-Quasiorders. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{doveri_et_al:LIPIcs.CONCUR.2021.3,
author = {Doveri, Kyveli and Ganty, Pierre and Parolini, Francesco and Ranzato, Francesco},
title = {{Inclusion Testing of B\"{u}chi Automata Based on Well-Quasiorders}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {3:1--3:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.3},
URN = {urn:nbn:de:0030-drops-143802},
doi = {10.4230/LIPIcs.CONCUR.2021.3},
annote = {Keywords: B\"{u}chi (Pushdown) Automata, \omega-Language Inclusion, Well-quasiorders}
}
Document
Nominal Büchi Automata with Name Allocation
Abstract
Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach ω-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking.
Cite as
Henning Urbat, Daniel Hausmann, Stefan Milius, and Lutz Schröder. Nominal Büchi Automata with Name Allocation. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{urbat_et_al:LIPIcs.CONCUR.2021.4,
author = {Urbat, Henning and Hausmann, Daniel and Milius, Stefan and Schr\"{o}der, Lutz},
title = {{Nominal B\"{u}chi Automata with Name Allocation}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {4:1--4:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.4},
URN = {urn:nbn:de:0030-drops-143813},
doi = {10.4230/LIPIcs.CONCUR.2021.4},
annote = {Keywords: Data languages, infinite words, nominal sets, inclusion checking}
}
Document
Enforcing ω-Regular Properties in Markov Chains by Restarting
Abstract
Restarts are used in many computer systems to improve performance. Examples include reloading a webpage, reissuing a request, or restarting a randomized search. The design of restart strategies has been extensively studied by the performance evaluation community. In this paper, we address the problem of designing universal restart strategies, valid for arbitrary finite-state Markov chains, that enforce a given ω-regular property while not knowing the chain. A strategy enforces a property φ if, with probability 1, the number of restarts is finite, and the run of the Markov chain after the last restart satisfies φ. We design a simple "cautious" strategy that solves the problem, and a more sophisticated "bold" strategy with an almost optimal number of restarts.
Cite as
Javier Esparza, Stefan Kiefer, Jan Křetínský, and Maximilian Weininger. Enforcing ω-Regular Properties in Markov Chains by Restarting. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{esparza_et_al:LIPIcs.CONCUR.2021.5,
author = {Esparza, Javier and Kiefer, Stefan and K\v{r}et{\'\i}nsk\'{y}, Jan and Weininger, Maximilian},
title = {{Enforcing \omega-Regular Properties in Markov Chains by Restarting}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {5:1--5:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.5},
URN = {urn:nbn:de:0030-drops-143824},
doi = {10.4230/LIPIcs.CONCUR.2021.5},
annote = {Keywords: Markov chains, omega-regular properties, runtime enforcement}
}
Document
Linear-Time Model Checking Branching Processes
Abstract
(Multi-type) branching processes are a natural and well-studied model for generating random infinite trees. Branching processes feature both nondeterministic and probabilistic branching, generalizing both transition systems and Markov chains (but not generally Markov decision processes). We study the complexity of model checking branching processes against linear-time omega-regular specifications: is it the case almost surely that every branch of a tree randomly generated by the branching process satisfies the omega-regular specification? The main result is that for LTL specifications this problem is in PSPACE, subsuming classical results for transition systems and Markov chains, respectively. The underlying general model-checking algorithm is based on the automata-theoretic approach, using unambiguous Büchi automata.
Cite as
Stefan Kiefer, Pavel Semukhin, and Cas Widdershoven. Linear-Time Model Checking Branching Processes. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2021.6,
author = {Kiefer, Stefan and Semukhin, Pavel and Widdershoven, Cas},
title = {{Linear-Time Model Checking Branching Processes}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {6:1--6:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.6},
URN = {urn:nbn:de:0030-drops-143834},
doi = {10.4230/LIPIcs.CONCUR.2021.6},
annote = {Keywords: model checking, Markov chains, branching processes, automata, computational complexity}
}
Document
Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking
Abstract
Quantified linear temporal logic (QLTL) is an ω-regular extension of LTL allowing quantification over propositional variables. We study the model checking problem of QLTL-formulas over Markov chains and Markov decision processes (MDPs) with respect to the number of quantifier alternations of formulas in prenex normal form. For formulas with k{-}1 quantifier alternations, we prove that all qualitative and quantitative model checking problems are k-EXPSPACE-complete over Markov chains and k{+}1-EXPTIME-complete over MDPs.
As an application of these results, we generalize vacuity checking for LTL specifications from the non-probabilistic to the probabilistic setting. We show how to check whether an LTL-formula is affected by a subformula, and also study inherent vacuity for probabilistic systems.
Cite as
Jakob Piribauer, Christel Baier, Nathalie Bertrand, and Ocan Sankur. Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{piribauer_et_al:LIPIcs.CONCUR.2021.7,
author = {Piribauer, Jakob and Baier, Christel and Bertrand, Nathalie and Sankur, Ocan},
title = {{Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.7},
URN = {urn:nbn:de:0030-drops-143842},
doi = {10.4230/LIPIcs.CONCUR.2021.7},
annote = {Keywords: Quantified linear temporal logic, Markov chain, Markov decision process, vacuity}
}
Document
Subgame-Perfect Equilibria in Mean-Payoff Games
Abstract
In this paper, we provide an effective characterization of all the subgame-perfect equilibria in infinite duration games played on finite graphs with mean-payoff objectives. To this end, we introduce the notion of requirement, and the notion of negotiation function. We establish that the plays that are supported by SPEs are exactly those that are consistent with the least fixed point of the negotiation function. Finally, we show that the negotiation function is piecewise linear, and can be analyzed using the linear algebraic tool box. As a corollary, we prove the decidability of the SPE constrained existence problem, whose status was left open in the literature.
Cite as
Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Subgame-Perfect Equilibria in Mean-Payoff Games. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{brice_et_al:LIPIcs.CONCUR.2021.8,
author = {Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
title = {{Subgame-Perfect Equilibria in Mean-Payoff Games}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {8:1--8:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.8},
URN = {urn:nbn:de:0030-drops-143854},
doi = {10.4230/LIPIcs.CONCUR.2021.8},
annote = {Keywords: Games on graphs, subgame-perfect equilibria, mean-payoff objectives.}
}
Document
Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games
Abstract
Two-player mean-payoff Stackelberg games are nonzero-sum infinite duration games played on a bi-weighted graph by Leader (Player 0) and Follower (Player 1). Such games are played sequentially: first, Leader announces her strategy, second, Follower chooses his best-response. If we cannot impose which best-response is chosen by Follower, we say that Follower, though strategic, is adversarial towards Leader. The maximal value that Leader can get in this nonzero-sum game is called the adversarial Stackelberg value (ASV) of the game.
We study the robustness of strategies for Leader in these games against two types of deviations: (i) Modeling imprecision - the weights on the edges of the game arena may not be exactly correct, they may be delta-away from the right one. (ii) Sub-optimal response - Follower may play epsilon-optimal best-responses instead of perfect best-responses. First, we show that if the game is zero-sum then robustness is guaranteed while in the nonzero-sum case, optimal strategies for ASV are fragile. Second, we provide a solution concept to obtain strategies for Leader that are robust to both modeling imprecision, and as well as to the epsilon-optimal responses of Follower, and study several properties and algorithmic problems related to this solution concept.
Cite as
Mrudula Balachander, Shibashis Guha, and Jean-François Raskin. Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{balachander_et_al:LIPIcs.CONCUR.2021.9,
author = {Balachander, Mrudula and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
title = {{Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {9:1--9:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.9},
URN = {urn:nbn:de:0030-drops-143863},
doi = {10.4230/LIPIcs.CONCUR.2021.9},
annote = {Keywords: mean-payoff, Stackelberg games, synthesis}
}
Document
Continuous Positional Payoffs
Abstract
What payoffs are positionally determined for deterministic two-player antagonistic games on finite directed graphs? In this paper we study this question for payoffs that are continuous. The main reason why continuous positionally determined payoffs are interesting is that they include the multi-discounted payoffs.
We show that for continuous payoffs positional determinacy is equivalent to a simple property called prefix-monotonicity. We provide three proofs of it, using three major techniques of establishing positional determinacy - inductive technique, fixed point technique and strategy improvement technique. A combination of these approaches provides us with better understanding of the structure of continuous positionally determined payoffs as well as with some algorithmic results.
Cite as
Alexander Kozachinskiy. Continuous Positional Payoffs. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{kozachinskiy:LIPIcs.CONCUR.2021.10,
author = {Kozachinskiy, Alexander},
title = {{Continuous Positional Payoffs}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {10:1--10:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.10},
URN = {urn:nbn:de:0030-drops-143874},
doi = {10.4230/LIPIcs.CONCUR.2021.10},
annote = {Keywords: Games on graphs, positional strategies, continuous payoffs}
}
Document
Transience in Countable MDPs
Abstract
The Transience objective is not to visit any state infinitely often. While this is not possible in any finite Markov Decision Process (MDP), it can be satisfied in countably infinite ones, e.g., if the transition graph is acyclic.
We prove the following fundamental properties of Transience in countably infinite MDPs.
1) There exist uniformly ε-optimal MD strategies (memoryless deterministic) for Transience, even in infinitely branching MDPs.
2) Optimal strategies for Transience need not exist, even if the MDP is finitely branching. However, if an optimal strategy exists then there is also an optimal MD strategy.
3) If an MDP is universally transient (i.e., almost surely transient under all strategies) then many other objectives have a lower strategy complexity than in general MDPs. E.g., ε-optimal strategies for Safety and co-Büchi and optimal strategies for {0,1,2}-Parity (where they exist) can be chosen MD, even if the MDP is infinitely branching.
Cite as
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Transience in Countable MDPs. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2021.11,
author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
title = {{Transience in Countable MDPs}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {11:1--11:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.11},
URN = {urn:nbn:de:0030-drops-143881},
doi = {10.4230/LIPIcs.CONCUR.2021.11},
annote = {Keywords: Markov decision processes, Parity, Transience}
}
Document
Strategy Complexity of Mean Payoff, Total Payoff and Point Payoff Objectives in Countable MDPs
Abstract
We study countably infinite Markov decision processes (MDPs) with real-valued transition rewards. Every infinite run induces the following sequences of payoffs: 1. Point payoff (the sequence of directly seen transition rewards), 2. Total payoff (the sequence of the sums of all rewards so far), and 3. Mean payoff. For each payoff type, the objective is to maximize the probability that the liminf is non-negative. We establish the complete picture of the strategy complexity of these objectives, i.e., how much memory is necessary and sufficient for ε-optimal (resp. optimal) strategies. Some cases can be won with memoryless deterministic strategies, while others require a step counter, a reward counter, or both.
Cite as
Richard Mayr and Eric Munday. Strategy Complexity of Mean Payoff, Total Payoff and Point Payoff Objectives in Countable MDPs. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{mayr_et_al:LIPIcs.CONCUR.2021.12,
author = {Mayr, Richard and Munday, Eric},
title = {{Strategy Complexity of Mean Payoff, Total Payoff and Point Payoff Objectives in Countable MDPs}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {12:1--12:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.12},
URN = {urn:nbn:de:0030-drops-143893},
doi = {10.4230/LIPIcs.CONCUR.2021.12},
annote = {Keywords: Markov decision processes, Strategy complexity, Mean payoff}
}
Document
Model Checking Quantum Continuous-Time Markov Chains
Abstract
Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialise the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-the-art real root isolation algorithm under Schanuel’s conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.
Cite as
Ming Xu, Jingyi Mei, Ji Guan, and Nengkun Yu. Model Checking Quantum Continuous-Time Markov Chains. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{xu_et_al:LIPIcs.CONCUR.2021.13,
author = {Xu, Ming and Mei, Jingyi and Guan, Ji and Yu, Nengkun},
title = {{Model Checking Quantum Continuous-Time Markov Chains}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.13},
URN = {urn:nbn:de:0030-drops-143908},
doi = {10.4230/LIPIcs.CONCUR.2021.13},
annote = {Keywords: Model Checking, Formal Logic, Quantum Computing, Computer Algebra}
}
Document
A Unifying Framework for Deciding Synchronizability
Abstract
Several notions of synchronizability of a message-passing system have been introduced in the literature. Roughly, a system is called synchronizable if every execution can be rescheduled so that it meets certain criteria, e.g., a channel bound. We provide a framework, based on MSO logic and (special) tree-width, that unifies existing definitions, explains their good properties, and allows one to easily derive other, more general definitions and decidability results for synchronizability.
Cite as
Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, and Amrita Suresh. A Unifying Framework for Deciding Synchronizability. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bollig_et_al:LIPIcs.CONCUR.2021.14,
author = {Bollig, Benedikt and Di Giusto, Cinzia and Finkel, Alain and Laversa, Laetitia and Lozes, Etienne and Suresh, Amrita},
title = {{A Unifying Framework for Deciding Synchronizability}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.14},
URN = {urn:nbn:de:0030-drops-143917},
doi = {10.4230/LIPIcs.CONCUR.2021.14},
annote = {Keywords: communicating finite-state machines, message sequence charts, synchronizability, MSO logic, special tree-width}
}
Document
Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms
Abstract
Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstracts infinite-state distributed systems that represent distributed algorithms into finite-state guard automata. The soundness of the approach corresponds to the Scott-continuity of the abstraction, which relies on the assumption that the distributed algorithms are layered. Guard automata thus enable the verification of safety and liveness properties of distributed algorithms.
Cite as
Nathalie Bertrand, Bastien Thomas, and Josef Widder. Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2021.15,
author = {Bertrand, Nathalie and Thomas, Bastien and Widder, Josef},
title = {{Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.15},
URN = {urn:nbn:de:0030-drops-143926},
doi = {10.4230/LIPIcs.CONCUR.2021.15},
annote = {Keywords: Verification, Distributed algorithms, Domain theory}
}
Document
Dynamic Data-Race Detection Through the Fine-Grained Lens
Abstract
Data races are among the most common bugs in concurrency. The standard approach to data-race detection is via dynamic analyses, which work over executions of concurrent programs, instead of the program source code. The rich literature on the topic has created various notions of dynamic data races, which are known to be detected efficiently when certain parameters (e.g., number of threads) are small. However, the fine-grained complexity of all these notions of races has remained elusive, making it impossible to characterize their trade-offs between precision and efficiency.
In this work we establish several fine-grained separations between many popular notions of dynamic data races. The input is an execution trace σ with 𝒩 events, 𝒯 threads and ℒ locks. Our main results are as follows. First, we show that happens-before HB races can be detected in O(𝒩⋅ min(𝒯, ℒ)) time, improving over the standard O(𝒩⋅ 𝒯) bound when ℒ = o(𝒯). Moreover, we show that even reporting an HB race that involves a read access is hard for 2-orthogonal vectors (2-OV). This is the first rigorous proof of the conjectured quadratic lower-bound in detecting HB races. Second, we show that the recently introduced synchronization-preserving races are hard to detect for 3-OV and thus have a cubic lower bound, when 𝒯 = Ω(𝒩). This establishes a complexity separation from HB races which are known to be strictly less expressive. Third, we show that lock-cover races are hard for 2-OV, and thus have a quadratic lower-bound, even when 𝒯 = 2 and ℒ = ω(log 𝒩). The similar notion of lock-set races is known to be detectable in O(𝒩⋅ ℒ) time, and thus we achieve a complexity separation between the two. Moreover, we show that lock-set races become hitting-set (HS)-hard when ℒ = Θ(𝒩), and thus also have a quadratic lower bound, when the input is sufficiently complex. To our knowledge, this is the first work that characterizes the complexity of well-established dynamic race-detection techniques, allowing for a rigorous comparison between them.
Cite as
Rucha Kulkarni, Umang Mathur, and Andreas Pavlogiannis. Dynamic Data-Race Detection Through the Fine-Grained Lens. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 16:1-16:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{kulkarni_et_al:LIPIcs.CONCUR.2021.16,
author = {Kulkarni, Rucha and Mathur, Umang and Pavlogiannis, Andreas},
title = {{Dynamic Data-Race Detection Through the Fine-Grained Lens}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {16:1--16:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.16},
URN = {urn:nbn:de:0030-drops-143931},
doi = {10.4230/LIPIcs.CONCUR.2021.16},
annote = {Keywords: dynamic analyses, data races, fine-grained complexity}
}
Document
Adaptive Synchronisation of Pushdown Automata
Abstract
We introduce the notion of adaptive synchronisation for pushdown automata, in which there is an external observer who has no knowledge about the current state of the pushdown automaton, but can observe the contents of the stack. The observer would then like to decide if it is possible to bring the automaton from any state into some predetermined state by giving inputs to it in an adaptive manner, i.e., the next input letter to be given can depend on how the contents of the stack changed after the current input letter. We show that for non-deterministic pushdown automata, this problem is 2-EXPTIME-complete and for deterministic pushdown automata, we show EXPTIME-completeness.
To prove the lower bounds, we first introduce (different variants of) subset-synchronisation and show that these problems are polynomial-time equivalent with the adaptive synchronisation problem. We then prove hardness results for the subset-synchronisation problems. For proving the upper bounds, we consider the problem of deciding if a given alternating pushdown system has an accepting run with at most k leaves and we provide an n^O(k²) time algorithm for this problem.
Cite as
A. R. Balasubramanian and K. S. Thejaswini. Adaptive Synchronisation of Pushdown Automata. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{balasubramanian_et_al:LIPIcs.CONCUR.2021.17,
author = {Balasubramanian, A. R. and Thejaswini, K. S.},
title = {{Adaptive Synchronisation of Pushdown Automata}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {17:1--17:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.17},
URN = {urn:nbn:de:0030-drops-143948},
doi = {10.4230/LIPIcs.CONCUR.2021.17},
annote = {Keywords: Adaptive synchronisation, Pushdown automata, Alternating pushdown systems}
}
Document
Decomposing Permutation Automata
Abstract
A deterministic finite automaton (DFA) 𝒜 is composite if its language L(𝒜) can be decomposed into an intersection ⋂_{i = 1}^k L(𝒜_i) of languages of smaller DFAs. Otherwise, 𝒜 is prime. This notion of primality was introduced by Kupferman and Mosheiff in 2013, and while they proved that we can decide whether a DFA is composite, the precise complexity of this problem is still open, with a doubly-exponential gap between the upper and lower bounds. In this work, we focus on permutation DFAs, i.e., those for which the transition monoid is a group. We provide an NP algorithm to decide whether a permutation DFA is composite, and show that the difficulty of this problem comes from the number of non-accepting states of the instance: we give a fixed-parameter tractable algorithm with the number of rejecting states as the parameter. Moreover, we investigate the class of commutative permutation DFAs. Their structural properties allow us to decide compositionality in NL, and even in LOGSPACE if the alphabet size is fixed. Despite this low complexity, we show that complex behaviors still arise in this class: we provide a family of composite DFAs each requiring polynomially many factors with respect to its size. We also consider the variant of the problem that asks whether a DFA is k-factor composite, that is, decomposable into k smaller DFAs, for some given integer k ∈ ℕ. We show that, for commutative permutation DFAs, restricting the number of factors makes the decision computationally harder, and yields a problem with tight bounds: it is NP-complete. Finally, we show that in general, this problem is in PSPACE, and it is in LOGSPACE for DFAs with a singleton alphabet.
Cite as
Ismaël Jecker, Nicolas Mazzocchi, and Petra Wolf. Decomposing Permutation Automata. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{jecker_et_al:LIPIcs.CONCUR.2021.18,
author = {Jecker, Isma\"{e}l and Mazzocchi, Nicolas and Wolf, Petra},
title = {{Decomposing Permutation Automata}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {18:1--18:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.18},
URN = {urn:nbn:de:0030-drops-143956},
doi = {10.4230/LIPIcs.CONCUR.2021.18},
annote = {Keywords: Deterministic finite automata (DFA), Permutation automata, Commutative languages, Decomposition, Regular Languages, Primality}
}
Document
Algebra and Coalgebra of Stream Products
Abstract
We study connections among polynomials, differential equations and streams over a field 𝕂, in terms of algebra and coalgebra. We first introduce the class of (F,G)-products on streams, those where the stream derivative of a product can be expressed as a polynomial of the streams themselves and their derivatives. Our first result is that, for every (F,G)-product, there is a canonical way to construct a transition function on polynomials such that the induced unique final coalgebra morphism from polynomials into streams is the (unique) 𝕂-algebra homomorphism - and vice-versa. This implies one can reason algebraically on streams, via their polynomial representation. We apply this result to obtain an algebraic-geometric decision algorithm for polynomial stream equivalence, for an underlying generic (F,G)-product. As an example of reasoning on streams, we focus on specific products (convolution, shuffle, Hadamard) and show how to obtain closed forms of algebraic generating functions of combinatorial sequences, as well as solutions of nonlinear ordinary differential equations.
Cite as
Michele Boreale and Daniele Gorla. Algebra and Coalgebra of Stream Products. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{boreale_et_al:LIPIcs.CONCUR.2021.19,
author = {Boreale, Michele and Gorla, Daniele},
title = {{Algebra and Coalgebra of Stream Products}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.19},
URN = {urn:nbn:de:0030-drops-143969},
doi = {10.4230/LIPIcs.CONCUR.2021.19},
annote = {Keywords: Streams, coalgebras, polynomials, differential equations}
}
Document
Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL
Abstract
Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is necessary to provide unifying semantics and automation for both activities. In this paper we apply Interaction Trees in Isabelle/HOL to produce a verification and simulation framework for state-rich process languages. We develop the core theory and verification techniques for Interaction Trees, use them to give a semantics to the CSP and Circus languages, and formally link our new semantics with the failures-divergences semantic model. We also show how the Isabelle code generator can be used to generate verified executable simulations for reactive and concurrent programs.
Cite as
Simon Foster, Chung-Kil Hur, and Jim Woodcock. Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{foster_et_al:LIPIcs.CONCUR.2021.20,
author = {Foster, Simon and Hur, Chung-Kil and Woodcock, Jim},
title = {{Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {20:1--20:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.20},
URN = {urn:nbn:de:0030-drops-143973},
doi = {10.4230/LIPIcs.CONCUR.2021.20},
annote = {Keywords: Coinduction, Process Algebra, Theorem Proving, Simulation}
}
Document
Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down
Abstract
The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of stability of chain colimits; we extend the framework to the presence of a monadic effect, too, restricting to fibrations of complete lattice-valued predicates. Practical benefits of our categorical theory are exemplified by new "upside-down" witness notions for three verification problems: probabilistic liveness, and acceptance and model-checking with respect to bottom-up tree automata.
Cite as
Mayuko Kori, Ichiro Hasuo, and Shin-ya Katsumata. Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{kori_et_al:LIPIcs.CONCUR.2021.21,
author = {Kori, Mayuko and Hasuo, Ichiro and Katsumata, Shin-ya},
title = {{Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {21:1--21:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.21},
URN = {urn:nbn:de:0030-drops-143982},
doi = {10.4230/LIPIcs.CONCUR.2021.21},
annote = {Keywords: initial algebra, final coalgebra, fibration, category theory}
}
Document
SMT-Based Model Checking of Max-Plus Linear Systems
Abstract
Max-Plus Linear (MPL) systems are an algebraic formalism with practical applications in transportation networks, manufacturing and biological systems. MPL systems can be naturally modeled as infinite-state transition systems, and exhibit interesting structural properties (e.g. periodicity or steady state), for which analysis methods have been recently proposed. In this paper, we tackle the open problem of specifying and analyzing user-defined temporal properties for MPL systems. We propose Time-Difference LTL (TDLTL), a logic that encompasses the delays between the discrete-time events governed by an MPL system, and characterize the problem of model checking TDLTL over MPL. We propose a family of specialized algorithms leveraging the periodic behaviour of an MPL system. We prove soundness and completeness, showing that the transient and cyclicity of the MPL system induce a completeness threshold for the verification problem. The algorithms are cast in the setting of SMT-based verification of infinite-state transition systems over the reals, with variants depending on the (incremental vs upfront) computation of the bound, and on the (explicit vs implicit) unrolling of the transition relation. Our comprehensive experiments show that the proposed techniques can be applied to MPL systems of large dimensions and on general TDLTL formulae, with remarkable performance gains against a dedicated abstraction-based technique and a translation to the nuXmv symbolic model checker.
Cite as
Muhammad Syifa'ul Mufid, Andrea Micheli, Alessandro Abate, and Alessandro Cimatti. SMT-Based Model Checking of Max-Plus Linear Systems. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{mufid_et_al:LIPIcs.CONCUR.2021.22,
author = {Mufid, Muhammad Syifa'ul and Micheli, Andrea and Abate, Alessandro and Cimatti, Alessandro},
title = {{SMT-Based Model Checking of Max-Plus Linear Systems}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {22:1--22:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.22},
URN = {urn:nbn:de:0030-drops-143993},
doi = {10.4230/LIPIcs.CONCUR.2021.22},
annote = {Keywords: Max-Plus Linear Systems, Satisfiability Modulo Theory, Model Checking, Linear Temporal Logic}
}
Document
A Decidable Non-Regular Modal Fixpoint Logic
Abstract
Fixpoint Logic with Chop (FLC) extends the modal μ-calculus with an operator for sequential composition between predicate transformers. This makes it an expressive modal fixpoint logic which is capable of formalising many non-regular program properties. Its satisfiability problem is highly undecidable. Here we define Visibly Pushdown Fixpoint Logic with Chop, a fragment in which fixpoint formulas are required to be of a certain form resembling visibly pushdown grammars. We give a sound and complete game-theoretic characterisation of FLC’s satisfiability problem and show that the games corresponding to formulas from this fragment are stair-parity games and therefore effectively solvable, resulting in 2EXPTIME-completeness of this fragment. The lower bound is inherited from PDL over Recursive Programs, which is structurally similar but considerably weaker in expressive power.
Cite as
Florian Bruse and Martin Lange. A Decidable Non-Regular Modal Fixpoint Logic. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bruse_et_al:LIPIcs.CONCUR.2021.23,
author = {Bruse, Florian and Lange, Martin},
title = {{A Decidable Non-Regular Modal Fixpoint Logic}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {23:1--23:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.23},
URN = {urn:nbn:de:0030-drops-144003},
doi = {10.4230/LIPIcs.CONCUR.2021.23},
annote = {Keywords: formal specification, temporal logic, expressive power}
}
Document
A Temporal Logic for Strategic Hyperproperties
Abstract
Hyperproperties are commonly used in computer security to define information-flow policies and other requirements that reason about the relationship between multiple computations. In this paper, we study a novel class of hyperproperties where the individual computation paths are chosen by the strategic choices of a coalition of agents in a multi-agent system. We introduce HyperATL^*, an extension of computation tree logic with path variables and strategy quantifiers. HyperATL^* can express strategic hyperproperties, such as that the scheduler in a concurrent system has a strategy to avoid information leakage. HyperATL^* is particularly useful to specify asynchronous hyperproperties, i.e., hyperproperties where the speed of the execution on the different computation paths depends on the choices of the scheduler. Unlike other recent logics for the specification of asynchronous hyperproperties, our logic is the first to admit decidable model checking for the full logic. We present a model checking algorithm for HyperATL^* based on alternating word automata, and show that our algorithm is asymptotically optimal by providing a matching lower bound. We have implemented a prototype model checker for a fragment of HyperATL^*, able to check various security properties on small programs.
Cite as
Raven Beutner and Bernd Finkbeiner. A Temporal Logic for Strategic Hyperproperties. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{beutner_et_al:LIPIcs.CONCUR.2021.24,
author = {Beutner, Raven and Finkbeiner, Bernd},
title = {{A Temporal Logic for Strategic Hyperproperties}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {24:1--24:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.24},
URN = {urn:nbn:de:0030-drops-144019},
doi = {10.4230/LIPIcs.CONCUR.2021.24},
annote = {Keywords: hyperproperties, temporal logic, alternating-time temporal logic, model checking, multi-agent systems, information flow, asynchronous hyperproperties}
}
Document
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives
Abstract
The window mechanism was introduced by Chatterjee et al. to reinforce mean-payoff and total-payoff objectives with time bounds in two-player turn-based games on graphs [Krishnendu Chatterjee et al., 2015]. It has since proved useful in a variety of settings, including parity objectives in games [Véronique Bruyère et al., 2016] and both mean-payoff and parity objectives in Markov decision processes [Thomas Brihaye et al., 2020].
We study window parity objectives in timed automata and timed games: given a bound on the window size, a path satisfies such an objective if, in all states along the path, we see a sufficiently small window in which the smallest priority is even. We show that checking that all time-divergent paths of a timed automaton satisfy such a window parity objective can be done in polynomial space, and that the corresponding timed games can be solved in exponential time. This matches the complexity class of timed parity games, while adding the ability to reason about time bounds. We also consider multi-dimensional objectives and show that the complexity class does not increase. To the best of our knowledge, this is the first study of the window mechanism in a real-time setting.
Cite as
James C. A. Main, Mickael Randour, and Jeremy Sproston. Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{main_et_al:LIPIcs.CONCUR.2021.25,
author = {Main, James C. A. and Randour, Mickael and Sproston, Jeremy},
title = {{Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.25},
URN = {urn:nbn:de:0030-drops-144021},
doi = {10.4230/LIPIcs.CONCUR.2021.25},
annote = {Keywords: Window objectives, timed automata, timed games, parity games}
}
Document
Arena-Independent Finite-Memory Determinacy in Stochastic Games
Abstract
We study stochastic zero-sum games on graphs, which are prevalent tools to model decision-making in presence of an antagonistic opponent in a random environment. In this setting, an important question is the one of strategy complexity: what kinds of strategies are sufficient or required to play optimally (e.g., randomization or memory requirements)? Our contributions further the understanding of arena-independent finite-memory (AIFM) determinacy, i.e., the study of objectives for which memory is needed, but in a way that only depends on limited parameters of the game graphs. First, we show that objectives for which pure AIFM strategies suffice to play optimally also admit pure AIFM subgame perfect strategies. Second, we show that we can reduce the study of objectives for which pure AIFM strategies suffice in two-player stochastic games to the easier study of one-player stochastic games (i.e., Markov decision processes). Third, we characterize the sufficiency of AIFM strategies through two intuitive properties of objectives. This work extends a line of research started on deterministic games in [Bouyer et al., 2020] to stochastic ones.
Cite as
Patricia Bouyer, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Arena-Independent Finite-Memory Determinacy in Stochastic Games. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2021.26,
author = {Bouyer, Patricia and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre},
title = {{Arena-Independent Finite-Memory Determinacy in Stochastic Games}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {26:1--26:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.26},
URN = {urn:nbn:de:0030-drops-144037},
doi = {10.4230/LIPIcs.CONCUR.2021.26},
annote = {Keywords: two-player games on graphs, stochastic games, Markov decision processes, finite-memory determinacy, optimal strategies}
}
Document
Stackelberg-Pareto Synthesis
Abstract
In this paper, we study the framework of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1 responds rationally with a strategy that is an optimal response. While it is usually assumed that Player 1 has a single objective, we consider here the new setting where he has several. In this context, after responding with his strategy, Player 1 gets a payoff in the form of a vector of Booleans corresponding to his satisfied objectives. Rationality of Player 1 is encoded by the fact that his response must produce a Pareto-optimal payoff given the strategy of Player 0. We study the Stackelberg-Pareto Synthesis problem which asks whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1. For games in which objectives are either all parity or all reachability objectives, we show that this problem is fixed-parameter tractable and NEXPTIME-complete. This problem is already NP-complete in the simple case of reachability objectives and graphs that are trees.
Cite as
Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Stackelberg-Pareto Synthesis. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2021.27,
author = {Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Tamines, Cl\'{e}ment},
title = {{Stackelberg-Pareto Synthesis}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {27:1--27:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.27},
URN = {urn:nbn:de:0030-drops-144040},
doi = {10.4230/LIPIcs.CONCUR.2021.27},
annote = {Keywords: Stackelberg non-zero sum games played on graphs, synthesis, parity objectives}
}
Document
The Orbit Problem for Parametric Linear Dynamical Systems
Abstract
We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters.
More precisely, consider a d-dimensional square matrix M whose entries are algebraic functions in one or more real variables. Given initial and target vectors u,v ∈ ℚ^d, the parametric point-to-point orbit problem asks whether there exist values of the parameters giving rise to a concrete matrix N ∈ ℝ^{d× d}, and a positive integer n ∈ ℕ, such that N^{n} u = v.
We show decidability for the case in which M depends only upon a single parameter, and we exhibit a reduction from the well-known Skolem Problem for linear recurrence sequences, suggesting intractability in the case of two or more parameters.
Cite as
Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell. The Orbit Problem for Parametric Linear Dynamical Systems. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{baier_et_al:LIPIcs.CONCUR.2021.28,
author = {Baier, Christel and Funke, Florian and Jantsch, Simon and Karimov, Toghrul and Lefaucheux, Engel and Luca, Florian and Ouaknine, Jo\"{e}l and Purser, David and Whiteland, Markus A. and Worrell, James},
title = {{The Orbit Problem for Parametric Linear Dynamical Systems}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {28:1--28:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.28},
URN = {urn:nbn:de:0030-drops-144053},
doi = {10.4230/LIPIcs.CONCUR.2021.28},
annote = {Keywords: Orbit problem, parametric, linear dynamical systems}
}
Document
Scope-Bounded Reachability in Valence Systems
Abstract
Multi-pushdown systems are a standard model for concurrent recursive programs, but they have an undecidable reachability problem. Therefore, there have been several proposals to underapproximate their sets of runs so that reachability in this underapproximation becomes decidable. One such underapproximation that covers a relatively high portion of runs is scope boundedness. In such a run, after each push to stack i, the corresponding pop operation must come within a bounded number of visits to stack i.
In this work, we generalize this approach to a large class of infinite-state systems. For this, we consider the model of valence systems, which consist of a finite-state control and an infinite-state storage mechanism that is specified by a finite undirected graph. This framework captures pushdowns, vector addition systems, integer vector addition systems, and combinations thereof. For this framework, we propose a notion of scope boundedness that coincides with the classical notion when the storage mechanism happens to be a multi-pushdown.
We show that with this notion, reachability can be decided in PSPACE for every storage mechanism in the framework. Moreover, we describe the full complexity landscape of this problem across all storage mechanisms, both in the case of (i) the scope bound being given as input and (ii) for fixed scope bounds. Finally, we provide an almost complete description of the complexity landscape if even a description of the storage mechanism is part of the input.
Cite as
Aneesh K. Shetty, S. Krishna, and Georg Zetzsche. Scope-Bounded Reachability in Valence Systems. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{shetty_et_al:LIPIcs.CONCUR.2021.29,
author = {Shetty, Aneesh K. and Krishna, S. and Zetzsche, Georg},
title = {{Scope-Bounded Reachability in Valence Systems}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {29:1--29:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.29},
URN = {urn:nbn:de:0030-drops-144069},
doi = {10.4230/LIPIcs.CONCUR.2021.29},
annote = {Keywords: multi-pushdown systems, underapproximations, valence systems, reachability}
}
Document
Deciding Polynomial Termination Complexity for VASS Programs
Abstract
We show that for every fixed degree k ≥ 3, the problem whether the termination/counter complexity of a given demonic VASS is O(n^k), Ω(n^k), and Θ(n^k) is coNP-complete, NP-complete, and DP-complete, respectively. We also classify the complexity of these problems for k ≤ 2. This shows that the polynomial-time algorithm designed for strongly connected demonic VASS in previous works cannot be extended to the general case. Then, we prove that the same problems for VASS games are PSPACE-complete. Again, we classify the complexity also for k ≤ 2. Tractable subclasses of demonic VASS and VASS games are obtained by bounding certain structural parameters, which opens the way to applications in program analysis despite the presented lower complexity bounds.
Cite as
Michal Ajdarów and Antonín Kučera. Deciding Polynomial Termination Complexity for VASS Programs. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 30:1-30:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{ajdarow_et_al:LIPIcs.CONCUR.2021.30,
author = {Ajdar\'{o}w, Michal and Ku\v{c}era, Anton{\'\i}n},
title = {{Deciding Polynomial Termination Complexity for VASS Programs}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {30:1--30:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.30},
URN = {urn:nbn:de:0030-drops-144076},
doi = {10.4230/LIPIcs.CONCUR.2021.30},
annote = {Keywords: Termination complexity, vector addition systems}
}
Document
Bisimulation by Partitioning Is Ω((m+n)log n)
Abstract
An asymptotic lowerbound of Ω((m+n)log n) is established for partition refinement algorithms that decide bisimilarity on labeled transition systems. The lowerbound is obtained by subsequently analysing two families of deterministic transition systems - one with a growing action set and another with a fixed action set.
For deterministic transition systems with a one-letter action set, bisimilarity can be decided with fundamentally different techniques than partition refinement. In particular, Paige, Tarjan, and Bonic give a linear algorithm for this specific situation. We show, exploiting the concept of an oracle, that the approach of Paige, Tarjan, and Bonic is not of help to develop a generic algorithm for deciding bisimilarity on labeled transition systems that is faster than the established lowerbound of Ω((m+n)log n).
Cite as
Jan Friso Groote, Jan Martens, and Erik de Vink. Bisimulation by Partitioning Is Ω((m+n)log n). In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{groote_et_al:LIPIcs.CONCUR.2021.31,
author = {Groote, Jan Friso and Martens, Jan and de Vink, Erik},
title = {{Bisimulation by Partitioning Is \Omega((m+n)log n)}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {31:1--31:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.31},
URN = {urn:nbn:de:0030-drops-144087},
doi = {10.4230/LIPIcs.CONCUR.2021.31},
annote = {Keywords: Bisimilarity, partition refinement, labeled transition system, lowerbound}
}
Document
Explaining Behavioural Inequivalence Generically in Quasilinear Time
Abstract
We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time 𝒪((m+n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was 𝒪(m n).
Cite as
Thorsten Wißmann, Stefan Milius, and Lutz Schröder. Explaining Behavioural Inequivalence Generically in Quasilinear Time. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{wimann_et_al:LIPIcs.CONCUR.2021.32,
author = {Wi{\ss}mann, Thorsten and Milius, Stefan and Schr\"{o}der, Lutz},
title = {{Explaining Behavioural Inequivalence Generically in Quasilinear Time}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {32:1--32:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.32},
URN = {urn:nbn:de:0030-drops-144094},
doi = {10.4230/LIPIcs.CONCUR.2021.32},
annote = {Keywords: bisimulation, partition refinement, modal logic, distinguishing formulae, coalgebra}
}
Document
Enabling Preserving Bisimulation Equivalence
Abstract
Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.
Cite as
Rob van Glabbeek, Peter Höfner, and Weiyou Wang. Enabling Preserving Bisimulation Equivalence. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{vanglabbeek_et_al:LIPIcs.CONCUR.2021.33,
author = {van Glabbeek, Rob and H\"{o}fner, Peter and Wang, Weiyou},
title = {{Enabling Preserving Bisimulation Equivalence}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {33:1--33:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.33},
URN = {urn:nbn:de:0030-drops-144107},
doi = {10.4230/LIPIcs.CONCUR.2021.33},
annote = {Keywords: bisimilarity, liveness properties, fairness assumptions, process algebra}
}
Document
Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes
Abstract
We address the problem of analysing the complexity of concurrent programs written in Pi-calculus. We are interested in parallel complexity, or span, understood as the execution time in a model with maximal parallelism. A type system for parallel complexity has been recently proposed by the first two authors but it is too imprecise for non-linear channels and cannot analyse some concurrent processes. Aiming for a more precise analysis, we design a type system which builds on the concepts of sized types and usages. The sized types allow us to parametrize the complexity by the size of inputs, and the usages allow us to achieve a kind of rely-guarantee reasoning on the timing each process communicates with its environment. We prove that our new type system soundly estimates the parallel complexity, and show through examples that it is often more precise than the previous type system of the first two authors.
Cite as
Patrick Baillot, Alexis Ghyselen, and Naoki Kobayashi. Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 34:1-34:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{baillot_et_al:LIPIcs.CONCUR.2021.34,
author = {Baillot, Patrick and Ghyselen, Alexis and Kobayashi, Naoki},
title = {{Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {34:1--34:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.34},
URN = {urn:nbn:de:0030-drops-144111},
doi = {10.4230/LIPIcs.CONCUR.2021.34},
annote = {Keywords: Type Systems, Pi-calculus, Process Calculi, Complexity Analysis, Usages, Sized Types}
}
Document
Generalising Projection in Asynchronous Multiparty Session Types
Abstract
Multiparty session types (MSTs) provide an efficient methodology for specifying and verifying message passing software systems. In the theory of MSTs, a global type specifies the interaction among the roles at the global level. A local specification for each role is generated by projecting from the global type on to the message exchanges it participates in. Whenever a global type can be projected on to each role, the composition of the projections is deadlock free and has exactly the behaviours specified by the global type. The key to the usability of MSTs is the projection operation: a more expressive projection allows more systems to be type-checked but requires a more difficult soundness argument.
In this paper, we generalise the standard projection operation in MSTs. This allows us to model and type-check many design patterns in distributed systems, such as load balancing, that are rejected by the standard projection. The key to the new projection is an analysis that tracks causality between messages. Our soundness proof uses novel graph-theoretic techniques from the theory of message-sequence charts. We demonstrate the efficacy of the new projection operation by showing many global types for common patterns that can be projected under our projection but not under the standard projection operation.
Cite as
Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. Generalising Projection in Asynchronous Multiparty Session Types. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 35:1-35:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{majumdar_et_al:LIPIcs.CONCUR.2021.35,
author = {Majumdar, Rupak and Mukund, Madhavan and Stutz, Felix and Zufferey, Damien},
title = {{Generalising Projection in Asynchronous Multiparty Session Types}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {35:1--35:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.35},
URN = {urn:nbn:de:0030-drops-144125},
doi = {10.4230/LIPIcs.CONCUR.2021.35},
annote = {Keywords: Multiparty session types, Verification, Communicating state machines}
}
Document
Separating Sessions Smoothly
Abstract
This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard’s Mix rule, a crucial ingredient for channel forwarding and exceptions.
Cite as
Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating Sessions Smoothly. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{fowler_et_al:LIPIcs.CONCUR.2021.36,
author = {Fowler, Simon and Kokke, Wen and Dardha, Ornela and Lindley, Sam and Morris, J. Garrett},
title = {{Separating Sessions Smoothly}},
booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
pages = {36:1--36:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-203-7},
ISSN = {1868-8969},
year = {2021},
volume = {203},
editor = {Haddad, Serge and Varacca, Daniele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.36},
URN = {urn:nbn:de:0030-drops-144138},
doi = {10.4230/LIPIcs.CONCUR.2021.36},
annote = {Keywords: session types, hypersequents, linear lambda calculus}
}