Volume
LIPIcs, Volume 348
36th International Conference on Concurrency Theory (CONCUR 2025)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Event
CONCUR 2025, August 26-29, 2025, Aarhus, DenmarkEditors
Publication Details
- published at: 2025-08-18
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-389-8
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 348, CONCUR 2025, Complete Volume
Abstract
LIPIcs, Volume 348, CONCUR 2025, Complete Volume
Cite as
36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 1-774, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Proceedings{bouyer_et_al:LIPIcs.CONCUR.2025,
title = {{LIPIcs, Volume 348, CONCUR 2025, Complete Volume}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {1--774},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025},
URN = {urn:nbn:de:0030-drops-244431},
doi = {10.4230/LIPIcs.CONCUR.2025},
annote = {Keywords: LIPIcs, Volume 348, CONCUR 2025, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2025.0,
author = {Bouyer, Patricia and van de Pol, Jaco},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {0:i--0:xii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.0},
URN = {urn:nbn:de:0030-drops-244386},
doi = {10.4230/LIPIcs.CONCUR.2025.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Linear Temporal Logic with Standpoint Modalities (Invited Talk)
Abstract
Standpoint logics have been introduced in recent work by Alvarez et al. as a multi-modal logic to reason about the integrated knowledge of multiple agents that might have different, possibly contradicting views ("standpoints"). The essential new feature are modalities for expressing that a property is conceivable according to the view of an agent. The talk considers the model checking problem for a standpoint extension of classical linear temporal logic (LTL) with five semantics for the standpoint modalities. The semantics differ in the information an agent can extract from the history. Starting with a generic non-elementary model checking algorithm that is applicable to all five semantics, a more detailed complexity analysis leads to improved upper bounds for four of the semantics. In three cases, the model checking problem turns out to be PSPACE-complete, i.e., not harder than the model checking problem for classical LTL, which stands in contrast to the known EXPSPACE-completeness result for the satisfiability problem for standpoint LTL.
Cite as
Christel Baier. Linear Temporal Logic with Standpoint Modalities (Invited Talk). In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{baier:LIPIcs.CONCUR.2025.1,
author = {Baier, Christel},
title = {{Linear Temporal Logic with Standpoint Modalities}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.1},
URN = {urn:nbn:de:0030-drops-239513},
doi = {10.4230/LIPIcs.CONCUR.2025.1},
annote = {Keywords: Linear Temporal Logic, LTL, standpoint logics, multi-modal logic, model checking}
}
Document
Invited Talk
Towards Categorical Quantum Concurrency Theory (Invited Talk)
Abstract
Quantum computing inherently has concurrent aspects. Even with only local operations, qubits can influence each other. This ability leads to genuinely new quantum communication protocols, but also raises even thornier questions of causality than in classical concurrent computing. Monoidal categories and their string diagrams form a convenient and popular language for quantum computing. After an introduction to quantum concurrency, I will discuss the framework of tensor topology, which aims to analyse the interaction of several agents in monoidal categories, using notions from sheaf theory and ordered locales.
Cite as
Chris Heunen. Towards Categorical Quantum Concurrency Theory (Invited Talk). In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{heunen:LIPIcs.CONCUR.2025.2,
author = {Heunen, Chris},
title = {{Towards Categorical Quantum Concurrency Theory}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.2},
URN = {urn:nbn:de:0030-drops-239527},
doi = {10.4230/LIPIcs.CONCUR.2025.2},
annote = {Keywords: Quantum computing, causality, monoidal categories, tensor topology}
}
Document
Invited Talk
On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk)
Abstract
Dependency graphs have emerged as a versatile and powerful formalism with wide-ranging applications in formal verification. In this extended abstract, we provide an overview of selected advancements in on-the-fly verification techniques based on dependency graphs, focusing on the recent developments, optimizations and generalizations of this generic verification framework.
Cite as
Jiří Srba. On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk). In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{srba:LIPIcs.CONCUR.2025.3,
author = {Srba, Ji\v{r}{\'\i}},
title = {{On-The-Fly Verification: Advancements in Dependency Graphs}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {3:1--3:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.3},
URN = {urn:nbn:de:0030-drops-239534},
doi = {10.4230/LIPIcs.CONCUR.2025.3},
annote = {Keywords: dependency graphs, Boolean equation systems, on-the-fly algorithms, fixed-point computation, applications}
}
Document
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory
Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as
Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
author = {Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
title = {{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {4:1--4:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4},
URN = {urn:nbn:de:0030-drops-239546},
doi = {10.4230/LIPIcs.CONCUR.2025.4},
annote = {Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces
Abstract
We study fragments of temporal logics over Mazurkiewicz traces which are well known and established partial-order models of concurrent behaviours. We focus on concurrent versions of "strict past" and "strict future" modalities. Over words, the corresponding fragments have been shown to coincide with natural algebraic conditions on the recognizing monoids. We provide non-trivial generalizations of these classical results to traces. We exploit the local nature of the temporal modalities and obtain modular translations of specifications into asynchronous automata. More specifically, we provide novel characterizations of these fragments via local cascade products of a very simple two-state asynchronous automaton operating on a single process.
Cite as
Bharat Adsul, Paul Gastin, and Shantanu Kulkarni. Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{adsul_et_al:LIPIcs.CONCUR.2025.5,
author = {Adsul, Bharat and Gastin, Paul and Kulkarni, Shantanu},
title = {{Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {5:1--5:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.5},
URN = {urn:nbn:de:0030-drops-239551},
doi = {10.4230/LIPIcs.CONCUR.2025.5},
annote = {Keywords: Mazurkiewicz traces, temporal logics, asynchronous automata, cascade product, Green’s relations, algebraic automata theory}
}
Document
Omega-Regular Verification and Control for Distributional Specifications in MDPs
Abstract
A classical approach to studying Markov decision processes (MDPs) is to view them as state transformers. However, MDPs can also be viewed as distribution transformers, where an MDP under a strategy generates a sequence of probability distributions over MDP states. This view arises in several applications, even as the probabilistic model checking problem becomes much harder compared to the classical state transformer counterpart. It is known that even distributional reachability and safety problems become computationally intractable (Skolem- and positivity-hard). To address this challenge, recent works focused on sound but possibly incomplete methods for verification and control of MDPs under the distributional view. However, existing automated methods are applicable only to distributional reachability, safety and reach-avoidance specifications.
In this work, we present the first automated method for verification and control of MDPs with respect to distributional omega-regular specifications. To achieve this, we propose a novel notion of distributional certificates, which are sound and complete proof rules for proving that an MDP under a distributionally memoryless strategy satisfies some distributional omega-regular specification. We then use our distributional certificates to design the first fully automated algorithms for verification and control of MDPs with respect to distributional omega-regular specifications. Our algorithms follow a template-based synthesis approach and provide soundness and relative completeness guarantees, while running in PSPACE. Our prototype implementation demonstrates practical applicability of our algorithms to challenging examples collected from the literature.
Cite as
S. Akshay, Ouldouz Neysari, and Ðorđe Žikelić. Omega-Regular Verification and Control for Distributional Specifications in MDPs. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{akshay_et_al:LIPIcs.CONCUR.2025.6,
author = {Akshay, S. and Neysari, Ouldouz and \v{Z}ikeli\'{c}, Ðor{\d}e},
title = {{Omega-Regular Verification and Control for Distributional Specifications in MDPs}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {6:1--6:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.6},
URN = {urn:nbn:de:0030-drops-239562},
doi = {10.4230/LIPIcs.CONCUR.2025.6},
annote = {Keywords: MDPs, Distributional objectives, \omega-regularity, Certificates}
}
Document
Temporal Explorability Games
Abstract
Temporal graphs extend ordinary graphs with discrete time that affects the availability of edges. We consider solving games played on temporal graphs where one player aims to explore the graph, i.e., visit all vertices. The complexity depends majorly on two factors: the presence of an adversary and how edge availability is specified.
We demonstrate that on static graphs, where edges are always available, solving explorability games is just as hard as solving reachability games. In contrast, on temporal graphs, the complexity of explorability coincides with generalized reachability (NP-complete for one-player and PSPACE-complete for two player games). We show that if temporal graphs are given symbolically, even one-player reachability (and thus explorability and generalized reachability) games are PSPACE-hard. For one player, all these are also solvable in PSPACE and for two players, they are in PSPACE, EXP and EXP, respectively.
Cite as
Pete Austin, Sougata Bose, Nicolas Mazzocchi, and Patrick Totzke. Temporal Explorability Games. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{austin_et_al:LIPIcs.CONCUR.2025.7,
author = {Austin, Pete and Bose, Sougata and Mazzocchi, Nicolas and Totzke, Patrick},
title = {{Temporal Explorability Games}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {7:1--7:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.7},
URN = {urn:nbn:de:0030-drops-239575},
doi = {10.4230/LIPIcs.CONCUR.2025.7},
annote = {Keywords: Temporal Graphs, Explorability, Reachability, Games}
}
Document
Model Checking as Program Verification by Abstract Interpretation
Abstract
Abstract interpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions based on (bi)simulation and property-preserving state relations have been successfully applied to abstract model checking. Here, we pursue a different track in which model checking is seen as an instance of program verification. To this purpose, we introduce a suitable language - called MOKA (for MOdel checking as abstract interpretation of 𝖪leene 𝖠lgebras) - which is used to encode temporal formulae as programs. In particular, we show that (universal fragments of) temporal logics, such as ACTL or, more generally, universal μ-calculus can be transformed into MOKA programs. Such programs return all and only the initial states which violate the formula. By applying abstract interpretation to MOKA programs, we pave the way for reusing more general abstractions than partitions as well as for tuning the precision of the abstraction to remove or avoid false alarms. We show how to perform model checking via a program logic that combines under-approximation and abstract interpretation analysis to avoid false alarms. The notion of locally complete abstraction is used to dynamically improve the analysis precision via counterexample-guided domain refinement.
Cite as
Paolo Baldan, Roberto Bruni, Francesco Ranzato, and Diletta Rigo. Model Checking as Program Verification by Abstract Interpretation. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{baldan_et_al:LIPIcs.CONCUR.2025.8,
author = {Baldan, Paolo and Bruni, Roberto and Ranzato, Francesco and Rigo, Diletta},
title = {{Model Checking as Program Verification by Abstract Interpretation}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {8:1--8:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.8},
URN = {urn:nbn:de:0030-drops-239583},
doi = {10.4230/LIPIcs.CONCUR.2025.8},
annote = {Keywords: ACTL, \mu-calculus, model checking, abstract interpretation, program analysis, local completeness, abstract interpretation repair, domain refinement, Kleene algebra with tests}
}
Document
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
Abstract
Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from stochastic parity games (SPGs) to SSGs have been presented in the literature through the use of multiple intermediate game models, a direct and simple reduction has been notably absent. This paper introduces a novel and direct polynomial-time reduction from quantitative SPGs to quantitative SSGs. By leveraging a gadget-based transformation that effectively removes the priority function, we construct an SSG that simulates the behavior of a given SPG. We formally establish the correctness of our direct reduction. Furthermore, we demonstrate that under binary encoding this reduction is polynomial, thereby directly corroborating the known NP ∩ coNP complexity of SPGs and providing new understanding in the relationship between parity and reachability objectives in turn-based stochastic games.
Cite as
Raphaël Berthon, Joost-Pieter Katoen, and Zihan Zhou. A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{berthon_et_al:LIPIcs.CONCUR.2025.9,
author = {Berthon, Rapha\"{e}l and Katoen, Joost-Pieter and Zhou, Zihan},
title = {{A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {9:1--9:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.9},
URN = {urn:nbn:de:0030-drops-239595},
doi = {10.4230/LIPIcs.CONCUR.2025.9},
annote = {Keywords: stochastic games, parity, reduction}
}
Document
Abstract Subtyping for Asynchronous Multiparty Sessions
Abstract
Session subtyping answers the question of whether a program in a communicating system can be safely substituted for another, when their communication behaviour is described by session types. Asynchronous session subtyping is undecidable, even for two participants, hence the interest in sound, but incomplete, subtyping algorithms. Asynchronous multiparty subtyping can be formulated by decomposing session types into single input and output types which preclude, respectively, external and internal choice. This paper shows how abstract interpretation can sit atop this approach and how it leads to an algorithm that can prove subtyping for intricate communication patterns.
Cite as
Laura Bocchi, Andy King, Maurizio Murgia, and Simon Thompson. Abstract Subtyping for Asynchronous Multiparty Sessions. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bocchi_et_al:LIPIcs.CONCUR.2025.10,
author = {Bocchi, Laura and King, Andy and Murgia, Maurizio and Thompson, Simon},
title = {{Abstract Subtyping for Asynchronous Multiparty Sessions}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.10},
URN = {urn:nbn:de:0030-drops-239605},
doi = {10.4230/LIPIcs.CONCUR.2025.10},
annote = {Keywords: asynchrony, session subtyping, automata, abstract interpretation}
}
Document
A Sound and Complete Characterization of Fair Asynchronous Session Subtyping
Abstract
Session types are abstractions of communication protocols enabling the static analysis of message-passing processes. Refinement notions for session types are key to support safe forms of process substitution while preserving their compatibility with the rest of the system. Recently, a fair refinement relation for asynchronous session types has been defined allowing the anticipation of message outputs with respect to an unbounded number of message inputs. This refinement is useful to capture common patterns in communication protocols that take advantage of asynchrony. However, while the semantic (à la testing) definition of such refinement is straightforward, its characterization has proved to be quite challenging. In fact, only a sound but not complete characterization is known so far. In this paper we close this open problem by presenting a sound and complete characterization of asynchronous fair refinement for session types. We relate this characterization to those given in the literature for synchronous session types by leveraging a novel labelled transition system of session types that embeds their asynchronous semantics.
Cite as
Mario Bravetti, Luca Padovani, and Gianluigi Zavattaro. A Sound and Complete Characterization of Fair Asynchronous Session Subtyping. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bravetti_et_al:LIPIcs.CONCUR.2025.11,
author = {Bravetti, Mario and Padovani, Luca and Zavattaro, Gianluigi},
title = {{A Sound and Complete Characterization of Fair Asynchronous Session Subtyping}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {11:1--11:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.11},
URN = {urn:nbn:de:0030-drops-239615},
doi = {10.4230/LIPIcs.CONCUR.2025.11},
annote = {Keywords: Binary sessions, session types, fair asynchronous subtyping}
}
Document
The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives
Abstract
This paper studies the rational synthesis problem for multi-player games played on graphs when rational players are following subgame perfect equilibria. In these games, one player, the system, declares his strategy upfront, and the other players, composing the environment, then rationally respond by playing strategies forming a subgame perfect equilibrium. We study the complexity of the rational synthesis problem when the players have ω-regular objectives encoded as parity objectives. Our algorithm is based on an encoding into a three-player game with imperfect information, showing that the problem is in 2ExpTime. When the number of environment players is fixed, the problem is in ExpTime and is NP- and coNP-hard. Moreover, for a fixed number of players and reachability objectives, we get a polynomial algorithm.
Cite as
Véronique Bruyère, Jean-François Raskin, Alexis Reynouard, and Marie Van Den Bogaard. The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2025.12,
author = {Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Reynouard, Alexis and Van Den Bogaard, Marie},
title = {{The Non-Cooperative Rational Synthesis Problem for SPEs and \omega-Regular Objectives}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {12:1--12:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.12},
URN = {urn:nbn:de:0030-drops-239622},
doi = {10.4230/LIPIcs.CONCUR.2025.12},
annote = {Keywords: non-zero-sum games, subgame perfect equilibria, rational synthesis}
}
Document
Languages of Boundedly-Ambiguous Vector Addition Systems with States
Abstract
The aim of this paper is to deliver broad understanding of a class of languages of boundedly-ambiguous VASSs, that is k-ambiguous VASSs for some natural k. These are languages of Vector Addition Systems with States with the acceptance condition defined by the set of accepting states such that each accepted word has at most k accepting runs. We develop tools for proving that a given language is not accepted by any k-ambiguous VASS. Using them we show a few negative results: lack of some closure properties of languages of k-ambiguous VASSs and undecidability of the k-ambiguity problem, namely the question whether a given VASS language is a language of some k-ambiguous VASS. In fact we show an even more general undecidability result stating that for any class containing all regular languages and only k-ambiguous VASS languages for some k ∈ ℕ it is undecidable whether a language of a given 1-dimensional VASS belongs to this class. Finally, we show that the regularity problem is decidable for k-ambiguous VASSs.
Cite as
Wojciech Czerwiński and Łukasz Orlikowski. Languages of Boundedly-Ambiguous Vector Addition Systems with States. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 13:1-13:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2025.13,
author = {Czerwi\'{n}ski, Wojciech and Orlikowski, {\L}ukasz},
title = {{Languages of Boundedly-Ambiguous Vector Addition Systems with States}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {13:1--13:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.13},
URN = {urn:nbn:de:0030-drops-239635},
doi = {10.4230/LIPIcs.CONCUR.2025.13},
annote = {Keywords: vector addition systems, Petri nets, unambiguity, bounded-ambiguity, languages}
}
Document
Reversible Pebble Transducers
Abstract
Deterministic two-way transducers with pebbles (aka pebble transducers) capture the class of polyregular functions, which extend the string-to-string regular functions allowing polynomial growth instead of linear growth. One of the most fundamental operations on functions is composition, and (poly)regular functions can be realized as a composition of several simpler functions. In general, composition of deterministic two-way transducers incur a doubly exponential blow-up in the size of the inputs. A major improvement in this direction comes from the fundamental result of Dartois et al. [Luc Dartois et al., 2017] showing a polynomial construction for the composition of reversible two-way transducers.
A precise complexity analysis for existing composition techniques of pebble transducers is missing. But they rely on the classic composition of two-way transducers and inherit the double exponential complexity. To overcome this problem, we introduce reversible pebble transducers. Our main results are efficient uniformization techniques for non-deterministic pebble transducers to reversible ones and efficient composition for reversible pebble transducers.
Cite as
Luc Dartois, Paul Gastin, Loïc Germerie Guizouarn, and Shankaranarayanan Krishna. Reversible Pebble Transducers. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dartois_et_al:LIPIcs.CONCUR.2025.14,
author = {Dartois, Luc and Gastin, Paul and Germerie Guizouarn, Lo\"{i}c and Krishna, Shankaranarayanan},
title = {{Reversible Pebble Transducers}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {14:1--14:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.14},
URN = {urn:nbn:de:0030-drops-239645},
doi = {10.4230/LIPIcs.CONCUR.2025.14},
annote = {Keywords: Transducers, Polyregular functions, Reversibility, Composition, Uniformization}
}
Document
On the Send-Synchronizability Problem for Mailbox Communication
Abstract
A system of communicating automata is send-synchronizable if its set of send sequences (i.e., the projection on send actions of its executions) is the same when communications are asynchronous and when they are rendez-vous synchronizations. Send-synchronizability was claimed to be decidable for the mailbox semantics (Basu and Bultan, 2011) and for the peer-to-peer semantics (Basu and Bultan, 2016). Finkel and Lozes showed in 2017 that the proofs of these results are flawed, and they proved that send-synchronizability is in fact undecidable for peer-to-peer systems. The send-synchronizability problem for mailbox systems was left open. A partial solution was recently proposed in (Di Giusto, Laversa and Peters, 2024). In this paper, we revisit the send-synchronizability problem for mailbox systems. Firstly, we show that send-synchronizability is undecidable for mailbox systems, thus closing the question left open in (Finkel and Lozes, 2023) and (Di Giusto, Laversa and Peters, 2024). Secondly, we show that send-synchronizability is decidable for the class of 1-schedulable mailbox systems. A system is 1-schedulable if every execution can be re-scheduled into an equivalent execution where each send is either immediately followed by its matching receive, or is never matched. Despite the apparent similarity between send-synchronizability and 1-schedulability, the proof that send-synchronizability is decidable for 1-schedulable mailbox systems is quite involved. We believe that the techniques that we develop in this proof could be used to address other problems on mailbox systems, such as the realizability problem.
Cite as
Romain Delpy, Anca Muscholl, and Grégoire Sutre. On the Send-Synchronizability Problem for Mailbox Communication. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{delpy_et_al:LIPIcs.CONCUR.2025.15,
author = {Delpy, Romain and Muscholl, Anca and Sutre, Gr\'{e}goire},
title = {{On the Send-Synchronizability Problem for Mailbox Communication}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {15:1--15:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.15},
URN = {urn:nbn:de:0030-drops-239659},
doi = {10.4230/LIPIcs.CONCUR.2025.15},
annote = {Keywords: Concurrent programming, Mailbox communication, Verification, Synchronizability}
}
Document
Expectation in Stochastic Games with Prefix-Independent Objectives
Abstract
Stochastic two-player games model systems with an environment that is both adversarial and stochastic. In this paper, we study the expected value of bounded quantitative prefix-independent objectives in the context of stochastic games. We show a generic reduction from the expectation problem to linearly many instances of the almost-sure satisfaction problem for threshold Boolean objectives. The result follows from partitioning the vertices of the game into so-called value classes where each class consists of vertices of the same value. Our procedure further entails that the memory required by both players to play optimally for the expectation problem is no more than the memory required by the players to play optimally for the almost-sure satisfaction problem for a corresponding threshold Boolean objective.
We show the applicability of the framework to compute the expected window mean-payoff measure in stochastic games. The window mean-payoff measure strengthens the classical mean-payoff measure by computing the mean payoff over windows of bounded length that slide along an infinite path. We show that the decision problem to check if the expected window mean-payoff value is at least a given threshold is in UP ∩ coUP when the window length is given in unary.
Cite as
Laurent Doyen, Pranshu Gaba, and Shibashis Guha. Expectation in Stochastic Games with Prefix-Independent Objectives. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{doyen_et_al:LIPIcs.CONCUR.2025.16,
author = {Doyen, Laurent and Gaba, Pranshu and Guha, Shibashis},
title = {{Expectation in Stochastic Games with Prefix-Independent Objectives}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {16:1--16:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.16},
URN = {urn:nbn:de:0030-drops-239668},
doi = {10.4230/LIPIcs.CONCUR.2025.16},
annote = {Keywords: Stochastic games, finitary objectives, mean payoff, reactive synthesis}
}
Document
Just Verification of Mutual Exclusion Algorithms
Abstract
We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where those registers can be atomic or non-atomic. For the verification of liveness properties, it is necessary to assume a completeness criterion to eliminate spurious counterexamples. We use justness as completeness criterion. Justness depends on a concurrency relation; we consider several such relations, modelling different assumptions on the working of the shared registers. We present executions demonstrating the violation of correctness properties by several algorithms, and in some cases suggest improvements.
Cite as
Rob van Glabbeek, Bas Luttik, and Myrthe S. C. Spronck. Just Verification of Mutual Exclusion Algorithms. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 17:1-17:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{vanglabbeek_et_al:LIPIcs.CONCUR.2025.17,
author = {van Glabbeek, Rob and Luttik, Bas and Spronck, Myrthe S. C.},
title = {{Just Verification of Mutual Exclusion Algorithms}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {17:1--17:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.17},
URN = {urn:nbn:de:0030-drops-239670},
doi = {10.4230/LIPIcs.CONCUR.2025.17},
annote = {Keywords: Mutual exclusion, safe registers, regular registers, overlapping reads and writes, atomicity, safety, liveness, starvation freedom, justness, model checking, mCRL2}
}
Document
A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity
Abstract
We present a new O(mlog n) algorithm to calculate branching bisimulation equivalence, which is the finest commonly used behavioural equivalence on labelled transition systems that takes the internal action τ into account. This algorithm combines the simpler data structure of an earlier algorithm for Kripke structures (without action labels) with the memory-efficiency of a later algorithm partitioning sets of labelled transitions. It employs a particularly elegant four-way split of blocks of states, which refines a block under two splitters and isolates all new bottom states, simultaneously. Benchmark results show that this new algorithm outperforms the best known algorithm for branching bisimulation both in time and space.
Cite as
Jan Friso Groote and David N. Jansen. A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{groote_et_al:LIPIcs.CONCUR.2025.18,
author = {Groote, Jan Friso and Jansen, David N.},
title = {{A State-Based O(m log n) Partitioning Algorithm for Branching Bisimilarity}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {18:1--18:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.18},
URN = {urn:nbn:de:0030-drops-239688},
doi = {10.4230/LIPIcs.CONCUR.2025.18},
annote = {Keywords: Algorithm, Branching bisimulation, Partition refinement of states}
}
Document
Time for Timed Monitorability
Abstract
Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time.
Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata.
Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.
Cite as
Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann. Time for Timed Monitorability. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{grosen_et_al:LIPIcs.CONCUR.2025.19,
author = {Grosen, Thomas M. and Kauffman, Sean and Larsen, Kim G. and Zimmermann, Martin},
title = {{Time for Timed Monitorability}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {19:1--19:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.19},
URN = {urn:nbn:de:0030-drops-239690},
doi = {10.4230/LIPIcs.CONCUR.2025.19},
annote = {Keywords: Monitorability, Monitoring, Timed Automata, MITL}
}
Document
Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement
Abstract
Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches for concurrent systems have recently emerged. We take a significant step beyond available results, including those by the authors, and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. Our approach automatically refines the global alphabet into component alphabets while learning the component models. We develop a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets. We characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. We present a compositional learning algorithm implementing these ideas, where learning counterexamples precisely correspond to distribution counterexamples under well-defined conditions. We provide an implementation, called CoalA, using the state-of-the-art active learning library LearnLib. Our experiments show that in more than 630 subject systems, CoalA delivers orders of magnitude improvements (up to five orders) in membership queries and in systems with significant concurrency, it also achieves better scalability in the number of equivalence queries.
Cite as
Léo Henry, Mohammad Reza Mousavi, Thomas Neele, and Matteo Sammartino. Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{henry_et_al:LIPIcs.CONCUR.2025.20,
author = {Henry, L\'{e}o and Mousavi, Mohammad Reza and Neele, Thomas and Sammartino, Matteo},
title = {{Compositional Active Learning of Synchronizing Systems Through Automated Alphabet Refinement}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {20:1--20:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.20},
URN = {urn:nbn:de:0030-drops-239700},
doi = {10.4230/LIPIcs.CONCUR.2025.20},
annote = {Keywords: Active learning, Compositional methods, Concurrency theory, Labelled transition systems, Formal methods}
}
Document
Quantitative Language Automata
Abstract
A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA 𝒜 obtains a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained by nondeterministic runs of 𝒜 over w. We introduce quantitative language automata (QLAs) that define functions from language generators (i.e., implementations) to values, where a language generator can be nonprobabilistic, defining a set of infinite words, or probabilistic, defining a probability measure over infinite words. A QLA consists of a QWA and an aggregator function. For example, given a QWA 𝒜, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest lower bound assigned by 𝒜 to any word in L. For boolean value sets, QWAs define boolean properties of traces, and QLAs define boolean properties of sets of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a specification language for a generalization of hyperproperties, called quantitative hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty assigns a value to each set (resp. distribution) G of traces, e.g., the minimal (resp. expected) average response time exhibited by the traces in G. We give several examples of quantitative hyperproperties and investigate three paradigmatic problems for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem, given a QLA 𝔸 and an implementation G, we ask for the value that 𝔸 assigns to G. In the nonemptiness (resp. universality) problem, given a QLA 𝔸 and a value k, we ask whether 𝔸 assigns at least k to some (resp. every) language. We provide a comprehensive picture of decidability for these problems for QLAs with common aggregators as well as their restrictions to ω-regular languages and trace distributions generated by finite-state Markov chains.
Cite as
Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç. Quantitative Language Automata. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2025.21,
author = {Henzinger, Thomas A. and Kebis, Pavol and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
title = {{Quantitative Language Automata}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {21:1--21:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.21},
URN = {urn:nbn:de:0030-drops-239718},
doi = {10.4230/LIPIcs.CONCUR.2025.21},
annote = {Keywords: Quantitative hyperproperties, quantitative automata, automata-based verification}
}
Document
Partial-Order Reduction Is Hard
Abstract
The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach builds a transition system with representative runs, while the stateless method simply enumerates them. The stateless approach may be preferable if the transition system is tree-like; otherwise, the stateful method is more effective.
In the last decade, optimality has been a guiding principle for developing stateless partial-order reduction algorithms, and without doubt contributed to big progress in the field. In this paper we ask if we can get a similar principle for the stateful approach. We show that in stateful exploration, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. The result holds even for acyclic programs with just await instructions. This lower bound result justifies systematic study of heuristics for stateful partial-order reduction. We propose a notion of IFS oracle as a useful abstraction. The oracle can be used to get a very simple optimal stateless algorithm, which can then be adapted to a non-optimal stateful algorithm. While in general the oracle problem is NP-hard, we show a simple case where it can be solved in linear time.
Cite as
Frédéric Herbreteau, Sarah Larroze-Jardiné, and Igor Walukiewicz. Partial-Order Reduction Is Hard. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{herbreteau_et_al:LIPIcs.CONCUR.2025.22,
author = {Herbreteau, Fr\'{e}d\'{e}ric and Larroze-Jardin\'{e}, Sarah and Walukiewicz, Igor},
title = {{Partial-Order Reduction Is Hard}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {22:1--22:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.22},
URN = {urn:nbn:de:0030-drops-239727},
doi = {10.4230/LIPIcs.CONCUR.2025.22},
annote = {Keywords: Formal verification, Concurrent systems, Partial-order reduction, Complexity}
}
Document
First-Order Store and Visibility in Name-Passing Calculi
Abstract
The π-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store.
We study how π-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. We discuss the impact of visibility on the behavioural theory. We propose characterisations of may-testing and barbed equivalence, based on (variants of) trace equivalence and labelled bisimilarity, in the case where computation is sequential, and in the case where computation is well-bracketed.
Cite as
Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi. First-Order Store and Visibility in Name-Passing Calculi. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{hirschkoff_et_al:LIPIcs.CONCUR.2025.23,
author = {Hirschkoff, Daniel and Qu\'{e}merais, Iwan and Sangiorgi, Davide},
title = {{First-Order Store and Visibility in Name-Passing Calculi}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {23:1--23:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.23},
URN = {urn:nbn:de:0030-drops-239737},
doi = {10.4230/LIPIcs.CONCUR.2025.23},
annote = {Keywords: process calculi, behavioural equivalence, type system}
}
Document
Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics.
Abstract
We demonstrate a surprising and first-of-its-kind expressive equivalence between decidable metric and freeze logics over timed words in pointwise semantics. Our main result states that Metric Interval Temporal Logic with future, past and Pnueli modalities, MITPPL, and full unilateral timed propositional temporal logic with both future and past temporal modalities, UPTL, have identical expressiveness. One of the highlights of this paper, which allows for this equivalence, is to prove that UPTL formulas admit monadic decomposition. Our result also implies that several decidable logics for real-time specifications, such as one-variable UPTL, unilateral MITPPL, and Q2MLO, are all expressively equivalent, and the reductions between them are effective. Hence, our result unifies the fragmented expressiveness boundary of timed temporal logics. As corollaries, we resolve the open question of the decidability for full UPTL, and the variable or clock hierarchy problem for the future fragment of UPTL.
Cite as
Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Paritosh Pandya. Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics.. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ho_et_al:LIPIcs.CONCUR.2025.24,
author = {Ho, Hsi-Ming and Krishna, Shankara Narayanan and Madnani, Khushraj and Majumdar, Rupak and Pandya, Paritosh},
title = {{Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics.}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {24:1--24:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.24},
URN = {urn:nbn:de:0030-drops-239744},
doi = {10.4230/LIPIcs.CONCUR.2025.24},
annote = {Keywords: Timed Propositional Temporal Logic, Expressiveness, Metric Interval Temporal Logic, Satisfiability, Decidability}
}
Document
On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions
Abstract
Verification of real-time systems with multiple components controlled by multiple parties is a challenging task due to its computational complexity. We present an on-the-fly algorithm for verifying timed alternating-time temporal logic (TATL), a branching-time logic with quantifiers over outcomes that results from coalitions of players in such systems. We combine existing work on games and timed CTL verification in the abstract dependency graph (ADG) framework, which allows for easy creation of on-the-fly algorithms that only explore the state space as needed. In addition, we generalize the conventional inclusion check to the ADG framework which enables dynamic reductions of the dependency graph. Using the insights from the generalization, we present a novel abstraction that eliminates the need for inclusion checking altogether in our domain. We implement our algorithms in Uppaal and our experiments show that while inclusion checking considerably enhances performance, our abstraction provides even more significant improvements, almost two orders of magnitude faster than the naive method. In addition, we outperform Uppaal Tiga, which can verify only a strict subset of TATL. After implementing our new abstraction in Uppaal Tiga, we also improve its performance by almost an order of magnitude.
Cite as
Nicolaj Ø. Jensen, Kim G. Larsen, Didier Lime, and Jiří Srba. On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jensen_et_al:LIPIcs.CONCUR.2025.25,
author = {Jensen, Nicolaj {\O}. and Larsen, Kim G. and Lime, Didier and Srba, Ji\v{r}{\'\i}},
title = {{On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {25:1--25:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.25},
URN = {urn:nbn:de:0030-drops-239756},
doi = {10.4230/LIPIcs.CONCUR.2025.25},
annote = {Keywords: Timed ATL, Symbolic Algorithms, Dependency Graphs, Timed Games}
}
Document
Optimal Concolic Dynamic Partial Order Reduction
Abstract
Stateless model checking (SMC) software implementations requires exploring both concurrency- and data nondeterminism. Unfortunately, most SMC algorithms focus on efficient exploration of concurrency nondeterminism, thereby neglecting an important source of bugs.
We present ConDpor, an SMC algorithm for unmodified Java programs that combines optimal dynamic partial order reduction (DPOR) for concurrency nondeterminism, with concolic execution for data nondeterminism. ConDpor is sound, complete, optimal, and parametric w.r.t. the memory consistency model. Our experiments confirm that ConDpor is exponentially faster than DPOR with small-domain enumeration. Overall, ConDpor opens the door for efficient exploration of concurrent programs with data nondeterminism.
Cite as
Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra. Optimal Concolic Dynamic Partial Order Reduction. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{khoshechinjorshari_et_al:LIPIcs.CONCUR.2025.26,
author = {Khoshechin Jorshari, Mohammad Hossein and Kokologiannakis, Michalis and Majumdar, Rupak and Nagendra, Srinidhi},
title = {{Optimal Concolic Dynamic Partial Order Reduction}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {26:1--26:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.26},
URN = {urn:nbn:de:0030-drops-239765},
doi = {10.4230/LIPIcs.CONCUR.2025.26},
annote = {Keywords: Stateless model checking, dynamic symbolic execution}
}
Document
Coverage Games
Abstract
We introduce and study coverage games - a novel framework for multi-agent planning in settings in which a system operates several agents but do not have full control on them, or interacts with an environment that consists of several agents.
The game is played between a coverer, who has a set of objectives, and a disruptor. The coverer operates several agents that interact with the adversarial disruptor. The coverer wins if every objective is satisfied by at least one agent. Otherwise, the disruptor wins.
Coverage games thus extend traditional two-player games with multiple objectives by allowing a (possibly dynamic) decomposition of the objectives among the different agents. They have many applications, both in settings where the system is the coverer (e.g., multi-robot surveillance, coverage in multi-threaded systems) and settings where it is the disruptor (e.g., prevention of resource exhaustion, ensuring non-congestion). We study the theoretical properties of coverage games, including determinacy, and the ability to a priori decompose the objectives among the agents. We solve the problems of deciding whether the coverer or the disruptor wins, analyze their tight complexity, and consider useful special cases.
Cite as
Orna Kupferman and Noam Shenwald. Coverage Games. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kupferman_et_al:LIPIcs.CONCUR.2025.27,
author = {Kupferman, Orna and Shenwald, Noam},
title = {{Coverage Games}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {27:1--27:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.27},
URN = {urn:nbn:de:0030-drops-239776},
doi = {10.4230/LIPIcs.CONCUR.2025.27},
annote = {Keywords: Two-Player Games, \omega-Regular Objectives, Coverage, Planning}
}
Document
Arbitrary-Arity Tree Automata for QCTL
Abstract
We introduce a new class of automata (which we coin EU-automata) running on infinite trees of arbitrary (finite) arity. We develop and study several algorithms to perform classical operations (union, intersection, complement, projection, alternation removal) for those automata, and precisely characterise their complexities. We also develop algorithms for solving membership and emptiness for the languages of trees accepted by EU-automata. We then use EU-automata to obtain several algorithmic and expressiveness results for the temporal logics QCTL and QCTL* (which extends CTL and CTL* with quantification over atomic propositions) and for MSO.
Cite as
François Laroussinie and Nicolas Markey. Arbitrary-Arity Tree Automata for QCTL. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{laroussinie_et_al:LIPIcs.CONCUR.2025.28,
author = {Laroussinie, Fran\c{c}ois and Markey, Nicolas},
title = {{Arbitrary-Arity Tree Automata for QCTL}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {28:1--28:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.28},
URN = {urn:nbn:de:0030-drops-239783},
doi = {10.4230/LIPIcs.CONCUR.2025.28},
annote = {Keywords: Model-checking, Verification, Automata theory, Quantified CTL}
}
Document
Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems
Abstract
We provide a generic decision procedure for energy games with energy-bounded attacker and reachability objective, moving beyond vector-valued energies and vector-addition updates. All we demand is that energies form well-founded bounded join-semilattices, and that energy updates have an upward-closed domain and can be "undone" through a Galois-connected function. We instantiate these Galois energy games to common energy games, declining energy games, multi-weighted reachability games, coverability on vector addition systems with states, and shortest path problems, supported by an Isabelle-formalization and two implementations. For the instantiations, our simple algorithm is polynomial w.r.t. game graph size and exponential w.r.t. dimension.
Cite as
Caroline Lemke and Benjamin Bisping. Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lemke_et_al:LIPIcs.CONCUR.2025.29,
author = {Lemke, Caroline and Bisping, Benjamin},
title = {{Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {29:1--29:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.29},
URN = {urn:nbn:de:0030-drops-239795},
doi = {10.4230/LIPIcs.CONCUR.2025.29},
annote = {Keywords: Energy games, Galois connection, Reachability, Game theory, Decidability}
}
Document
Open Bisimilarity for the π-Calculus with Mismatch
Abstract
Open bisimilarity is an equivalence relation for the π-calculus that is also congruence, making it suitable to use in compositional reasoning for mobile processes and communication protocols. The original definition of open bisimilarity, due to Sangiorgi, does not account for the mismatch operator, that is crucial in modelling real-world protocols. When mismatch is present, the congruence property no longer holds for open bisimilarity. In a LICS 2018 paper, Horne et al. proposed an extension of open bisimilarity, using a history-indexed class of relations, to address this problem. That definition, however, turns out to be non-compositional as we shall demonstrate in this paper. This paper presents a new definition of open bisimilarity in the π-calculus that incorporates mismatch. This is achieved by augmenting the transition semantics of the π-calculus with an explicit assumption about name distinctions, and by requiring that open bisimulation to be closed under an arbitary extension of the name distinctions assumption. We then prove that the resulting open bisimilarity is both an equivalence relation and a congruence.
Cite as
Tiange Liu, Alwen Tiu, and Ross Horne. Open Bisimilarity for the π-Calculus with Mismatch. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{liu_et_al:LIPIcs.CONCUR.2025.30,
author = {Liu, Tiange and Tiu, Alwen and Horne, Ross},
title = {{Open Bisimilarity for the \pi-Calculus with Mismatch}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {30:1--30:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.30},
URN = {urn:nbn:de:0030-drops-239805},
doi = {10.4230/LIPIcs.CONCUR.2025.30},
annote = {Keywords: mismatch, open bisimilarity, pi calculus}
}
Document
Compositional Reasoning for Parametric Probabilistic Automata
Abstract
We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) - an extension to probabilistic automata (PA), where transition probabilities are functions over a finite set of parameters. We lift an existing framework for PA to the pPA setting, incorporating asymmetric, circular, and interleaving proof rules. Our approach enables the verification of a broad spectrum of multi-objective queries for pPA, encompassing probabilistic properties and (parametric) expected total rewards. Additionally, we introduce a rule for reasoning about monotonicity in composed pPAs.
Cite as
Hannah Mertens, Tim Quatmann, and Joost-Pieter Katoen. Compositional Reasoning for Parametric Probabilistic Automata. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{mertens_et_al:LIPIcs.CONCUR.2025.31,
author = {Mertens, Hannah and Quatmann, Tim and Katoen, Joost-Pieter},
title = {{Compositional Reasoning for Parametric Probabilistic Automata}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {31:1--31:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.31},
URN = {urn:nbn:de:0030-drops-239810},
doi = {10.4230/LIPIcs.CONCUR.2025.31},
annote = {Keywords: Verification, Probabilistic systems, Assume-guarantee reasoning, Parametric Probabilistic Automata, Parameter synthesis}
}
Document
Resolving Nondeterminism by Chance
Abstract
History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting.
Motivated by checking qualitative properties in probabilistic verification, we consider the setting where the resolver strategy can randomise and only needs to succeed with lower-bounded probability. We study the expressiveness of such stochastically-resolvable automata as well as consider the decision questions of whether a given automaton has this property. In particular, we show that it is undecidable to check if a given NFA is λ-stochastically resolvable. This problem is decidable for finitely-ambiguous automata. We also present complexity upper and lower bounds for several well-studied classes of automata for which this problem remains decidable.
Cite as
Soumyajit Paul, David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke, and Di-De Yen. Resolving Nondeterminism by Chance. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{paul_et_al:LIPIcs.CONCUR.2025.32,
author = {Paul, Soumyajit and Purser, David and Schewe, Sven and Tang, Qiyi and Totzke, Patrick and Yen, Di-De},
title = {{Resolving Nondeterminism by Chance}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {32:1--32:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.32},
URN = {urn:nbn:de:0030-drops-239822},
doi = {10.4230/LIPIcs.CONCUR.2025.32},
annote = {Keywords: History-determinism, finite automata, probabilistic automata}
}
Document
Chance and Mass Interpretations of Probabilities in Markov Decision Processes
Abstract
Markov decision processes (MDPs) are a popular model for decision-making in the presence of uncertainty. The conventional view of MDPs in verification treats them as state transformers with probabilities defined over sequences of states and with schedulers making random choices. An alternative view, especially well-suited for modeling dynamical systems, defines MDPs as distribution transformers with schedulers distributing probability masses. Our main contribution is a unified semantical framework that accommodates these two views and two new ones. These four semantics of MDPs arise naturally through identifying different sources of randomness in an MDP (namely schedulers, configurations, and transitions) and providing different ways of interpreting these probabilities (called the chance and mass interpretations). These semantics are systematically unified through a mathematical construct called chance-mass (CM) classifier. As another main contribution, we study a reachability problem in each of the two new semantics, demonstrating their hardness and providing two algorithms for solving them.
Cite as
Yun Chen Tsai, Kittiphon Phalakarn, S. Akshay, and Ichiro Hasuo. Chance and Mass Interpretations of Probabilities in Markov Decision Processes. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{tsai_et_al:LIPIcs.CONCUR.2025.33,
author = {Tsai, Yun Chen and Phalakarn, Kittiphon and Akshay, S. and Hasuo, Ichiro},
title = {{Chance and Mass Interpretations of Probabilities in Markov Decision Processes}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {33:1--33:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.33},
URN = {urn:nbn:de:0030-drops-239838},
doi = {10.4230/LIPIcs.CONCUR.2025.33},
annote = {Keywords: MDP, distribution transformer, antichain, template-based synthesis}
}
Document
New Fault Domains for Conformance Testing of Finite State Machines
Abstract
A fault domain reflects a tester’s assumptions about faults that may occur in an implementation and that need to be detected during testing. A fault domain that has been widely studied in the literature on black-box conformance testing is the class of finite state machines (FSMs) with at most m states. Numerous strategies for generating test suites have been proposed that guarantee fault coverage for this class. These so-called m-complete test suites grow exponentially in m-n, where n is the number of states of the specification, so one can only run them for small values of m-n. But the assumption that m-n is small is not realistic in practice. In his seminal paper from 1964, Hennie raised the challenge to design checking experiments in which the number of states may increase appreciably. In order to solve this long-standing open problem, we propose (much larger) fault domains that capture the assumption that all states in an implementation can be reached by first performing a sequence from some set A (typically a state cover for the specification), followed by k arbitrary inputs, for some small k. The number of states of FSMs in these fault domains grows exponentially in k. We present a sufficient condition for k-A-completeness of test suites with respect to these fault domains. Our condition implies k-A-completeness of two prominent m-complete test suite generation strategies, the Wp and HSI methods. Thus these strategies are complete for much larger fault domains than those for which they were originally designed, and thereby solve Hennie’s challenge. We show that three other prominent m-complete methods (H, SPY and SPYH) do not always generate k-A-complete test suites.
Cite as
Frits Vaandrager and Ivo Melse. New Fault Domains for Conformance Testing of Finite State Machines. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 34:1-34:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{vaandrager_et_al:LIPIcs.CONCUR.2025.34,
author = {Vaandrager, Frits and Melse, Ivo},
title = {{New Fault Domains for Conformance Testing of Finite State Machines}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {34:1--34:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.34},
URN = {urn:nbn:de:0030-drops-239843},
doi = {10.4230/LIPIcs.CONCUR.2025.34},
annote = {Keywords: conformance testing, finite state machines, Mealy machines, apartness, observation tree, fault domains, k-A-complete test suites}
}
Document
From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases
Abstract
We consider process algebras with inaction, action prefix, non-deterministic choice and interleaving parallel composition modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum, and study the existence of finite bases (i.e., finite sound and complete axiomatisations) for these algebras. We prove that if the alphabet of actions is infinite and the behavioural equivalence is either simulation equivalence or trace equivalence, then a finite basis exists and is obtained by extending the known ground-complete axiomatisations for these behavioural equivalences. We prove that if the alphabet of actions is finite, then a finite basis does not exist for these equivalences. We also prove for all behavioural equivalences between ready simulation and completed traces there cannot exist a finite basis irrespective of the cardinality of the alphabet of actions (provided that it is non-empty). Finally, we prove that these results are maintained if the process algebra is extended with a constant for successful termination.
Cite as
Rowin Versteeg, Valentina Castiglioni, and Bas Luttik. From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{versteeg_et_al:LIPIcs.CONCUR.2025.35,
author = {Versteeg, Rowin and Castiglioni, Valentina and Luttik, Bas},
title = {{From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {35:1--35:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.35},
URN = {urn:nbn:de:0030-drops-239854},
doi = {10.4230/LIPIcs.CONCUR.2025.35},
annote = {Keywords: Equational basis, Parallel composition, Preorders, Equivalences, Linear time - branching time spectrum}
}
Document
Explainability is a Game for Probabilistic Bisimilarity Distances
Abstract
We revisit a game from the literature that characterizes the probabilistic bisimilarity distances of a labelled Markov chain. We illustrate how an optimal policy of the game can explain these distances. Like the games that characterize bisimilarity and probabilistic bisimilarity, the game is played on pairs of states and matches transitions of those states. To obtain more convincing and interpretable explanations than those provided by generic optimal policies, we restrict to optimal policies that delay reaching observably inequivalent state pairs for as long as possible (called 1-maximal) while quickly reaching equivalent ones (called 0-minimal). We present iterative algorithms that compute 1-maximal and 0-minimal policies and prove an exponential lower bound for the number of iterations of the algorithm that computes 1-maximal policies.
Cite as
Emily Vlasman, Anto Nanah Ji, James Worrell, and Franck van Breugel. Explainability is a Game for Probabilistic Bisimilarity Distances. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{vlasman_et_al:LIPIcs.CONCUR.2025.36,
author = {Vlasman, Emily and Nanah Ji, Anto and Worrell, James and van Breugel, Franck},
title = {{Explainability is a Game for Probabilistic Bisimilarity Distances}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {36:1--36:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.36},
URN = {urn:nbn:de:0030-drops-239861},
doi = {10.4230/LIPIcs.CONCUR.2025.36},
annote = {Keywords: probabilistic bisimilarity distance, labelled Markov chain, game, policy, explainability}
}
Document
Prophecies All the Way: Game-Based Model-Checking for HyperQPTL Beyond ∀*∃*
Abstract
Model-checking HyperLTL, a temporal logic expressing properties of sets of traces with applications to information-flow based security and privacy, has a decidable, but TOWER-complete, model-checking problem. While the classical model-checking algorithm for full HyperLTL is automata-theoretic, more recently, a game-based alternative for the ∀*∃*-fragment has been presented.
Here, we employ imperfect information-games to extend the game-based approach to full HyperQPTL, which features arbitrary quantifier prefixes and quantification over propositions and can express every ω-regular hyperproperty. As a byproduct of our game-based algorithm, we obtain finite-state implementations of Skolem functions via transducers with lookahead that explain satisfaction or violation of HyperQPTL properties.
Cite as
Sarah Winter and Martin Zimmermann. Prophecies All the Way: Game-Based Model-Checking for HyperQPTL Beyond ∀*∃*. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{winter_et_al:LIPIcs.CONCUR.2025.37,
author = {Winter, Sarah and Zimmermann, Martin},
title = {{Prophecies All the Way: Game-Based Model-Checking for HyperQPTL Beyond \forall*\exists*}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {37:1--37:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.37},
URN = {urn:nbn:de:0030-drops-239872},
doi = {10.4230/LIPIcs.CONCUR.2025.37},
annote = {Keywords: HyperLTL, HyperQPTL, model-checking games, prophecies}
}
Document
Reachability in Vector Addition System with States Parameterized by Geometric Dimension
Abstract
The geometric dimension of a vector addition system with states (VASS), emerged in Leroux and Schmitz (2019) and formalized by Fu, Yang, and Zheng (2024), quantifies the dimension of the vector space spanned by cycle effects in the system. This paper examines the VASS reachability problem through the lens of geometric dimension, revealing key differences from the traditional dimensional parameterization. Notably, we establish that the reachability problem for both geometrically 1-dimensional and 2-dimensional VASS is PSPACE-complete, achieved by extending the pumping technique initially proposed by Czerwiński et al. (2019).
Cite as
Yangluo Zheng. Reachability in Vector Addition System with States Parameterized by Geometric Dimension. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{zheng:LIPIcs.CONCUR.2025.38,
author = {Zheng, Yangluo},
title = {{Reachability in Vector Addition System with States Parameterized by Geometric Dimension}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {38:1--38:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.38},
URN = {urn:nbn:de:0030-drops-239888},
doi = {10.4230/LIPIcs.CONCUR.2025.38},
annote = {Keywords: Petri net, vector addition system, reachability, geometric dimension, pumping}
}
Document
Denotational Semantics for Probabilistic and Concurrent Programs
Abstract
We develop a denotational model for probabilistic and concurrent imperative programs, a class of programs with standard control flow via conditionals and while-loops, as well as probabilistic actions and parallel composition. Whereas semantics for concurrent or randomized programs in isolation is well studied, their combination has not been thoroughly explored and presents unique challenges. The crux of the problem is that interactions between control flow, probabilistic actions, and concurrent execution cannot be captured by straightforward generalizations of prior work on pomsets and convex languages, prominent models for those effects, individually. Our model has good domain theoretic properties, important for semantics of unbounded loops. We also prove two adequacy theorems, showing that the model subsumes typical powerdomain semantics for concurrency and convex powerdomain semantics for probabilistic nondeterminism.
Cite as
Noam Zilberstein, Daniele Gorla, and Alexandra Silva. Denotational Semantics for Probabilistic and Concurrent Programs. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 39:1-39:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{zilberstein_et_al:LIPIcs.CONCUR.2025.39,
author = {Zilberstein, Noam and Gorla, Daniele and Silva, Alexandra},
title = {{Denotational Semantics for Probabilistic and Concurrent Programs}},
booktitle = {36th International Conference on Concurrency Theory (CONCUR 2025)},
pages = {39:1--39:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-389-8},
ISSN = {1868-8969},
year = {2025},
volume = {348},
editor = {Bouyer, Patricia and van de Pol, Jaco},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.39},
URN = {urn:nbn:de:0030-drops-239890},
doi = {10.4230/LIPIcs.CONCUR.2025.39},
annote = {Keywords: Denotational Semantics, Pomsets, Concurrency, Convex Powerset}
}