Bastien Maubert

AIJ Journal 2025 Journal Article

Formal verification and synthesis of mechanisms for social choice

• Munyque Mittelmann
• Bastien Maubert
• Aniello Murano
• Laurent Perrussel

Mechanism Design (MD) aims at defining resources allocation protocols that satisfy a predefined set of properties, and Auction Mechanisms are of foremost importance. Core properties of mechanisms, such as strategy-proofness or budget balance, involve: (i) complex strategic concepts such as Nash equilibria, (ii) quantitative aspects such as utilities, and often (iii) imperfect information, with agents' private valuations. We demonstrate that Strategy Logic provides a formal framework fit to model mechanisms and express such properties, and we show that it can be used either to automatically check that a given mechanism satisfies some property (verification), or automatically produce a mechanism that does (synthesis). To do so, we consider a quantitative and variant of Strategy Logic. We first show how to express the implementation of social choice functions. Second, we show how fundamental mechanism properties can be expressed as logical formulas, and thus evaluated by model checking. We then prove that model checking for this particular variant of Strategy Logic can be done in polynomial space. Next, we show how MD can be rephrased as a synthesis problem, where mechanisms are automatically synthesized from a partial or complete logical specification. We solve the automated synthesis of mechanisms in two cases: when the number of actions is bounded, and when agents play in turns. Finally, we provide examples of auction design based for each of these two cases. The benefit of our approach in relation to classical MD is to provide a general framework for addressing a large spectrum of MD problems, which is not tailored to a particular setting or problem.

AAAI Conference 2023 Conference Paper

Formal Verification of Bayesian Mechanisms

• Munyque Mittelmann
• Bastien Maubert
• Aniello Murano
• Laurent Perrussel

In this paper, for the first time, we study the formal verification of Bayesian mechanisms through strategic reasoning. We rely on the framework of Probabilistic Strategy Logic (PSL), which is well-suited for representing and verifying multi-agent systems with incomplete information. We take advantage of the recent results on the decidability of PSL model checking under memoryless strategies, and reduce the problem of formally verifying Bayesian mechanisms to PSL model checking. We show how to encode Bayesian-Nash equilibrium and economical properties, and illustrate our approach with different kinds of mechanisms.

IJCAI Conference 2022 Conference Paper

Automated Synthesis of Mechanisms

• Munyque Mittelmann
• Bastien Maubert
• Aniello Murano
• Laurent Perrussel

Mechanism Design aims to design a game so that a desirable outcome is reached regardless of agents' self-interests. In this paper, we show how this problem can be rephrased as a synthesis problem, where mechanisms are automatically synthesized from a partial or complete specification in a high-level logical language. We show that Quantitative Strategy Logic is a perfect candidate for specifying mechanisms as it can express complex strategic and quantitative properties. We solve automated mechanism design in two cases: when the number of actions is bounded, and when agents play in turn.

KR Conference 2022 Conference Paper

Public and Private Affairs in Strategic Reasoning

• Nathanaël Fijalkow
• Bastien Maubert
• Aniello Murano
• Sasha Rubin
• Moshe Vardi

Do agents know each others’ strategies? In multi-process software construction, each process has access to the processes already constructed; but in typical human-robot interactions, a human may not announce its strategy to the robot (indeed, the human may not even know their own strategy). This question has often been overlooked when modeling and reasoning about multi-agent systems. In this work, we study how it impacts strategic reasoning. To do so we consider Strategy Logic (SL), a well-established and highly expressive logic for strategic reasoning. Its usual semantics, which we call “white-box semantics”, models systems in which agents “broadcast” their strategies. By adding imperfect information to the evaluation games for the usual semantics, we obtain a new semantics called “black-box semantics”, in which agents keep their strategies private. We consider the model-checking problem and show that the black-box semantics has much lower complexity than white-box semantics for an important fragment of Strategy Logic.

LAMAS&SR Workshop 2022 Workshop Paper

Strategic Reasoning in Automated Mechanism Design

