arXiv subjects

Raphaël Berthon

Publications and source records attributed to Raphaël Berthon.

14 recordsLinked to original sources

arXiv2026

Positional Determinacy with Colored Vertices: a 1-to-2-Player Lift

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.

cs.GT↗

arXiv2026

Verification of Robust Multi-Agent Systems

Stochastic multi-agent systems are a central modeling framework for autonomous controllers, communication protocols, and cyber-physical infrastructures. In many such systems, however, transition probabilities are only estimated from data and may therefore be partially unknown or subject to perturbations. In this paper, we study the verification of robust strategies in stochastic multi-agent systems with imperfect information, in which coalitions must satisfy a temporal specification while dealing with uncertain system transitions, partial observation, and adversarial agents. By focusing on bounded-memory strategies, we introduce a robust variant of the model-checking problem for a probabilistic, observation-based extension of Alternating-time Temporal Logic. We characterize the complexity of this problem under different notions of perturbation, thereby clarifying the computational cost of robustness in stochastic multi-agent verification and supporting the use of bounded-memory strategies in uncertain environments.

cs.LO↗

arXiv2025

Natural Strategic Ability in Stochastic Multi-Agent Systems

Strategies synthesized using formal methods can be complex and often require infinite memory, which does not correspond to the expected behavior when trying to model Multi-Agent Systems (MAS). To capture such behaviors, natural strategies are a recently proposed framework striking a balance between the ability of agents to strategize with memory and the model-checking complexity, but until now has been restricted to fully deterministic settings. For the first time, we consider the probabilistic temporal logics PATL and PATL* under natural strategies (NatPATL and NatPATL*, resp.). As main result we show that, in stochastic MAS, NatPATL model-checking is NP-complete when the active coalition is restricted to deterministic strategies. We also give a 2NEXPTIME complexity result for NatPATL* with the same restriction. In the unrestricted case, we give an EXPSPACE complexity for NatPATL and 3EXPSPACE complexity for NatPATL*.

cs.LO↗

arXiv2025

A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games

Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from stochastic parity games (SPGs) to SSGs have been presented in the literature through the use of multiple intermediate game models, a direct and simple reduction has been notably absent. This paper introduces a novel and direct polynomial-time reduction from quantitative SPGs to quantitative SSGs. By leveraging a gadget-based transformation that effectively removes the priority function, we construct an SSG that simulates the behavior of a given SPG. We formally establish the correctness of our direct reduction. Furthermore, we demonstrate that under binary encoding this reduction is polynomial, thereby directly corroborating the known $\textbf{NP}\,\mathbf{\cap}\,\textbf{coNP}$ complexity of SPGs and providing new understanding in the relationship between parity and reachability objectives in turn-based stochastic games.

cs.GT↗

arXiv2024

Markov Decision Processes with Sure Parity and Multiple Reachability Objectives

This paper considers the problem of finding strategies that satisfy a mixture of sure and threshold objectives in Markov decision processes. We focus on a single $ω$-regular objective expressed as parity that must be surely met while satisfying $n$ reachability objectives towards sink states with some probability thresholds too. We consider three variants of the problem: (a) strict and (b) non-strict thresholds on all reachability objectives, and (c) maximizing the thresholds with respect to a lexicographic order. We show that (a) and (c) can be reduced to solving parity games, and (b) can be solved in $\sf{EXPTIME}$. Strategy complexities as well as algorithms are provided for all cases.

cs.GT↗

arXiv2021

Active Learning of Sequential Transducers with Side Information about the Domain

Active learning is a setting in which a student queries a teacher, through membership and equivalence queries, in order to learn a language. Performance on these algorithms is often measured in the number of queries required to learn a target, with an emphasis on costly equivalence queries. In graybox learning, the learning process is accelerated by foreknowledge of some information on the target. Here, we consider graybox active learning of subsequential string transducers, where a regular overapproximation of the domain is known by the student. We show that there exists an algorithm using string equation solvers that uses this knowledge to learn subsequential string transducers with a better guarantee on the required number of equivalence queries than classical active learning.

cs.FL↗

arXiv2020

Alternating Tree Automata with Qualitative Semantics

We study alternating automata with qualitative semantics over infinite binary trees: alternation means that two opposing players construct a decoration of the input tree called a run, and the qualitative semantics says that a run of the automaton is accepting if almost all branches of the run are accepting. In this paper we prove a positive and a negative result for the emptiness problem of alternating automata with qualitative semantics. The positive result is the decidability of the emptiness problem for the case of Büchi acceptance condition. An interesting aspect of our approach is that we do not extend the classical solution for solving the emptiness problem of alternating automata, which first constructs an equivalent non-deterministic automaton. Instead, we directly construct an emptiness game making use of imperfect information. The negative result is the undecidability of the emptiness problem for the case of co-Büchi acceptance condition. This result has two direct consequences: the undecidability of monadic second-order logic extended with the qualitative path-measure quantifier, and the undecidability of the emptiness problem for alternating tree automata with non-zero semantics, a recently introduced probabilistic model of alternating tree automata.

cs.FL↗

arXiv2020

Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes

In this paper, we consider algorithms to decide the existence of strategies in MDPs for Boolean combinations of objectives. These objectives are omega-regular properties that need to be enforced either surely, almost surely, existentially, or with non-zero probability. In this setting, relevant strategies are randomized infinite memory strategies: both infinite memory and randomization may be needed to play optimally. We provide algorithms to solve the general case of Boolean combinations and we also investigate relevant subcases. We further report on complexity bounds for these problems.

cs.LO↗

arXiv2020

Strategy Logic with Imperfect Information

