Volume
LIPIcs, Volume 243
33rd International Conference on Concurrency Theory (CONCUR 2022)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Event
CONCUR 2022, September 12-16, 2022, Warsaw, PolandEditors
Publication Details
- published at: 2022-09-06
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-246-4
- DBLP: db/conf/concur/concur2022
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 243, CONCUR 2022, Complete Volume
Abstract
LIPIcs, Volume 243, CONCUR 2022, Complete Volume
Cite as
33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 1-712, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Proceedings{klin_et_al:LIPIcs.CONCUR.2022,
title = {{LIPIcs, Volume 243, CONCUR 2022, Complete Volume}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {1--712},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022},
URN = {urn:nbn:de:0030-drops-170623},
doi = {10.4230/LIPIcs.CONCUR.2022},
annote = {Keywords: LIPIcs, Volume 243, CONCUR 2022, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{klin_et_al:LIPIcs.CONCUR.2022.0,
author = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.0},
URN = {urn:nbn:de:0030-drops-170631},
doi = {10.4230/LIPIcs.CONCUR.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
CONCUR Test-Of-Time Award 2022 (Invited Paper)
Abstract
This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the four papers that received the Award in 2022.
Cite as
Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi. CONCUR Test-Of-Time Award 2022 (Invited Paper). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 1:1-1:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{castellani_et_al:LIPIcs.CONCUR.2022.1,
author = {Castellani, Ilaria and Gastin, Paul and Kupferman, Orna and Randour, Mickael and Sangiorgi, Davide},
title = {{CONCUR Test-Of-Time Award 2022}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {1:1--1:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.1},
URN = {urn:nbn:de:0030-drops-170644},
doi = {10.4230/LIPIcs.CONCUR.2022.1},
annote = {Keywords: CONCUR Test-of-Time Award}
}
Document
Invited Talk
Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk)
Abstract
Scalable verification for concurrent programs with shared memory is a long-standing, difficult problem. In 2004, O'Hearn and Brookes introduced concurrent separation logic to provide compositional reasoning about coarse-grained concurrent programs with synchronisation primitives (Gödel prize, 2016).
In 2010, I introduced logical abstraction (the fiction of separation) to CSL, developing the CAP logic for reasoning about fine-grained concurrent programs in general and fine-grained lock algorithms in particular. In one logic, it was possible to provide two-sided specifications of concurrent operations, with formally verified implementations and clients.
In 2014, I introduced logical atomicity (the fiction of atomicity) to concurrent separation logics, developing the TaDA logic to capture when individual operations behave atomically. Unlike CAP, where synchronisation primitives leak into the specifications, with TaDA the specifications are "just right" in that they provide more general atomic functions specifications to capture, for example, the full behaviour of lock operations.
In 2021, I introduced environment liveness conditions to concurrent separation logics, developing the TaDA Live logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. The fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment.
In this talk, I will explain this on-going journey in the wonderful world of concurrent separation logics. I will also explain why I have a bright green office chair in the corner of my office, patterned in gold lamé.
Many thanks to my fabulous coauthors on concurrent separation logics: Thomas Dinsdale-Young, Emanuele D'Osualdo, Mike Dodds, Azadeh Farzan, Matthew Parkinson, Pedro da Rocha Pinto, Julian Sutherland, Viktor Vafeiadis and more. Suggested Reading:
- Peter O'Hearn: Resources, Concurrency and Local Reasoning, Journal of Theoretical Computer Science, Festschrift for John C Reynolds 70th birthday, 2007.
- Thomas Dinsdale-Young, Pedro da Rocha Pinto and Philippa Gardner: A Perspective on Specifying and Verifying Concurrent Modules, Journal of Logical and Algebraic Methods in Programming, 2018.
- Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner and Julian Sutherland: TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), 2021.
Cite as
Philippa Gardner. Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{gardner:LIPIcs.CONCUR.2022.2,
author = {Gardner, Philippa},
title = {{Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.2},
URN = {urn:nbn:de:0030-drops-170659},
doi = {10.4230/LIPIcs.CONCUR.2022.2},
annote = {Keywords: Concurrent separation logic}
}
Document
Invited Talk
Distributed Decision Problems: Concurrent Specifications Beyond Binary Relations (Invited Talk)
Abstract
Much discussion exists about what is computation, but less about is a computational problem. Turing’s definition of computation was based on computing functions. When we move from sequential computing to interactive computing, discussions concentrate on computations that do not terminate, overlooking notions of distributed problems. Many models where concurrency happens have been proposed, ranging from those equivalent to a Turing machine, to those where much heated discussion has taken place, claiming that interactive models are fundamentally different from Turing machines.
It is argued here that there is no need to go all the way to non-terminating interaction, to appreciate how different distributed computation is from sequential computation. The discussion concentrates on the various ways that exist of representing a distributed decision problem. Each process of a distributed system starts with an initial private input value, and after communicating with other processes in the system, produces a local output value. An input/output relation is needed, to specify which output values are legal for a particular assignment of input values to the processes.
An overview is provided of some results that show how rich the topic of distributed decision problems can be, when asynchronous processes can fail, but mostly independent of particular models of distributed computing and their many intricate details (types of failures and of communication). We are in a world very different from that of the functions of sequential computation; moving away from the world of graphs beyond binary relations, to the world of simplicial complexes.
Cite as
Sergio Rajsbaum. Distributed Decision Problems: Concurrent Specifications Beyond Binary Relations (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 3:1-3:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{rajsbaum:LIPIcs.CONCUR.2022.3,
author = {Rajsbaum, Sergio},
title = {{Distributed Decision Problems: Concurrent Specifications Beyond Binary Relations}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {3:1--3:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.3},
URN = {urn:nbn:de:0030-drops-170660},
doi = {10.4230/LIPIcs.CONCUR.2022.3},
annote = {Keywords: Distributed decision tasks, simplicial complex, linearizability, interval-linearizability, Arrow’s impossibility, Speedup theorems}
}
Document
Invited Talk
Sequential Decision Making With Information Asymmetry (Invited Talk)
Abstract
We survey some recent results in sequential decision making under uncertainty, where there is an information asymmetry among the decision-makers. We consider two versions of the problem: persuasion and mechanism design. In persuasion, a more-informed principal influences the actions of a less-informed agent by signaling information. In mechanism design, a less-informed principal incentivizes a more-informed agent to reveal information by committing to a mechanism, so that the principal can make more informed decisions. We define Markov persuasion processes and Markov mechanism processes that model persuasion and mechanism design into dynamic models. Then we survey results on optimal persuasion and optimal mechanism design on myopic and far-sighted agents. These problems are solvable in polynomial time for myopic agents but hard for far-sighted agents.
Cite as
Jiarui Gan, Rupak Majumdar, Goran Radanovic, and Adish Singla. Sequential Decision Making With Information Asymmetry (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{gan_et_al:LIPIcs.CONCUR.2022.4,
author = {Gan, Jiarui and Majumdar, Rupak and Radanovic, Goran and Singla, Adish},
title = {{Sequential Decision Making With Information Asymmetry}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {4:1--4:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.4},
URN = {urn:nbn:de:0030-drops-170673},
doi = {10.4230/LIPIcs.CONCUR.2022.4},
annote = {Keywords: Bayesian persuasion, Automated mechanism design, Markov persuasion processes, Markov mechanism processes, Myopic agents}
}
Document
Invited Talk
Involved VASS Zoo (Invited Talk)
Abstract
We briefly describe recent advances on understanding the complexity of the reachability problem for vector addition systems (or equivalently for vector addition systems with states - VASSes). We present a zoo of a few involved VASS examples, which illustrate various aspects of hardness of VASSes and various techniques of proving lower complexity bounds.
Cite as
Wojciech Czerwiński. Involved VASS Zoo (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{czerwinski:LIPIcs.CONCUR.2022.5,
author = {Czerwi\'{n}ski, Wojciech},
title = {{Involved VASS Zoo}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {5:1--5:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.5},
URN = {urn:nbn:de:0030-drops-170681},
doi = {10.4230/LIPIcs.CONCUR.2022.5},
annote = {Keywords: vector addition systems, reachability problem, low dimensions, examples}
}
Document
On the Axiomatisation of Branching Bisimulation Congruence over CCS
Abstract
In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contribution, we show that, when the set of actions is finite, rooted branching bisimilarity has a finite equational basis over CCS enriched with the left merge and communication merge operators from ACP.
Cite as
Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik. On the Axiomatisation of Branching Bisimulation Congruence over CCS. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CONCUR.2022.6,
author = {Aceto, Luca and Castiglioni, Valentina and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas},
title = {{On the Axiomatisation of Branching Bisimulation Congruence over CCS}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {6:1--6:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.6},
URN = {urn:nbn:de:0030-drops-170692},
doi = {10.4230/LIPIcs.CONCUR.2022.6},
annote = {Keywords: Equational basis, Weak semantics, CCS, Parallel composition}
}
Document
Non-Deterministic Abstract Machines
Abstract
We present a generic design of abstract machines for non-deterministic programming languages, such as process calculi or concurrent lambda calculi, that provides a simple way to implement them. Such a machine traverses a term in the search for a redex, making non-deterministic choices when several paths are possible and backtracking when it reaches a dead end, i.e., an irreducible subterm. The search is guaranteed to terminate thanks to term annotations the machine introduces along the way.
We show how to automatically derive a non-deterministic abstract machine from a zipper semantics - a form of structural operational semantics in which the decomposition process of a term into a context and a redex is made explicit. The derivation method ensures the soundness and completeness of the machines w.r.t. the zipper semantics.
Cite as
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Non-Deterministic Abstract Machines. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{biernacka_et_al:LIPIcs.CONCUR.2022.7,
author = {Biernacka, Ma{\l}gorzata and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Schmitt, Alan},
title = {{Non-Deterministic Abstract Machines}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {7:1--7:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.7},
URN = {urn:nbn:de:0030-drops-170705},
doi = {10.4230/LIPIcs.CONCUR.2022.7},
annote = {Keywords: Abstract machines, non-determinism, lambda-calculus, process calculi}
}
Document
Slimming down Petri Boxes: Compact Petri Net Models of Control Flows
Abstract
We look at the construction of compact Petri net models corresponding to process algebra expressions supporting sequential, choice, and parallel compositions. If "silent" transitions are disallowed, a construction based on Cartesian product is traditionally used to construct places in the target Petri net, resulting in an exponential explosion in the net size. We demonstrate that this exponential explosion can be avoided, by developing a link between this construction problem and the problem of finding an edge clique cover of a graph that is guaranteed to be complement-reducible (i.e., a cograph). It turns out that the exponential number of places created by the Cartesian product construction can be reduced down to polynomial (quadratic) even in the worst case, and to logarithmic in the best (non-degraded) case. As these results affect the "core" modelling techniques based on Petri nets, eliminating a source of an exponential explosion, we hope they will have applications in Petri net modelling and translations of various formalisms to Petri nets.
Cite as
Victor Khomenko, Maciej Koutny, and Alex Yakovlev. Slimming down Petri Boxes: Compact Petri Net Models of Control Flows. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{khomenko_et_al:LIPIcs.CONCUR.2022.8,
author = {Khomenko, Victor and Koutny, Maciej and Yakovlev, Alex},
title = {{Slimming down Petri Boxes: Compact Petri Net Models of Control Flows}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {8:1--8:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.8},
URN = {urn:nbn:de:0030-drops-170710},
doi = {10.4230/LIPIcs.CONCUR.2022.8},
annote = {Keywords: Petri net, Petri box, cograph, edge clique cover, control flow, static construction, local construction, interface graph, Burst automata, composition}
}
Document
On the Sequential Probability Ratio Test in Hidden Markov Models
Abstract
We consider the Sequential Probability Ratio Test applied to Hidden Markov Models. Given two Hidden Markov Models and a sequence of observations generated by one of them, the Sequential Probability Ratio Test attempts to decide which model produced the sequence. We show relationships between the execution time of such an algorithm and Lyapunov exponents of random matrix systems. Further, we give complexity results about the execution time taken by the Sequential Probability Ratio Test.
Cite as
Oscar Darwin and Stefan Kiefer. On the Sequential Probability Ratio Test in Hidden Markov Models. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{darwin_et_al:LIPIcs.CONCUR.2022.9,
author = {Darwin, Oscar and Kiefer, Stefan},
title = {{On the Sequential Probability Ratio Test in Hidden Markov Models}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.9},
URN = {urn:nbn:de:0030-drops-170728},
doi = {10.4230/LIPIcs.CONCUR.2022.9},
annote = {Keywords: Markov chains, hidden Markov models, probabilistic systems, verification}
}
Document
Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications
Abstract
We consider the model-checking problem for parametric probabilistic dynamical systems, formalised as Markov chains with parametric transition functions, analysed under the distribution-transformer semantics (in which a Markov chain induces a sequence of distributions over states).
We examine the problem of synthesising the set of parameter valuations of a parametric Markov chain such that the orbits of induced state distributions satisfy a prefix-independent ω-regular property.
Our main result establishes that in all non-degenerate instances, the feasible set of parameters is (up to a null set) semialgebraic, and can moreover be computed (in polynomial time assuming that the ambient dimension, corresponding to the number of states of the Markov chain, is fixed).
Cite as
Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell. Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{baier_et_al:LIPIcs.CONCUR.2022.10,
author = {Baier, Christel and Funke, Florian and Jantsch, Simon and Karimov, Toghrul and Lefaucheux, Engel and Ouaknine, Jo\"{e}l and Purser, David and Whiteland, Markus A. and Worrell, James},
title = {{Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {10:1--10:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.10},
URN = {urn:nbn:de:0030-drops-170732},
doi = {10.4230/LIPIcs.CONCUR.2022.10},
annote = {Keywords: Model checking, parametric Markov chains, distribution transformer semantics}
}
Document
Anytime Guarantees for Reachability in Uncountable Markov Decision Processes
Abstract
We consider the problem of approximating the reachability probabilities in Markov decision processes (MDP) with uncountable (continuous) state and action spaces. While there are algorithms that, for special classes of such MDP, provide a sequence of approximations converging to the true value in the limit, our aim is to obtain an algorithm with guarantees on the precision of the approximation.
As this problem is undecidable in general, assumptions on the MDP are necessary. Our main contribution is to identify sufficient assumptions that are as weak as possible, thus approaching the "boundary" of which systems can be correctly and reliably analyzed. To this end, we also argue why each of our assumptions is necessary for algorithms based on processing finitely many observations.
We present two solution variants. The first one provides converging lower bounds under weaker assumptions than typical ones from previous works concerned with guarantees. The second one then utilizes stronger assumptions to additionally provide converging upper bounds. Altogether, we obtain an anytime algorithm, i.e. yielding a sequence of approximants with known and iteratively improving precision, converging to the true value in the limit. Besides, due to the generality of our assumptions, our algorithms are very general templates, readily allowing for various heuristics from literature in contrast to, e.g., a specific discretization algorithm. Our theoretical contribution thus paves the way for future practical improvements without sacrificing correctness guarantees.
Cite as
Kush Grover, Jan Křetínský, Tobias Meggendorfer, and Maximilian Weininger. Anytime Guarantees for Reachability in Uncountable Markov Decision Processes. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{grover_et_al:LIPIcs.CONCUR.2022.11,
author = {Grover, Kush and K\v{r}et{\'\i}nsk\'{y}, Jan and Meggendorfer, Tobias and Weininger, Maximilian},
title = {{Anytime Guarantees for Reachability in Uncountable Markov Decision Processes}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {11:1--11:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.11},
URN = {urn:nbn:de:0030-drops-170743},
doi = {10.4230/LIPIcs.CONCUR.2022.11},
annote = {Keywords: Uncountable system, Markov decision process, discrete-time Markov control process, probabilistic verification, anytime guarantee}
}
Document
Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics
Abstract
We study the Büchi non-emptiness problem for networks of timed automata. Standard solutions consider the network as a monolithic timed automaton obtained as a synchronized product and build its zone graph on-the-fly under the classical global-time semantics. In the global-time semantics, all processes are assumed to have a common global timeline.
Bengtsson et al. in 1998 have proposed a local-time semantics where each process in the network moves independently according to a local timeline, and processes synchronize their timelines when they do a common action. It has been shown that the local-time semantics is equivalent to the global-time semantics for finite runs, and hence can be used for checking reachability. The local-time semantics allows computation of a local zone graph which has good independence properties and is amenable to partial-order methods. Hence local zone graphs are able to better tackle the state-space explosion due to concurrency.
In this work, we extend the results to the Büchi setting. We propose a local zone graph computation that can be coupled with a partial-order method, to solve the Büchi non-emptiness problem in timed networks. In the process, we develop a theory of regions for the local-time semantics.
Cite as
Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Checking Timed Büchi Automata Emptiness Using the Local-Time Semantics. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 12:1-12:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{herbreteau_et_al:LIPIcs.CONCUR.2022.12,
author = {Herbreteau, Fr\'{e}d\'{e}ric and Srivathsan, B. and Walukiewicz, Igor},
title = {{Checking Timed B\"{u}chi Automata Emptiness Using the Local-Time Semantics}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {12:1--12:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.12},
URN = {urn:nbn:de:0030-drops-170756},
doi = {10.4230/LIPIcs.CONCUR.2022.12},
annote = {Keywords: Timed B\"{u}chi automata, local-time semantics, zones, abstraction, partial-order reduction}
}
Document
Simulations for Event-Clock Automata
Abstract
Event-clock automata are a well-known subclass of timed automata which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for event-clock automata. A main reason for this is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied in [Gilles Geeraerts et al., 2011; Gilles Geeraerts et al., 2014], where the authors also proposed a solution using zone extrapolations.
In this paper, we propose an alternative zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. Our algorithm exploits the 𝒢-simulation framework, which is the coarsest known simulation relation for reachability, and has been recently used for advances in other extensions of timed automata.
Cite as
S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. Simulations for Event-Clock Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{akshay_et_al:LIPIcs.CONCUR.2022.13,
author = {Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.},
title = {{Simulations for Event-Clock Automata}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.13},
URN = {urn:nbn:de:0030-drops-170766},
doi = {10.4230/LIPIcs.CONCUR.2022.13},
annote = {Keywords: Event-clock automata, verification, zones, simulations, reachability}
}
Document
History-Deterministic Timed Automata
Abstract
We explore the notion of history-determinism in the context of timed automata (TA). History-deterministic automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and history-deterministic specifications allow for game-based verification without an expensive determinization step.
We show yet another characterisation of history-determinism in terms of fair simulation, at the general level of labelled transition systems: a system is history-deterministic precisely if and only if it fairly simulates all language smaller systems.
For timed automata over infinite timed words it is known that universality is undecidable for Büchi TA. We show that for history-deterministic TA with arbitrary parity acceptance, timed universality, inclusion, and synthesis all remain decidable and are ExpTime-complete.
For the subclass of TA with safety or reachability acceptance, we show that checking whether such an automaton is history-deterministic is decidable (in ExpTime), and history-deterministic TA with safety acceptance are effectively determinizable without introducing new automata states.
Cite as
Thomas A. Henzinger, Karoliina Lehtinen, and Patrick Totzke. History-Deterministic Timed Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2022.14,
author = {Henzinger, Thomas A. and Lehtinen, Karoliina and Totzke, Patrick},
title = {{History-Deterministic Timed Automata}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {14:1--14:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.14},
URN = {urn:nbn:de:0030-drops-170778},
doi = {10.4230/LIPIcs.CONCUR.2022.14},
annote = {Keywords: Timed Automata, History-determinism, Good-for-games, fair simulation, synthesis}
}
Document
Decidability of One-Clock Weighted Timed Games with Arbitrary Weights
Abstract
Weighted Timed Games (WTG for short) are the most widely used model to describe controller synthesis problems involving real-time issues. Unfortunately, they are notoriously difficult, and undecidable in general. As a consequence, one-clock WTG has attracted a lot of attention, especially because they are known to be decidable when only non-negative weights are allowed. However, when arbitrary weights are considered, despite several recent works, their decidability status was still unknown. In this paper, we solve this problem positively and show that the value function can be computed in exponential time (if weights are encoded in unary).
Cite as
Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Decidability of One-Clock Weighted Timed Games with Arbitrary Weights. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{monmege_et_al:LIPIcs.CONCUR.2022.15,
author = {Monmege, Benjamin and Parreaux, Julie and Reynier, Pierre-Alain},
title = {{Decidability of One-Clock Weighted Timed Games with Arbitrary Weights}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {15:1--15:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.15},
URN = {urn:nbn:de:0030-drops-170786},
doi = {10.4230/LIPIcs.CONCUR.2022.15},
annote = {Keywords: Weighted timed games, Algorithmic game theory, Timed automata}
}
Document
Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable
Abstract
We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASSes) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed conditions). In general the problem of language equivalence is undecidable even for one-dimensional VASSes, thus to get decidability we investigate restricted subclasses. On one hand we show that the problem of language inclusion of a VASS in k-ambiguous VASS (for any natural k) is decidable and even in Ackermann. On the other hand we prove that the language equivalence problem is Ackermann-hard already for deterministic VASSes. These two results imply Ackermann-completeness for language inclusion and equivalence in several possible restrictions. Some of our techniques can be also applied in much broader generality in infinite-state systems, namely for some subclass of well-structured transition systems.
Cite as
Wojciech Czerwiński and Piotr Hofman. Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2022.16,
author = {Czerwi\'{n}ski, Wojciech and Hofman, Piotr},
title = {{Language Inclusion for Boundedly-Ambiguous Vector Addition Systems Is Decidable}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {16:1--16:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.16},
URN = {urn:nbn:de:0030-drops-170796},
doi = {10.4230/LIPIcs.CONCUR.2022.16},
annote = {Keywords: vector addition systems, language inclusion, language equivalence, determinism, unambiguity, bounded ambiguity, Petri nets, well-structured transition systems}
}
Document
Complexity of Coverability in Depth-Bounded Processes
Abstract
We consider the class of depth-bounded processes in π-calculus. These processes are the most expressive fragment of π-calculus, for which verification problems are known to be decidable. The decidability of the coverability problem for this class has been achieved by means of well-quasi orders. (Meyer, IFIP TCS 2008; Wies, Zufferey and Henzinger, FoSSaCS 2010). However, the precise complexity of this problem has not been known so far, with only a known EXPSPACE-lower bound.
In this paper, we prove that coverability for depth-bounded processes is 𝐅_ε₀-complete, where 𝐅_ε₀ is a class in the fast-growing hierarchy of complexity classes. This solves an open problem mentioned by Haase, Schmitz, and Schnoebelen (LMCS, Vol 10, Issue 4) and also addresses a question raised by Wies, Zufferey and Henzinger (FoSSaCS 2010).
Cite as
A. R. Balasubramanian. Complexity of Coverability in Depth-Bounded Processes. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{balasubramanian:LIPIcs.CONCUR.2022.17,
author = {Balasubramanian, A. R.},
title = {{Complexity of Coverability in Depth-Bounded Processes}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {17:1--17:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.17},
URN = {urn:nbn:de:0030-drops-170809},
doi = {10.4230/LIPIcs.CONCUR.2022.17},
annote = {Keywords: \pi-calculus, Depth-bounded processes, Fast-growing complexity classes}
}
Document
Determinization of One-Counter Nets
Abstract
One-Counter Nets (OCNs) are finite-state automata equipped with a counter that is not allowed to become negative, but does not have zero tests. Their simplicity and close connection to various other models (e.g., VASS, Counter Machines and Pushdown Automata) make them an attractive model for studying the border of decidability for the classical decision problems.
The deterministic fragment of OCNs (DOCNs) typically admits more tractable decision problems, and while these problems and the expressive power of DOCNs have been studied, the determinization problem, namely deciding whether an OCN admits an equivalent DOCN, has not received attention.
We introduce four notions of OCN determinizability, which arise naturally due to intricacies in the model, and specifically, the interpretation of the initial counter value. We show that in general, determinizability is undecidable under most notions, but over a singleton alphabet (i.e., 1 dimensional VASS) one definition becomes decidable, and the rest become trivial, in that there is always an equivalent DOCN.
Cite as
Shaull Almagor and Asaf Yeshurun. Determinization of One-Counter Nets. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CONCUR.2022.18,
author = {Almagor, Shaull and Yeshurun, Asaf},
title = {{Determinization of One-Counter Nets}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {18:1--18:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.18},
URN = {urn:nbn:de:0030-drops-170812},
doi = {10.4230/LIPIcs.CONCUR.2022.18},
annote = {Keywords: Determinization, One-Counter Net, Vector Addition System, Automata, Semilinear}
}
Document
Energy Games with Resource-Bounded Environments
Abstract
An energy game is played between two players, modeling a resource-bounded system and its environment. The players take turns moving a token along a finite graph. Each edge of the graph is labeled by an integer, describing an update to the energy level of the system that occurs whenever the edge is traversed. The system wins the game if it never runs out of energy. Different applications have led to extensions of the above basic setting. For example, addressing a combination of the energy requirement with behavioral specifications, researchers have studied richer winning conditions, and addressing systems with several bounded resources, researchers have studied games with multi-dimensional energy updates. All extensions, however, assume that the environment has no bounded resources.
We introduce and study both-bounded energy games (BBEGs), in which both the system and the environment have multi-dimensional energy bounds. In BBEGs, each edge in the game graph is labeled by two integer vectors, describing updates to the multi-dimensional energy levels of the system and the environment. A system wins a BBEG if it never runs out of energy or if its environment runs out of energy. We show that BBEGs are determined, and that the problem of determining the winner in a given BBEG is decidable iff both the system and the environment have energy vectors of dimension 1. We also study how restrictions on the memory of the system and/or the environment as well as upper bounds on their energy levels influence the winner and the complexity of the problem.
Cite as
Orna Kupferman and Naama Shamash Halevy. Energy Games with Resource-Bounded Environments. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kupferman_et_al:LIPIcs.CONCUR.2022.19,
author = {Kupferman, Orna and Shamash Halevy, Naama},
title = {{Energy Games with Resource-Bounded Environments}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {19:1--19:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.19},
URN = {urn:nbn:de:0030-drops-170823},
doi = {10.4230/LIPIcs.CONCUR.2022.19},
annote = {Keywords: Energy Games, Infinite-State Systems, Decidability}
}
Document
Half-Positional Objectives Recognized by Deterministic Büchi Automata
Abstract
A central question in the theory of two-player games over graphs is to understand which objectives are half-positional, that is, which are the objectives for which the protagonist does not need memory to implement winning strategies. Objectives for which both players do not need memory have already been characterized (both in finite and infinite graphs); however, less is known about half-positional objectives. In particular, no characterization of half-positionality is known for the central class of ω-regular objectives.
In this paper, we characterize objectives recognizable by deterministic Büchi automata (a class of ω-regular objectives) that are half-positional, in both finite and infinite graphs. Our characterization consists of three natural conditions linked to the language-theoretic notion of right congruence. Furthermore, this characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.
Cite as
Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-Positional Objectives Recognized by Deterministic Büchi Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2022.20,
author = {Bouyer, Patricia and Casares, Antonio and Randour, Mickael and Vandenhove, Pierre},
title = {{Half-Positional Objectives Recognized by Deterministic B\"{u}chi Automata}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {20:1--20:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.20},
URN = {urn:nbn:de:0030-drops-170833},
doi = {10.4230/LIPIcs.CONCUR.2022.20},
annote = {Keywords: two-player games on graphs, half-positionality, memoryless optimal strategies, B\"{u}chi automata, \omega-regularity}
}
Document
Two-Player Boundedness Counter Games
Abstract
We consider two-player zero-sum games with winning objectives beyond regular languages, expressed as a parity condition in conjunction with a Boolean combination of boundedness conditions on a finite set of counters which can be incremented, reset to 0, but not tested. A boundedness condition requires that a given counter is bounded along the play. Such games are decidable, though with non-optimal complexity, by an encoding into the logic WMSO with the unbounded and path quantifiers, which is known to be decidable over infinite trees. Our objective is to give tight or tighter complexity results for particular classes of counter games with boundedness conditions, and study their strategy complexity. In particular, counter games with conjunction of boundedness conditions are easily seen to be equivalent to Streett games, so, they are CoNP-c. Moreover, finite-memory strategies suffice for Eve and memoryless strategies suffice for Adam. For counter games with a disjunction of boundedness conditions, we prove that they are in solvable in NP∩CoNP, and in PTime if the parity condition is fixed. In that case memoryless strategies suffice for Eve while infinite memory strategies might be necessary for Adam. Finally, we consider an extension of those games with a max operation. In that case, the complexity increases: for conjunctions of boundedness conditions, counter games are EXPTIME-c.
Cite as
Emmanuel Filiot and Edwin Hamel-de le Court. Two-Player Boundedness Counter Games. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{filiot_et_al:LIPIcs.CONCUR.2022.21,
author = {Filiot, Emmanuel and Hamel-de le Court, Edwin},
title = {{Two-Player Boundedness Counter Games}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {21:1--21:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.21},
URN = {urn:nbn:de:0030-drops-170841},
doi = {10.4230/LIPIcs.CONCUR.2022.21},
annote = {Keywords: Controller synthesis, Game theory, Counter Games, Boundedness objectives}
}
Document
Different Strokes in Randomised Strategies: Revisiting Kuhn’s Theorem Under Finite-Memory Assumptions
Abstract
Two-player (antagonistic) games on (possibly stochastic) graphs are a prevalent model in theoretical computer science, notably as a framework for reactive synthesis.
Optimal strategies may require randomisation when dealing with inherently probabilistic goals, balancing multiple objectives, or in contexts of partial information. There is no unique way to define randomised strategies. For instance, one can use so-called mixed strategies or behavioural ones. In the most general settings, these two classes do not share the same expressiveness. A seminal result in game theory - Kuhn’s theorem - asserts their equivalence in games of perfect recall.
This result crucially relies on the possibility for strategies to use infinite memory, i.e., unlimited knowledge of all past observations. However, computer systems are finite in practice. Hence it is pertinent to restrict our attention to finite-memory strategies, defined as automata with outputs. Randomisation can be implemented in these in different ways: the initialisation, outputs or transitions can be randomised or deterministic respectively. Depending on which aspects are randomised, the expressiveness of the corresponding class of finite-memory strategies differs.
In this work, we study two-player turn-based stochastic games and provide a complete taxonomy of the classes of finite-memory strategies obtained by varying which of the three aforementioned components are randomised. Our taxonomy holds both in settings of perfect and imperfect information, and in games with more than two players.
Cite as
James C. A. Main and Mickael Randour. Different Strokes in Randomised Strategies: Revisiting Kuhn’s Theorem Under Finite-Memory Assumptions. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{main_et_al:LIPIcs.CONCUR.2022.22,
author = {Main, James C. A. and Randour, Mickael},
title = {{Different Strokes in Randomised Strategies: Revisiting Kuhn’s Theorem Under Finite-Memory Assumptions}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {22:1--22:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.22},
URN = {urn:nbn:de:0030-drops-170854},
doi = {10.4230/LIPIcs.CONCUR.2022.22},
annote = {Keywords: two-player games on graphs, stochastic games, Markov decision processes, finite-memory strategies, randomised strategies}
}
Document
Regular Model Checking Upside-Down: An Invariant-Based Approach
Abstract
Regular model checking is a technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. It applies to systems whose set of initial configurations is regular, and whose transition relation is captured by a length-preserving transducer. To verify safety properties, regular model checking iteratively computes automata recognizing increasingly larger regular sets of reachable configurations, and checks if they contain unsafe configurations. Since this procedure often does not terminate, acceleration, abstraction, and widening techniques have been developed to compute a regular superset of the reachable configurations.
In this paper we develop a complementary procedure. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and approach it from above. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since this intersection is non-regular in general, we introduce b-bounded invariants, defined as those representable by CNF-formulas with at most b clauses. We prove that, for every b ≥ 0, the intersection of all b-bounded inductive invariants is regular, and we construct an automaton recognizing it. We show that whether this automaton accepts some unsafe configuration is in EXPSPACE for every b ≥ 0, and PSPACE-complete for b = 1. Finally, we study how large must b be to prove safety properties of a number of benchmarks.
Cite as
Javier Esparza, Mikhail Raskin, and Christoph Welzel. Regular Model Checking Upside-Down: An Invariant-Based Approach. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{esparza_et_al:LIPIcs.CONCUR.2022.23,
author = {Esparza, Javier and Raskin, Mikhail and Welzel, Christoph},
title = {{Regular Model Checking Upside-Down: An Invariant-Based Approach}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.23},
URN = {urn:nbn:de:0030-drops-170862},
doi = {10.4230/LIPIcs.CONCUR.2022.23},
annote = {Keywords: parameterized verification, structural analysis, regular languages, regular model-checking, traps}
}
Document
On an Invariance Problem for Parameterized Concurrent Systems
Abstract
We consider concurrent systems consisting of replicated finite-state processes that synchronize via joint interactions in a network with user-defined topology. The system is specified using a resource logic with a multiplicative connective and inductively defined predicates, reminiscent of Separation Logic [John C. Reynolds, 2002]. The problem we consider is if a given formula in this logic defines an invariant, namely whether any model of the formula, following an arbitrary firing sequence of interactions, is transformed into another model of the same formula. This property, called havoc invariance, is quintessential in proving the correctness of reconfiguration programs that change the structure of the network at runtime. We show that the havoc invariance problem is many-one reducible to the entailment problem ϕ ⊧ ψ, asking if any model of ϕ is also a model of ψ. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.
Cite as
Marius Bozga, Lucas Bueri, and Radu Iosif. On an Invariance Problem for Parameterized Concurrent Systems. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bozga_et_al:LIPIcs.CONCUR.2022.24,
author = {Bozga, Marius and Bueri, Lucas and Iosif, Radu},
title = {{On an Invariance Problem for Parameterized Concurrent Systems}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {24:1--24:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.24},
URN = {urn:nbn:de:0030-drops-170874},
doi = {10.4230/LIPIcs.CONCUR.2022.24},
annote = {Keywords: parameterized verification, invariant checking, resource logics, reconfigurable systems, tree automata}
}
Document
Towards Concurrent Quantitative Separation Logic
Abstract
In this paper, we develop a novel verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointers is well studied, little is known about the combination of all three paradigms. To close this gap, we combine two kinds of separation logic - Quantitative Separation Logic and Concurrent Separation Logic - into a new separation logic that enables reasoning about lower bounds of the probability to realise a postcondition by executing such a program.
Cite as
Ira Fesefeldt, Joost-Pieter Katoen, and Thomas Noll. Towards Concurrent Quantitative Separation Logic. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{fesefeldt_et_al:LIPIcs.CONCUR.2022.25,
author = {Fesefeldt, Ira and Katoen, Joost-Pieter and Noll, Thomas},
title = {{Towards Concurrent Quantitative Separation Logic}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {25:1--25:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.25},
URN = {urn:nbn:de:0030-drops-170881},
doi = {10.4230/LIPIcs.CONCUR.2022.25},
annote = {Keywords: Randomization, Pointers, Heap-Manipulating, Separation Logic, Concurrency}
}
Document
Completeness Theorems for Kleene Algebra with Top
Abstract
We prove two completeness results for Kleene algebra with a top element, with respect to languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant "top" for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom. We recover that the two equational theories coincide if we slightly generalise the notion of relational model, allowing sub-algebras of relations where top is a greatest element but not necessarily the full relation.
We use models of closed languages and reductions in order to prove our completeness results, which are relative to any axiomatisation of the algebra of regular events.
Cite as
Damien Pous and Jana Wagemaker. Completeness Theorems for Kleene Algebra with Top. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{pous_et_al:LIPIcs.CONCUR.2022.26,
author = {Pous, Damien and Wagemaker, Jana},
title = {{Completeness Theorems for Kleene Algebra with Top}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {26:1--26:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.26},
URN = {urn:nbn:de:0030-drops-170890},
doi = {10.4230/LIPIcs.CONCUR.2022.26},
annote = {Keywords: Kleene algebra, Hypotheses, Completeness, Closed languages}
}
Document
Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties
Abstract
Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyperproperties have been investigated. Though model checking of these logics is undecidable, useful decidable fragments have been identified with applications e.g. for asynchronous security analysis. In this paper, we address expressiveness and decidability issues of temporal logics for asynchronous hyperproperties. We compare the expressiveness of these logics together with the extension S1S[E] of S1S with the equal-level predicate by obtaining an almost complete expressiveness picture. We also study the expressive power of these logics when interpreted on singleton sets of traces. We show that for two asynchronous extensions of HyperLTL, checking the existence of a singleton model is already undecidable, and for one of them, namely Context HyperLTL (HyperLTL_C), we establish a characterization of the singleton models in terms of the extension of standard FO[<] over traces with addition. This last result generalizes the well-known equivalence between FO[<] and LTL. Finally, we identify new boundaries on the decidability of model checking HyperLTL_C.
Cite as
Laura Bozzelli, Adriano Peron, and César Sánchez. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bozzelli_et_al:LIPIcs.CONCUR.2022.27,
author = {Bozzelli, Laura and Peron, Adriano and S\'{a}nchez, C\'{e}sar},
title = {{Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {27:1--27:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.27},
URN = {urn:nbn:de:0030-drops-170905},
doi = {10.4230/LIPIcs.CONCUR.2022.27},
annote = {Keywords: Hyperproperties, Asynchronous hyperproperties, Temporal logics for hyperproperties, Expressiveness, Decidability, Model checking}
}
Document
Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages
Abstract
One of the main motivations for this work is to obtain a distributed Krohn-Rhodes theorem for Mazurkiewicz traces. Concretely, we focus on the recently introduced operation of local cascade product of asynchronous automata and ask if every regular trace language can be accepted by a local cascade product of "simple" asynchronous automata.
Our approach crucially relies on the development of a local and past-oriented propositional dynamic logic (LocPastPDL) over traces which is shown to be expressively complete with respect to all regular trace languages. An event-formula of LocPastPDL allows to reason about the causal past of an event and a path-formula of LocPastPDL, localized at a process, allows to march along the sequence of past-events in which that process participates, checking for local regular patterns interspersed with local tests of other event-formulas. We also use additional constant formulas to compare the leading process events from the causal past. The new logic LocPastPDL is of independent interest, and the proof of its expressive completeness is rather subtle.
Finally, we provide a translation of LocPastPDL formulas into local cascade products. More precisely, we show that every LocPastPDL formula can be computed by a restricted local cascade product of the gossip automaton and localized 2-state asynchronous reset automata and localized asynchronous permutation automata.
Cite as
Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{adsul_et_al:LIPIcs.CONCUR.2022.28,
author = {Adsul, Bharat and Gastin, Paul and Sarkar, Saptarshi and Weil, Pascal},
title = {{Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {28:1--28:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.28},
URN = {urn:nbn:de:0030-drops-170915},
doi = {10.4230/LIPIcs.CONCUR.2022.28},
annote = {Keywords: Mazurkiewicz traces, propositional dynamic logic, regular trace languages, asynchronous automata, cascade product, Krohn Rhodes theorem}
}
Document
A Kleene Theorem for Higher-Dimensional Automata
Abstract
We prove a Kleene theorem for higher-dimensional automata (HDAs). It states that the languages they recognise are precisely the rational subsumption-closed sets of interval pomsets. The rational operations include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce HDAs with interfaces as presheaves over labelled precube categories and use tools inspired by algebraic topology, such as cylinders and (co)fibrations. HDAs are a general model of non-interleaving concurrency, which subsumes many other models in this field. Interval orders are used as models for concurrent or distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.
Cite as
Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemiański. A Kleene Theorem for Higher-Dimensional Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{fahrenberg_et_al:LIPIcs.CONCUR.2022.29,
author = {Fahrenberg, Uli and Johansen, Christian and Struth, Georg and Ziemia\'{n}ski, Krzysztof},
title = {{A Kleene Theorem for Higher-Dimensional Automata}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {29:1--29:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.29},
URN = {urn:nbn:de:0030-drops-170925},
doi = {10.4230/LIPIcs.CONCUR.2022.29},
annote = {Keywords: higher-dimensional automata, interval posets, Kleene theorem, concurrency theory, labelled precube categories}
}
Document
Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus
Abstract
We introduce a non-interleaving structural operational semantics for the applied π-calculus and prove that it satisfies the properties expected of a labelled asynchronous transition system (LATS). LATS have well-studied relations with other standard non-interleaving models, such as Mazurkiewicz traces or event structures, and are a natural extension of labelled transition systems where the independence of transitions is made explicit. We build on a considerable body of literature on located semantics for process algebras and adopt a static view on locations to identify the parallel processes that perform a transition. By lifting, in this way, work on CCS and π-calculus to the applied π-calculus, we lay down a principled foundation for reusing verification techniques such as partial-order reduction and non-interleaving equivalences in the field of security. The key technical device we develop is the notion of located aliases to refer unambiguously to a specific output originating from a specific process. This light mechanism ensures stability, avoiding disjunctive causality problems that parallel extrusion incurs in similar non-interleaving semantics for the π-calculus.
Cite as
Clément Aubert, Ross Horne, and Christian Johansen. Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{aubert_et_al:LIPIcs.CONCUR.2022.30,
author = {Aubert, Cl\'{e}ment and Horne, Ross and Johansen, Christian},
title = {{Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {30:1--30:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.30},
URN = {urn:nbn:de:0030-drops-170930},
doi = {10.4230/LIPIcs.CONCUR.2022.30},
annote = {Keywords: Security, Processes, Structural operational semantics, Asynchronous transition systems, Applied pi-calculus}
}
Document
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement
Abstract
Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with only finite traces. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a (weak) progress condition, and prove that this weak progressive forward simulation is equivalent to strong observational refinement.
Cite as
Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dongol_et_al:LIPIcs.CONCUR.2022.31,
author = {Dongol, Brijesh and Schellhorn, Gerhard and Wehrheim, Heike},
title = {{Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {31:1--31:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.31},
URN = {urn:nbn:de:0030-drops-170947},
doi = {10.4230/LIPIcs.CONCUR.2022.31},
annote = {Keywords: Strong Observational Refinement, Hyperproperties, Forward Simulation, Weak Progressiveness}
}
Document
Strategies for MDP Bisimilarity Equivalence and Inequivalence
Abstract
A labelled Markov decision process (MDP) is a labelled Markov chain with nondeterminism; i.e., together with a strategy a labelled MDP induces a labelled Markov chain. Motivated by applications to the verification of probabilistic noninterference in security, we study problems whether there exist strategies such that the labelled MDPs become bisimilarity equivalent/inequivalent. We show that the equivalence problem is decidable; in fact, it is EXPTIME-complete and becomes NP-complete if one of the MDPs is a Markov chain. Concerning the inequivalence problem, we show that (1) it is decidable in polynomial time; (2) if there are strategies for inequivalence then there are memoryless strategies for inequivalence; (3) such memoryless strategies can be computed in polynomial time.
Cite as
Stefan Kiefer and Qiyi Tang. Strategies for MDP Bisimilarity Equivalence and Inequivalence. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2022.32,
author = {Kiefer, Stefan and Tang, Qiyi},
title = {{Strategies for MDP Bisimilarity Equivalence and Inequivalence}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {32:1--32:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.32},
URN = {urn:nbn:de:0030-drops-170955},
doi = {10.4230/LIPIcs.CONCUR.2022.32},
annote = {Keywords: Markov decision processes, Markov chains}
}
Document
Pareto-Rational Verification
Abstract
We study the rational verification problem which consists in verifying the correctness of a system executing in an environment that is assumed to behave rationally. We consider the model of rationality in which the environment only executes behaviors that are Pareto-optimal with regard to its set of objectives, given the behavior of the system (which is committed in advance of any interaction). We examine two ways of specifying this behavior, first by means of a deterministic Moore machine, and then by lifting its determinism. In the latter case the machine may embed several different behaviors for the system, and the universal rational verification problem aims at verifying that all of them are correct when the environment is rational. For parity objectives, we prove that the Pareto-rational verification problem is co-NP-complete and that its universal version is in PSPACE and both NP-hard and co-NP-hard. For Boolean Büchi objectives, the former problem is Π₂𝖯-complete and the latter is PSPACE-complete. We also study the case where the objectives are expressed using LTL formulas and show that the first problem is PSPACE-complete, and that the second is 2EXPTIME-complete. Both problems are also shown to be fixed-parameter tractable for parity and Boolean Büchi objectives.
Cite as
Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-Rational Verification. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2022.33,
author = {Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Tamines, Cl\'{e}ment},
title = {{Pareto-Rational Verification}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {33:1--33:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.33},
URN = {urn:nbn:de:0030-drops-170968},
doi = {10.4230/LIPIcs.CONCUR.2022.33},
annote = {Keywords: Rational verification, Model-checking, Pareto-optimality, \omega-regular objectives}
}
Document
Concurrent Games with Multiple Topologies
Abstract
Concurrent multi-player games with ω-regular objectives are a standard model for systems that consist of several interacting components, each with its own objective. The standard solution concept for such games is Nash Equilibrium, which is a "stable" strategy profile for the players.
In many settings, the system is not fully observable by the interacting components, e.g., due to internal variables. Then, the interaction is modelled by a partial information game. Unfortunately, the problem of whether a partial information game has an NE is not known to be decidable. A particular setting of partial information arises naturally when processes are assigned IDs by the system, but these IDs are not known to the processes. Then, the processes have full information about the state of the system, but are uncertain of the effect of their actions on the transitions.
We generalize the setting above and introduce Multi-Topology Games (MTGs) - concurrent games with several possible topologies, where the players do not know which topology is actually used. We show that extending the concept of NE to these games can take several forms. To this end, we propose two notions of NE: Conservative NE, in which a player deviates if she can strictly add topologies to her winning set, and Greedy NE, where she deviates if she can win in a previously-losing topology. We study the properties of these NE, and show that the problem of whether a game admits them is decidable.
Cite as
Shaull Almagor and Shai Guendelman. Concurrent Games with Multiple Topologies. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CONCUR.2022.34,
author = {Almagor, Shaull and Guendelman, Shai},
title = {{Concurrent Games with Multiple Topologies}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {34:1--34:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.34},
URN = {urn:nbn:de:0030-drops-170973},
doi = {10.4230/LIPIcs.CONCUR.2022.34},
annote = {Keywords: Concurrent games, Nash Equilibrium, Symmetry, Partial information}
}
Document
Generalised Multiparty Session Types with Crash-Stop Failures
Abstract
Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily.
Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures.
Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all crash scenarios can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checking, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness, even in presence of crashes. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature.
Cite as
Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised Multiparty Session Types with Crash-Stop Failures. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 35:1-35:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{barwell_et_al:LIPIcs.CONCUR.2022.35,
author = {Barwell, Adam D. and Scalas, Alceste and Yoshida, Nobuko and Zhou, Fangyi},
title = {{Generalised Multiparty Session Types with Crash-Stop Failures}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {35:1--35:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.35},
URN = {urn:nbn:de:0030-drops-170982},
doi = {10.4230/LIPIcs.CONCUR.2022.35},
annote = {Keywords: Session Types, Concurrency, Failure Handling, Model Checking}
}
Document
An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus
Abstract
Fair termination is the property of programs that may diverge "in principle" but that terminate "in practice", i.e. under suitable fairness assumptions concerning the resolution of non-deterministic choices. We study a conservative extension of μMALL^∞, the infinitary proof system of the multiplicative additive fragment of linear logic with least and greatest fixed points, such that cut elimination corresponds to fair termination. Proof terms are processes of πLIN, a variant of the linear π-calculus with (co)recursive types into which binary and (some) multiparty sessions can be encoded. As a result we obtain a behavioral type system for πLIN (and indirectly for session calculi through their encoding into πLIN) that ensures fair termination: although well-typed processes may engage in arbitrarily long interactions, they are fairly guaranteed to eventually perform all pending actions.
Cite as
Luca Ciccone and Luca Padovani. An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{ciccone_et_al:LIPIcs.CONCUR.2022.36,
author = {Ciccone, Luca and Padovani, Luca},
title = {{An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear \pi-Calculus}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {36:1--36:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.36},
URN = {urn:nbn:de:0030-drops-170990},
doi = {10.4230/LIPIcs.CONCUR.2022.36},
annote = {Keywords: Linear \pi-calculus, Linear Logic, Fixed Points, Fair Termination}
}
Document
On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments
Abstract
A system of session types is introduced as induced by a Curry Howard correspondence applied to bounded linear logic, suitably extended with probabilistic choice operators and ground types. The resulting system satisfies some expected properties, like subject reduction and progress, but also unexpected ones, like a polynomial bound on the time needed to reduce processes. This makes the system suitable for modelling experiments and proofs from the so-called computational model of cryptography.
Cite as
Ugo Dal Lago and Giulia Giusti. On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dallago_et_al:LIPIcs.CONCUR.2022.37,
author = {Dal Lago, Ugo and Giusti, Giulia},
title = {{On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments}},
booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)},
pages = {37:1--37:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-246-4},
ISSN = {1868-8969},
year = {2022},
volume = {243},
editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.37},
URN = {urn:nbn:de:0030-drops-171000},
doi = {10.4230/LIPIcs.CONCUR.2022.37},
annote = {Keywords: Session Types, Probabilistic Computation, Bounded Linear Logic, Cryptographic Experiments}
}