• Bastien Maubert
• Munyque Mittelmann
• Aniello Murano
• Laurent Perrussel

IJCAI Conference 2021 Conference Paper

Reasoning About Agents That May Know Other Agents’ Strategies

• Francesco Belardinelli
• Sophia Knight
• Alessio Lomuscio
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

We study the semantics of knowledge in strategic reasoning. Most existing works either implicitly assume that agents do not know one another’s strategies, or that all strategies are known to all; and some works present inconsistent mixes of both features. We put forward a novel semantics for Strategy Logic with Knowledge that cleanly models whose strategies each agent knows. We study how adopting this semantics impacts agents’ knowledge and strategic ability, as well as the complexity of the model-checking problem.

KR Conference 2021 Conference Paper

Strategic Reasoning in Automated Mechanism Design

• Bastien Maubert
• Munyque Mittelmann
• Aniello Murano
• Laurent Perrussel

Mechanism Design aims at defining mechanisms that satisfy a predefined set of properties, and Auction Mechanisms are of foremost importance. Core properties of mechanisms, such as strategy-proofness or budget-balance, involve: (i) complex strategic concepts such as Nash equilibria, (ii) quantitative aspects such as utilities, and often (iii) imperfect information, with agents’ private valuations. We demonstrate that Strategy Logic provides a formal framework fit to model mechanisms, express such properties, and verify them. To do so, we consider a quantitative and epistemic variant of Strategy Logic. We first show how to express the implementation of social choice functions. Second, we show how fundamental mechanism properties can be expressed as logical formulas, and thus evaluated by model checking. Finally, we prove that model checking for this particular variant of Strategy Logic can be done in polynomial space.

IJCAI Conference 2020 Conference Paper

Assume-Guarantee Synthesis for Prompt Linear Temporal Logic

• Nathanaël Fijalkow
• Bastien Maubert
• Aniello Murano
• Moshe Vardi

Prompt-LTL extends Linear Temporal Logic with a bounded version of the ``eventually'' operator to express temporal requirements such as bounding waiting times. We study assume-guarantee synthesis for prompt-LTL: the goal is to construct a system such that for all environments satisfying a first prompt-LTL formula (the assumption) the system composed with this environment satisfies a second prompt-LTL formula (the guarantee). This problem has been open for a decade. We construct an algorithm for solving it and show that, like classical LTL synthesis, it is 2-EXPTIME-complete.

Highlights Conference 2020 Conference Abstract

Assume-Guarantee Synthesis for Prompt Linear Temporal Logic

• Bastien Maubert

Prompt-LTL extends Linear Temporal Logic with a bounded version of the “eventually” operator to express temporal requirements such as bounding waiting times. We study assume-guarantee synthesis for prompt-LTL: the goal is to construct a system such that for all environments satisfying a first prompt-LTL formula (the assumption) the system composed with this environment satisfies a second prompt-LTL formula (the guarantee). This problem has been open for a decade. We construct an algorithm for solving it and show that, like classical LTL synthesis, it is 2-EXPTIME-complete.

IJCAI Conference 2020 Conference Paper

Concurrent Games in Dynamic Epistemic Logic

• Bastien Maubert
• Sophie Pinchinat
• Francois Schwarzentruber
• Silvia Stranieri

Action models of Dynamic Epistemic Logic (DEL) represent precisely how actions are perceived by agents. DEL has recently been used to define infinite multi-player games, and it was shown that they can be solved in some cases. However, the dynamics being defined by the classic DEL update product for individual actions, only turn-based games have been considered so far. In this work we define a concurrent DEL product, propose a mechanism to resolve conflicts between actions, and define concurrent DEL games. As in the turn-based case, the obtained concurrent infinite game arenas can be finitely represented when all actions are public, or all are propositional. Thus we identify cases where the strategic epistemic logic ATL*K can be model checked on such games.

ECAI Conference 2020 Conference Paper

Dynamic Epistemic Logic Games with Epistemic Temporal Goals

