Volume
LIPIcs, Volume 171
31st International Conference on Concurrency Theory (CONCUR 2020)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Publication Details
- published at: 2020-08-26
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-160-3
- DBLP: db/conf/concur/concur2020
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 171, CONCUR 2020, Complete Volume
Abstract
LIPIcs, Volume 171, CONCUR 2020, Complete Volume
Cite as
31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 1-984, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Proceedings{konnov_et_al:LIPIcs.CONCUR.2020,
title = {{LIPIcs, Volume 171, CONCUR 2020, Complete Volume}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {1--984},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020},
URN = {urn:nbn:de:0030-drops-128115},
doi = {10.4230/LIPIcs.CONCUR.2020},
annote = {Keywords: LIPIcs, Volume 171, CONCUR 2020, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{konnov_et_al:LIPIcs.CONCUR.2020.0,
author = {Konnov, Igor and Kov\'{a}cs, Laura},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {0:i--0:xvi},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.0},
URN = {urn:nbn:de:0030-drops-128125},
doi = {10.4230/LIPIcs.CONCUR.2020.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
On Privacy and Accuracy in Data Releases (Invited Paper)
Abstract
In this paper we study the relationship between privacy and accuracy in the context of correlated datasets. We use a model of quantitative information flow to describe the the trade-off between privacy of individuals' data and and the utility of queries to that data by modelling the effectiveness of adversaries attempting to make inferences after a data release.
We show that, where correlations exist in datasets, it is not possible to implement optimal noise-adding mechanisms that give the best possible accuracy or the best possible privacy in all situations. Finally we illustrate the trade-off between accuracy and privacy for local and oblivious differentially private mechanisms in terms of inference attacks on medium-scale datasets.
Cite as
Mário S. Alvim, Natasha Fernandes, Annabelle McIver, and Gabriel H. Nunes. On Privacy and Accuracy in Data Releases (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{alvim_et_al:LIPIcs.CONCUR.2020.1,
author = {Alvim, M\'{a}rio S. and Fernandes, Natasha and McIver, Annabelle and Nunes, Gabriel H.},
title = {{On Privacy and Accuracy in Data Releases}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {1:1--1:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.1},
URN = {urn:nbn:de:0030-drops-128130},
doi = {10.4230/LIPIcs.CONCUR.2020.1},
annote = {Keywords: Privacy/utility trade-off, Quantitative Information Flow, inference attacks}
}
Document
Invited Paper
A Survey of Bidding Games on Graphs (Invited Paper)
Abstract
A graph game is a two-player zero-sum game in which the players move a token throughout a graph to produce an infinite path, which determines the winner or payoff of the game. In bidding games, both players have budgets, and in each turn, we hold an "auction" (bidding) to determine which player moves the token. In this survey, we consider several bidding mechanisms and study their effect on the properties of the game. Specifically, bidding games, and in particular bidding games of infinite duration, have an intriguing equivalence with random-turn games in which in each turn, the player who moves is chosen randomly. We show how minor changes in the bidding mechanism lead to unexpected differences in the equivalence with random-turn games.
Cite as
Guy Avni and Thomas A. Henzinger. A Survey of Bidding Games on Graphs (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{avni_et_al:LIPIcs.CONCUR.2020.2,
author = {Avni, Guy and Henzinger, Thomas A.},
title = {{A Survey of Bidding Games on Graphs}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {2:1--2:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.2},
URN = {urn:nbn:de:0030-drops-128147},
doi = {10.4230/LIPIcs.CONCUR.2020.2},
annote = {Keywords: Bidding games, Richman bidding, poorman bidding, mean-payoff, parity}
}
Document
Invited Paper
Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper)
Abstract
This paper concerns the efficient construction of a safety shield for reinforcement learning. We specifically target scenarios that incorporate uncertainty and use Markov decision processes (MDPs) as the underlying model to capture such problems. Reinforcement learning (RL) is a machine learning technique that can determine near-optimal policies in MDPs that may be unknown before exploring the model. However, during exploration, RL is prone to induce behavior that is undesirable or not allowed in safety- or mission-critical contexts. We introduce the concept of a probabilistic shield that enables RL decision-making to adhere to safety constraints with high probability. We employ formal verification to efficiently compute the probabilities of critical decisions within a safety-relevant fragment of the MDP. These results help to realize a shield that, when applied to an RL algorithm, restricts the agent from taking unsafe actions, while optimizing the performance objective. We discuss tradeoffs between sufficient progress in the exploration of the environment and ensuring safety. In our experiments, we demonstrate on the arcade game PAC-MAN and on a case study involving service robots that the learning efficiency increases as the learning needs orders of magnitude fewer episodes.
Cite as
Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, and Roderick Bloem. Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{jansen_et_al:LIPIcs.CONCUR.2020.3,
author = {Jansen, Nils and K\"{o}nighofer, Bettina and Junges, Sebastian and Serban, Alex and Bloem, Roderick},
title = {{Safe Reinforcement Learning Using Probabilistic Shields}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {3:1--3:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.3},
URN = {urn:nbn:de:0030-drops-128155},
doi = {10.4230/LIPIcs.CONCUR.2020.3},
annote = {Keywords: Safe Reinforcement Learning, Formal Verification, Safe Exploration, Model Checking, Markov Decision Process}
}
Document
Invited Paper
Modern Applications of Game-Theoretic Principles (Invited Paper)
Abstract
Game theory is the study of the strategic behavior of rational decision makers who are aware that their decisions affect one another. Its simple but universal principles have found applications in the most diverse disciplines, including economics, social sciences, evolutionary biology, as well as logic, system science and computer science. Despite its long-standing tradition and its many advances, game theory is still a young and developing science. In this paper, we describe some recent and exciting applications in the fields of machine learning and privacy.
Cite as
Catuscia Palamidessi and Marco Romanelli. Modern Applications of Game-Theoretic Principles (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{palamidessi_et_al:LIPIcs.CONCUR.2020.4,
author = {Palamidessi, Catuscia and Romanelli, Marco},
title = {{Modern Applications of Game-Theoretic Principles}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {4:1--4:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.4},
URN = {urn:nbn:de:0030-drops-128167},
doi = {10.4230/LIPIcs.CONCUR.2020.4},
annote = {Keywords: Game theory, machine learning, privacy, security}
}
Document
Invited Paper
CONCUR Test-Of-Time Award 2020 Announcement (Invited Paper)
Abstract
This short article announces the recipients of the CONCUR Test-of-Time Award 2020.
Cite as
Luca Aceto, Jos Baeten, Patricia Bouyer-Decitre, Holger Hermanns, and Alexandra Silva. CONCUR Test-Of-Time Award 2020 Announcement (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CONCUR.2020.5,
author = {Aceto, Luca and Baeten, Jos and Bouyer-Decitre, Patricia and Hermanns, Holger and Silva, Alexandra},
title = {{CONCUR Test-Of-Time Award 2020 Announcement}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {5:1--5:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.5},
URN = {urn:nbn:de:0030-drops-128172},
doi = {10.4230/LIPIcs.CONCUR.2020.5},
annote = {Keywords: Concurrency, CONCUR Test-of-Time Award}
}
Document
Reactive Bisimulation Semantics for a Process Algebra with Time-Outs
Abstract
This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with time-out transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.
Cite as
Rob van Glabbeek. Reactive Bisimulation Semantics for a Process Algebra with Time-Outs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{vanglabbeek:LIPIcs.CONCUR.2020.6,
author = {van Glabbeek, Rob},
title = {{Reactive Bisimulation Semantics for a Process Algebra with Time-Outs}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {6:1--6:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.6},
URN = {urn:nbn:de:0030-drops-128181},
doi = {10.4230/LIPIcs.CONCUR.2020.6},
annote = {Keywords: Process algebra, time-outs, labelled transition systems, reactive bisimulation semantics, Hennessy-Milner logic, modal characterisations, recursion, complete axiomatisations}
}
Document
How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation
Abstract
Reversible computation opens up the possibility of overcoming some of the hardware’s current physical limitations. It also offers theoretical insights, as it enriches multiple paradigms and models of computation, and sometimes retrospectively enlightens them. Concurrent reversible computation, for instance, offered interesting extensions to the Calculus of Communicating Systems, but was still lacking a natural and pertinent bisimulation to study processes equivalences. Our paper formulates an equivalence exploiting the two aspects of reversibility: backward moves and memory mechanisms. This bisimulation captures classical equivalences relations for denotational models of concurrency (history- and hereditary history-preserving bisimulation, (H)HPB), that were up to now only partially characterized by process algebras. This result gives an insight on the expressiveness of reversibility, as both backward moves and a memory mechanism - providing "backward determinism" - are needed to capture HHPB.
Cite as
Clément Aubert and Ioana Cristescu. How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{aubert_et_al:LIPIcs.CONCUR.2020.7,
author = {Aubert, Cl\'{e}ment and Cristescu, Ioana},
title = {{How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {7:1--7:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.7},
URN = {urn:nbn:de:0030-drops-128196},
doi = {10.4230/LIPIcs.CONCUR.2020.7},
annote = {Keywords: Formal semantics, Process algebras and calculi, Distributed and reversible computation, Configuration structures, Reversible CCS, Bisimulation}
}
Document
A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains
Abstract
This article improves the time bound for calculating the weak/branching bisimulation minimisation quotient on state-labelled discrete-time Markov chains from O(m n) to an expected-time O(m log⁴ n), where n is the number of states and m the number of transitions. For these results we assume that the set of state labels AP is small (|AP| ∈ O(m/n log⁴ n)). It follows the ideas of Groote et al. (ACM ToCL 2017) in combination with an efficient algorithm to handle decremental strongly connected components (Bernstein et al., STOC 2019).
Cite as
David N. Jansen, Jan Friso Groote, Ferry Timmers, and Pengfei Yang. A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{jansen_et_al:LIPIcs.CONCUR.2020.8,
author = {Jansen, David N. and Groote, Jan Friso and Timmers, Ferry and Yang, Pengfei},
title = {{A Near-Linear-Time Algorithm for Weak Bisimilarity on Markov Chains}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {8:1--8:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.8},
URN = {urn:nbn:de:0030-drops-128209},
doi = {10.4230/LIPIcs.CONCUR.2020.8},
annote = {Keywords: Behavioural Equivalence, weak Bisimulation, Markov Chain}
}
Document
Characterizing Consensus in the Heard-Of Model
Abstract
The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm.
Cite as
A. R. Balasubramanian and Igor Walukiewicz. Characterizing Consensus in the Heard-Of Model. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{balasubramanian_et_al:LIPIcs.CONCUR.2020.9,
author = {Balasubramanian, A. R. and Walukiewicz, Igor},
title = {{Characterizing Consensus in the Heard-Of Model}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.9},
URN = {urn:nbn:de:0030-drops-128217},
doi = {10.4230/LIPIcs.CONCUR.2020.9},
annote = {Keywords: consensus problem, Heard-Of model, verification}
}
Document
A Classification of Weak Asynchronous Models of Distributed Computing
Abstract
We conduct a systematic study of asynchronous models of distributed computing consisting of identical finite-state devices that cooperate in a network to decide if the network satisfies a given graph-theoretical property. Models discussed in the literature differ in the detection capabilities of the agents residing at the nodes of the network (detecting the set of states of their neighbors, or counting the number of neighbors in each state), the notion of acceptance (acceptance by halting in a particular configuration, or by stable consensus), the notion of step (synchronous move, interleaving, or arbitrary timing), and the fairness assumptions (non-starving, or stochastic-like). We study the expressive power of the combinations of these features, and show that the initially twenty possible combinations fit into seven equivalence classes. The classification is the consequence of several equi-expressivity results with a clear interpretation. In particular, we show that acceptance by halting configuration only has non-trivial expressive power if it is combined with counting, and that synchronous and interleaving models have the same power as those in which an arbitrary set of nodes can move at the same time. We also identify simple graph properties that distinguish the expressive power of the seven classes.
Cite as
Javier Esparza and Fabian Reiter. A Classification of Weak Asynchronous Models of Distributed Computing. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{esparza_et_al:LIPIcs.CONCUR.2020.10,
author = {Esparza, Javier and Reiter, Fabian},
title = {{A Classification of Weak Asynchronous Models of Distributed Computing}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {10:1--10:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.10},
URN = {urn:nbn:de:0030-drops-128229},
doi = {10.4230/LIPIcs.CONCUR.2020.10},
annote = {Keywords: Asynchrony, Concurrency theory, Weak models of distributed computing}
}
Document
Scalable Termination Detection for Distributed Actor Systems
Abstract
Automatic garbage collection (GC) prevents certain kinds of bugs and reduces programming overhead. GC techniques for sequential programs are based on reachability analysis. However, testing reachability from a root set is inadequate for determining whether an actor is garbage because an unreachable actor may send a message to a reachable actor. Instead, it is sufficient to check termination (sometimes also called quiescence): an actor is terminated if it is not currently processing a message and cannot receive a message in the future. Moreover, many actor frameworks provide all actors with access to file I/O or external storage; without inspecting an actor’s internal code, it is necessary to check that the actor has terminated to ensure that it may be garbage collected in these frameworks. Previous algorithms to detect actor garbage require coordination mechanisms such as causal message delivery or nonlocal monitoring of actors for mutation. Such coordination mechanisms adversely affect concurrency and are therefore expensive in distributed systems. We present a low-overhead reference listing technique (called DRL) for termination detection in actor systems. DRL is based on asynchronous local snapshots and message-passing between actors. This enables a decentralized implementation and transient network partition tolerance. The paper provides a formal description of DRL, shows that all actors identified as garbage have indeed terminated (safety), and that all terminated actors - under certain reasonable assumptions - will eventually be identified (liveness).
Cite as
Dan Plyukhin and Gul Agha. Scalable Termination Detection for Distributed Actor Systems. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{plyukhin_et_al:LIPIcs.CONCUR.2020.11,
author = {Plyukhin, Dan and Agha, Gul},
title = {{Scalable Termination Detection for Distributed Actor Systems}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {11:1--11:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.11},
URN = {urn:nbn:de:0030-drops-128231},
doi = {10.4230/LIPIcs.CONCUR.2020.11},
annote = {Keywords: actors, concurrency, termination detection, quiescence detection, garbage collection, distributed systems}
}
Document
Session Subtyping and Multiparty Compatibility Using Circular Sequents
Abstract
We present a structural proof theory for multi-party sessions, exploiting the expressive power of non-commutative logic which can capture explicitly the message sequence order in sessions. The approach in this work uses a more flexible form of subtyping than standard, for example, allowing a single thread to be substituted by multiple parallel threads which fulfil the role of the single thread. The resulting subtype system has the advantage that it can be used to capture compatibility in the multiparty setting (addressing limitations of pairwise duality). We establish standard results: that the type system is algorithmic, that multiparty compatible processes which are race free are also deadlock free, and that subtyping is sound with respect to the substitution principle. Interestingly, each of these results can be established using cut elimination. We remark that global types are optional in this approach to typing sessions; indeed we show that this theory can be presented independently of the concept of global session types, or even named participants.
Cite as
Ross Horne. Session Subtyping and Multiparty Compatibility Using Circular Sequents. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{horne:LIPIcs.CONCUR.2020.12,
author = {Horne, Ross},
title = {{Session Subtyping and Multiparty Compatibility Using Circular Sequents}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {12:1--12:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.12},
URN = {urn:nbn:de:0030-drops-128245},
doi = {10.4230/LIPIcs.CONCUR.2020.12},
annote = {Keywords: session types, subtyping, compatibility, linear logic, deadlock freedom}
}
Document
Session Types with Arithmetic Refinements
Abstract
Session types statically prescribe bidirectional communication protocols for message-passing processes. However, simple session types cannot specify properties beyond the type of exchanged messages. In this paper we extend the type system by using index refinements from linear arithmetic capturing intrinsic attributes of data structures and algorithms. We show that, despite the decidability of Presburger arithmetic, type equality and therefore also subtyping and type checking are now undecidable, which stands in contrast to analogous dependent refinement type systems from functional languages. We also present a practical, but incomplete algorithm for type equality, which we have used in our implementation of Rast, a concurrent session-typed language with arithmetic index refinements as well as ergometric and temporal types. Moreover, if necessary, the programmer can propose additional type bisimulations that are smoothly integrated into the type equality algorithm.
Cite as
Ankush Das and Frank Pfenning. Session Types with Arithmetic Refinements. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.CONCUR.2020.13,
author = {Das, Ankush and Pfenning, Frank},
title = {{Session Types with Arithmetic Refinements}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.13},
URN = {urn:nbn:de:0030-drops-128252},
doi = {10.4230/LIPIcs.CONCUR.2020.13},
annote = {Keywords: Session Types, Refinement Types, Type Equality}
}
Document
Probabilistic Analysis of Binary Sessions
Abstract
We study a probabilistic variant of binary session types that relate to a class of Finite-State Markov Chains. The probability annotations in session types enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the success probability of well-typed processes agrees with that of the sessions they use. To this aim, the type system needs to track the propagation of probabilistic choices across different sessions.
Cite as
Omar Inverso, Hernán Melgratti, Luca Padovani, Catia Trubiani, and Emilio Tuosto. Probabilistic Analysis of Binary Sessions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{inverso_et_al:LIPIcs.CONCUR.2020.14,
author = {Inverso, Omar and Melgratti, Hern\'{a}n and Padovani, Luca and Trubiani, Catia and Tuosto, Emilio},
title = {{Probabilistic Analysis of Binary Sessions}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {14:1--14:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.14},
URN = {urn:nbn:de:0030-drops-128264},
doi = {10.4230/LIPIcs.CONCUR.2020.14},
annote = {Keywords: Probabilistic choices, session types, static analysis, deadlock freedom}
}
Document
On Ranking Function Synthesis and Termination for Polynomial Programs
Abstract
We consider the problem of synthesising polynomial ranking functions for single-path loops over the reals with continuous semi-algebraic update function and compact semi-algebraic guard set. We show that a loop of this form has a polynomial ranking function if and only if it terminates. We further show that termination is decidable for such loops in the special case where the update function is affine.
Cite as
Eike Neumann, Joël Ouaknine, and James Worrell. On Ranking Function Synthesis and Termination for Polynomial Programs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{neumann_et_al:LIPIcs.CONCUR.2020.15,
author = {Neumann, Eike and Ouaknine, Jo\"{e}l and Worrell, James},
title = {{On Ranking Function Synthesis and Termination for Polynomial Programs}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {15:1--15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.15},
URN = {urn:nbn:de:0030-drops-128278},
doi = {10.4230/LIPIcs.CONCUR.2020.15},
annote = {Keywords: Semi-algebraic sets, Polynomial ranking functions, Polynomial programs}
}
Document
On the Separability Problem of String Constraints
Abstract
We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of the separability problem for straight-line string constraints by piece-wise testable languages, though the precise complexity is open. In our third result, we consider the positive fragment of piece-wise testable languages as a separator, and obtain an ExpSpace algorithm for the separability of a useful class of straight-line string constraints, and a Pspace-hardness result.
Cite as
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna. On the Separability Problem of String Constraints. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2020.16,
author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Dave, Vrunda and Krishna, Shankara Narayanan},
title = {{On the Separability Problem of String Constraints}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {16:1--16:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.16},
URN = {urn:nbn:de:0030-drops-128286},
doi = {10.4230/LIPIcs.CONCUR.2020.16},
annote = {Keywords: string constraints, separability, interpolants}
}
Document
Weighted Transducers for Robustness Verification
Abstract
Automata theory provides us with fundamental notions such as languages, membership, emptiness and inclusion that in turn allow us to specify and verify properties of reactive systems in a useful manner. However, these notions all yield "yes"/"no" answers that sometimes fall short of being satisfactory answers when the models being analyzed are imperfect, and the observations made are prone to errors. To address this issue, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so robustly. We present notions of robustness that place a metric on words, thus providing a natural notion of distance between words. Such a metric naturally leads to a topological neighborhood of words and languages, leading to quantitative and robust versions of the membership, emptiness and inclusion problems. More generally, we consider weighted transducers to model the cost of errors. Such a transducer models neighborhoods of words by providing the cost of rewriting a word into another. The main contribution of this work is to study robustness verification problems in the context of weighted transducers. We provide algorithms for solving the robust and quantitative versions of the membership and inclusion problems while providing useful motivating case studies including approximate pattern matching problems to detect clinically relevant events in a large type-1 diabetes dataset.
Cite as
Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin, Sriram Sankaranarayanan, and Ashutosh Trivedi. Weighted Transducers for Robustness Verification. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{filiot_et_al:LIPIcs.CONCUR.2020.17,
author = {Filiot, Emmanuel and Mazzocchi, Nicolas and Raskin, Jean-Fran\c{c}ois and Sankaranarayanan, Sriram and Trivedi, Ashutosh},
title = {{Weighted Transducers for Robustness Verification}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {17:1--17:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.17},
URN = {urn:nbn:de:0030-drops-128290},
doi = {10.4230/LIPIcs.CONCUR.2020.17},
annote = {Keywords: Weighted transducers, Quantitative verification, Fault-tolerance}
}
Document
On the Axiomatisability of Parallel Composition: A Journey in the Spectrum
Abstract
This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. On the other hand, we show that no congruence over that language that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation. This negative result applies to all the nested trace and nested simulation semantics.
Cite as
Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen. On the Axiomatisability of Parallel Composition: A Journey in the Spectrum. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CONCUR.2020.18,
author = {Aceto, Luca and Castiglioni, Valentina and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas and Pedersen, Mathias Ruggaard},
title = {{On the Axiomatisability of Parallel Composition: A Journey in the Spectrum}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {18:1--18:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.18},
URN = {urn:nbn:de:0030-drops-128303},
doi = {10.4230/LIPIcs.CONCUR.2020.18},
annote = {Keywords: Axiomatisation, Parallel composition, Linear time-branching time spectrum}
}
Document
Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces
Abstract
We develop a new algebraic framework to reason about languages of Mazurkiewicz traces. This framework supports true concurrency and provides a non-trivial generalization of the wreath product operation to the trace setting. A novel local wreath product principle has been established. The new framework is crucially used to propose a decomposition result for recognizable trace languages, which is an analogue of the Krohn-Rhodes theorem. We prove this decomposition result in the special case of acyclic architectures and apply it to extend Kamp’s theorem to this setting. We also introduce and analyze distributed automata-theoretic operations called local and global cascade products. Finally, we show that aperiodic trace languages can be characterized using global cascade products of localized and distributed two-state reset automata.
Cite as
Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{adsul_et_al:LIPIcs.CONCUR.2020.19,
author = {Adsul, Bharat and Gastin, Paul and Sarkar, Saptarshi and Weil, Pascal},
title = {{Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.19},
URN = {urn:nbn:de:0030-drops-128319},
doi = {10.4230/LIPIcs.CONCUR.2020.19},
annote = {Keywords: Mazurkiewicz traces, asynchronous automata, wreath product, cascade product, Krohn Rhodes decomposition theorem, local temporal logic over traces}
}
Document
Partially Observable Concurrent Kleene Algebra
Abstract
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with variables as well as control structures, such as conditionals and loops, that depend on those variables. We illustrate the use of POCKA through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.
Cite as
Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot, and Alexandra Silva. Partially Observable Concurrent Kleene Algebra. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{wagemaker_et_al:LIPIcs.CONCUR.2020.20,
author = {Wagemaker, Jana and Brunet, Paul and Docherty, Simon and Kapp\'{e}, Tobias and Rot, Jurriaan and Silva, Alexandra},
title = {{Partially Observable Concurrent Kleene Algebra}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {20:1--20:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.20},
URN = {urn:nbn:de:0030-drops-128324},
doi = {10.4230/LIPIcs.CONCUR.2020.20},
annote = {Keywords: Concurrent Kleene algebra, Kleene algebra with tests, observations, axiomatisation, completeness, sequential consistency}
}
Document
Model-Free Reinforcement Learning for Stochastic Parity Games
Abstract
This paper investigates the use of model-free reinforcement learning to compute the optimal value in two-player stochastic games with parity objectives. In this setting, two decision makers, player Min and player Max, compete on a finite game arena - a stochastic game graph with unknown but fixed probability distributions - to minimize and maximize, respectively, the probability of satisfying a parity objective. We give a reduction from stochastic parity games to a family of stochastic reachability games with a parameter ε, such that the value of a stochastic parity game equals the limit of the values of the corresponding simple stochastic games as the parameter ε tends to 0. Since this reduction does not require the knowledge of the probabilistic transition structure of the underlying game arena, model-free reinforcement learning algorithms, such as minimax Q-learning, can be used to approximate the value and mutual best-response strategies for both players in the underlying stochastic parity game. We also present a streamlined reduction from 1 1/2-player parity games to reachability games that avoids recourse to nondeterminism. Finally, we report on the experimental evaluations of both reductions.
Cite as
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtczak. Model-Free Reinforcement Learning for Stochastic Parity Games. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{hahn_et_al:LIPIcs.CONCUR.2020.21,
author = {Hahn, Ernst Moritz and Perez, Mateo and Schewe, Sven and Somenzi, Fabio and Trivedi, Ashutosh and Wojtczak, Dominik},
title = {{Model-Free Reinforcement Learning for Stochastic Parity Games}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {21:1--21:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.21},
URN = {urn:nbn:de:0030-drops-128332},
doi = {10.4230/LIPIcs.CONCUR.2020.21},
annote = {Keywords: Reinforcement learning, Stochastic games, Omega-regular objectives}
}
Document
Decidability of Cutpoint Isolation for Probabilistic Finite Automata on Letter-Bounded Inputs
Abstract
We show the surprising result that the cutpoint isolation problem is decidable for probabilistic finite automata where input words are taken from a letter-bounded context-free language. A context-free language ℒ is letter-bounded when ℒ ⊆ a₁^* a₂^* ⋯ a_𝓁^* for some finite 𝓁 > 0 where each letter is distinct. A cutpoint is isolated when it cannot be approached arbitrarily closely. The decidability of this problem is in marked contrast to the situation for the (strict) emptiness problem for PFA which is undecidable under the even more severe restrictions of PFA with polynomial ambiguity, commutative matrices and input over a letter-bounded language as well as to the injectivity problem which is undecidable for PFA over letter-bounded languages. We provide a constructive nondeterministic algorithm to solve the cutpoint isolation problem, which holds even when the PFA is exponentially ambiguous. We also show that the problem is at least NP-hard and use our decision procedure to solve several related problems.
Cite as
Paul C. Bell and Pavel Semukhin. Decidability of Cutpoint Isolation for Probabilistic Finite Automata on Letter-Bounded Inputs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bell_et_al:LIPIcs.CONCUR.2020.22,
author = {Bell, Paul C. and Semukhin, Pavel},
title = {{Decidability of Cutpoint Isolation for Probabilistic Finite Automata on Letter-Bounded Inputs}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {22:1--22:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.22},
URN = {urn:nbn:de:0030-drops-128344},
doi = {10.4230/LIPIcs.CONCUR.2020.22},
annote = {Keywords: Probabilistic finite automata, cutpoint isolation problem, letter-bounded context-free languages}
}
Document
Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States
Abstract
A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.
Cite as
Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 23:1-23:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2020.23,
author = {Chatterjee, Krishnendu and Henzinger, Thomas A. and Otop, Jan},
title = {{Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {23:1--23:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.23},
URN = {urn:nbn:de:0030-drops-128359},
doi = {10.4230/LIPIcs.CONCUR.2020.23},
annote = {Keywords: vector addition systems, mean-payoff, multidimension, probabilistic semantics}
}
Document
Games Where You Can Play Optimally with Arena-Independent Finite Memory
Abstract
For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies might be simple or quite complex, for example having to use (possibly infinite) memory. Hence, research strives to understand which settings allow for simple strategies.
In 2005, Gimbert and Zielonka [Hugo Gimbert and Wieslaw Zielonka, 2005] provided a complete characterization of preference relations (a formal framework to model specifications and game objectives) that admit memoryless optimal strategies for both players. In the last fifteen years however, practical applications have driven the community toward games with complex or multiple objectives, where memory - finite or infinite - is almost always required. Despite much effort, the exact frontiers of the class of preference relations that admit finite-memory optimal strategies still elude us.
In this work, we establish a complete characterization of preference relations that admit optimal strategies using arena-independent finite memory, generalizing the work of Gimbert and Zielonka to the finite-memory case. We also prove an equivalent to their celebrated corollary of great practical interest: if both players have optimal (arena-independent-)finite-memory strategies in all one-player games, then it is also the case in all two-player games. Finally, we pinpoint the boundaries of our results with regard to the literature: our work completely covers the case of arena-independent memory (e.g., multiple parity objectives, lower- and upper-bounded energy objectives), and paves the way to the arena-dependent case (e.g., multiple lower-bounded energy objectives).
Cite as
Patricia Bouyer, Stéphane Le Roux, Youssouf Oualhadj, Mickael Randour, and Pierre Vandenhove. Games Where You Can Play Optimally with Arena-Independent Finite Memory. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2020.24,
author = {Bouyer, Patricia and Le Roux, St\'{e}phane and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre},
title = {{Games Where You Can Play Optimally with Arena-Independent Finite Memory}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {24:1--24:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.24},
URN = {urn:nbn:de:0030-drops-128360},
doi = {10.4230/LIPIcs.CONCUR.2020.24},
annote = {Keywords: two-player games on graphs, finite-memory determinacy, optimal strategies}
}
Document
Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations
Abstract
Systems of fixpoint equations over complete lattices, consisting of (mixed) least and greatest fixpoint equations, allow one to express many verification tasks such as model-checking of various kinds of specification logics or the check of coinductive behavioural equivalences. In this paper we develop a theory of approximation for systems of fixpoint equations in the style of abstract interpretation: a system over some concrete domain is abstracted to a system in a suitable abstract domain, with conditions ensuring that the abstract solution represents a sound/complete overapproximation of the concrete solution. Interestingly, up-to techniques, a classical approach used in coinductive settings to obtain easier or feasible proofs, can be interpreted as abstractions in a way that they naturally fit into our framework and extend to systems of equations. Additionally, relying on the approximation theory, we can characterise the solution of systems of fixpoint equations over complete lattices in terms of a suitable parity game, generalising some recent work that was restricted to continuous lattices. The game view opens the way for the development of local algorithms for characterising the solution of such equation systems and we explore some special cases.
Cite as
Paolo Baldan, Barbara König, and Tommaso Padoan. Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{baldan_et_al:LIPIcs.CONCUR.2020.25,
author = {Baldan, Paolo and K\"{o}nig, Barbara and Padoan, Tommaso},
title = {{Abstraction, Up-To Techniques and Games for Systems of Fixpoint Equations}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {25:1--25:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.25},
URN = {urn:nbn:de:0030-drops-128373},
doi = {10.4230/LIPIcs.CONCUR.2020.25},
annote = {Keywords: fixpoint equation systems, complete lattices, parity games, abstract interpretation, up-to techniques, \mu-calculus, bisimilarity}
}
Document
Reaching Your Goal Optimally by Playing at Random with No Memory
Abstract
Shortest-path games are two-player zero-sum games played on a graph equipped with integer weights. One player, that we call Min, wants to reach a target set of states while minimising the total weight, and the other one has an antagonistic objective. This combination of a qualitative reachability objective and a quantitative total-payoff objective is one of the simplest settings where Min needs memory (pseudo-polynomial in the weights) to play optimally. In this article, we aim at studying a tradeoff allowing Min to play at random, but using no memory. We show that Min can achieve the same optimal value in both cases. In particular, we compute a randomised memoryless ε-optimal strategy when it exists, where probabilities are parametrised by ε. We also show that for some games, no optimal randomised strategies exist. We then characterise, and decide in polynomial time, the class of games admitting an optimal randomised memoryless strategy.
Cite as
Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Reaching Your Goal Optimally by Playing at Random with No Memory. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 26:1-26:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{monmege_et_al:LIPIcs.CONCUR.2020.26,
author = {Monmege, Benjamin and Parreaux, Julie and Reynier, Pierre-Alain},
title = {{Reaching Your Goal Optimally by Playing at Random with No Memory}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {26:1--26:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.26},
URN = {urn:nbn:de:0030-drops-128381},
doi = {10.4230/LIPIcs.CONCUR.2020.26},
annote = {Keywords: Weighted games, Algorithmic game theory, Randomisation}
}
Document
Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions
Abstract
Behavioural distances provide a fine-grained measure of equivalence in systems involving quantitative data, such as probabilistic, fuzzy, or metric systems. Like in the classical setting of crisp bisimulation-type equivalences, the wide variation found in system types creates a need for generic methods that apply to many system types at once. Approaches of this kind are emerging within the paradigm of universal coalgebra, based either on lifting pseudometrics along set functors or on lifting general real-valued (fuzzy) relations along functors by means of fuzzy lax extensions. An immediate benefit of the latter is that they allow bounding behavioural distance by means of fuzzy bisimulations that need not themselves be (pseudo-)metrics, in analogy to classical bisimulations (which need not be equivalence relations). The known instances of generic pseudometric liftings, specifically the generic Kantorovich and Wasserstein liftings, both can be extended to yield fuzzy lax extensions, using the fact that both are effectively given by a choice of quantitative modalities. Our central result then shows that in fact all fuzzy lax extensions are Kantorovich extensions for a suitable set of quantitative modalities, the so-called Moss modalities. For non-expansive fuzzy lax extensions, this allows for the extraction of quantitative modal logics that characterize behavioural distance, i.e. satisfy a quantitative version of the Hennessy-Milner theorem; equivalently, we obtain expressiveness of a quantitative version of Moss' coalgebraic logic.
Cite as
Paul Wild and Lutz Schröder. Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{wild_et_al:LIPIcs.CONCUR.2020.27,
author = {Wild, Paul and Schr\"{o}der, Lutz},
title = {{Characteristic Logics for Behavioural Metrics via Fuzzy Lax Extensions}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {27:1--27:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.27},
URN = {urn:nbn:de:0030-drops-128394},
doi = {10.4230/LIPIcs.CONCUR.2020.27},
annote = {Keywords: Modal logic, behavioural distance, coalgebra, bisimulation, lax extension}
}
Document
Monads and Quantitative Equational Theories for Nondeterminism and Probability
Abstract
The monad of convex sets of probability distributions is a well-known tool for modelling the combination of nondeterministic and probabilistic computational effects. In this work we lift this monad from the category of sets to the category of extended metric spaces, by means of the Hausdorff and Kantorovich metric liftings. Our main result is the presentation of this lifted monad in terms of the quantitative equational theory of convex semilattices, using the framework of quantitative algebras recently introduced by Mardare, Panangaden and Plotkin.
Cite as
Matteo Mio and Valeria Vignudelli. Monads and Quantitative Equational Theories for Nondeterminism and Probability. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{mio_et_al:LIPIcs.CONCUR.2020.28,
author = {Mio, Matteo and Vignudelli, Valeria},
title = {{Monads and Quantitative Equational Theories for Nondeterminism and Probability}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.28},
URN = {urn:nbn:de:0030-drops-128407},
doi = {10.4230/LIPIcs.CONCUR.2020.28},
annote = {Keywords: Computational Effects, Monads, Metric Spaces, Quantitative Algebras}
}
Document
Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms
Abstract
We study the equational theories of composition and intersection on binary relations, with or without their associated neutral elements (identity and full relation). Without these constants, the equational theory coincides with that of semilattice-ordered semigroups. We show that the equational theory is no longer finitely based when adding one or the other constant, refuting a conjecture from the literature. Our proofs exploit a characterisation in terms of graphs and homomorphisms, which we show how to adapt in order to capture standard equational theories over the considered signatures.
Cite as
Amina Doumane and Damien Pous. Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{doumane_et_al:LIPIcs.CONCUR.2020.29,
author = {Doumane, Amina and Pous, Damien},
title = {{Non Axiomatisability of Positive Relation Algebras with Constants, via Graph Homomorphisms}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {29:1--29:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.29},
URN = {urn:nbn:de:0030-drops-128411},
doi = {10.4230/LIPIcs.CONCUR.2020.29},
annote = {Keywords: Relation algebra, graph homomorphisms, (in)equational theories}
}
Document
Decidability and Synthesis of Abstract Inductive Invariants
Abstract
Decidability and synthesis of inductive invariants ranging in a given domain play an important role in software verification. We consider here inductive invariants belonging to an abstract domain A as defined in abstract interpretation, namely, ensuring the existence of the best approximation in A of any system property. In this setting, we study the decidability of the existence of abstract inductive invariants in A of transition systems and their corresponding algorithmic synthesis. Our model relies on some general results which relate the existence of abstract inductive invariants with least fixed points of best correct approximations in A of the transfer functions of transition systems and their completeness properties. This approach allows us to derive decidability and synthesis results for abstract inductive invariants which are applied to the well-known Karr’s numerical abstract domain of affine equalities. Moreover, we show that a recent general algorithm for synthesizing inductive invariants in domains of logical formulae can be systematically derived from our results and generalized to a range of algorithms for computing abstract inductive invariants.
Cite as
Francesco Ranzato. Decidability and Synthesis of Abstract Inductive Invariants. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{ranzato:LIPIcs.CONCUR.2020.30,
author = {Ranzato, Francesco},
title = {{Decidability and Synthesis of Abstract Inductive Invariants}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {30:1--30:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.30},
URN = {urn:nbn:de:0030-drops-128429},
doi = {10.4230/LIPIcs.CONCUR.2020.30},
annote = {Keywords: Inductive invariant, program verification, abstract interpretation}
}
Document
Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
Abstract
We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied πcalc, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, we introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Our core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Our invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. We provide a prototype implementation and we report on its performance on some textbook examples.
Cite as
Emanuele D'Osualdo and Felix Stutz. Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{dosualdo_et_al:LIPIcs.CONCUR.2020.31,
author = {D'Osualdo, Emanuele and Stutz, Felix},
title = {{Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {31:1--31:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.31},
URN = {urn:nbn:de:0030-drops-128433},
doi = {10.4230/LIPIcs.CONCUR.2020.31},
annote = {Keywords: Security Protocols, Infinite-State Verification, Ideal Completions for WSTS}
}
Document
Algebraic Invariants for Linear Hybrid Automata
Abstract
We exhibit an algorithm to compute the strongest algebraic (or polynomial) invariants that hold at each location of a given guard-free linear hybrid automaton (i.e., a hybrid automaton having only unguarded transitions, all of whose assignments are given by affine expressions, and all of whose continuous dynamics are given by linear differential equations). Our main tool is a control-theoretic result of independent interest: given such a linear hybrid automaton, we show how to discretise the continuous dynamics in such a way that the resulting automaton has precisely the same algebraic invariants.
Cite as
Rupak Majumdar, Joël Ouaknine, Amaury Pouly, and James Worrell. Algebraic Invariants for Linear Hybrid Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{majumdar_et_al:LIPIcs.CONCUR.2020.32,
author = {Majumdar, Rupak and Ouaknine, Jo\"{e}l and Pouly, Amaury and Worrell, James},
title = {{Algebraic Invariants for Linear Hybrid Automata}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {32:1--32:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.32},
URN = {urn:nbn:de:0030-drops-128443},
doi = {10.4230/LIPIcs.CONCUR.2020.32},
annote = {Keywords: Hybrid automata, algebraic invariants}
}
Document
A General Approach to Derive Uncontrolled Reversible Semantics
Abstract
Reversible computing is a paradigm where programs can execute backward as well as in the usual forward direction. Reversible computing is attracting interest due to its applications in areas as different as biochemical modelling, simulation, robotics and debugging, among others. In concurrent systems the main notion of reversible computing is called causal-consistent reversibility, and it allows one to undo an action if and only if its consequences, if any, have already been undone.
This paper presents a general and automatic technique to define a causal-consistent reversible extension for given forward models. We support models defined using a reduction semantics in a specific format and consider a causality relation based on resources consumed and produced. The considered format is general enough to fit many formalisms studied in the literature on causal-consistent reversibility, notably Higher-Order π-calculus and Core Erlang, an intermediate language in the Erlang compilation. Reversible extensions of these models in the literature are ad hoc, while we build them using the same general technique. This also allows us to show in a uniform way that a number of relevant properties, causal-consistency in particular, hold in the reversible extensions we build. Our technique also allows us to go beyond the reversible models in the literature: we cover a larger fragment of Core Erlang, including remote error handling based on links, which has never been considered in the reversibility literature.
Cite as
Ivan Lanese and Doriana Medić. A General Approach to Derive Uncontrolled Reversible Semantics. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{lanese_et_al:LIPIcs.CONCUR.2020.33,
author = {Lanese, Ivan and Medi\'{c}, Doriana},
title = {{A General Approach to Derive Uncontrolled Reversible Semantics}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {33:1--33:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.33},
URN = {urn:nbn:de:0030-drops-128457},
doi = {10.4230/LIPIcs.CONCUR.2020.33},
annote = {Keywords: Reversible computing, causality, process calculi, Erlang}
}
Document
On the Representation of References in the Pi-Calculus
Abstract
The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. Often these languages make use of forms of references (and hence viewing a store as set of references). While translations of references in π-calculi (and CCS) have appeared, the precision of such translations has not been fully investigated. In this paper we address this issue.
We focus on the asynchronous π-calculus (Aπ), where translations of references are simpler. We first define π^ref, an extension of Aπ with references and operators to manipulate them, and illustrate examples of the subtleties of behavioural equivalence in π^ref. We then consider a translation of π^ref into Aπ. References of π^ref are mapped onto names of Aπ belonging to a dedicated "reference" type. We show how the presence of reference names affects the definition of barbed congruence. We establish full abstraction of the translation w.r.t. barbed congruence and barbed equivalence in the two calculi. We investigate proof techniques for barbed equivalence in Aπ, based on two forms of labelled bisimilarities. For one bisimilarity we derive both soundness and completeness; for another, more efficient and involving an inductive "game" on reference names, we derive soundness, leaving completeness open. Finally, we discuss examples of uses of the bisimilarities.
Cite as
Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On the Representation of References in the Pi-Calculus. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{hirschkoff_et_al:LIPIcs.CONCUR.2020.34,
author = {Hirschkoff, Daniel and Prebet, Enguerrand and Sangiorgi, Davide},
title = {{On the Representation of References in the Pi-Calculus}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {34:1--34:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.34},
URN = {urn:nbn:de:0030-drops-128466},
doi = {10.4230/LIPIcs.CONCUR.2020.34},
annote = {Keywords: Process calculus, Bisimulation, Asynchrony, Imperative programming}
}
Document
Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations
Abstract
In this paper we prove completeness of four axiomatisations for finite-state behaviours with respect to behavioural equivalences at various τ-abstract levels: branching congruence, delay congruence, η-congruence, and weak congruence. Instead of merging guarded recursive equations, which was the approach originally used by Robin Milner and has since become the standard strategy for proving completeness results of this kind, in this work we take a new approach by solving guarded recursive equations with canonical solutions which are those with the fewest reachable states. The new strategy allows uniform treatment of the axiomatisations with respect to different behavioural equivalences.
Cite as
Xinxin Liu and TingTing Yu. Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{liu_et_al:LIPIcs.CONCUR.2020.35,
author = {Liu, Xinxin and Yu, TingTing},
title = {{Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {35:1--35:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.35},
URN = {urn:nbn:de:0030-drops-128479},
doi = {10.4230/LIPIcs.CONCUR.2020.35},
annote = {Keywords: Bisimulation, Congruence, Axiomatisation, Soundness and Completeness}
}
Document
Universality Problem for Unambiguous VASS
Abstract
We study languages of unambiguous VASS, that is, Vector Addition Systems with States, whose transitions read letters from a finite alphabet, and whose acceptance condition is defined by a set of final states (i.e., the coverability language). We show that the problem of universality for unambiguous VASS is ExpSpace-complete, in sheer contrast to Ackermann-completeness for arbitrary VASS, even in dimension 1. When the dimension d ∈ ℕ is fixed, the universality problem is PSpace-complete if d ≥ 2, and coNP-hard for 1-dimensional VASSes (also known as One Counter Nets).
Cite as
Wojciech Czerwiński, Diego Figueira, and Piotr Hofman. Universality Problem for Unambiguous VASS. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2020.36,
author = {Czerwi\'{n}ski, Wojciech and Figueira, Diego and Hofman, Piotr},
title = {{Universality Problem for Unambiguous VASS}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {36:1--36:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.36},
URN = {urn:nbn:de:0030-drops-128486},
doi = {10.4230/LIPIcs.CONCUR.2020.36},
annote = {Keywords: unambiguity, vector addition systems, universality problems}
}
Document
Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free
Abstract
Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The problem is decidable and it was recently proved that the dimension of the vector addition system is an important parameter of the complexity. In fixed dimensions larger than two, the complexity is not known (with huge complexity gaps). In dimension two, the reachability problem was shown to be PSPACE-complete by Blondin et al. in 2015. We consider an extension of this model, called 2-TVASS, where the first counter can be tested for zero. This model naturally extends the classical model of one counter automata (OCA). We show that reachability is still solvable in polynomial space for 2-TVASS. As in the work Blondin et al., our approach relies on the existence of small reachability certificates obtained by concatenating polynomially many cycles.
Cite as
Jérôme Leroux and Grégoire Sutre. Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{leroux_et_al:LIPIcs.CONCUR.2020.37,
author = {Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
title = {{Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {37:1--37:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.37},
URN = {urn:nbn:de:0030-drops-128498},
doi = {10.4230/LIPIcs.CONCUR.2020.37},
annote = {Keywords: Counter machine, Vector addition system, Reachability problem, Formal verification, Infinite-state system}
}
Document
Coverability in 1-VASS with Disequality Tests
Abstract
We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model of vector addition systems with states (VASS). We consider a version of the vertex-to-vertex reachability problem in which the accumulated weight of a path is required always to be non-negative. This is equivalent to the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional VASS. We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. In our main result we generalise the problem to allow disequality constraints on edges (i.e., we allow edges to be disabled if the accumulated weight is equal to a specific value). We show that in this case the vertex-to-vertex reachability problem is solvable in polynomial time even though a shortest path may have exponential length. In the language of VASS this means that control-state reachability is in polynomial time for 1-dimensional VASS with disequality tests.
Cite as
Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell. Coverability in 1-VASS with Disequality Tests. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CONCUR.2020.38,
author = {Almagor, Shaull and Cohen, Nathann and P\'{e}rez, Guillermo A. and Shirmohammadi, Mahsa and Worrell, James},
title = {{Coverability in 1-VASS with Disequality Tests}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {38:1--38:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.38},
URN = {urn:nbn:de:0030-drops-128501},
doi = {10.4230/LIPIcs.CONCUR.2020.38},
annote = {Keywords: Reachability, Vector addition systems with states, Weighted graphs}
}
Document
Strategy Complexity of Parity Objectives in Countable MDPs
Abstract
We study countably infinite MDPs with parity objectives. Unlike in finite MDPs, optimal strategies need not exist, and may require infinite memory if they do. We provide a complete picture of the exact strategy complexity of ε-optimal strategies (and optimal strategies, where they exist) for all subclasses of parity objectives in the Mostowski hierarchy. Either MD-strategies, Markov strategies, or 1-bit Markov strategies are necessary and sufficient, depending on the number of colors, the branching degree of the MDP, and whether one considers ε-optimal or optimal strategies. In particular, 1-bit Markov strategies are necessary and sufficient for ε-optimal (resp. optimal) strategies for general parity objectives.
Cite as
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Strategy Complexity of Parity Objectives in Countable MDPs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2020.39,
author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
title = {{Strategy Complexity of Parity Objectives in Countable MDPs}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {39:1--39:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.39},
URN = {urn:nbn:de:0030-drops-128513},
doi = {10.4230/LIPIcs.CONCUR.2020.39},
annote = {Keywords: Markov decision processes, Parity objectives, Levy’s zero-one law}
}
Document
Monte Carlo Tree Search Guided by Symbolic Advice for MDPs
Abstract
In this paper, we consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS). We augment the MCTS algorithm with the notion of symbolic advice, and show that its classical theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We describe how to use QBF and SAT solvers to implement symbolic advice in an efficient way. We illustrate our new algorithm using the popular game Pac-Man and show that the performances of our algorithm exceed those of plain MCTS as well as the performances of human players.
Cite as
Damien Busatto-Gaston, Debraj Chakraborty, and Jean-Francois Raskin. Monte Carlo Tree Search Guided by Symbolic Advice for MDPs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 40:1-40:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{busattogaston_et_al:LIPIcs.CONCUR.2020.40,
author = {Busatto-Gaston, Damien and Chakraborty, Debraj and Raskin, Jean-Francois},
title = {{Monte Carlo Tree Search Guided by Symbolic Advice for MDPs}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {40:1--40:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.40},
URN = {urn:nbn:de:0030-drops-128523},
doi = {10.4230/LIPIcs.CONCUR.2020.40},
annote = {Keywords: Markov decision process, Monte Carlo tree search, symbolic advice, simulation}
}
Document
The Big-O Problem for Labelled Markov Chains and Weighted Automata
Abstract
Given two weighted automata, we consider the problem of whether one is big-O of the other, i.e., if the weight of every finite word in the first is not greater than some constant multiple of the weight in the second.
We show that the problem is undecidable, even for the instantiation of weighted automata as labelled Markov chains. Moreover, even when it is known that one weighted automaton is big-O of another, the problem of finding or approximating the associated constant is also undecidable.
Our positive results show that the big-O problem is polynomial-time solvable for unambiguous automata, coNP-complete for unlabelled weighted automata (i.e., when the alphabet is a single character) and decidable, subject to Schanuel’s conjecture, when the language is bounded (i.e., a subset of w_1^* … w_m^* for some finite words w_1,… ,w_m).
On labelled Markov chains, the problem can be restated as a ratio total variation distance, which, instead of finding the maximum difference between the probabilities of any two events, finds the maximum ratio between the probabilities of any two events. The problem is related to ε-differential privacy, for which the optimal constant of the big-O notation is exactly exp(ε).
Cite as
Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser. The Big-O Problem for Labelled Markov Chains and Weighted Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2020.41,
author = {Chistikov, Dmitry and Kiefer, Stefan and Murawski, Andrzej S. and Purser, David},
title = {{The Big-O Problem for Labelled Markov Chains and Weighted Automata}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {41:1--41:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.41},
URN = {urn:nbn:de:0030-drops-128534},
doi = {10.4230/LIPIcs.CONCUR.2020.41},
annote = {Keywords: weighted automata, labelled Markov chains, probabilistic systems}
}
Document
Determinisability of One-Clock Timed Automata
Abstract
The deterministic membership problem for timed automata asks whether the timed language recognised by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the deterministic timed automaton is fixed. We show that the problem in all the other cases is undecidable, i.e., when either 1) the input nondeterministic timed automaton has two clocks or more, or 2) it uses epsilon transitions, or 3) the number of clocks of the output deterministic automaton is not fixed.
Cite as
Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Determinisability of One-Clock Timed Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{clemente_et_al:LIPIcs.CONCUR.2020.42,
author = {Clemente, Lorenzo and Lasota, S{\l}awomir and Pi\'{o}rkowski, Rados{\l}aw},
title = {{Determinisability of One-Clock Timed Automata}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {42:1--42:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.42},
URN = {urn:nbn:de:0030-drops-128542},
doi = {10.4230/LIPIcs.CONCUR.2020.42},
annote = {Keywords: Timed automata, determinisation, deterministic membership problem}
}
Document
Synthesis of Computable Regular Functions of Infinite Words
Abstract
Regular functions from infinite words to infinite words can be equivalently specified by MSO-transducers, streaming ω-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. Even though regular functions are robustly characterised by several finite-state devices, even the subclass of rational functions may contain functions which are not computable (by a Turing machine with infinite input). This paper proposes a decision procedure for the following synthesis problem: given a regular function f (equivalently specified by one of the aforementioned transducer model), is f computable and if it is, synthesize a Turing machine computing it.
For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in NLogSpace (it was already known to be in PTime by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.
Cite as
Vrunda Dave, Emmanuel Filiot, Shankara Narayanan Krishna, and Nathan Lhote. Synthesis of Computable Regular Functions of Infinite Words. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 43:1-43:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{dave_et_al:LIPIcs.CONCUR.2020.43,
author = {Dave, Vrunda and Filiot, Emmanuel and Krishna, Shankara Narayanan and Lhote, Nathan},
title = {{Synthesis of Computable Regular Functions of Infinite Words}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {43:1--43:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.43},
URN = {urn:nbn:de:0030-drops-128554},
doi = {10.4230/LIPIcs.CONCUR.2020.43},
annote = {Keywords: transducers, infinite words, computability, continuity, synthesis}
}
Document
Residual Nominal Automata
Abstract
We are motivated by the following question: which nominal languages admit an active learning algorithm? This question was left open in previous work, and is particularly challenging for languages recognised by nondeterministic automata. To answer it, we develop the theory of residual nominal automata, a subclass of nondeterministic nominal automata. We prove that this class has canonical representatives, which can always be constructed via a finite number of observations. This property enables active learning algorithms, and makes up for the fact that residuality - a semantic property - is undecidable for nominal automata. Our construction for canonical residual automata is based on a machine-independent characterisation of residual languages, for which we develop new results in nominal lattice theory. Studying residuality in the context of nominal languages is a step towards a better understanding of learnability of automata with some sort of nondeterminism.
Cite as
Joshua Moerman and Matteo Sammartino. Residual Nominal Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 44:1-44:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{moerman_et_al:LIPIcs.CONCUR.2020.44,
author = {Moerman, Joshua and Sammartino, Matteo},
title = {{Residual Nominal Automata}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {44:1--44:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.44},
URN = {urn:nbn:de:0030-drops-128563},
doi = {10.4230/LIPIcs.CONCUR.2020.44},
annote = {Keywords: nominal automata, residual automata, derivative language, decidability, closure, exact learning, lattice theory}
}
Document
Flatness and Complexity of Immediate Observation Petri Nets
Abstract
In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the coverability and reachability problem for BIO nets, and even a certain set-parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.
Cite as
Mikhail Raskin, Chana Weil-Kennedy, and Javier Esparza. Flatness and Complexity of Immediate Observation Petri Nets. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 45:1-45:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{raskin_et_al:LIPIcs.CONCUR.2020.45,
author = {Raskin, Mikhail and Weil-Kennedy, Chana and Esparza, Javier},
title = {{Flatness and Complexity of Immediate Observation Petri Nets}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {45:1--45:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.45},
URN = {urn:nbn:de:0030-drops-128574},
doi = {10.4230/LIPIcs.CONCUR.2020.45},
annote = {Keywords: Petri Nets, Reachability Analysis, Parameterized Verification, Flattability}
}
Document
Deciding the Existence of Cut-Off in Parameterized Rendez-Vous Networks
Abstract
We study networks of processes which all execute the same finite-state protocol and communicate thanks to a rendez-vous mechanism. Given a protocol, we are interested in checking whether there exists a number, called a cut-off, such that in any networks with a bigger number of participants, there is an execution where all the entities end in some final states. We provide decidability and complexity results of this problem under various assumptions, such as absence/presence of a leader or symmetric/asymmetric rendez-vous.
Cite as
Florian Horn and Arnaud Sangnier. Deciding the Existence of Cut-Off in Parameterized Rendez-Vous Networks. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{horn_et_al:LIPIcs.CONCUR.2020.46,
author = {Horn, Florian and Sangnier, Arnaud},
title = {{Deciding the Existence of Cut-Off in Parameterized Rendez-Vous Networks}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {46:1--46:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.46},
URN = {urn:nbn:de:0030-drops-128581},
doi = {10.4230/LIPIcs.CONCUR.2020.46},
annote = {Keywords: Parameterized networks, Verification, Cut-offs}
}
Document
Parametrized Universality Problems for One-Counter Nets
Abstract
We study the language universality problem for One-Counter Nets, also known as 1-dimensional Vector Addition Systems with States (1-VASS), parameterized either with an initial counter value, or with an upper bound on the allowed counter value during runs. The language accepted by an OCN (defined by reaching a final control state) is monotone in both parameters. This yields two natural questions: 1) does there exist an initial counter value that makes the language universal? 2) does there exist a sufficiently high ceiling so that the bounded language is universal?
Although the ordinary universality problem is decidable (and Ackermann-complete) and these parameterized variants seem to reduce to checking basic structural properties of the underlying automaton, we show that in fact both problems are undecidable. We also look into the complexities of the problems for several decidable subclasses, namely for unambiguous, and deterministic systems, and for those over a single-letter alphabet.
Cite as
Shaull Almagor, Udi Boker, Piotr Hofman, and Patrick Totzke. Parametrized Universality Problems for One-Counter Nets. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 47:1-47:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CONCUR.2020.47,
author = {Almagor, Shaull and Boker, Udi and Hofman, Piotr and Totzke, Patrick},
title = {{Parametrized Universality Problems for One-Counter Nets}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {47:1--47:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.47},
URN = {urn:nbn:de:0030-drops-128592},
doi = {10.4230/LIPIcs.CONCUR.2020.47},
annote = {Keywords: Counter net, VASS, Unambiguous Automata, Universality}
}
Document
Reachability in Fixed Dimension Vector Addition Systems with States
Abstract
The reachability problem is a central decision problem in verification of vector addition systems with states (VASS). In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability.
We obtain three main results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional ones. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14.
Cite as
Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. Reachability in Fixed Dimension Vector Addition Systems with States. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 48:1-48:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2020.48,
author = {Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and Lazi\'{c}, Ranko and Leroux, J\'{e}r\^{o}me and Mazowiecki, Filip},
title = {{Reachability in Fixed Dimension Vector Addition Systems with States}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {48:1--48:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.48},
URN = {urn:nbn:de:0030-drops-128605},
doi = {10.4230/LIPIcs.CONCUR.2020.48},
annote = {Keywords: reachability problem, vector addition systems, Petri nets}
}
Document
Bounded Reachability Problems Are Decidable in FIFO Machines
Abstract
The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e. the sequence of messages sent through a particular channel belongs to a given bounded language). We prove, by reducing this model to a counter machine with restricted zero tests, that the rational-reachability problem (and by extension, control-state reachability, unboundedness, deadlock, etc.) is decidable. This class of machines subsumes input-letter-bounded machines, flat machines, linear FIFO nets, and monogeneous machines, for which some of these problems were already shown to be decidable. These theoretical results can form the foundations to build a tool to verify general FIFO machines based on the analysis of input-bounded machines.
Cite as
Benedikt Bollig, Alain Finkel, and Amrita Suresh. Bounded Reachability Problems Are Decidable in FIFO Machines. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 49:1-49:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bollig_et_al:LIPIcs.CONCUR.2020.49,
author = {Bollig, Benedikt and Finkel, Alain and Suresh, Amrita},
title = {{Bounded Reachability Problems Are Decidable in FIFO Machines}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {49:1--49:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.49},
URN = {urn:nbn:de:0030-drops-128615},
doi = {10.4230/LIPIcs.CONCUR.2020.49},
annote = {Keywords: FIFO machines, reachability, underapproximation, counter machines}
}
Document
Propositional Dynamic Logic for Hyperproperties
Abstract
Information security properties of reactive systems like non-interference often require relating different executions of the system to each other and following them simultaneously. Such hyperproperties can also be useful in other contexts, e.g., when analysing properties of distributed systems like linearizability. Since common logics like LTL, CTL, or the modal μ-calculus cannot express hyperproperties, the hyperlogics HyperLTL and HyperCTL^* were developed to cure this defect. However, these logics are not able to express arbitrary ω-regular properties. In this paper, we introduce HyperPDL-Δ, an adaptation of the Propositional Dynamic Logic of Fischer and Ladner for hyperproperties, in order to remove this limitation. Using an elegant automata-theoretic framework, we show that HyperPDL-Δ model checking is asymptotically not more expensive than HyperCTL^* model checking, despite its vastly increased expressive power. We further investigate fragments of HyperPDL-Δ with regard to satisfiability checking.
Cite as
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Propositional Dynamic Logic for Hyperproperties. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 50:1-50:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{gutsfeld_et_al:LIPIcs.CONCUR.2020.50,
author = {Gutsfeld, Jens Oliver and M\"{u}ller-Olm, Markus and Ohrem, Christoph},
title = {{Propositional Dynamic Logic for Hyperproperties}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {50:1--50:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Konnov, Igor and Kov\'{a}cs, Laura},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.50},
URN = {urn:nbn:de:0030-drops-128628},
doi = {10.4230/LIPIcs.CONCUR.2020.50},
annote = {Keywords: Hyperlogics, Hyperproperties, Model Checking, Automata}
}