Volume
LIPIcs, Volume 391
37th International Conference on Concurrency Theory (CONCUR 2026)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR)
Event
Editors
Publication Details
- published at: 2026-08-24
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-447-5
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 391, CONCUR 2026, Complete Volume
Abstract
LIPIcs, Volume 391, CONCUR 2026, Complete Volume
Cite as
37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 1-970, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{sokolova_et_al:LIPIcs.CONCUR.2026,
title = {{LIPIcs, Volume 391, CONCUR 2026, Complete Volume}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {1--970},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026},
URN = {urn:nbn:de:0030-drops-277132},
doi = {10.4230/LIPIcs.CONCUR.2026},
annote = {Keywords: LIPIcs, Volume 391, CONCUR 2026, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{sokolova_et_al:LIPIcs.CONCUR.2026.0,
author = {Sokolova, Ana and Totzke, Patrick},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {0:i--0:xvi},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.0},
URN = {urn:nbn:de:0030-drops-277124},
doi = {10.4230/LIPIcs.CONCUR.2026.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
On the Role of Prose in Specifications (Invited Talk)
Abstract
Specifications should let users find answers to their questions. Those answers should be accessible, unambiguous, consensual, reproducible, auditable, and they should be traceable to the artefacts users actually read.
This paper uses work done by the Arm Architecture Formal Team as a case study in the tensions between those requirements.
Cite as
Jade Alglave. On the Role of Prose in Specifications (Invited Talk). In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 1:1-1:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{alglave:LIPIcs.CONCUR.2026.1,
author = {Alglave, Jade},
title = {{On the Role of Prose in Specifications}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {1:1--1:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.1},
URN = {urn:nbn:de:0030-drops-273326},
doi = {10.4230/LIPIcs.CONCUR.2026.1},
annote = {Keywords: Arm Architecture, (prose, formal, executable, queryable, accessible) specifications, concurrency, herdtools, litmus tests, instruction set, Architecture Specification Language (ASL), The Architecture Speaks, query interface}
}
Document
Invited Talk
Reasoning About Probabilistic Loops, Moment by Moment (Invited Talk)
Abstract
Probabilistic programs and stochastic models have become a central paradigm for describing systems operating under uncertainty, ranging from randomised algorithms and Bayesian inference to cyber-physical systems. Their formal analysis, however, remains highly challenging due to the interplay among probabilistic behaviour, nondeterminism, and potentially unbounded computations. In recent years, martingale-based reasoning and moment-based and recurrence-equation approaches have emerged as powerful techniques for the automated verification of probabilistic loops [Ezio Bartocci et al., 2019; Marcel Moosbrugger et al., 2022].
We present a line of work [Daneshvar Amrollahi et al., 2022; Daneshvar Amrollahi et al., 2025; Ezio Bartocci, 2024; Ezio Bartocci et al., 2019; Ezio Bartocci et al., 2020; Ezio Bartocci et al., 2020; Andrey Kofnov et al., 2022; Andrey Kofnov et al., 2024; Marcel Moosbrugger et al., 2021; Marcel Moosbrugger et al., 2021; Marcel Moosbrugger et al., 2023; Marcel Moosbrugger et al., 2024; Marcel Moosbrugger et al., 2022; Miroslav Stankovic and Ezio Bartocci, 2024; Miroslav Stankovic et al., 2022] on the automated reasoning about probabilistic programs through moment-based analysis, recurrence solving, and asymptotic reasoning. A key observation is that, for the class of Prob-Solvable loops, it is always possible to characterise higher-order statistical moments via systems of linear recurrence equations admitting computable closed forms [Ezio Bartocci et al., 2019; Ezio Bartocci et al., 2020]. This feature enables the systematic derivation of quantitative properties such as expected values, variances, and probabilistic termination guarantees.
We first introduce the class of probabilistic (potentially infinite) loops that we call Prob-Solvable. For every loop in this class we can compute, analytically and without sampling, the exact higher-order statistical moments as closed-form expressions of the number of iterations. Moreover, we develop a faithful encoding of several families of Bayesian networks (BNs) into Prob-Solvable loops. In particular, BNs can be represented as probabilistic loops with polynomial assignments over random variables, enabling automated reasoning about exact inference, filtering, sensitivity analysis, and sampling-based procedures through invariant generation and closed-form recurrence solving [Ezio Bartocci et al., 2020; Miroslav Stankovic et al., 2022]. The proposed framework supports discrete, Gaussian, conditional linear Gaussian, and dynamic BNs, extending probabilistic program analysis to a broad family of probabilistic graphical models.
Beyond Prob-Solvable loops, we also characterise a hierarchy of solvable and unsolvable probabilistic loop classes and extend moment-based analysis to loops with non-polynomial assignments [Daneshvar Amrollahi et al., 2022; Daneshvar Amrollahi et al., 2025; Andrey Kofnov et al., 2022; Andrey Kofnov et al., 2024]. These works widen the applicability of symbolic techniques beyond the original polynomial setting.
The resulting algorithms are implemented in tools such as Mora [Ezio Bartocci et al., 2020] and Polar [Marcel Moosbrugger et al., 2024]. While Mora focuses on the automatic generation of moment-based invariants only for probabilistic loops with polynomial assignments, Polar provides a more general algebraic framework for exact symbolic analysis of probabilistic loops and related stochastic models [Marcel Moosbrugger et al., 2024]. We further investigate the inverse problem of synthesising probabilistic loops from prescribed moment sequences, thereby complementing analysis with program construction techniques [Miroslav Stankovic and Ezio Bartocci, 2024].
We then turn to verifying probabilistic termination properties. In this setting, martingale-based proof rules provide sufficient conditions for establishing almost-sure termination (AST), positive almost-sure termination (PAST), as well as non-termination properties. The key challenge lies in automating these proof obligations. To overcome this, we introduce Amber, a fully automated framework for proving and refuting the probabilistic termination of polynomial loops [Marcel Moosbrugger et al., 2021; Marcel Moosbrugger et al., 2021; Marcel Moosbrugger et al., 2023]. Amber blends martingale reasoning with asymptotic bounds obtained from recurrence equations and handles symbolic constants as well as standard probability distributions.
A common thread running through these papers is the reduction of probabilistic reasoning to symbolic algebraic reasoning. By expressing expected values and higher-order moments of stochastic updates as systems of recurrence equations, automated techniques can be applied for solving recurrences, generating invariants, and performing asymptotic analysis. This combination of probability theory, formal methods, and symbolic computation yields exact or asymptotically tight properties of stochastic systems and offers a viable pathway to automate quantitative verification tasks that would otherwise be intractable.
Cite as
Ezio Bartocci. Reasoning About Probabilistic Loops, Moment by Moment (Invited Talk). In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bartocci:LIPIcs.CONCUR.2026.2,
author = {Bartocci, Ezio},
title = {{Reasoning About Probabilistic Loops, Moment by Moment}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {2:1--2:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.2},
URN = {urn:nbn:de:0030-drops-273331},
doi = {10.4230/LIPIcs.CONCUR.2026.2},
annote = {Keywords: Probabilistic programs, probabilistic loops, moment-based analysis, martingales, recurrence equations, invariant generation, probabilistic termination, Bayesian networks, symbolic computation, formal verification}
}
Document
Invited Talk
Word Automata with Limited Nondeterminism (Invited Talk)
Abstract
We survey word automata with limited nondeterminism, a family of models lying between deterministic and fully nondeterministic automata. While determinism provides a simple algorithmic basis for verification, reactive synthesis, and probabilistic analysis, determinisation incurs large state blow-up, especially for ω-regular specifications. Limited nondeterminism offers a middle ground: it preserves some of the succinctness of nondeterministic automata while retaining enough structure for algorithmic use. We focus on three notions: unambiguous automata, in which each accepted word has at most one accepting run; good-for-games automata, whose nondeterministic choices can be resolved on the fly from the input prefix; and good-for-MDPs automata, which preserve optimal satisfaction probabilities when composed with MDPs. We compare these models in terms of expressiveness, succinctness, decision problems, minimisation, and applications to model checking, synthesis, reinforcement learning, and stochastic planning. Finally, we discuss how these threads converge: recent work has used good-for-games minimisation as a preprocessing step to reduce unambiguous and good-for-MDPs automata before composition, yielding more compact constructions for probabilistic analysis and planning. We present this as a recurring algorithmic pattern - resolving an automaton’s nondeterminism before it is amplified by the product with the system - that unifies otherwise separate lines of work.
Cite as
Yong Li, Soumyajit Paul, Sven Schewe, and Qiyi Tang. Word Automata with Limited Nondeterminism (Invited Talk). In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{li_et_al:LIPIcs.CONCUR.2026.3,
author = {Li, Yong and Paul, Soumyajit and Schewe, Sven and Tang, Qiyi},
title = {{Word Automata with Limited Nondeterminism}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {3:1--3:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.3},
URN = {urn:nbn:de:0030-drops-273341},
doi = {10.4230/LIPIcs.CONCUR.2026.3},
annote = {Keywords: History-determinism, finite automata, probabilistic automata}
}
Document
Invited Talk
An Introduction to Multi-Environment Markov Decision Processes (Invited Talk)
Abstract
Markov Decision Processes (MDPs) are the standard model for decision-making under stochastic uncertainty. With full observability, reachability, safety and parity problems admit efficient algorithms and memoryless pure optimal strategies. Full observability is, however, often unrealistic. Partially Observable MDPs (POMDPs) replace it by an observation function, but the price is steep: most natural problems become undecidable. This motivates the study of structured subclasses or variants of POMDPs that preserve enough modelling power while restoring decidability. Multi-Environment MDPs (MEMDPs) are one such variant. An MEMDP is a finite family of MDPs with the same state and action spaces but distinct transition functions, and the active MDP, called the environment, is fixed throughout the run but hidden from the controller. The goal is to synthesize a single strategy that works well in every environment. Two semantics have been considered for MEMDPs: a universal, worst-case one, and a prior, Bayesian one based on a distribution over environments. We survey the main results obtained for both semantics since the introduction of the model in 2014. We cover reachability, parity and Rabin objectives, under the qualitative criteria (almost-sure, limit-sure) and the quantitative value-threshold problem, and we outline the key algorithmic ideas.
Cite as
Jean-François Raskin. An Introduction to Multi-Environment Markov Decision Processes (Invited Talk). In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{raskin:LIPIcs.CONCUR.2026.4,
author = {Raskin, Jean-Fran\c{c}ois},
title = {{An Introduction to Multi-Environment Markov Decision Processes}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {4:1--4:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.4},
URN = {urn:nbn:de:0030-drops-273355},
doi = {10.4230/LIPIcs.CONCUR.2026.4},
annote = {Keywords: Multi-Environment Markov Decision Processes, partially observable MDPs, qualitative analysis, universal semantics, prior semantics, parity objectives}
}
Document
Invited Talk
A Coalgebraic Dijkstra Algorithm (Invited Talk)
Abstract
The Dijkstra algorithm is a classical method for solving the shortest path problem on weighted graphs. There are several variations of the Dijkstra algorithm, including algorithms for the widest path problem and for two-player games. In this paper, we introduce the coalgebraic shortest path problem (CSPP), a unifying framework for a broad class of optimization problems on state-transition systems. This framework encompasses not only the aforementioned problems but also new ones such as the shortest binary tree problem. We further present a coalgebraic Dijkstra algorithm for solving the CSPP efficiently under a suitable condition. Our condition is necessary and sufficient for the algorithm to return correct solutions, thereby providing a precise criterion for when Dijkstra-style acceleration is possible. We also show that the proposed algorithm achieves asymptotic complexity comparable to that of the classical Dijkstra algorithm.
Cite as
Takahiro Sanada, Yoàv Montacute, Kittiphon Phalakarn, and Ichiro Hasuo. A Coalgebraic Dijkstra Algorithm (Invited Talk). In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{sanada_et_al:LIPIcs.CONCUR.2026.5,
author = {Sanada, Takahiro and Montacute, Yo\`{a}v and Phalakarn, Kittiphon and Hasuo, Ichiro},
title = {{A Coalgebraic Dijkstra Algorithm}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {5:1--5:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.5},
URN = {urn:nbn:de:0030-drops-273365},
doi = {10.4230/LIPIcs.CONCUR.2026.5},
annote = {Keywords: Coalgebra, Greatest fixed point, Dijkstra’s algorithm, Shortest path}
}
Document
Invited Contribution for the Test-of-Time Award
A Look Back at Strategy Logic (Invited Contribution for the Test-of-Time Award)
Abstract
In this note, we recall the history and our motivation behind the development of Strategy Logic and we discuss some of the work that ensued from its introduction.
Cite as
Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. A Look Back at Strategy Logic (Invited Contribution for the Test-of-Time Award). In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 6:1-6:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2026.6,
author = {Chatterjee, Krishnendu and Henzinger, Thomas A. and Piterman, Nir},
title = {{A Look Back at Strategy Logic}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {6:1--6:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.6},
URN = {urn:nbn:de:0030-drops-273378},
doi = {10.4230/LIPIcs.CONCUR.2026.6},
annote = {Keywords: Strategy Logic, Games, Automata}
}
Document
Reachability in Fixed-Dimensional Continuous VASS
Abstract
Vector Addition System with States (VASS) are a ubiquitous model of infinite-state systems consisting of a set of non-negative counters which can be incremented and decremented. It is known that the reachability problem for VASS is Ackermann-complete. Because of this huge complexity, various over-approximations of VASS have been studied in the literature. One such over-approximation is continuous VASS (CVASS), in which the counters are (non-negative) rational numbers and whenever a vector is added to the current counter values, it is first scaled with an arbitrarily chosen rational factor between zero and one. It is known that the reachability problem for CVASS is NP-complete.
In this paper, we initiate the study of fixed-dimensional CVASS, i.e., CVASS with a fixed number of counters. We study both the reachability and coverability problems, under both unary and binary encodings as well as over both the non-negative and the rational semantics. This gives rise to a collection of eight different problems. As our main result, we prove a complexity dichotomy for all of these eight problems when the transition vectors are over the rationals: For dimension 1, all of the eight problems are in AC¹, and so within 𝖯, whereas for any dimension at least 2, all of the eight problems are NP-complete. Furthermore, the hardness holds even when the underlying automaton is acyclic. To achieve this hardness result, we present a new technique called the Egyptian prime fractions technique.
Finally, we also study these problems when the transition vectors are over the integers. Except for dimension 2, we classify the complexity of these problems over the non-negative semantics: For dimension 1, all of the problems are in AC¹, whereas for dimensions 3 and above, all of the problems are NP-complete.
Cite as
Michal Ajdarów, A. R. Balasubramanian, and Łukasz Orlikowski. Reachability in Fixed-Dimensional Continuous VASS. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ajdarow_et_al:LIPIcs.CONCUR.2026.7,
author = {Ajdar\'{o}w, Michal and Balasubramanian, A. R. and Orlikowski, {\L}ukasz},
title = {{Reachability in Fixed-Dimensional Continuous VASS}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.7},
URN = {urn:nbn:de:0030-drops-273385},
doi = {10.4230/LIPIcs.CONCUR.2026.7},
annote = {Keywords: Continuous Counters, Vector Addition Systems, Complexity, Reachability}
}
Document
Complementing Emerson-Lei Elevator Automata
Abstract
Büchi elevator automata naturally appear in several areas of formal methods as a structural expressibly-equivalent subclass of Büchi automata where every strongly connected component is either deterministic or inherently weak. It was shown that this class contains the majority of Büchi automata generated in practical applications, including LTL model-checking and verification of hyperproperties. Moreover, the elevator subclass enables more efficient complementation and determinization algorithms than unrestricted Büchi automata. In this paper, we introduce Emerson-Lei elevator automata, which is a generalization of Büchi elevator automata to richer acceptance conditions. We provide a complementation algorithm with a significantly better asymptotic complexity than the best known algorithm for unrestricted Emerson-Lei automata. The practical efficiency of our algorithm is demonstrated by an experimental comparison with the popular state-of-the-art tool Spot. Our work is, to the best of our knowledge, the first step towards practical algorithms for complementing, determinizing, and testing universality and inclusion of Emerson-Lei automata with rich acceptance conditions.
Cite as
Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, and Nicolas Mazzocchi. Complementing Emerson-Lei Elevator Automata. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{alexaj_et_al:LIPIcs.CONCUR.2026.8,
author = {Alexaj, Ondrej and Havlena, Vojt\v{e}ch and Leng\'{a}l, Ond\v{r}ej and Li, Yong and Mazzocchi, Nicolas},
title = {{Complementing Emerson-Lei Elevator Automata}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {8:1--8:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.8},
URN = {urn:nbn:de:0030-drops-273390},
doi = {10.4230/LIPIcs.CONCUR.2026.8},
annote = {Keywords: Emerson-Lei elevator automata, complementation, elevator automata, omega automata, infinite words, omega-regular languages}
}
Document
A Factorization Theorem for Forest Algebras
Abstract
Simon’s factorization theorem is a celebrated tool in algebraic automata theory, providing bounded-depth decompositions of words with respect to morphisms into finite semigroups.
We develop an analogue of Simon’s theorem for forests in the setting of forest algebras. In contrast with words, this presents a basic difficulty: recursively factoring a forest requires keeping track of where each subforest "fits". This difficulty ripples throughout the proof, and we overcome it by augmenting the free forest algebra and by developing a framework that supports recursive factorization of forests, along with its semantic implications.
Our main result identifies a new semantic restriction on morphisms (called R-alignment) which intuitively ensures that different ways of cutting a forest remain compatible (in a certain sense) at the semigroup level. Under this condition, we prove that every morphism admits decompositions of bounded depth. We also prove that without this restriction, there are morphisms for which no bounded-depth decomposition exists (under our notion of decomposition).
Cite as
Shaull Almagor, Michaël Cadilhac, and Asaf Shoham. A Factorization Theorem for Forest Algebras. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CONCUR.2026.9,
author = {Almagor, Shaull and Cadilhac, Micha\"{e}l and Shoham, Asaf},
title = {{A Factorization Theorem for Forest Algebras}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.9},
URN = {urn:nbn:de:0030-drops-273403},
doi = {10.4230/LIPIcs.CONCUR.2026.9},
annote = {Keywords: Factorization Forest, Semigroup, Forest Algebra, Green’s relations, Tree Languages}
}
Document
Representing One Letter Weighted Automata over the Tropical Semiring
Abstract
We consider weighted automata over the tropical semiring ℤ_∞(min, +). Recently, it was shown that determinisation is decidable; in this paper we focus on the complexity when the alphabet is unary. In 2001, Lombardy showed this problem is decidable, a close inspection of his proof yields a coNP upper bound on the complexity. Earlier Gaubert showed that every weighted automaton in this setting can be effectively turned into an equivalent union of deterministic weighted automata. We prove Gaubert’s result efficiently, presenting it as a generalisation of Chrobak’s normal form for unary NFA. In particular, we prove that the equivalent union of deterministic weighted automata can be represented by a weighted automaton of quadratic size in the size of the original one, and this representation can be computed in polynomial time. Building on this, we show that determinisation, and even register minimisation (which generalises determinisation), is coNP-complete. We complete the paper with observations that the boundedness problem is also coNP-complete by reductions with determinisation. Lastly, we provide evidence that all of these problems are not FPT (by proving coW₁-hardness) when parametrised by the number of deterministic automata in the union.
Cite as
Shaull Almagor, Ismaël Jecker, Filip Mazowiecki, Łukasz Orlikowski, David Purser, and Henry Sinclair-Banks. Representing One Letter Weighted Automata over the Tropical Semiring. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CONCUR.2026.10,
author = {Almagor, Shaull and Jecker, Isma\"{e}l and Mazowiecki, Filip and Orlikowski, {\L}ukasz and Purser, David and Sinclair-Banks, Henry},
title = {{Representing One Letter Weighted Automata over the Tropical Semiring}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {10:1--10:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.10},
URN = {urn:nbn:de:0030-drops-273419},
doi = {10.4230/LIPIcs.CONCUR.2026.10},
annote = {Keywords: weighted automata, determinisation, register minimisation}
}
Document
Buffered Control for Opacity in Timed Automata
Abstract
Timed automata are an extension of finite automata that can measure and react to the passage of time, handling real-time constraints by using clocks. The timed opacity problem, where an attacker attempts to infer from observed actions and timestamps whether a secret location was visited, was shown undecidable for timed automata. Execution-time opacity is a decidable though limited setting in which the attacker attempts to detect whether the secret location was visited, by only relying on the run duration. Here, we significantly extend this setting, by allowing the attacker to observe all observable actions, in the right order though with only the integral parts of their timestamps, which we call buffered observations. We consider the controlled setting, in which we aim at dynamically defining a sequence of sets of enabled actions ensuring opacity with buffered observations. We first prove the inter-reducibility of full opacity (observations must not leak the visit of the secret location) and weak opacity (the attacker might prove that the location was not visited, but not that it was visited) in this new controlled setting. Then, we prove the undecidability of the problem of existence of a sequential control strategy ensuring opacity under buffered observations. Finally and most importantly, we prove that decidability is retrieved in two independent cases, with their theoretical complexities, with and without control. These two assumptions express realistic limitations of the controller. The first case is when the strategy of the controller changes at most an a priori fixed number of times per time unit, which is not a strong practical assumption. The second case is when all controllable actions are observable and distinguishable by an attacker.
Cite as
Étienne André, Sarah Dépernet, and Engel Lefaucheux. Buffered Control for Opacity in Timed Automata. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 11:1-11:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{andre_et_al:LIPIcs.CONCUR.2026.11,
author = {Andr\'{e}, \'{E}tienne and D\'{e}pernet, Sarah and Lefaucheux, Engel},
title = {{Buffered Control for Opacity in Timed Automata}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {11:1--11:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.11},
URN = {urn:nbn:de:0030-drops-273421},
doi = {10.4230/LIPIcs.CONCUR.2026.11},
annote = {Keywords: timed automata, side-channel attack, observation with finite precision, control}
}
Document
PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance
Abstract
Reachability is the most fundamental logical objective, yet it is notoriously difficult to learn in reinforcement learning settings: even for Markov decision processes, PAC learning of reachability is impossible without additional assumptions. This difficulty also holds in turn-based stochastic games (TBSGs), where two adversarial players interact on a finite state space. In this work, we consider turn-based stochastic games with reachability objectives. For such settings, adversarial learning, in which players are adversarial even in the learning phase, is impossible. Therefore, the goal is to consider learning, in which both players learn the unknown model together. In this spirit, previous literature on PAC learning in TBSGs considers (a) public information shared by both players; and (b) centralized learning, which means that players share the same learning algorithm. In this work, our contribution is two-fold. First, we relax these strong assumptions and ensure learning: (i) with private information not shared with the other player; and (ii) decentralized learning where the players do not share the same learning algorithm. To the best of our knowledge, this work is the first positive result for decentralized and private information learning of TBSGs with reachability objectives. Second, we introduce a game-theoretic generalization of the Expected Conditional Distance (ECD) parameter, which measures the expected length of reaching the target set. We establish a polynomial-sample complexity bound with respect to the number of states, actions, ECD parameter, and inverses of error tolerance and failure probability.
Cite as
Ali Asadi, Krishnendu Chatterjee, and Pavol Kebis. PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{asadi_et_al:LIPIcs.CONCUR.2026.12,
author = {Asadi, Ali and Chatterjee, Krishnendu and Kebis, Pavol},
title = {{PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {12:1--12:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.12},
URN = {urn:nbn:de:0030-drops-273432},
doi = {10.4230/LIPIcs.CONCUR.2026.12},
annote = {Keywords: formal methods, games and logic, logical aspects of AI, model checking}
}
Document
Generalized Bidding Games: Where Bidding and Stochastic Games Meet
Abstract
Two-player games on graphs are a classical framework for analyzing strategic decision making. In turn-based games, two players move a token along the edges of the graph, and the right to move the token is determined by the current vertex. In traditional bidding games - referred to as pure bidding games - the right to move the token is determined at each step through bidding; here we consider Richman bidding, where the winning player of a bid pays the losing player. The winner is decided based on a temporal or quantitative specification evaluated over the resulting infinite play.
In this work, we combine turn-based games and pure bidding games into generalized bidding games, with player-1 vertices, player-2 vertices, and bidding vertices. This natural and simple generalization of bidding games has far-reaching consequences. First, we show that, as a model, generalized bidding games are more expressive than pure bidding games, and we provide several applications. Second, and most importantly, we show that generalized Richman bidding games are structurally equivalent to simple stochastic games, a well-studied model: they are linearly interreducible to each other. As was previously known, the special case of pure Richman bidding games corresponds to random-turn games. In other words, generalized bidding games extend pure bidding games in the same way that simple stochastic games extend random-turn games. We use this connection to solve generalized Richman bidding games for temporal (parity) and quantitative (mean-payoff and discounted-sum) specifications. From a computational perspective, we establish that generalized bidding games with parity and mean-payoff specifications retain the best known upper bounds for turn-based games and pure bidding games, namely NP∩coNP.
Finally, we study a repair problem that asks whether bidding vertices can be assigned "owners" so as to bring the threshold budget required to win the game below a given target. This problem has direct applications in compositional policy synthesis for multi-objective settings, and we show it to be NP-complete.
Cite as
Ali Asadi, Thomas A. Henzinger, Ehsan Kafshdar Goharshady, Pavol Kebis, and Kaushik Mallik. Generalized Bidding Games: Where Bidding and Stochastic Games Meet. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{asadi_et_al:LIPIcs.CONCUR.2026.13,
author = {Asadi, Ali and Henzinger, Thomas A. and Kafshdar Goharshady, Ehsan and Kebis, Pavol and Mallik, Kaushik},
title = {{Generalized Bidding Games: Where Bidding and Stochastic Games Meet}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {13:1--13:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.13},
URN = {urn:nbn:de:0030-drops-273440},
doi = {10.4230/LIPIcs.CONCUR.2026.13},
annote = {Keywords: Bidding Games, Stochastic Games}
}
Document
Asymmetrically Discounted Stochastic Games
Abstract
We study asymmetrically discounted stochastic games, in which players use distinct and reasonably apart discount factors. We show that optimal strategies in these games may require both memory and randomisation, in contrast to the classical symmetrically discounted setting. Our main technical contribution establishes that computing incentive Stackelberg equilibria - a variant of Stackelberg equilibria in which one player, called Player Max, can offer payments to the other player, called Player Min - is no harder than solving classical discounted games. We further show that optimal strategies in this setting can be realised by finite counting strategies, whereas restricting players to stationary strategies makes the problem computationally intractable. Finally, we establish that computing classical Stackelberg equilibria in these games under the constraint of memoryless strategies is NP-complete and remains NP-hard even when general or counting strategies are allowed.
Cite as
Sarvin Bahmani, Soumyajit Paul, Sven Schewe, Shadi Tasdighi Kalat, and Ashutosh Trivedi. Asymmetrically Discounted Stochastic Games. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bahmani_et_al:LIPIcs.CONCUR.2026.14,
author = {Bahmani, Sarvin and Paul, Soumyajit and Schewe, Sven and Kalat, Shadi Tasdighi and Trivedi, Ashutosh},
title = {{Asymmetrically Discounted Stochastic Games}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {14:1--14:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.14},
URN = {urn:nbn:de:0030-drops-273453},
doi = {10.4230/LIPIcs.CONCUR.2026.14},
annote = {Keywords: Stochastic Games, Asymmetric Discounting, Stackelberg Equilibrium}
}
Document
Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata
Abstract
Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes ω-regular languages by processing their ultimately periodic words. FDFA are known to enjoy many good properties and can be exponentially more succinct than deterministic ω-automata with Rabin, Streett or parity acceptance. This paper addresses two main questions: (1) Are FDFA suitable for probabilistic model checking purposes? and (2) Is it possible to obtain an even more compact representation of ω-regular languages by allowing the components of an FDFA to be unambiguous instead of deterministic? Question (1) is answered in the affirmative by presenting the first polynomial-time algorithm for computing the probability that a discrete-time Markov chain satisfies an ω-regular property represented as an FDFA. Question (2) is motivated by the fact that unambiguous finite automata may require exponentially fewer states than deterministic ones. This paper introduces a model of families of unambiguous finite automata (FUFA) that captures the class of ω-regular languages. FUFA can be exponentially more succinct than both FDFA and unambiguous Büchi automata, and there is a single-exponential translation from linear temporal logic (LTL) to FUFA. This stands in contrast to a double-exponential lower bound for the translation from LTL to FDFA. Moreover, the polynomial-time probabilistic model checking algorithm for discrete-time Markov chains against FDFA-specifications is extended to the case where the property is represented by an FUFA with a deterministic leading automaton.
Cite as
Christel Baier, Sascha Klüppelholz, and Timm Spork. Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{baier_et_al:LIPIcs.CONCUR.2026.15,
author = {Baier, Christel and Kl\"{u}ppelholz, Sascha and Spork, Timm},
title = {{Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {15:1--15:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.15},
URN = {urn:nbn:de:0030-drops-273461},
doi = {10.4230/LIPIcs.CONCUR.2026.15},
annote = {Keywords: Families of Finite Automata, FDFA, Unambiguous Automata, Discrete-time Markov Chains, Probabilistic Model Checking, Verification}
}
Document
Decomposition of Automata Recognizing Ideals
Abstract
Minimizing the size of finite automata is a fundamental problem in theoretical computer science. Beyond standard minimization, further reductions can be achieved by decomposing an automaton into smaller components whose languages combine via intersection or union to recover the original language. However, in general, no polynomial-time algorithm is known for computing such decompositions.
In this paper, we focus on automata that recognize ideals, that is, languages at level 1/2 in the Straubing–Thérien hierarchy. Equivalently, these languages are expressible as a finite union of languages of the form Σ^*a₁Σ^*… Σ^*a_nΣ^* where Σ is an alphabet and a_i are letters of Σ. We show that the two problems of deciding whether an automata recognizing an ideal can be decomposed into an intersection or a union of smaller automata are decidable in NL. Moreover, we provide a polynomial-time algorithm that computes a decomposition into an intersection, if one exists, while ensuring that the resulting components also recognize ideal languages.
Cite as
Mathias Berry, Pierre-Cyrille Héam, and Ismaël Jecker. Decomposition of Automata Recognizing Ideals. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{berry_et_al:LIPIcs.CONCUR.2026.16,
author = {Berry, Mathias and H\'{e}am, Pierre-Cyrille and Jecker, Isma\"{e}l},
title = {{Decomposition of Automata Recognizing Ideals}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.16},
URN = {urn:nbn:de:0030-drops-273473},
doi = {10.4230/LIPIcs.CONCUR.2026.16},
annote = {Keywords: Finite state automata, decomposition, Shuffle ideals}
}
Document
Positional Determinacy with Colored Vertices: A 1-To-2-Player Lift
Abstract
Positional determinacy of vertex-colored parity games was proved in the 1990s, which directly implies positional determinacy of edge-colored parity games. In 2006, it was shown that if a prefix-independent color-based objective ensures that every edge-colored two-player turn-based game is positionally determined, this objective is equivalent to a parity objective. We prove a similar result for vertex-colored games, namely that the following are equivalent for any prefix-independent objective W over a finite set of colors:
- W is positionally determined on all vertex-colored one-player games.
- W is positionally determined on all vertex-colored two-player games.
- W is equivalent to a parity objective on ordrerd pairs of colors. We prove that finiteness of the color set is required for our equivalence to hold. Beyond this 1-to-2-player lift, the technique that we develop to handle the pairs of colors establishes a promising 2-way correspondence between edge-colored games and vertex-colored games.
Cite as
Raphaël Berthon and Stéphane Le Roux. Positional Determinacy with Colored Vertices: A 1-To-2-Player Lift. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{berthon_et_al:LIPIcs.CONCUR.2026.17,
author = {Berthon, Rapha\"{e}l and Le Roux, St\'{e}phane},
title = {{Positional Determinacy with Colored Vertices: A 1-To-2-Player Lift}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {17:1--17:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.17},
URN = {urn:nbn:de:0030-drops-273480},
doi = {10.4230/LIPIcs.CONCUR.2026.17},
annote = {Keywords: two-player games, one-player games, parity objectives}
}
Document
WinPop: Making Populations Win Together
Abstract
We consider a novel graph-based problem, in which a population of arbitrary size aims at achieving a common objective. More specifically, WinPop is a synthesis problem defined by a finite graph with edges labels in {✓, -, x}. The instance is positive if there exists a sequence (π_i)_{i ∈ ℕ} of infinite paths such that for any fixed population size N ∈ ℕ_{> 0}, there is a path whose N-th transition is labelled ✓ and all previous paths have their N-th transition labelled by -.
Alternatively, WinPop can also be cast as a 2D-tiling problem with vertical and horizontal constraints: the horizontal constraint reflects the possible paths in the input graph, and the vertical one encodes that a ✓-label eventually occurs, before any x-label. Finally, WinPop also corresponds to the existence of a coalition strategy for a reachability objective in parameterized concurrent games.
We use algebraic tools to show that the problem can be solved in polynomial space. First we exhibit a finite semigroup whose elements summarize coalition strategies over a finite interval of population sizes. Then, we characterize the existence of winning strategies by the existence of particular elements in this semigroup. Finally, we provide a matching complexity lower bound, to conclude that WinPop is PSPACE-complete.
Cite as
Nathalie Bertrand, Patricia Bouyer, Luc Lapointe, and Corto Mascle. WinPop: Making Populations Win Together. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2026.18,
author = {Bertrand, Nathalie and Bouyer, Patricia and Lapointe, Luc and Mascle, Corto},
title = {{WinPop: Making Populations Win Together}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {18:1--18:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.18},
URN = {urn:nbn:de:0030-drops-273494},
doi = {10.4230/LIPIcs.CONCUR.2026.18},
annote = {Keywords: Parameterized systems, Automata, Semigroups, Concurrent games, Tiling Problem}
}
Document
Reaching as Cheap as Possible in 1-Clock Robust Weighted Timed Games
Abstract
The value problem for 2-player games on graph generally consists in determining the minimal value Min can ensure against any possible strategy for Max. We consider here the value problem for reachability objectives in weighted timed games (WTGs) under a robust semantics. WTGs are a modelling formalism combining real-time constraints and integer weights on transitions and locations in an adversarial setting. Robustness allows for representing timing imprecisions in the measurement of delays and clock values. Robust weighted timed games have been introduced more than a decade ago: they are undecidable in general, and were quite recently shown decidable for the subclasses of acyclic or divergent robust WTGs. This paper pursues the goal of identifying decidable subclasses and establishes the decidability of the robust value problem for 1-clock WTGs.
Cite as
Nathalie Bertrand, Maëlle Gautrin, and Julie Parreaux. Reaching as Cheap as Possible in 1-Clock Robust Weighted Timed Games. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2026.19,
author = {Bertrand, Nathalie and Gautrin, Ma\"{e}lle and Parreaux, Julie},
title = {{Reaching as Cheap as Possible in 1-Clock Robust Weighted Timed Games}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.19},
URN = {urn:nbn:de:0030-drops-273507},
doi = {10.4230/LIPIcs.CONCUR.2026.19},
annote = {Keywords: timed automata, weighted timed games, robustness, games on graphs}
}
Document
Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems
Abstract
Traditional model-checking techniques typically verify distributed algorithms only for a fixed number of finite-state processes. Parameterized model checking generalizes this to any number of processes, while still typically assuming that each process is finite-state. In this work, we consider asynchronous round-based distributed algorithms in which each process is infinite-state since it can execute for an infinite number of rounds. We show that the parameterized verification problem for asynchronous round-based distributed algorithms is undecidable, already for simple specifications. Nevertheless, as our main contribution, we provide a reduction to LTL model checking over finite-counter systems and prove that it is sound and complete. This enables the use of off-the-shelf, mature symbolic model checkers for finite-counter systems. We demonstrate the practical applicability of this reduction by verifying safety and liveness properties of several asynchronous round-based consensus and leader-election algorithms using the nuXmv model checker.
Cite as
Nathalie Bertrand, Pranav Ghorpade, and Sasha Rubin. Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 20:1-20:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2026.20,
author = {Bertrand, Nathalie and Ghorpade, Pranav and Rubin, Sasha},
title = {{Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {20:1--20:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.20},
URN = {urn:nbn:de:0030-drops-273511},
doi = {10.4230/LIPIcs.CONCUR.2026.20},
annote = {Keywords: parametrized verification, asynchronous round-based distributed algorithms, finite-counter systems, LTL model checking}
}
Document
Completeness for Probabilistic Boolean Tapes
Abstract
Probabilistic Boolean circuits have recently been proposed as a string-diagrammatic foundation for finite probabilistic programming. In this paper, we present a complete set of axioms for their semantics in terms of Markov kernels. Our approach is based on two intermediate results: completeness for partial Boolean circuits and completeness for probabilistic Boolean tapes, a diagrammatic language for rig categories.
Cite as
Filippo Bonchi and Cipriano Junior Cioffo. Completeness for Probabilistic Boolean Tapes. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2026.21,
author = {Bonchi, Filippo and Cioffo, Cipriano Junior},
title = {{Completeness for Probabilistic Boolean Tapes}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {21:1--21:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.21},
URN = {urn:nbn:de:0030-drops-273525},
doi = {10.4230/LIPIcs.CONCUR.2026.21},
annote = {Keywords: String diagrams, Rig categories, synthetic probability theory}
}
Document
Monitoring Discounted Sum Properties
Abstract
Runtime monitoring of quantitative signals faces a fundamental trade-off between volatility and over-aggregation: instantaneous observations are noisy, while long-run averages obscure local structure. Localisation measures such as discounted averages offer a principled middle ground, yet remain poorly understood in runtime verification. This paper studies discounted sums from a monitoring perspective, in both deterministic and stochastic settings. We formalize the discounted monitoring problem and show that exact, sound monitoring of discounted sums cannot be achieved with finite memory. To overcome this impossibility, we introduce ε-approximately sound monitoring, deriving explicit bounds on memory and observation requirements. We then extend the framework to stochastic processes via expected discounted sums, defining pointwise and uniform (ε,δ)-soundness notions, establishing statistical optimality, and proving impossibility beyond a precision threshold. We also formalize the resource complexity of deterministic discounted monitoring via affine register machines and prove a tight worst-case lower bound. Finally, we present a specification language for arithmetic expressions over multiple discounted sums with synchronous and asynchronous semantics, and evaluate our approach on practical scenarios including algorithmic fairness.
Cite as
Filip Cano, Thomas A. Henzinger, Konstantin Kueffner, and N. Ege Saraç. Monitoring Discounted Sum Properties. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cano_et_al:LIPIcs.CONCUR.2026.22,
author = {Cano, Filip and Henzinger, Thomas A. and Kueffner, Konstantin and Sara\c{c}, N. Ege},
title = {{Monitoring Discounted Sum Properties}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {22:1--22:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.22},
URN = {urn:nbn:de:0030-drops-273533},
doi = {10.4230/LIPIcs.CONCUR.2026.22},
annote = {Keywords: Runtime Verification, Probabilistic Systems, Quantitative Verification, Approximate Monitoring}
}
Document
When Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency
Abstract
Behaviour-oriented concurrency (BoC) is a recently established programming model in which programmers define concurrent operations that execute atomically across multiple isolated resources. This allows for expressive interactions but introduces complex causal dependencies determined by dynamic resource overlap. Previous work defines the causal guarantees of BoC operationally, but mixes intended design constraints with incidental implementation details, leading to unintended causal orders. BoC is now being implemented across multiple languages and runtimes, all relying on the operational descriptions of causality. This paper develops an axiomatic model of BoC executions that makes the intrinsic orders explicit and derives the intended causal relation from their interaction. Using a set of representative programs and candidate executions, we motivate the design of this causal relation. We then prove that a representative minimal core calculus for BoC is sound with respect to this axiomatic model. Together, these results provide an implementation-independent foundation for reasoning about BoC causality across runtimes, schedulers and optimisation decisions.
Cite as
Luke Cheeseman, Elias Castegren, Tobias Wrigstad, Sophia Drossopoulou, and Matthew J. Parkinson. When Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cheeseman_et_al:LIPIcs.CONCUR.2026.23,
author = {Cheeseman, Luke and Castegren, Elias and Wrigstad, Tobias and Drossopoulou, Sophia and Parkinson, Matthew J.},
title = {{When Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {23:1--23:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.23},
URN = {urn:nbn:de:0030-drops-273549},
doi = {10.4230/LIPIcs.CONCUR.2026.23},
annote = {Keywords: Concurrency, Parallelism, Language Design, Causality}
}
Document
Improving Reachability in Vector Addition Systems Through Pumpability
Abstract
Vector addition systems (VAS) constitute an important model of computation and concurrency that is equally expressive as the Petri net model. Recently, a lot of research has been conducted on vector addition systems with states (VASS), which are VASes equipped with a finite state control. Results on VASS naturally carry over to VAS, but no straightforward improvement is available. In this paper, we investigate the reachability problem in VAS in fixed dimensions. Based on a pumpability analysis of VAS that refines Rackoff’s extraction for VASS, we obtain an F_{d-2} upper bound for the d-dimensional VAS reachability problem, improving the F_d upper bound inherited from the d-dimensional VASS reachability problem. Low-dimensional VASes are also considered. In particular, we establish a PSPACE upper bound for reachability in 4-dimensional VAS and an ELEMENTARY upper bound for 5-dimensional VAS, while the same upper bounds were known only for 2-VASS and 3-VASS, respectively. The result for 4-VAS particularly hinges on a simplified projection technique developed for geometrically 2-dimensional VASSes, whose reachability problem is shown to be equivalent to 2-VASS.
Cite as
Weijun Chen, Yuxi Fu, and Yangluo Zheng. Improving Reachability in Vector Addition Systems Through Pumpability. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.CONCUR.2026.24,
author = {Chen, Weijun and Fu, Yuxi and Zheng, Yangluo},
title = {{Improving Reachability in Vector Addition Systems Through Pumpability}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {24:1--24:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.24},
URN = {urn:nbn:de:0030-drops-273550},
doi = {10.4230/LIPIcs.CONCUR.2026.24},
annote = {Keywords: vector addition system, reachability, pumpability}
}
Document
An MSO Framework for Weak-Memory Verification and Robustness
Abstract
Memory models are formal specifications of concurrent-program executions, accounting for weak behaviors introduced by compiler and architectural optimizations. The increase of their number and complexity has spawned efforts for uniform verification across whole classes of models, by axiomatizing the models in an adequate metatheory that admits a uniform treatment. In this work, we formally study Monadic Second-Order logic (MSO) as a metatheory for weak memory, by proving results on the treewidth and MSO-expressibility of various popular weak-memory models, as this combination allows us to uniformly tackle several verification problems. In summary, our results are as follows.
First, we prove that executions under Sequential Consistency (SC) have bounded treewidth, while already those under Total Store Order (TSO) do not. Second, we prove that a broad range of models, including Release/Acquire and the full RC20, are MSO-axiomatizable, while others, such as Strong Release/Acquire and TSO, are not, unless the Orthogonal Vectors problem - which requires quadratic time under SETH - can be solved in linear time. Finally, we introduce the notion of reads-from robustness, as an extension to recent work on coarse robustness criteria. We show that our treewidth bounds (both upper and lower) have far-reaching algorithmic implications for any of our MSO-axiomatizable models MM: there is an algorithm that, for every program 𝖯, either verifies 𝖯 under MM or reports that 𝖯 is not reads-from robust against MM. Overall, our results establish a rich and versatile theoretical framework for weak-memory verification and robustness.
Cite as
Giovanna Kobus Conrado and Andreas Pavlogiannis. An MSO Framework for Weak-Memory Verification and Robustness. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 25:1-25:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{conrado_et_al:LIPIcs.CONCUR.2026.25,
author = {Conrado, Giovanna Kobus and Pavlogiannis, Andreas},
title = {{An MSO Framework for Weak-Memory Verification and Robustness}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {25:1--25:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.25},
URN = {urn:nbn:de:0030-drops-273568},
doi = {10.4230/LIPIcs.CONCUR.2026.25},
annote = {Keywords: treewidth, monadic second order logic, reads-from robustness}
}
Document
Minimal and Canonical Quotients for Simulation Equivalences
Abstract
Quotients have only been studied for a handful of equivalences in the linear time-branching time spectrum, for which there are results pertaining to canonicity and minimality. We extend these results to weak simulation equivalence and coupled similarity, two closely related equivalences induced by simulation preorders. We describe abstract procedures for transforming an LTS into a unique representative of its equivalence class, and for transforming an LTS into an equivalent state- and transition-minimal LTS. Moreover, we show the minimisation problem is NP-complete.
Cite as
Eduardo Costa Martins and Tim A. C. Willemse. Minimal and Canonical Quotients for Simulation Equivalences. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{costamartins_et_al:LIPIcs.CONCUR.2026.26,
author = {Costa Martins, Eduardo and Willemse, Tim A. C.},
title = {{Minimal and Canonical Quotients for Simulation Equivalences}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {26:1--26:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.26},
URN = {urn:nbn:de:0030-drops-273725},
doi = {10.4230/LIPIcs.CONCUR.2026.26},
annote = {Keywords: Coupled Similarity, Weak Simulation, Minimisation}
}
Document
Wheeler Bisimulations
Abstract
Over the years, bisimulations have emerged as a pervasive paradigm, finding applications in numerous areas, including concurrency theory, model checking, automata theory, logic, programming languages and category theory. In this paper, we establish a connection between bisimulations and data compression. More precisely, we study the relationship between bisimulations and Wheeler automata (Alanko et al., SODA 2020), a class of automata that has received considerable attention in recent years. The standard notion of bisimulation is not appropriate, so we introduce Wheeler bisimulations, that is, bisimulations that respect the convex structure of the considered Wheeler automata. We show that Wheeler bisimilarity induces a unique minimal Wheeler NFA (analogously to standard bisimulations). In particular, in the deterministic case, we retrieve the minimal Wheeler deterministic automaton of a given language. We also show that the minimal Wheeler NFA induced by Wheeler bisimulations can be built in linear time. This is in contrast with standard bisimulations, for which the corresponding minimal NFA can be built in O(m log n) time (where m is the number of edges and n is the number of states) by adapting Paige-Tarjan partition refinement algorithm. Compared to previous state-reduction techniques, our bisimulation-induced construction is the first for which (i) we obtain a canonical Wheeler NFA and (ii) the resulting Wheeler NFA can be built in linear time.
Cite as
Nicola Cotumaccio. Wheeler Bisimulations. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 27:1-27:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cotumaccio:LIPIcs.CONCUR.2026.27,
author = {Cotumaccio, Nicola},
title = {{Wheeler Bisimulations}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {27:1--27:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.27},
URN = {urn:nbn:de:0030-drops-273579},
doi = {10.4230/LIPIcs.CONCUR.2026.27},
annote = {Keywords: Wheeler automata, bisimulation, minimal automata}
}
Document
Monadic Presburger Predicates Have Robust Population Protocols
Abstract
Population protocols are a model of distributed computation in which a collection of indistinguishable finite-state agents interact randomly in pairs to decide a predicate of their initial configuration. The agents decide by achieving a stable consensus on whether the predicate holds or not. It is known that population protocols can decide exactly the predicates expressible in Presburger arithmetic.
Recently, Lossin et al. have introduced a notion of protocol robustness against adversarial crash failures. They show that all atomic Presburger predicates can be decided by robust protocols, and ask whether the same holds for every Presburger predicate. We make progress towards settling this question by proving that all predicates expressible in monadic Presburger arithmetic have robust protocols. In addition, we analyze the cost of robustness in terms of state complexity. We study the ratio between the number of states of the smallest robust protocol for a given predicate and the smallest protocol for it. We show that the cost of robustness is at least double exponential in the size of the predicate, and prove that the robust protocols by Lossin et al. for threshold predicates x ≥ k have optimal state complexity.
Cite as
Philipp Czerner, Javier Esparza, Vincent Fischer, Roland Guttenberg, Julian Pins, and Simon Reilich. Monadic Presburger Predicates Have Robust Population Protocols. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{czerner_et_al:LIPIcs.CONCUR.2026.28,
author = {Czerner, Philipp and Esparza, Javier and Fischer, Vincent and Guttenberg, Roland and Pins, Julian and Reilich, Simon},
title = {{Monadic Presburger Predicates Have Robust Population Protocols}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {28:1--28:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.28},
URN = {urn:nbn:de:0030-drops-273585},
doi = {10.4230/LIPIcs.CONCUR.2026.28},
annote = {Keywords: Population protocols, fault-tolerance, state complexity}
}
Document
Coinductive Reasoning for Parametrized Functors and Monads
Abstract
Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs.
In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters.
Cite as
Ugo Dal Lago and Zeinab Galal. Coinductive Reasoning for Parametrized Functors and Monads. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 29:1-29:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dallago_et_al:LIPIcs.CONCUR.2026.29,
author = {Dal Lago, Ugo and Galal, Zeinab},
title = {{Coinductive Reasoning for Parametrized Functors and Monads}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {29:1--29:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.29},
URN = {urn:nbn:de:0030-drops-273598},
doi = {10.4230/LIPIcs.CONCUR.2026.29},
annote = {Keywords: categorical semantics, parametrized monads, effects, relations, lax extensions, behavioral equivalence, coalgebra, global state}
}
Document
Mean-Payoff-Parity and Lifting Strategies from MDPs to 2-Player Stochastic Games
Abstract
We consider the strategy complexity (i.e., memory and randomization) of optimal strategies in turn-based 2-player zero-sum stochastic games. Results in [Gimbert and Kelmendi, 2023; Richard Mayr et al., 2021] show how to lift optimal memoryless strategies for shift-invariant inverse-submixing objectives from MDPs to 2-player stochastic games with an exponential increase in the number of memory modes. We show the corresponding lower bound, i.e., the extra exponential memory is required in general, even for randomized strategies.
Moreover, we solve the strategy complexity of the well-studied mean-payoff-parity objective (MP > 0 ∩ EPAR) in 2-player stochastic games. This objective is also shift-invariant inverse-submixing, but easier than the worst case for this class. In MDPs, Maximizer has optimal memoryless randomized strategies, while optimal deterministic strategies require exponential memory. However, in stochastic games, optimal randomized strategies require, at least and at most, linear memory (equal to the number of even colors).
Finally, we show that the different construction in [Gimbert and Zielonka, 2009; Patricia Bouyer et al., 2023] for lifting memoryless (resp. finite-memory) deterministic strategies from MDPs (resp. 1-player games) to 2-player games cannot be generalized even to memoryless randomized strategies. We construct a shift-invariant objective where Max and Min each have optimal memoryless randomized strategies in all MDPs, but optimal (randomized) Max strategies still require infinite memory in deterministic 2-player games.
Cite as
Mohan Dantam and Richard Mayr. Mean-Payoff-Parity and Lifting Strategies from MDPs to 2-Player Stochastic Games. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dantam_et_al:LIPIcs.CONCUR.2026.30,
author = {Dantam, Mohan and Mayr, Richard},
title = {{Mean-Payoff-Parity and Lifting Strategies from MDPs to 2-Player Stochastic Games}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {30:1--30:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.30},
URN = {urn:nbn:de:0030-drops-273601},
doi = {10.4230/LIPIcs.CONCUR.2026.30},
annote = {Keywords: MDPs, Stochastic Games, Parity, Mean-payoff, Strategy complexity}
}
Document
On Parameterized Verification over Tree Topologies
Abstract
Parameterized verification of finite-state processes with rendez-vous synchronization is notoriously undecidable when processes are linearly ordered. In this paper we study two kinds of bounds under which we determine the complexity of safety checking over tree topologies. When bounding the depth we obtain that the complexity is related to the fast growing hierarchy. Our second bound limits the alternations between upwards and downwards synchronizations in the tree (phases), and occurs naturally in many concrete settings. If we fix the number of phases then the complexity of safety checking is EXPSPACE complete, and if the number of phases is part of the input it is 2EXPSPACE complete (both for arbitrary depth).
Cite as
Romain Delpy, Anca Muscholl, and Grégoire Sutre. On Parameterized Verification over Tree Topologies. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{delpy_et_al:LIPIcs.CONCUR.2026.31,
author = {Delpy, Romain and Muscholl, Anca and Sutre, Gr\'{e}goire},
title = {{On Parameterized Verification over Tree Topologies}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {31:1--31:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.31},
URN = {urn:nbn:de:0030-drops-273613},
doi = {10.4230/LIPIcs.CONCUR.2026.31},
annote = {Keywords: Concurrent programming, Parameterized verification}
}
Document
Algebraic Characterization of FO-Definable Languages of Higher-Dimensional Automata
Abstract
Higher-dimensional automata (HDA) are a model of concurrency that models simultaneous execution of events using higher dimensional cells. HDA recognize languages of pomsets, a generalization of finite words whose letters are partially ordered. We prove a new algebraic characterization of HDA languages: a language of pomsets is regular if and only if it is the inverse image of a functor from the category of pomsets into a finite category. Furthermore, the language is definable in first-order logic exactly when it is recognized by an aperiodic category, generalizing the McNaughton-Papert theorem to HDA languages. We also investigate a notion of counter-free HDA, and show that if a language is accepted by a counter-free HDA, it must be definable in first-order logic. The converse, however, is still open.
Cite as
Enzo Erlich, Jérémy Ledent, and Krzysztof Ziemiański. Algebraic Characterization of FO-Definable Languages of Higher-Dimensional Automata. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{erlich_et_al:LIPIcs.CONCUR.2026.32,
author = {Erlich, Enzo and Ledent, J\'{e}r\'{e}my and Ziemia\'{n}ski, Krzysztof},
title = {{Algebraic Characterization of FO-Definable Languages of Higher-Dimensional Automata}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {32:1--32:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.32},
URN = {urn:nbn:de:0030-drops-273620},
doi = {10.4230/LIPIcs.CONCUR.2026.32},
annote = {Keywords: Higher-dimensional automata, Pomset languages, McNaughton-Papert theorem, Counter-free HDA, Aperiodic category}
}
Document
Revisiting True Concurrency Bisimilarities: On the Role of Backward Ready Multisets and Why They Are Not Enough for HPB and HHPB
Abstract
Bisimilarities over stable configuration structures can be divided into three families. In the first one - including interleaving, step, pomset, and forward-reverse bisimilarities - no isomorphism is required between the events matched during the bisimulation game. In the second one - including weak history-preserving, weak history-preserving pomset, and weak hereditary history-preserving bisimilarities - a labeling- and causality-preserving isomorphism is required between matched events, which is specific to each pair of configurations related by the bisimulation relation and hence can vary for a matched event from pair to pair. In the third one - including history-preserving and hereditary history-preserving bisimilarities - a single isomorphism is built incrementally, which is therefore fixed for all matched events. We revisit true concurrency bisimilarities by introducing variants that additionally check that the backward ready multisets of related configurations coincide. While the distinguishing power of the bisimilarities of the second and third families does not change, the power of the revised bisimilarities of the first family is equal to that of the bisimilarities of the second family. The latter bisimilarities can thus be characterized by replacing variable isomorphisms with simply counting incoming transitions. In contrast, backward ready multisets are not enough to characterize the third family in the simultaneous presence of autoconcurrency and non-local conflicts. We show that a further check for the existence of diamond and half-diamond substructures is necessary in that case to achieve the same distinguishing power as incremental isomorphisms.
Cite as
Andrea Esposito and Marco Bernardo. Revisiting True Concurrency Bisimilarities: On the Role of Backward Ready Multisets and Why They Are Not Enough for HPB and HHPB. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 33:1-33:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{esposito_et_al:LIPIcs.CONCUR.2026.33,
author = {Esposito, Andrea and Bernardo, Marco},
title = {{Revisiting True Concurrency Bisimilarities: On the Role of Backward Ready Multisets and Why They Are Not Enough for HPB and HHPB}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {33:1--33:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.33},
URN = {urn:nbn:de:0030-drops-273634},
doi = {10.4230/LIPIcs.CONCUR.2026.33},
annote = {Keywords: True Concurrency, Bisimilarity, Configuration Structures, Modal Logic}
}
Document
On the Continuity of the Probabilistic Bisimilarity Distance
Abstract
The probabilistic bisimilarity distance provides a quantitative measure of behavioural difference for labelled Markov chains, but it may be discontinuous under perturbations of the transition probabilities. This lack of continuity undermines its applicability to empirically derived models, where transition probabilities are often approximations. Recently, we introduced robust probabilistic bisimilarity as a sufficient condition for continuity at distance zero. In this paper, we show that it is also a necessary condition, that is, two states are robustly probabilistic bisimilar if and only if their probabilistic bisimilarity distance is small for any small enough perturbation of the transition probabilities. We further extend robustness to non-bisimilar state pairs to establish a complete characterization for continuity of the probabilistic bisimilarity distance. Based on this characterization, we develop a polynomial time algorithm to decide continuity. Finally, we complement our theoretical contributions with an experimental evaluation demonstrating the proposed approach in practice. Our results show that the extra step of deciding continuity requires minimal additional cost when compared to computing the probabilistic bisimilarity distance.
Cite as
Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, and Franck van Breugel. On the Continuity of the Probabilistic Bisimilarity Distance. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 34:1-34:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{fatmi_et_al:LIPIcs.CONCUR.2026.34,
author = {Fatmi, Syyeda Zainab and Kiefer, Stefan and Parker, David and van Breugel, Franck},
title = {{On the Continuity of the Probabilistic Bisimilarity Distance}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {34:1--34:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.34},
URN = {urn:nbn:de:0030-drops-273648},
doi = {10.4230/LIPIcs.CONCUR.2026.34},
annote = {Keywords: probabilistic model checking, labelled Markov chain, probabilistic bisimilarity distance}
}
Document
Threshold-Based Behavioural Distances
Abstract
Behavioural distances generally offer more fine-grained means of comparing quantitative systems than two-valued behavioural equivalences. They often relate to quantitative modal logics that characterize a given behavioural distance in terms of the induced logical distance. We develop a unified framework for behavioural distances and logics induced by a special type of modalities that lift two-valued predicates to quantitative predicates. A typical example is the probability operator, which maps a two-valued predicate A to a quantitative predicate on probability distributions assigning to each distribution the respective probability of A. Correspondingly, the prototypical example of our framework is ε-bisimulation distance of Markov chains, which has recently been shown to coincide with the behavioural distance induced by the popular Lévy-Prokhorov distance on distributions. Other examples include behavioural distance on metric transition systems and Hausdorff behavioural distance on fuzzy transition systems. We establish a number of general results in this framework, including existence and polynomial-time computation of distinguishing formulae in two characteristic modal logics: A two-valued logic with a notion of satisfaction up to ε, and a quantitative logic. These general results instantiate to new results in many of the mentioned examples. Notably, we obtain polynomial-time computation of distinguishing formulae for ε-bisimulation distance of Markov chains in a quantitative logic featuring a "generally" modality used in probabilistic knowledge representation.
Cite as
Jonas Forster, Lutz Schröder, Paul Wild, Barbara König, and Pedro Nora. Threshold-Based Behavioural Distances. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{forster_et_al:LIPIcs.CONCUR.2026.35,
author = {Forster, Jonas and Schr\"{o}der, Lutz and Wild, Paul and K\"{o}nig, Barbara and Nora, Pedro},
title = {{Threshold-Based Behavioural Distances}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {35:1--35:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.35},
URN = {urn:nbn:de:0030-drops-273657},
doi = {10.4230/LIPIcs.CONCUR.2026.35},
annote = {Keywords: Behavioural distance, modal logic, quantitative logic, coalgebra, Sugeno integration}
}
Document
Sure-Almost-Sure and Sure-Limit-Sure Window Mean Payoff in Markov Decision Processes
Abstract
Given rationals α and β, the sure-almost-sure problem for a threshold Boolean objective φ in a Markov decision process (MDP) asks if one can simultaneously ensure that all outcomes of the MDP have φ-value at least α (i.e. sure α satisfaction), and with probability 1 the outcome has φ-value at least β (i.e. almost-sure β satisfaction). The sure-limit-sure problem asks if for all ε > 0, one can simultaneously ensure that all outcomes have φ-value at least α, and with probability at least 1 - ε the outcome has φ-value at least β. Moreover, if simultaneous satisfaction of objectives is possible, then one would also like to construct a strategy (for sure-almost-sure) or a family of strategies (for sure-limit-sure) that achieves this. Even if both sure satisfaction and almost-sure (resp., limit-sure) satisfaction for an objective are known, combining the two is often non-trivial and requires novel techniques and approaches.
In this paper, we solve the sure-almost-sure and sure-limit-sure problems for window mean-payoff objectives. While it is known that almost-sure satisfaction and limit-sure satisfaction for window mean-payoff coincide in MDPs, we show that sure-almost-sure satisfaction is distinct from sure-limit-sure satisfaction. The window mean-payoff objective strengthens the standard mean-payoff objective by requiring that eventually, from every point in the infinite run, the average payoff becomes greater than a given threshold within a finite window length. We study two variants of window mean payoff: in the fixed variant, the window length 𝓁 is given, while in the bounded variant, the length is not given but is required to be bounded throughout the run. We show that the sure-almost-sure problem and the sure-limit-sure problem are both in PTIME for the fixed variant (if 𝓁 is given in unary) and are both in NP ∩ coNP for the bounded variant, matching the computational complexity of sure satisfaction and almost-sure satisfaction when considered separately for these objectives. We also give bounds for the memory requirement of winning strategies for all considered problems.
Cite as
Pranshu Gaba and Shibashis Guha. Sure-Almost-Sure and Sure-Limit-Sure Window Mean Payoff in Markov Decision Processes. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{gaba_et_al:LIPIcs.CONCUR.2026.36,
author = {Gaba, Pranshu and Guha, Shibashis},
title = {{Sure-Almost-Sure and Sure-Limit-Sure Window Mean Payoff in Markov Decision Processes}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {36:1--36:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.36},
URN = {urn:nbn:de:0030-drops-273664},
doi = {10.4230/LIPIcs.CONCUR.2026.36},
annote = {Keywords: Beyond worst-case synthesis, sure-almost-sure satisfaction, window mean payoff, finitary objectives, Markov decision processes}
}
Document
Active Diagnosis with Costs and Rewards
Abstract
Diagnosis is the task of detecting fault occurrences in a partially observed system. Depending on the possible observations, a discrete-event system may be diagnosable or not. Active diagnosis aims at controlling the system to render it diagnosable. In the past, the main analyzed criterion of the quality of an active diagnoser has been the delay between the fault occurrence and its detection. Here we generalize this study by (1) associating costs or rewards with faulty runs, (2) defining three related decision problems, and (3) analyzing their decidability/complexity in the non-deterministic and probabilistic frameworks under several hypotheses. We study non-deterministic and probabilistic semantics and compare their decidability and complexity. In particular, we exhibit one problem decidable for non-deterministic systems but undecidable for probabilistic ones. Furthermore we establish tight lower and upper bounds for the size of the active diagnoser (when it exists).
Cite as
Serge Haddad, Engel Lefaucheux, and Stefan Schwoon. Active Diagnosis with Costs and Rewards. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{haddad_et_al:LIPIcs.CONCUR.2026.37,
author = {Haddad, Serge and Lefaucheux, Engel and Schwoon, Stefan},
title = {{Active Diagnosis with Costs and Rewards}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {37:1--37:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.37},
URN = {urn:nbn:de:0030-drops-273674},
doi = {10.4230/LIPIcs.CONCUR.2026.37},
annote = {Keywords: Partial observation, diagnosis, game and automata theory, controller synthesis, probabilistic discrete event systems}
}
Document
Compositionality in Coalgebraic Trace Semantics
Abstract
A key requirement on any well-behaved process language is its compositionality: behavioural equivalence of processes should be respected by the constructors of the language. Turi and Plotkin’s abstract GSOS provides an elegant bialgebraic framework for modelling rule formats that guarantee compositionality from the outset. Their original results, however, are restricted to compositionality of strong bisimilarity, a rather fine-grained notion of process equivalence. In the present paper, we demonstrate that Turi and Plotkin’s approach also applies to trace equivalence, which only observes external actions of processes. To this end, we revisit the general compositionality result of their original theory and present it in a refined form with regard to the required naturality conditions. This step makes abstract GSOS applicable over Kleisli categories and thereby enables reasoning about compositionality in the setting of coalgebraic trace semantics. As our main contribution, we introduce De Simone laws, a type of GSOS laws over Kleisli categories, and prove that their operational models are compositional for coalgebraic trace equivalence. This result recovers and explains compositionality of the well-known De Simone rule format for labelled transition systems in a natural categorical setting. As a further application, we derive from our general framework a novel De Simone-type format for probabilistic systems, compositional for probabilistic trace equivalence.
Cite as
Robin Jourde, Henning Urbat, Sergey Goncharov, Stelios Tsampas, and Jonas Forster. Compositionality in Coalgebraic Trace Semantics. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{jourde_et_al:LIPIcs.CONCUR.2026.38,
author = {Jourde, Robin and Urbat, Henning and Goncharov, Sergey and Tsampas, Stelios and Forster, Jonas},
title = {{Compositionality in Coalgebraic Trace Semantics}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {38:1--38:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.38},
URN = {urn:nbn:de:0030-drops-273680},
doi = {10.4230/LIPIcs.CONCUR.2026.38},
annote = {Keywords: Coalgebra, Operational Semantics, Process Algebra, Abstract GSOS, Trace Semantics, Rule Formats}
}
Document
From Coalgebraic Determinization to Belief Construction for Partial Observability
Abstract
The belief construction is a fundamental technique for transforming partially observable systems to fully observable ones while preserving the relevant semantics. It plays a central role in the analysis of partially observable systems, in particular partially observable Markov decision processes (POMDPs), which is a central model in artificial intelligence and formal verification. In this paper, we develop a coalgebraic framework for the belief construction. To handle observations categorically, we lift a monad to slice categories and introduce a belief decomposition that reorganizes states according to their observations. This allows us to introduce a coalgebraic generalization of the belief construction, obtained by combining the belief decomposition with the coalgebraic determinization of Silva, Bonchi, Bonsangue, and Rutten. In this framework, we show that the semantics of a partially observable system coincides with that of the corresponding belief coalgebra. We then study when the latter further agrees with the semantics of its fully observable counterpart, and use this to identify conditions under which the semantics of a partially observable system coincides with that of the corresponding fully observable belief system. As a consequence, we recover the standard equivalence between POMDPs and belief MDPs, and obtain a new equivalence result for weighted transition systems with the semimodule monad.
Cite as
Mayuko Kori and Kazuki Watanabe. From Coalgebraic Determinization to Belief Construction for Partial Observability. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 39:1-39:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kori_et_al:LIPIcs.CONCUR.2026.39,
author = {Kori, Mayuko and Watanabe, Kazuki},
title = {{From Coalgebraic Determinization to Belief Construction for Partial Observability}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {39:1--39:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.39},
URN = {urn:nbn:de:0030-drops-273692},
doi = {10.4230/LIPIcs.CONCUR.2026.39},
annote = {Keywords: coalgebra, coalgebraic determinization, belief construction, POMDP}
}
Document
Classification Under Uncertainty
Abstract
Consider a fixed number of disjoint regular languages L_1,…,L_k ⊆ Σ^*. A classifier for L_1,…,L_k is a transducer that receives each moment t in time an input letter σ_t ∈ Σ and outputs an index in {1,…,k} such that if the word σ_1 ⋯ σ_t, generated so far, is in some (unique) language L_i, then this index is i. Classifiers arise naturally in runtime monitoring and online stream processing, where a system must continuously determine which of several specifications or behaviors is currently being realized. The problem of generating classifiers of minimal size has been well studied.
In many applications, the input alphabet is of the form 2^P, for a finite set P of signals. There, the complexity of classification stems not only from the languages but also from the presence of uncertainty, namely when the valuation to some signals may not be known. We introduce and study classification under uncertainty, where the input words may be partially observed. We consider three sources for uncertainty: (1) Given: the input to the problem specifies which signals may be sensed after each behavior. (2) Privacy: the input includes a list of secret behaviors, and the classifier should restrict sensing so that secrets are not revealed. (3) Budget: Sensing of signals incurs a cost, which the classifier should minimize.
Cite as
Orna Kupferman and Ofer Leshkowitz. Classification Under Uncertainty. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kupferman_et_al:LIPIcs.CONCUR.2026.40,
author = {Kupferman, Orna and Leshkowitz, Ofer},
title = {{Classification Under Uncertainty}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {40:1--40:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.40},
URN = {urn:nbn:de:0030-drops-273705},
doi = {10.4230/LIPIcs.CONCUR.2026.40},
annote = {Keywords: Formal methods, Automata, Incomplete Information}
}
Document
On the Encodability of Reversible Process Calculi
Abstract
Reversibility, allowing one to execute a program not only forwards as usual, but also backwards, has emerged as a fundamental concept in computing, with applications ranging from debugging and fault tolerance to biological and quantum systems. CCSK, a reversible extension of CCS, is a paradigmatic model of reversible concurrent computation. In this paper, we investigate the encodability of CCSK into classical forward-only concurrent models. We establish a separation theorem showing that there is no basic, success-sensitive encoding of CCSK into CCS or the π-calculus, highlighting the strong impact of reversibility on expressive power. We then present an encoding of CCSK processes with only top-level parallel composition into the internal π-calculus, correct up to strong bisimilarity. We also identify a fundamental limitation: no parallel-preserving encoding of CCSK (with arbitrary parallel composition) into the π-calculus can be correct up to strong bisimilarity. Finally, we provide a parallel-preserving encoding correct under a weaker behavioural correspondence: weak mutual simulation. Our findings extend the literature of encodability results to reversible process calculi.
Cite as
Ivan Lanese, Claudio Antares Mezzina, Iain Phillips, Irek Ulidowski, and Shoji Yuen. On the Encodability of Reversible Process Calculi. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 41:1-41:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lanese_et_al:LIPIcs.CONCUR.2026.41,
author = {Lanese, Ivan and Mezzina, Claudio Antares and Phillips, Iain and Ulidowski, Irek and Yuen, Shoji},
title = {{On the Encodability of Reversible Process Calculi}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {41:1--41:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.41},
URN = {urn:nbn:de:0030-drops-273715},
doi = {10.4230/LIPIcs.CONCUR.2026.41},
annote = {Keywords: Reversible computation, Process calculi, Encodings, Impossibility results}
}
Document
Continuous Algebras with Hypotheses
Abstract
In the literature on Kleene algebra (KA), a number of variants have been proposed such as Kleene algebra with tests, commutative KA, bi-KA, and concurrent KA. The equational theories of some of these structures have then been studied in the presence of additional assumptions, called hypotheses. We propose a unifying framework encompassing all the previous structures, as well as regular tree languages. This is done by considering algebras ordered by complete lattices, where least fixpoints can be computed. We provide a canonical model consisting of closed languages, which we prove sound and complete with respect to all continuous models. Then we study quasi-equational axiomatisations. It is illusory to hope for a generic axiomatisation which would be sound and complete for all instances. Instead, we provide a generic axiomatisation which we prove sound and we setup tools that make it possible to get complete ones in a modular way, building on previous works from the literature. We showcase these tools by proving new completeness results for commutative KA, bi-KA, and regular tree languages, in each case extended with various hypotheses.
Cite as
Lukas Mulder, Damien Pous, and Jana Wagemaker. Continuous Algebras with Hypotheses. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 42:1-42:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mulder_et_al:LIPIcs.CONCUR.2026.42,
author = {Mulder, Lukas and Pous, Damien and Wagemaker, Jana},
title = {{Continuous Algebras with Hypotheses}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {42:1--42:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.42},
URN = {urn:nbn:de:0030-drops-273735},
doi = {10.4230/LIPIcs.CONCUR.2026.42},
annote = {Keywords: Kleene algebra, complete lattices, languages, completeness}
}
Document
Prophecy-Based Automated Verification of Message-Passing Programs
Abstract
We propose a fully automated method for verifying functional correctness of message-passing concurrent programs by reducing verification problems to constrained Horn clause (CHC) solving. Inspired by RustHorn’s prophecy-based technique, we represent each sender channel by a list of values to be sent over the channel in the future, which enables modular encoding of sender and receiver threads in CHCs. To capture causal dependencies between different channels, we further attach timestamps to messages. We prove that the resulting reduction is sound and complete: a program is free from assertion failures if and only if the corresponding system of CHCs is satisfiable. We have also implemented a prototype verifier for Rust-like programs and experimentally confirmed the effectiveness of the approach.
Cite as
Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi, Yusuke Matsushita, and Ken Sakayori. Prophecy-Based Automated Verification of Message-Passing Programs. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 43:1-43:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{nagatomi_et_al:LIPIcs.CONCUR.2026.43,
author = {Nagatomi, Takashi and Katsura, Musashi and Kobayashi, Naoki and Matsushita, Yusuke and Sakayori, Ken},
title = {{Prophecy-Based Automated Verification of Message-Passing Programs}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {43:1--43:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.43},
URN = {urn:nbn:de:0030-drops-273747},
doi = {10.4230/LIPIcs.CONCUR.2026.43},
annote = {Keywords: Program verification, message-passing concurrent programs, constrained Horn clauses, prophecies}
}
Document
Positional Properties in Temporal Logic
Abstract
We study positional properties in the context of game-based reactive synthesis. Our motivation stems from having a usable specification logic, for which tractable synthesis is guaranteed. We demonstrate that every ω-regular positional property (with respect to state- or edge-labelled game graphs), is expressible in linear-time temporal logic. Additionally, we provide some necessary and sufficient conditions for when an ω-regular property is positional, and identify well-behaved subclasses of ω-regular positional properties. Using varieties of languages, we prove that no class of ω-regular positional properties can simultaneously contain a prefix-independent property and be closed under Boolean operations. We conclude by discussing the implications on alternating-time temporal logic, where we isolate a few different fragments with tractable model checking, and compare the associated expressivity of such fragments.
Cite as
Jessica Newman and Benjamin Plummer. Positional Properties in Temporal Logic. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 44:1-44:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{newman_et_al:LIPIcs.CONCUR.2026.44,
author = {Newman, Jessica and Plummer, Benjamin},
title = {{Positional Properties in Temporal Logic}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {44:1--44:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.44},
URN = {urn:nbn:de:0030-drops-273755},
doi = {10.4230/LIPIcs.CONCUR.2026.44},
annote = {Keywords: Positionality, Temporal Logic, ATL, Games on graphs}
}
Document
Concurrent Visibility: Higher-Order Concurrency with First-Order Store
Abstract
We propose an Operational Game Semantics for a (call-by-value) concurrent higher-order language with first-order store (references may contain other references or first-order values such as integers or booleans; however they may not store higher-order values such as functions). We adapt the game-semantic notion of visibility, which semantically captures the absence of higher-order references and developed for sequential higher-order languages, to a concurrent setting. We thus define a complete-trace preorder, and prove it sound for the contextual preorder, by introducing a synchronization-based composition of semantic configurations and establishing an observational adequacy result. We also prove completeness for the subset of the language in which functions return first-order values.
In contrast to the case of sequential visibility, in the labeled transition semantics we have to account for the presence of multiple active threads with possibly different visibilities, and of a tree-like structure for managing the dependencies among the threads so created. Moreover, we have to reason on families of traces, rather than single traces, as in concurrent setting the order among certain actions cannot be enforced.
Cite as
Iwan Quémerais, Guilhème Jaber, Ken Sakayori, and Davide Sangiorgi. Concurrent Visibility: Higher-Order Concurrency with First-Order Store. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 45:1-45:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{quemerais_et_al:LIPIcs.CONCUR.2026.45,
author = {Qu\'{e}merais, Iwan and Jaber, Guilh\`{e}me and Sakayori, Ken and Sangiorgi, Davide},
title = {{Concurrent Visibility: Higher-Order Concurrency with First-Order Store}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {45:1--45:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.45},
URN = {urn:nbn:de:0030-drops-273760},
doi = {10.4230/LIPIcs.CONCUR.2026.45},
annote = {Keywords: Operational game semantics, higher-order effectful programs, mutable store}
}
Document
GKAT with Hoare Hypotheses
Abstract
Guarded Kleene Algebra with Tests (GKAT) is a variant of Kleene algebra which allows for reasoning about simple imperative programs, and which features a decision procedure for program equivalence in nearly linear time. In the current paper, we address the challenge of reasoning under assumptions about these programs. In particular, we develop a form of Hoare hypotheses, which allow modelling basic domain knowledge on pre- and postconditions of uninterpreted basic programs, and which are well-developed for classical Kleene algebra but not yet for GKAT. We show that the resulting axiomatisation is sound and complete. We then extend Hoare hypotheses to the more general form of word hypotheses. Based on an automata-theoretic approach, we show that equivalence of GKAT under word hypotheses is efficiently decidable.
Cite as
Jurriaan Rot, Todd Schmid, and Jana Wagemaker. GKAT with Hoare Hypotheses. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 46:1-46:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{rot_et_al:LIPIcs.CONCUR.2026.46,
author = {Rot, Jurriaan and Schmid, Todd and Wagemaker, Jana},
title = {{GKAT with Hoare Hypotheses}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {46:1--46:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.46},
URN = {urn:nbn:de:0030-drops-273770},
doi = {10.4230/LIPIcs.CONCUR.2026.46},
annote = {Keywords: Kleene Algebra, GKAT, Hypotheses}
}
Document
Graded Semantics of Nominal Systems
Abstract
Nominal automata models and transition systems serve as formalisms for languages and processes carrying data, and as such relate closely to classical register-based models. The paradigm of name allocation in nominal systems helps alleviate the pervasive computational hardness of register-based models in a tradeoff between expressiveness and computational tractability. For instance, regular nondeterministic nominal automata (RNNAs) correspond, under their local freshness semantics, to a form of lossy register automata. Unlike the full register automaton model, RNNAs allow for inclusion checking in elementary complexity (parametrized PSpace); similarly, trace inclusion in the underlying nominal transition systems is in parametrized PSpace. In the present work, we develop a unified algebraic treatment of spectra of behavioural equivalences on nominal systems in the framework of graded monads, working in the setting of universal coalgebra. In particular, we extend the associated notion of graded algebraic theory to the nominal setting, and use this to give an algebraic axiomatization of the (linear-time) global and local freshness semantics of nominal systems with name allocation. As an illustration of the benefits of graded monads, we develop a nominal version of the generic game characterization of graded semantics, which we instantiate to obtain trace equivalence games for nominal transition systems under global and local freshness semantics.
Cite as
Hannes Schulze, Lutz Schröder, and Üsame Cengiz. Graded Semantics of Nominal Systems. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 47:1-47:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{schulze_et_al:LIPIcs.CONCUR.2026.47,
author = {Schulze, Hannes and Schr\"{o}der, Lutz and Cengiz, \"{U}same},
title = {{Graded Semantics of Nominal Systems}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {47:1--47:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.47},
URN = {urn:nbn:de:0030-drops-273785},
doi = {10.4230/LIPIcs.CONCUR.2026.47},
annote = {Keywords: Nominal transition systems, trace semantics, graded monads, coalgebra, nominal algebra}
}
Document
On the Complexity of Robust Markov Decision Processes and Bisimulation Metrics
Abstract
Robust Markov decision processes (RMDPs) extend standard Markov decision processes (MDPs) to account for uncertainty in the transition probabilities. RMDPs have an uncertainty set that defines a set of possible transition functions, each of which induces a standard MDP. The natural objective in an RMDP is to optimize the discounted cumulative reward under the worst-case transition function in the uncertainty set. We study the complexity of the associated threshold problem for RMDPs with polytopic uncertainty sets in halfspace representation. Previous results focused on approximating the optimum or restricted attention to specific subclasses of RMDPs, such as interval MDPs or L_∞-RMDPs. Our contributions are threefold: (1) For (s,a)-rectangular RMDPs, we prove that robust policy evaluation is in P via robust linear programming, and that the threshold problem is in NP. As a corollary, robust policy iteration is a polynomial-time algorithm for these RMDPs when the discount factor is fixed. (2) For s-rectangular RMDPs, we show that the threshold problem is in PSPACE via the first-order theory of the reals. (3) We establish lower bounds by reducing both parity games and bisimulation metrics between MDP states to the RMDP threshold problem. A polynomial-time algorithm for the threshold problem would resolve the long-standing open question of whether parity games can be solved in polynomial time. The reduction from bisimulation metrics also yields a practical benefit: it allows us to apply robust policy iteration as a more efficient alternative to the standard fixed-point iteration, as our empirical evaluation demonstrates.
Cite as
Marnix Suilen and Guillermo A. Pérez. On the Complexity of Robust Markov Decision Processes and Bisimulation Metrics. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 48:1-48:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{suilen_et_al:LIPIcs.CONCUR.2026.48,
author = {Suilen, Marnix and P\'{e}rez, Guillermo A.},
title = {{On the Complexity of Robust Markov Decision Processes and Bisimulation Metrics}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {48:1--48:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.48},
URN = {urn:nbn:de:0030-drops-273796},
doi = {10.4230/LIPIcs.CONCUR.2026.48},
annote = {Keywords: Robust Markov decision processes, bisimulation metrics}
}
Document
Bisimulations and Modal Logics for Higher Dimensional Automata
Abstract
Higher-Dimensional Automata (HDAs) provide a geometric model of true concurrency. While hereditary history-preserving (hhp) bisimilarity is the finest behavioural equivalence in van Glabbeek’s spectrum, no modal logic has previously characterised it on HDAs. We introduce several new intermediate equivalences that sit strictly between ST- and hhp-bisimilarity. We show how separating similarity and subsumption of paths leads to a clean formulation of these equivalences, and we present a modal logic that characterises hhp-bisimilarity. Natural fragments characterise ST-bisimilarity and the intermediate notions.
Cite as
Safa Zouari, Rob van Glabbeek, and Krzysztof Ziemiański. Bisimulations and Modal Logics for Higher Dimensional Automata. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 49:1-49:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{zouari_et_al:LIPIcs.CONCUR.2026.49,
author = {Zouari, Safa and van Glabbeek, Rob and Ziemia\'{n}ski, Krzysztof},
title = {{Bisimulations and Modal Logics for Higher Dimensional Automata}},
booktitle = {37th International Conference on Concurrency Theory (CONCUR 2026)},
pages = {49:1--49:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-447-5},
ISSN = {1868-8969},
year = {2026},
volume = {391},
editor = {Sokolova, Ana and Totzke, Patrick},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.49},
URN = {urn:nbn:de:0030-drops-273809},
doi = {10.4230/LIPIcs.CONCUR.2026.49},
annote = {Keywords: higher-dimensional automata, bisimilarity, history-preserving bisimulation, modal logic, concurrency theory}
}