35 citations · 56 across the 13 of their papers we have counts for
14 papers
Positional Determinacy with Colored Vertices: a 1-to-2-Player Lift
Raphaël Berthon, Stéphane Le Roux
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 tha…
Verification of Robust Multi-Agent Systems
Raphaël Berthon, Joost-Pieter Katoen, Munyque Mittelmann +1
Stochastic multi-agent systems are a central modeling framework for autonomous controllers, communication protocols, and cyber-physical infrastructures. In many such systems, howev…
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
Raphaël Berthon, Joost-Pieter Katoen, Zihan Zhou
Significant progress has been recently achieved in developing efficient solutions for simple stochastic games (SSGs), focusing on reachability objectives. While reductions from sto…
Markov Decision Processes with Sure Parity and Multiple Reachability Objectives
Raphaël Berthon, Joost-Pieter Katoen, Tobias Winkler
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 object…
Natural Strategic Ability in Stochastic Multi-Agent Systems
Raphaël Berthon, Joost-Pieter Katoen, Munyque Mittelmann +1
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 Sy…
Active Learning of Sequential Transducers with Side Information about the Domain
Raphaël Berthon, Adrien Boiret, Guillermo A. Perez +1
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 ofte…
Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes
Raphaël Berthon, Shibashis Guha, Jean-François Raskin
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…
Strategy Logic with Imperfect Information
Raphaël Berthon, Bastien Maubert, Aniello Murano +2
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…
Alternating Tree Automata with Qualitative Semantics
Raphaël Berthon, Nathanaël Fijalkow, Emmanuel Filiot +7
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 r…
Monadic Second-Order Logic with Path-Measure Quantifier is Undecidable
Raphaël Berthon, Emmanuel Filiot, Shibashis Guha +5
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…
Strategy Logic with Imperfect Information
Raphaël Berthon, Bastien Maubert, Aniello Murano +2
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…
Decidability results for ATL* with imperfect information and perfect recall
Raphaël Berthon, Bastien Maubert, Aniello Murano
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 m…
Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes
Raphaël Berthon, Mickael Randour, Jean-François Raskin
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 guaran…
Quantified CTL with imperfect information
Raphaël Berthon, Bastien Maubert, Aniello Murano
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 fr…