• Bastien Maubert
• Aniello Murano
• Sophie Pinchinat
• François Schwarzentruber
• Silvia Stranieri

Dynamic Epistemic Logic (DEL) is a logical framework in which one can describe in great detail how actions are perceived by the agents, and how they affect the world. DEL games were recently introduced as a way to define classes of games with imperfect information where the actions available to the players are described very precisely. This framework makes it possible to define easily, for instance, classes of games where players can only use public actions or public announcements. These games have been studied for reachability objectives, where the aim is to reach a situation satisfying some epistemic property expressed in epistemic logic; several (un)decidability results have been established. In this work we show that the decidability results obtained for reachability objectives extend to a much more general class of winning conditions, namely those expressible in the epistemic temporal logic LTLK. To do so we establish that the infinite game structures generated by DEL public actions are regular, and we describe how to obtain finite representations on which we rely to solve them.

KR Conference 2020 Conference Paper

Nondeterministic Strategies and their Refinement in Strategy Logic

• Giuseppe De Giacomo
• Bastien Maubert
• Aniello Murano

Nondeterministic strategies are strategies (or protocols, or plans) that, given a history in a game, assign a set of possible actions, all of which are winning. An important problem is that of refining such strategies. For instance, given a nondeterministic strategy that allows only safe executions, refine it to, additionally, eventually reach a desired state of affairs. We show that strategic problems involving strategy refinement can be solved elegantly in the framework of Strategy Logic (SL), a very expressive logic to reason about strategic abilities. Specifically, we introduce an extension of SL with nondeterministic strategies and an operator expressing strategy refinement. We show that model checking this logic can be done at no additional computational cost with respect to standard SL, and can be used to solve a variety of problems such as synthesis of maximally permissive strategies or refinement of Nash equilibria.

ECAI Conference 2020 Conference Paper

Reasoning About Quality and Fuzziness of Strategic Behaviours

• Patricia Bouyer
• Orna Kupferman
• Nicolas Markey
• Bastien Maubert
• Aniello Murano
• Giuseppe Perelli

IJCAI Conference 2019 Conference Paper

Probabilistic Strategy Logic

• Benjamin Aminof
• Marta Kwiatkowska
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

We introduce Probabilistic Strategy Logic, an extension of Strategy Logic for stochastic systems. The logic has probabilistic terms that allow it to express many standard solution concepts, such as Nash equilibria in randomised strategies, as well as constraints on probabilities, such as independence. We study the model-checking problem for agents with perfect- and imperfect-recall. The former is undecidable, while the latter is decidable in space exponential in the system and triple-exponential in the formula. We identify a natural fragment of the logic, in which every temporal operator is immediately preceded by a probabilistic operator, and show that it is decidable in space exponential in the system and the formula, and double-exponential in the nesting depth of the probabilistic terms. Taking a fixed nesting depth, this gives a fragment that still captures many standard solution concepts, and is decidable in exponential space.

IJCAI Conference 2019 Conference Paper

Reachability Games in Dynamic Epistemic Logic

• Bastien Maubert
• Sophie Pinchinat
• François Schwarzentruber

We define reachability games based on Dynamic Epistemic Logic (DEL), where the players? actions are finely described as DEL action models. We first consider the setting where a controller with perfect information interacts with an environment and aims at reaching some desired state of knowledge regarding the observers of the system. We study the problem of existence of a strategy for the controller, which generalises the classic epistemic planning problem, and we solve it for several types of actions such as public announcements and public actions. We then consider a yet richer setting where observers themselves are players, whose strategies must be based on their observations. We establish several decidability and undecidability results for the problem of existence of a distributed strategy, depending on the type of actions the players can use, and relate them to results from the literature on multiplayer games with imperfect information.

AAMAS Conference 2019 Conference Paper

Reasoning about Changes of Observational Power in Logics of Knowledge and Time

• Aurèle Barrière
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

We study dynamic changes of agents’ observational power in logics of knowledge and time. We consider CTL∗K, the extension of CTL∗ with knowledge operators, and enrich it with a new operator that models a change in an agent’s way of observing the system. We extend the classic semantics of knowledge for agents with perfect recall to account for changes of observational power, and we show that this new operator increases the expressivity of CTL∗K. We reduce the model-checking problem for our logic to that for CTL∗K, which is known to be decidable. This provides a solution to the model-checking problem for our logic, but it is not optimal, and we provide a direct model-checking procedure with better complexity.

IJCAI Conference 2019 Conference Paper

Reasoning about Quality and Fuzziness of Strategic Behaviours

• Patricia Bouyer
• Orna Kupferman
• Nicolas Markey
• Bastien Maubert
• Aniello Murano
• Giuseppe Perelli

We introduce and study SL[F], a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an SL[F] formula is a real value in [0, 1], reflecting ``how much'' or ``how well'' the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[F] in quantitative reasoning about multi-agent systems, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for ourlogic, based on a quantitative extension of Quantified CTL*.

IJCAI Conference 2019 Conference Paper

The Complexity of Model Checking Knowledge and Time

• Laura Bozzelli
• Bastien Maubert
• Aniello Murano

We establish the precise complexity of the model checking problem for the main logics of knowledge and time. While this problem was known to be non-elementary for agents with perfect recall, with a number of exponentials that increases with the alternation of knowledge operators, the precise complexity of the problem when the maximum alternation is fixed has been an open problem for twenty years. We close it by establishing improved upper bounds for CTL* with knowledge, and providing matching lower bounds that also apply for epistemic extensions of LTL and CTL.

KR Conference 2018 Short Paper

Changing Observations in Epistemic Temporal Logic

• Aurèle Barrière
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

We study dynamic changes of agents’ observational power in logics of knowledge and time. We consider CTL∗ K, the extension of CTL∗ with knowledge operators, and enrich it with a new operator that models a change in an agent’s way of observing the system. We extend the classic semantics of knowledge for agents with perfect recall to account for changes of observation, and we show that this new operator strictly increases the expressivity of CTL∗ K. We also provide a modelchecking procedure for the logic we introduce, which has the same complexity as the best known model-checking procedure for the less expressive logic CTL∗ K.

CSL Conference 2018 Conference Paper

Quantifying Bounds in Strategy Logic

• Nathanaël Fijalkow
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multi-agent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define Bounded-Outcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the model-checking problems for both these logics.

KR Conference 2018 Conference Paper

Reasoning about Knowledge and Strategies

• Bastien Maubert
• Aniello Murano

Distributed systems are often open systems, i. e., they interact with an environment and must react appropriately to actions taken by this environment. As a result, if we take the analogy where processors are players of a game, and processes are strategies for the processors, the task of synthesising distributed protocols can be seen as synthesising winning strategies in multi-player games with imperfect information. This analogy between the two settings is well known, and Ladner and Reif already wrote in (Ladner and Reif 1986) that “Distributed protocols are equivalent to (i. e., can be formally modelled as) games”. To reason about a certain type of game-related properties in distributed systems, Alternating-time Temporal Logic (ATL) was introduced (Alur, Henzinger, and Kupferman 2002). It can express the existence of strategies for coalitions of players in multi-player games, but cannot express some important game-theoretic concepts, such as the existence of Nash equilibria. To remedy this, Strategy Logic (SL) (Chatterjee, Henzinger, and Piterman 2010; Mogavero et al. 2014) was defined. Treating strategies as explicit first-order objects makes it very expressive, and it can for instance talk about Nash equilibria in a very natural way. These logics have been studied both for players with perfect information and players with imperfect information, and in the latter case either with the assumption that agents have no memory, or that they remember everything they observe. This last assumption, called perfect recall, is the one usually considered in distributed synthesis (Pnueli and Rosner 1990) and games with imperfect information (Reif 1984), and it is also central in logics of knowledge and time (Fagin et al. 1995). It is the one we consider in this work. In order to reason about knowledge and strategic abilities in distributed systems, epistemic temporal logics and strategic logics have been combined. In particular, both ATL and SL have been extended with knowledge operators (van der Hoek and Wooldridge 2003; Jamroga and van der Hoek 2004; Belardinelli 2015; Dima, Enea, and Guelev 2010; Belardinelli et al. 2017a; 2017b). However, few decidable cases are known for the model checking of these logics with imperfect information and perfect recall. This is not surprising since strategic logics typically can express the existence of distributed strategies, a problem known to be undecidable for perfect recall, already for purely temporal specifications (Peterson and Reif 1979; Pnueli and Rosner 1990). Two distinct semantics have been considered for knowledge in the context of strategic reasoning, depending on whether players know each other’s strategy or not. In the former case, that we call the informed semantics, distributed synthesis for epistemic temporal specifications is undecidable, already on systems with hierarchical information. However, for the other, uninformed semantics, the problem is decidable on such systems. In this work we generalise this result by introducing an epistemic extension of Strategy Logic with imperfect information. The semantics of knowledge operators is uninformed, and captures agents that can change observation power when they change strategies. We solve the model-checking problem on a class of “hierarchical instances”, which provides a solution to a vast class of strategic problems with epistemic temporal specifications, such as distributed or rational synthesis, on hierarchical systems.

