23 Search Results for "Doyen, Laurent"

Document
Invited Talk
DOI: 10.4230/LIPIcs.STACS.2026.1
Query Languages for Machine-Learning Models (Invited Talk)

Authors: Martin Grohe

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
In my invited talk and this accompanying paper, I discuss two logics for weighted finite structures: first-order logic with summation (FO(SUM)) and its recursive extension IFP(SUM). These logics originate from foundational work by Grädel, Gurevich, and Meer in the 1990s. In recent joint work with Standke, Steegmans, and Van den Bussche, we have investigated these logics as query languages for machine learning models, specifically neural networks, which are naturally represented as weighted graphs. I present illustrative examples of queries to neural networks that can be expressed in these logics and discuss fundamental results on their expressiveness and computational complexity.
Cite as

Martin Grohe. Query Languages for Machine-Learning Models (Invited Talk). In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{grohe:LIPIcs.STACS.2026.1,
  author =	{Grohe, Martin},
  title =	{{Query Languages for Machine-Learning Models}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{1:1--1:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.1},
  URN =		{urn:nbn:de:0030-drops-254904},
  doi =		{10.4230/LIPIcs.STACS.2026.1},
  annote =	{Keywords: Expressive power of query languages, fixed-point logics, weighted structures, neural networks, explainable AI}
}
Document
DOI: 10.4230/LIPIcs.STACS.2026.34
Algorithm and Strategy Construction for Sure-Almost-Sure Stochastic Parity Games

Authors: Laurent Doyen and Shibashis Guha

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
We consider turn-based stochastic two-player games with a combination of a parity condition that must hold surely, that is in all possible outcomes, and of a parity condition that must hold almost-surely, that is with probability 1. The problem of deciding the existence of a winning strategy in such games is central in the framework of synthesis beyond worst-case where a hard requirement that must hold surely is combined with a softer requirement. Recent works showed that the problem is coNP-complete, and infinite-memory strategies are necessary in general, even in one-player games (i.e., Markov decision processes). However, memoryless strategies are sufficient for the opponent player. Despite these comprehensive results, the known algorithmic solution enumerates all memoryless strategies of the opponent, which is exponential in all cases, and does not construct a winning strategy when one exists. We present a recursive algorithm, based on a characterisation of the winning region, that gives a deeper insight into the problem. In particular, we show how to construct a winning strategy to achieve the combination of sure and almost-sure parity, and we derive new complexity and memory bounds for special classes of the problem, defined by fixing the index of either of the two parity conditions.
Cite as

Laurent Doyen and Shibashis Guha. Algorithm and Strategy Construction for Sure-Almost-Sure Stochastic Parity Games. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{doyen_et_al:LIPIcs.STACS.2026.34,
  author =	{Doyen, Laurent and Guha, Shibashis},
  title =	{{Algorithm and Strategy Construction for Sure-Almost-Sure Stochastic Parity Games}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{34:1--34:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.34},
  URN =		{urn:nbn:de:0030-drops-255230},
  doi =		{10.4230/LIPIcs.STACS.2026.34},
  annote =	{Keywords: stochastic games, parity objectives, reactive synthesis}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.30
Reward Interfaces with Best-Effort Implementations

Authors: Rafael Dewes and Rayna Dimitrova

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Interface theories, notably interface automata, serve as expressive frameworks for component-based design, specifying component behavior and interaction in concurrent systems. Traditional interface formalisms specify assumptions that a component’s environment must satisfy and the guarantees that each component provides. This qualitative view of component interaction based on imposing strict assumptions and Boolean guarantees may, however, not be expressive enough to capture the system’s allowed or desired behaviors under different environments. In this paper, we introduce reward interfaces to support component-based design while accommodating multi-valued correctness requirements and adaptive best-effort satisfaction of component’s guarantees. Building upon interface automata, our framework enables modeling a rich class of quantitative component specifications. We propose formal notions of implementation, refinement and compatibility for reward interfaces. We study a class of reward interfaces with automata-based representations, for which we provide algorithms for checking compatibility and refinement, and existence of best-effort implementations. Our framework offers a comprehensive approach to reward interface specification and design.
Cite as

Rafael Dewes and Rayna Dimitrova. Reward Interfaces with Best-Effort Implementations. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dewes_et_al:LIPIcs.CSL.2026.30,
  author =	{Dewes, Rafael and Dimitrova, Rayna},
  title =	{{Reward Interfaces with Best-Effort Implementations}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{30:1--30:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.30},
  URN =		{urn:nbn:de:0030-drops-254553},
  doi =		{10.4230/LIPIcs.CSL.2026.30},
  annote =	{Keywords: Component-based design, interface automata, quantitative specifications}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.33
A Zone-Based Algorithm for Timed Parity Games

Authors: Gilles Geeraerts, Frédéric Herbreteau, Jean-François Raskin, and Alexis Reynouard

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
This paper revisits timed games by building upon the semantics introduced in "The Element of Surprise in Timed Games" [Luca de Alfaro et al., 2003]. We introduce some modifications to this semantics for two primary reasons: firstly, we recognize instances where the original semantics appears counterintuitive in the context of controller synthesis; secondly, we present methods to develop efficient zone-based algorithms. Our algorithm successfully addresses timed parity games, and we have implemented it using UPPAAL’s zone library. This prototype effectively demonstrates the feasibility of a zone-based algorithm for parity objectives and a rich semantics for timed interactions between the players.
Cite as

Gilles Geeraerts, Frédéric Herbreteau, Jean-François Raskin, and Alexis Reynouard. A Zone-Based Algorithm for Timed Parity Games. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{geeraerts_et_al:LIPIcs.FSTTCS.2025.33,
  author =	{Geeraerts, Gilles and Herbreteau, Fr\'{e}d\'{e}ric and Raskin, Jean-Fran\c{c}ois and Reynouard, Alexis},
  title =	{{A Zone-Based Algorithm for Timed Parity Games}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{33:1--33:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.33},
  URN =		{urn:nbn:de:0030-drops-251140},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.33},
  annote =	{Keywords: Timed Parity Games, Realtime Controller Synthesis}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.14
Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications

Authors: Ashwin Bhaskar and M. Praveen

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
When multiple software components interact via method calls, we may want to ensure that the order of invoked methods and the arguments provided adhere to some specification. The classic problem associated with interface automata checks for the existence of a mediator whose intention is to act as a buffer in between method invocations so that invocations do not go unanswered. We extend the base model underlying interface automata, enabling them to exchange integer values - one automaton generates an integer value and outputs it by firing a generating transition and another automaton receives the value by synchronously firing a receiving transition. Transitions in the automata can have guards with linear order constraints on the exchanged values, influencing which methods can or can not be invoked later. So the generated values influence the sequences of invocations that are enabled. We specify desirable properties of the sequence of method calls and the arguments passed to them using an extension of Linear Temporal Logic (LTL). We consider the interoperability problem, which is to check if it is possible to generate integer values in such a way that all enabled sequences satisfy the given specification. We show that the interoperability problem is undecidable in general, even when there are only two participating automata. We show decidability in the case where guards on generating transitions can only have equality constraints on the exchanged value (but receiving transitions can continue to have linear order constraints). We model this problem as a game between two players, one trying to generate integer values such that violating sequences are disabled while the other player tries to dig out violating sequences that are enabled. Interoperability is equivalent to the first player having a winning strategy. We solve this game via a finite abstraction, which results in a symbolic game. We then show that winning strategies for the symbolic game can be translated to winning strategies for the original game over integers.
Cite as

Ashwin Bhaskar and M. Praveen. Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bhaskar_et_al:LIPIcs.FSTTCS.2025.14,
  author =	{Bhaskar, Ashwin and Praveen, M.},
  title =	{{Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.14},
  URN =		{urn:nbn:de:0030-drops-250962},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.14},
  annote =	{Keywords: Distributed Systems, Interface Automata, Registers, Parity Games}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.13
Synthesising Full-Information Protocols

Authors: Dietmar Berwanger, Laurent Doyen, and Thomas Soullard

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
We study a communication model where processes reveal their entire local information whenever they interact. However, the system involves an indeterminate environment that may control when a communication event occurs and which participants are involved. As a result, the amount of information a process may receive at once is unbounded. Such full-information protocols are common in the distributed-computing literature. Here, we consider synchronous systems, modelled as infinite games with imperfect information played on finite graphs. We present a decision procedure for the synthesis of a process with an ω-regular specification in a system where the other participating processes are fixed. The challenge lies in constructing a finite representation of information trees with unbounded branching. Our construction is non-elementary in the size of the problem instance, and we establish a matching non-elementary lower bound for the complexity of the synthesis problem.
Cite as

Dietmar Berwanger, Laurent Doyen, and Thomas Soullard. Synthesising Full-Information Protocols. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berwanger_et_al:LIPIcs.FSTTCS.2025.13,
  author =	{Berwanger, Dietmar and Doyen, Laurent and Soullard, Thomas},
  title =	{{Synthesising Full-Information Protocols}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.13},
  URN =		{urn:nbn:de:0030-drops-250930},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.13},
  annote =	{Keywords: Infinite Games on Finite Graphs, Imperfect Information, Reactive Processes, Distributed Synthesis, Dynamic Networks}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.31
Games with ω-Automatic Preference Relations

Authors: Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
This paper investigates Nash equilibria (NEs) in multi-player turn-based games on graphs, where player preferences are modeled as ω-automatic relations via deterministic parity automata. Unlike much of the existing literature, which focuses on specific reward functions, our results apply to any preference relation definable by an ω-automatic relation. We analyze the computational complexity of determining the existence of an NE (possibly under some constraints), verifying whether a given strategy profile forms an NE, and checking whether a specific outcome can be realized by an NE. When a (constrained) NE exists, we show that there always exists one with finite-memory strategies. Finally, we explore fundamental properties of ω-automatic relations and their implications in the existence of equilibria.
Cite as

Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin. Games with ω-Automatic Preference Relations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.MFCS.2025.31,
  author =	{Bruy\`{e}re, V\'{e}ronique and Grandmont, Christophe and Raskin, Jean-Fran\c{c}ois},
  title =	{{Games with \omega-Automatic Preference Relations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.31},
  URN =		{urn:nbn:de:0030-drops-241381},
  doi =		{10.4230/LIPIcs.MFCS.2025.31},
  annote =	{Keywords: Games played on graphs, Nash equilibrium, \omega-automatic relations, \omega-recognizable relations, constrained Nash equilibria existence problem}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.12
The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives

Authors: Véronique Bruyère, Jean-François Raskin, Alexis Reynouard, and Marie Van Den Bogaard

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
This paper studies the rational synthesis problem for multi-player games played on graphs when rational players are following subgame perfect equilibria. In these games, one player, the system, declares his strategy upfront, and the other players, composing the environment, then rationally respond by playing strategies forming a subgame perfect equilibrium. We study the complexity of the rational synthesis problem when the players have ω-regular objectives encoded as parity objectives. Our algorithm is based on an encoding into a three-player game with imperfect information, showing that the problem is in 2ExpTime. When the number of environment players is fixed, the problem is in ExpTime and is NP- and coNP-hard. Moreover, for a fixed number of players and reachability objectives, we get a polynomial algorithm.
Cite as

Véronique Bruyère, Jean-François Raskin, Alexis Reynouard, and Marie Van Den Bogaard. The Non-Cooperative Rational Synthesis Problem for SPEs and ω-Regular Objectives. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2025.12,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Reynouard, Alexis and Van Den Bogaard, Marie},
  title =	{{The Non-Cooperative Rational Synthesis Problem for SPEs and \omega-Regular Objectives}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.12},
  URN =		{urn:nbn:de:0030-drops-239622},
  doi =		{10.4230/LIPIcs.CONCUR.2025.12},
  annote =	{Keywords: non-zero-sum games, subgame perfect equilibria, rational synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.16
Expectation in Stochastic Games with Prefix-Independent Objectives

Authors: Laurent Doyen, Pranshu Gaba, and Shibashis Guha

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Stochastic two-player games model systems with an environment that is both adversarial and stochastic. In this paper, we study the expected value of bounded quantitative prefix-independent objectives in the context of stochastic games. We show a generic reduction from the expectation problem to linearly many instances of the almost-sure satisfaction problem for threshold Boolean objectives. The result follows from partitioning the vertices of the game into so-called value classes where each class consists of vertices of the same value. Our procedure further entails that the memory required by both players to play optimally for the expectation problem is no more than the memory required by the players to play optimally for the almost-sure satisfaction problem for a corresponding threshold Boolean objective. We show the applicability of the framework to compute the expected window mean-payoff measure in stochastic games. The window mean-payoff measure strengthens the classical mean-payoff measure by computing the mean payoff over windows of bounded length that slide along an infinite path. We show that the decision problem to check if the expected window mean-payoff value is at least a given threshold is in UP ∩ coUP when the window length is given in unary.
Cite as

Laurent Doyen, Pranshu Gaba, and Shibashis Guha. Expectation in Stochastic Games with Prefix-Independent Objectives. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{doyen_et_al:LIPIcs.CONCUR.2025.16,
  author =	{Doyen, Laurent and Gaba, Pranshu and Guha, Shibashis},
  title =	{{Expectation in Stochastic Games with Prefix-Independent Objectives}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{16:1--16:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.16},
  URN =		{urn:nbn:de:0030-drops-239668},
  doi =		{10.4230/LIPIcs.CONCUR.2025.16},
  annote =	{Keywords: Stochastic games, finitary objectives, mean payoff, reactive synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.21
Quantitative Language Automata

Authors: Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA 𝒜 obtains a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained by nondeterministic runs of 𝒜 over w. We introduce quantitative language automata (QLAs) that define functions from language generators (i.e., implementations) to values, where a language generator can be nonprobabilistic, defining a set of infinite words, or probabilistic, defining a probability measure over infinite words. A QLA consists of a QWA and an aggregator function. For example, given a QWA 𝒜, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest lower bound assigned by 𝒜 to any word in L. For boolean value sets, QWAs define boolean properties of traces, and QLAs define boolean properties of sets of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a specification language for a generalization of hyperproperties, called quantitative hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty assigns a value to each set (resp. distribution) G of traces, e.g., the minimal (resp. expected) average response time exhibited by the traces in G. We give several examples of quantitative hyperproperties and investigate three paradigmatic problems for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem, given a QLA 𝔸 and an implementation G, we ask for the value that 𝔸 assigns to G. In the nonemptiness (resp. universality) problem, given a QLA 𝔸 and a value k, we ask whether 𝔸 assigns at least k to some (resp. every) language. We provide a comprehensive picture of decidability for these problems for QLAs with common aggregators as well as their restrictions to ω-regular languages and trace distributions generated by finite-state Markov chains.
Cite as

Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç. Quantitative Language Automata. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2025.21,
  author =	{Henzinger, Thomas A. and Kebis, Pavol and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
  title =	{{Quantitative Language Automata}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{21:1--21:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.21},
  URN =		{urn:nbn:de:0030-drops-239718},
  doi =		{10.4230/LIPIcs.CONCUR.2025.21},
  annote =	{Keywords: Quantitative hyperproperties, quantitative automata, automata-based verification}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.14
Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Authors: Kazuki Watanabe

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game with a given compositional structure and solve it efficiently as a divide-and-conquer algorithm by exploiting its compositional structure. Building on our recent progress in open Markov decision processes, we introduce Pareto fronts of open parity games, offering a framework for multi-objective solutions. We establish the positional determinacy of open parity games with respect to their Pareto fronts through a novel translation method. Our translation converts an open parity game into a parity game tailored to a given single-objective. Furthermore, we present a simple algorithm for solving open parity games, derived from this translation that allows the application of existing efficient algorithms for parity games. Expanding on this foundation, we develop a compositional algorithm for string diagrams of parity games.
Cite as

Kazuki Watanabe. Pareto Fronts for Compositionally Solving String Diagrams of Parity Games. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{watanabe:LIPIcs.CALCO.2025.14,
  author =	{Watanabe, Kazuki},
  title =	{{Pareto Fronts for Compositionally Solving String Diagrams of Parity Games}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.14},
  URN =		{urn:nbn:de:0030-drops-235734},
  doi =		{10.4230/LIPIcs.CALCO.2025.14},
  annote =	{Keywords: parity game, compositionality, string diagram}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.160
Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages

Authors: Olivier Idir and Karoliina Lehtinen

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
The parity index problem of tree automata asks, given a regular tree language L and a set of priorities J, is L J-feasible, that is, recognised by a nondeterministic parity automaton with priorities J? This is a long-standing open problem, of which only a few sub-cases and variations are known to be decidable. In a significant but technically difficult step, Colcombet and Löding reduced the problem to the uniform universality of distance-parity automata. In this article, we revisit the index problem using tools from the parity game literature. We add some counters to Lehtinen’s register game, originally used to solve parity games in quasipolynomial time, and use this novel game to characterise J-feasibility. This provides a alternative proof to Colcombet and Löding’s reduction. We then provide a second characterisation, based on the notion of attractor decompositions and the complexity of their structure, as measured by a parameterised version of their Strahler number, which we call n-Strahler number. Finally, we rephrase this result using the notion of universal tree extended to automata: a guidable automaton recognises a [1,2j]-feasible language if and only if it admits a universal tree with n-Strahler number j, for some n. In particular, a language recognised by a guidable automaton {A} is Büchi-feasible if and only if there is a uniform bound n ∈ ℕ such that all trees in the language admit an accepting run with an attractor decomposition of width bounded by n. Equivalently, the language is Büchi-feasible if and only if {A} admits a finite universal tree. While we do not solve the decidability of the index problem, our work makes the state-of-the-art more accessible and brings to light the deep relationships between the J-feasibility of a language and attractor decompositions, universal trees and Lehtinen’s register game.
Cite as

Olivier Idir and Karoliina Lehtinen. Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 160:1-160:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{idir_et_al:LIPIcs.ICALP.2025.160,
  author =	{Idir, Olivier and Lehtinen, Karoliina},
  title =	{{Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{160:1--160:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.160},
  URN =		{urn:nbn:de:0030-drops-235377},
  doi =		{10.4230/LIPIcs.ICALP.2025.160},
  annote =	{Keywords: Tree automata, parity automata, Mostowski index, Strahler number, attractor decomposition, universal trees}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.164
A Collapse of the Parity Index Hierarchy of Tree Automata, Based on Cantor-Bendixson Ranks

Authors: Karoliina Lehtinen and Nathan Lhote

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Over words, nondeterministic Büchi automata and alternating weak automata are as expressive as parity automata with any number of priorities. Over trees, the Büchi acceptance condition is strictly weaker and the more priorities we allow, the more languages parity automata can recognise. We say that on words, the parity-index hierarchies of nondeterministic and alternating automata collapse to the Büchi and weak level, respectively, while both are infinite over trees. We ask when is Büchi enough?, that is, on which classes of trees are nondeterministc Büchi automata as expressive as parity automata. Similarly for alternating weak automata. We work in the setting of unranked unordered trees, in which there is no order among the children of nodes. We find that for nondeterministic and alternating automata, the parity-index hierarchy collapses to the Büchi level and weak level, respectively, for any class of trees of finitely bounded Cantor-Bendixson rank, a topological measure of tree complexity. Over trees of countable Cantor-Bendixson rank, (a.k.a. thin trees) the parity-index hierarchy of both nondeterministic and alternating automata collapses to the level [1,2,3], as was already known for ordered trees. These results are in some sense optimal: on the class of trees of finite but unbounded Cantor-Bendixson rank, two priorities do not suffice to recognise all parity-recognisable languages, even for alternating automata.
Cite as

Karoliina Lehtinen and Nathan Lhote. A Collapse of the Parity Index Hierarchy of Tree Automata, Based on Cantor-Bendixson Ranks. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 164:1-164:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lehtinen_et_al:LIPIcs.ICALP.2025.164,
  author =	{Lehtinen, Karoliina and Lhote, Nathan},
  title =	{{A Collapse of the Parity Index Hierarchy of Tree Automata, Based on Cantor-Bendixson Ranks}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{164:1--164:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.164},
  URN =		{urn:nbn:de:0030-drops-235418},
  doi =		{10.4230/LIPIcs.ICALP.2025.164},
  annote =	{Keywords: Parity tree automata, alternating automata, Cantor-Bendixson rank}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.150
The Value Problem for Multiple-Environment MDPs with Parity Objective

Authors: Krishnendu Chatterjee, Laurent Doyen, Jean-François Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
We consider multiple-environment Markov decision processes (MEMDP), which consist of a finite set of MDPs over the same state space, representing different scenarios of transition structure and probability. The value of a strategy is the probability to satisfy the objective, here a parity objective, in the worst-case scenario, and the value of an MEMDP is the supremum of the values achievable by a strategy. We show that deciding whether the value is 1 is a PSPACE-complete problem, and even in P when the number of environments is fixed, along with new insights to the almost-sure winning problem, which is to decide if there exists a strategy with value 1. Pure strategies are sufficient for theses problems, whereas randomization is necessary in general when the value is smaller than 1. We present an algorithm to approximate the value, running in double exponential space. Our results are in contrast to the related model of partially-observable MDPs where all these problems are known to be undecidable.
Cite as

Krishnendu Chatterjee, Laurent Doyen, Jean-François Raskin, and Ocan Sankur. The Value Problem for Multiple-Environment MDPs with Parity Objective. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 150:1-150:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.ICALP.2025.150,
  author =	{Chatterjee, Krishnendu and Doyen, Laurent and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
  title =	{{The Value Problem for Multiple-Environment MDPs with Parity Objective}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{150:1--150:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.150},
  URN =		{urn:nbn:de:0030-drops-235272},
  doi =		{10.4230/LIPIcs.ICALP.2025.150},
  annote =	{Keywords: Markov decision processes, imperfect information, randomized strategies, limit-sure winning}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.145
Reducing Stochastic Games to Semidefinite Programming

Authors: Manuel Bodirsky, Georg Loho, and Mateusz Skomra

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
We present a polynomial-time reduction from max-average constraints to the feasibility problem for semidefinite programs. This shows that Condon’s simple stochastic games, stochastic mean payoff games, and in particular mean payoff games and parity games can all be reduced to semidefinite programming.
Cite as

Manuel Bodirsky, Georg Loho, and Mateusz Skomra. Reducing Stochastic Games to Semidefinite Programming. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 145:1-145:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.ICALP.2025.145,
  author =	{Bodirsky, Manuel and Loho, Georg and Skomra, Mateusz},
  title =	{{Reducing Stochastic Games to Semidefinite Programming}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{145:1--145:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.145},
  URN =		{urn:nbn:de:0030-drops-235224},
  doi =		{10.4230/LIPIcs.ICALP.2025.145},
  annote =	{Keywords: Mean-payoff games, stochastic games, semidefinite programming, max-average constraints, max-atom problem}
}
  • Refine by Type
  • 23 Document/PDF
  • 14 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 13 2025
  • 1 2024
  • 1 2020
  • 1 2019
  • Show More...

  • Refine by Author
  • 10 Doyen, Laurent
  • 5 Raskin, Jean-François
  • 3 Berwanger, Dietmar
  • 3 Chatterjee, Krishnendu
  • 2 Bruyère, Véronique
  • Show More...

  • Refine by Series/Journal
  • 22 LIPIcs
  • 1 LITES

  • Refine by Classification
  • 5 Theory of computation → Automata over infinite objects
  • 3 Theory of computation → Formal languages and automata theory
  • 3 Theory of computation → Logic and verification
  • 3 Theory of computation → Probabilistic computation
  • 2 Computing methodologies → Planning under uncertainty
  • Show More...

  • Refine by Keyword
  • 2 Imperfect Information
  • 2 Infinite Games on Finite Graphs
  • 2 imperfect information
  • 2 randomized strategies
  • 2 reactive synthesis
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact