Author name cluster

Raphaël Berthon

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

AAMAS Conference 2025 Conference Paper

Robust Strategies for Stochastic Multi-Agent Systems

Raphaël Berthon
Joost-Pieter Katoen
Munyque Mittelmann
Aniello Murano

The precise probabilities of stochastic systems are often partially unknown and may face perturbations. Finding a strategy in this setting is difficult, as it requires dealing with uncertainty on the system transitions while interacting with other agents. In this paper, we introduce the robust model checking problem for Multi-Agent Systems, in which agents play strategies that ensure the satisfaction of a specification is satisfied, even though the system probabilities are uncertain. We consider specifications in a variant of Alternatingtime Temporal Logic with bounded memory.

PDF

AAAI Conference 2024 Conference Paper

Natural Strategic Ability in Stochastic Multi-Agent Systems

Raphaël Berthon
Joost-Pieter Katoen
Munyque Mittelmann
Aniello Murano

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 complexity of the model-checking problem, 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∗). 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*.

PDF Details DOI

Highlights Conference 2020 Conference Abstract

Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes

Raphaël Berthon

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 almost surely or with non-zero probability, as usual in MDPs, surely as in games, or existentially as in automata. 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.

PDF Details

Highlights Conference 2018 Conference Abstract

Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes

Raphaël Berthon

ABSTRACT. The beyond worst-case synthesis problem was introduced recently by Bruyère et al. : 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. This talk presents an extension of this framework which focused on quantitative objectives, by addressing the case of omega-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 NP \cap coNP, the same complexity class as classical parity games. Hence, our framework provides additional modeling power while staying in the same complexity class.

Details