Highlights Conference 2018 Conference Abstract

Reasoning about Knowledge and Strategies

• Bastien Maubert

ABSTRACT. Two distinct semantics have been considered for knowledge in the context of strategic reasoning, depending on whether players know each other’s strategy or not. In the former case, that we call the informed semantics, distributed synthesis for epistemic temporal specifications is undecidable, already on systems with hierarchical information. However, for the other, uninformed semantics, the problem is decidable on such systems. In this work we generalise this result by introducing an epistemic extension of Strategy Logic with imperfect information. The semantics of knowledge operators is uninformed, and captures agents that can change observation power when they change strategies. We solve the model-checking problem on a class of "hierarchical instances", which provides a solution to a vast class of strategic problems with epistemic temporal specifications, such as distributed or rational synthesis, on hierarchical systems.

AAMAS Conference 2017 Conference Paper

Decidability Results for ATL* with Imperfect Information and Perfect Recall

• Raphaë l Berthon
• Bastien Maubert
• Aniello Murano

IJCAI Conference 2016 Conference Paper

On the Impact of Modal Depth in Epistemic Planning

• Tristan Charrier
• Bastien Maubert
• Franc
• ccedil; ois Schwarzentruber

Epistemic planning is a variant of automated planning in the framework of dynamic epistemic logic. In recent works, the epistemic planning problem has been proved to be undecidable when preconditions of events can be epistemic formulas of arbitrary complexity, and in particular arbitrary modal depth. It is known however that when preconditions are propositional (and there are no postconditions), the problem is between PSPACE and EXPSPACE. In this work we bring two new pieces to the picture. First, we prove that the epistemic planning problem with propositional preconditions and without postconditions is in PSPACE, and is thus PSPACE-complete. Second, we prove that very simple epistemic preconditions are enough to make the epistemic planning problem undecidable: preconditions of modal depth at most two suffice.

Highlights Conference 2015 Conference Abstract

Relating paths in transition systems: the fall of the modal mu-calculus

• Bastien Maubert

We revisit Janin and Walukiewicz’s classic result on the expressive completeness of the modal mu-calculus w. r. t. MSO, when transition systems are equipped with a binary relation over paths. We obtain two natural extensions of MSO and the mu-calculus: MSO with path relation and the jumping mu-calculus. While “bounded-memory” binary relations bring about no extra expressivity to either of the two logics, “unbounded-memory” binary relations make the bisimulation-invariant fragment of MSO with path relation more expressive than the jumping mu-calculus: the existence of winning strategies in games with imperfect-information inhabits the gap.

I&C Journal 2015 Journal Article