We introduce an extension of Strategy Logic for the imperfect-information setting, called SLii, and study its model-checking problem. As this logic naturally captures multi-player games with imperfect information, this problem is undecidable; but we introduce a syntactical class of "hierarchical instances" for which, intuitively, as one goes down the syntactic tree of the formula, strategy quantifications are concerned with finer observations of the model, and we prove that model-checking SLii restricted to hierarchical instances is decidable. To establish this result we go through QCTL, an intermediary, "low-level" logic much more adapted to automata techniques. QCTL is an extension of CTL with second-order quantification over atomic propositions. We extend it to the imperfect information setting by parameterising second-order quantifiers with observations. While the model-checking problem of QCTLii is, in general, undecidable, we identify a syntactic fragment of hierarchical formulas and prove, using an automata-theoretic approach, that it is decidable. We apply our result to solve complex strategic problems in the imperfect-information setting. We first show that the existence of Nash equilibria for deterministic strategies is decidable in games with hierarchical information. We also introduce distributed rational synthesis, a generalisation of rational synthesis to the imperfect-information setting. Because it can easily be expressed in our logic, our main result provides solution to this problem in the case of hierarchical information.

cs.LO↗

arXiv2019

Monadic Second-Order Logic with Path-Measure Quantifier is Undecidable

We prove that the theory of Monadic Second-Order logic (MSO) of the infinite binary tree extended with qualitative path-measure quantifier is undecidable. This quantifier says that the set of infinite paths in the tree that satisfies some formula has Lebesgue-measure one. To do this we prove that the emptiness problem of qualitative universal parity tree automata is undecidable. Qualitative means that a run of a tree automaton is accepting if the set of paths in the run that satisfy the acceptance condition has Lebesgue-measure one.

cs.LO↗

arXiv2018

Quantified CTL with imperfect information

Quantified CTL (QCTL) is a well-studied temporal logic that extends CTL with quantification over atomic propositions. It has recently come to the fore as a powerful intermediary framework to study logics for strategic reasoning. We extend it to include imperfect information by parameterising quantifiers with an observation that defines how well they observe the model, thus constraining their behaviour. We consider two different semantics, one related to the notion of no memory, the other to perfect recall. We study the expressiveness of our logic, and show that it coincides with MSO for the first semantics and with MSO with equal level for the second one. We establish that the model-checking problem is Pspace-complete for the first semantics. While it is undecidable for the second one, we identify a syntactic fragment, defined by a notion of hierarchical formula, which we prove to be decidable thanks to an automata-theoretic approach.

cs.LO↗

arXiv2018

Decidability results for ATL* with imperfect information and perfect recall

Alternating-time Temporal Logic (ATL*) is a central logic for multiagent systems. Its extension to the imperfect information setting (ATL*i ) is well known to have an undecidable model-checking problem when agents have perfect recall. Studies have thus mostly focused either on agents without memory, or on alternative semantics to retrieve decidability. In this work we establish new decidability results for agents with perfect recall: We first prove a meta-theorem that allows the transfer of decidability results for classes of multiplayer games with imperfect information, such as games with hierarchical observation, to the model-checking problem for ATL*i . We then establish that model checking ATL* with strategy context and imperfect information is decidable when restricted to hierarchical instances.

cs.LO↗

arXiv2018

Strategy Logic with Imperfect Information

We introduce an extension of Strategy Logic for the imperfect-information setting, called SLii, and study its model-checking problem. As this logic naturally captures multi-player games with imperfect information, the problem turns out to be undecidable. We introduce a syntactical class of "hierarchical instances" for which, intuitively, as one goes down the syntactic tree of the formula, strategy quantifications are concerned with finer observations of the model. We prove that model-checking SLii restricted to hierarchical instances is decidable. This result, because it allows for complex patterns of existential and universal quantification on strategies, greatly generalises previous ones, such as decidability of multi-player games with imperfect information and hierarchical observations, and decidability of distributed synthesis for hierarchical systems. To establish the decidability result, we introduce and study QCTL*ii, an extension of QCTL* (itself an extension of CTL* with second-order quantification over atomic propositions) by parameterising its quantifiers with observations. The simple syntax of QCTL* ii allows us to provide a conceptually neat reduction of SLii to QCTL*ii that separates concerns, allowing one to forget about strategies and players and focus solely on second-order quantification. While the model-checking problem of QCTL*ii is, in general, undecidable, we identify a syntactic fragment of hierarchical formulas and prove, using an automata-theoretic approach, that it is decidable. The decidability result for SLii follows since the reduction maps hierarchical instances of SLii to hierarchical formulas of QCTL*ii .

cs.LO↗

arXiv2017

Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes

The beyond worst-case synthesis problem was introduced recently by Bruyère et al. [BFRR14]: it aims at building system controllers that provide strict worst-case performance guarantees against an antagonistic environment while ensuring higher expected performance against a stochastic model of the environment. Our work extends the framework of [BFRR14] and follow-up papers, which focused on quantitative objectives, by addressing the case of $ω$-regular conditions encoded as parity objectives, a natural way to represent functional requirements of systems. We build strategies that satisfy a main parity objective on all plays, while ensuring a secondary one with sufficient probability. This setting raises new challenges in comparison to quantitative objectives, as one cannot easily mix different strategies without endangering the functional properties of the system. We establish that, for all variants of this problem, deciding the existence of a strategy lies in ${\sf NP} \cap {\sf coNP}$, the same complexity class as classical parity games. Hence, our framework provides additional modeling power while staying in the same complexity class. [BFRR14] Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In Ernst W. Mayr and Natacha Portier, editors, 31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, March 5-8, 2014, Lyon, France, volume 25 of LIPIcs, pages 199-213. Schloss Dagstuhl - Leibniz - Zentrum fuer Informatik, 2014.

cs.LO↗