Uniform strategies, rational relations and jumping automata

• Laura Bozzelli
• Bastien Maubert
• Sophie Pinchinat

A general concept of uniform strategies has recently been proposed as a relevant notion in game theory for computer science, which subsumes various notions from the literature. It relies on properties involving sets of plays in two-player turn-based arenas equipped with arbitrary binary relations between plays; these properties are expressed in a language based on CTL ⁎ with a quantifier over related plays. There are two semantics for our quantifier, a strict one and a full one, that we study separately. Regarding the strict semantics, the existence of a uniform strategy is undecidable for rational binary relations, but introducing jumping tree automata and restricting attention to recognizable relations allows us to establish a 2-Exptime-complete complexity – and still capture a class of two-player imperfect-information games with epistemic temporal objectives. Regarding the full semantics, relying on information set automata we establish that the existence of a uniform strategy is decidable for rational relations and we provide a nonelementary synthesis procedure. We also exhibit an essentially optimal subclass of rational relations for which the problem becomes 2-Exptime-complete. Considering rich classes of relations makes the theory of uniform strategies powerful: it directly entails various results in logics of knowledge and time, some of them already known, and others new.

Highlights Conference 2014 Conference Abstract

Automata Techniques for Epistemic Protocol Synthesis in DEL

• Bastien Maubert

In this talk we describe how automata techniques can be applied to problems studied in Dynamic Epistemic Logic, such as epistemic planning. To do so, we first remark that repeatedly executing ad infinitum a propositional event model from an initial epistemic model yields a relational structure that can be finitely represented with automata. This correspondence, together with recent results on uniform strategies, allows us to give an alternative decidability proof of the epistemic planning problem for propositional events, with as by-products accurate upper-bounds on its time complexity, and the possibility to synthesize a finite word automaton that describes the set of all solution plans. In fact, using automata techniques enables us to solve a much more general problem, that we introduce and call epistemic protocol synthesis.

JELIA Conference 2012 Conference Paper

Generalized DEL-Sequents

• Guillaume Aucher
• Bastien Maubert
• François Schwarzentruber

Abstract Let us consider a sequence of formulas providing partial information about an initial situation, about a set of events occurring sequentially in this situation, and about the resulting situation after the occurrence of each event. From this whole sequence, we want to infer more information, either about the initial situation, or about one of the events, or about the resulting situation after one of the events. Within the framework of Dynamic Epistemic Logic (DEL), we show that these different kinds of problems are all reducible to the problem of inferring what holds in the final situation after the occurrence of all the events. We then provide a tableau method deciding whether this kind of inference is valid. We implement it in LotrecScheme and show that these inference problems are NEXPTIME-complete. We extend our results to the cases where the accessibility relation is serial and reflexive and illustrate them with the coordinated attack problem.

GandALF Workshop 2011 Workshop Paper

Opacity Issues in Games with Imperfect Information

• Bastien Maubert
• Sophie Pinchinat
• Laura Bozzelli

We study in depth the class of games with opacity condition, which are two-player games with imperfect information in which one of the players only has imperfect information, and where the winning condition relies on the information he has along the play. Those games are relevant for security aspects of computing systems: a play is opaque whenever the player who has imperfect information never "knows" for sure that the current position is one of the distinguished "secret" positions. We study the problems of deciding the existence of a winning strategy for each player, and we call them the opacity-violate problem and the opacity-guarantee problem. Focusing on the player with perfect information is new in the field of games with imperfect-information because when considering classical winning conditions it amounts to solving the underlying perfect-information game. We establish the EXPTIME-completeness of both above-mentioned problems, showing that our winning condition brings a gap of complexity for the player with perfect information, and we exhibit the relevant opacity-verify problem, which noticeably generalizes approaches considered in the literature for opacity analysis in discrete-event systems. In the case of blindfold games, this problem relates to the two initial ones, yielding the determinacy of blindfold games with opacity condition and the PSPACE-completeness of the three problems.