Munyque Mittelmann

AAAI Conference 2026 Conference Paper

Formal Verification of Diffusion Auctions

• Rustam Galimullin
• Munyque Mittelmann
• Laurent Perrussel

In diffusion auctions, sellers can leverage an underlying social network to broaden participation, thereby increasing their potential revenue. Specifically, sellers can incentivise participants in their auction to diffuse information about the auction through the network. While numerous variants of such auctions have been recently studied in the literature, the formal verification and strategic reasoning perspectives have not been investigated yet. Our contribution is threefold. First, we introduce a logical formalism that captures the dynamics of diffusion and its strategic dimension. Second, for such a logic, we provide model-checking procedures that allow one to verify properties like the Nash equilibrium, and that pave the way towards checking the existence of sellers' strategies. Third, we establish computational complexity results for the presented algorithms.

AAMAS Conference 2026 Conference Paper

On Angels and Demons: Strategic (De)Construction of Dynamic Models

• Davide Catta
• Rustam Galimullin
• Munyque Mittelmann

In recent years, there has been growing interest in logics that formalise strategic reasoning about agents capable of modifying the structure of a given model. This line of research has been motivated by applications where a modelled system evolves over time, such as communication networks, security protocols, and multi-agent planning. In this paper, we introduce three logics for reasoning about strategies that modify the topology of weighted graphs. In Strategic Deconstruction Logic, a destructive agent (the demon) removes edges up to a certain cost. In Strategic Construction Logic, a constructive agent (the angel) adds edges within a cost bound. Finally, Strategic Update Logic combines both agents, who may cooperate or compete. We study the expressive power of these logics and the complexity of their model checking problems.

AAMAS Conference 2026 Conference Paper

The Dynamic Turn in Strategy Logics

• Rustam Galimullin
• Maksim Gladyshev
• Munyque Mittelmann
• Nima Motamed

Strategy Logics are well-studied frameworks for the specification and verification of strategic abilities in multi-agent systems (MAS). However, the current generation of Strategy Logics is limited to staticreasoningaboutfixedmodelsofMAS. Thislimitationexcludes a plethora of applications that require addressing dynamic changes and updates. Examples include verifying that a computer program executes correctly after an upgrade, automatically repairing MAS to meet safety requirements, and reasoning about robots operating in a dynamic environment. To address this limitation, we propose a new research agenda centered on enriching Strategy Logics with concepts and intuitions from Dynamic Epistemic Logic, aiming to develop a holistic and general framework that captures dynamic phenomena in MAS and facilitates their verification.

AAMAS Conference 2026 Conference Paper

Verification of Robust Multi-Agent Systems

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

Stochastic multi-agent systems are a central modeling framework for autonomous controllers, communication protocols, and cyberphysical 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.

AAMAS Conference 2025 Conference Paper

Changing the Rules of the Game: Reasoning About Dynamic Phenomena in Multi-Agent Systems

• Rustam Galimullin
• Maksim Gladyshev
• Munyque Mittelmann
• Nima Motamed

The design and application of multi-agent systems (MAS) require reasoning about the effects of modifications on their underlying structure. In particular, such changes may impact the satisfaction of system specifications and the strategic abilities of their autonomous components. In this paper, we are concerned with the problem of verifying and synthesising modifications (or updates) of MAS. We propose an extension of the Alternating-Time Temporal Logic (ATL) that enables reasoning about the dynamics of model change, called the Logic for ATL Model Building (LAMB). We show how LAMB can express various intuitions and ideas about the dynamics of MAS, from normative updates to mechanism design. As the main technical result, we prove that, while being strictly more expressive than ATL, LAMB enjoys a P-complete model-checking procedure.

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.

AAMAS Conference 2025 Conference Paper

Rational Capability in Concurrent Games

• Yinfeng Li
• Emiliano Lorini
• Munyque Mittelmann

We extend concurrent game structures (CGSs) with a simple notion of preference over computations and define a minimal notion of rationality for agents based on the concept of dominance. We use this notion to interpret a CL and an ATL languages that extend the basic CL and ATL languages with modalities for rational capability, namely, a coalition’s capability to rationally enforce a given property. For each of these languages, we provide results about the complexity of satisfiability checking and model checking as well as about axiomatization.

KR Conference 2025 Conference Paper

Repairing General Game Descriptions

• Yifan He
• Munyque Mittelmann
• Aniello Murano
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language (GDL) is a widely used formalism for specifying the rules of general games. Writing correct GDL descriptions can be challenging, especially for non-experts. Automated theorem proving has been proposed to assist game design by verifying if a GDL description satisfies desirable logical properties. However, when a description is proved to be faulty, the repair task itself can only be done manually. Motivated by the work on repairing unsolvable planning domain descriptions, we define a more general problem of finding minimal repairs for GDL descriptions that violate formal requirements, and we provide complexity results for various computational problems related to minimal repair. Moreover, we present an Answer Set Programming-based encoding for solving the minimal repair problem and demonstrate its application for automatically repairing ill-defined game descriptions.

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.

KR Conference 2024 Conference Paper

Incentive Design for Rational Agents

• David Hyland
• Munyque Mittelmann
• Aniello Murano
• Giuseppe Perelli
• Michael Wooldridge

We introduce Incentive Design: a new class of problems for equilibrium verification in multi-agent systems. In our model, agents attempt to maximize their utility functions, which are expressed as formulae in LTL[F], a quantitative extension of Linear Temporal Logic with functions computable in polynomial time. We assume agents are rational, in the sense that they adopt strategies consistent with game theoretic solution concepts such as Nash equilibrium. For each solution concept we consider, we analyze the problems of verifying whether an incentive scheme achieves a societal objective and finding one that does so, whether it be social welfare or any other aggregate measure of collective well-being. We study both static and dynamic incentive schemes, showing that the latter are more powerful than the former. Finally, we solve the incentive verification and synthesis problems for all the solution concepts we consider, and analyze their complexity.

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*.

AAMAS Conference 2024 Conference Paper

Playing Quantitative Games Against an Authority: On the Module Checking Problem

• Wojciech Jamroga
• Munyque Mittelmann
• Aniello Murano
• Giuseppe Perelli

Module checking is a decision problem to formalize the verification of systems that must adapt their behavior to the input they receive from the environment, also viewed as an authority. So far, module checking has been only considered in the Boolean setting, which does not capture the different levels of quality inherent to complex systems (e. g. , systems dealing with quantitative utilities or sensor inputs). In this paper, we address this issue by proposing quantitative module checking. We study the problem in the quantitative and multi-agent setting, which enables the verification of different levels of satisfaction in relation to a specification. We consider specifications given in Quantitative Alternating-time Temporal logics and investigate their complexity and expressivity.

KR Conference 2024 Conference Paper

Verification of General Games with Imperfect Information Using Strategy Logic

• Yifan He
• Munyque Mittelmann
• Aniello Murano
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language with Imperfect Information (GDL-II) is a lightweight formalism for representing the rules of arbitrary games, including those where players have private information. Its purpose is to build general game-playing systems, that is, automated players that can understand the rules of games and learn how to play them without human intervention. Epistemic Strategy Logic (SLK), on the other hand, is a rich logical framework for reasoning about multi-agent systems and the strategic behavior of agents with partial observability. To enable a general game-playing system to take advantage of this rich formalism for the automatic verification of properties of games, we present a formal translation from GDL-II to SLK models. We prove the correctness of this translation and show how crucial properties of general games, including playability and the existence of Nash equilibria, can be expressed as formulas in SLK. Finally, we demonstrate the application of an existing model-checking system for SLK to verify the properties of GDL-II games.

AAMAS Conference 2024 Conference Paper

Verification of Stochastic Multi-Agent Systems with Forgetful Strategies

• Francesco Belardinelli
• Wojtek Jamroga
• Munyque Mittelmann
• Aniello Murano

Intelligent autonomous agents need to reason about different kinds of uncertainty in a Multi-Agent System (MAS): first, due to the occurrence of randomization and, second, their inability to completely observe the state of the system. In this paper, we investigate the verification of system specifications in probabilistic variants of the logics ATL and ATL∗ under imperfect information (II). The resulting setting combines these two sources of uncertainty and captures the situation in which agents have qualitative uncertainty about the local state as well as quantitative uncertainty about the occurrence of future events. Since the model-checking problem is undecidable when considered in the context of strategies with perfect recall, we focus on memoryless (positional) strategies. As the main result, we show that, in stochastic MAS under II, model-checking Probabilistic ATL is in EXPTIME when agents play probabilistic strategies. Filling the gap in recent work, we also show that model-checking Probabilistic ATL∗ is PSPACE-complete when the proponent coalition is restricted to deterministic strategies.

IJCAI Conference 2023 Conference Paper

Discounting in Strategy Logic

• Munyque Mittelmann
• Aniello Murano
• Laurent Perrussel

Discounting is an important dimension in multi-agent systems as long as we want to reason about strategies and time. It is a key aspect in economics as it captures the intuition that the far-away future is not as important as the near future. Traditional verification techniques allow to check whether there is a winning strategy for a group of agents but they do not take into account the fact that satisfying a goal sooner is different from satisfying it after a long wait. In this paper, we augment Strategy Logic with future discounting over a set of discounted functions D, denoted SL[D]. We consider “until” operators with discounting functions: the satisfaction value of a specification in SL[D] is a value in [0, 1], where the longer it takes to fulfill requirements, the smaller the satisfaction value is. We motivate our approach with classical examples from Game Theory and study the complexity of model-checking SL[D]-formulas.

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.

AAMAS Conference 2023 Conference Paper

Representing and Reasoning about Auctions

• Munyque Mittelmann
• Laurent Perrussel
• Sylvain Bouveret

In this paper, we propose a framework for representing and reasoning about auction-based protocols. Such a framework is of interest for building digital marketplaces based on auctions and should fulfill two requirements: (i) it should enable bidders to express their preferences over combinations of items and (ii) it should allow the mechanism designer to describe the rules governing the market, namely the legality of bids, the allocative choice, and the payment rule. To do so, we define a logical language in the spirit of the Game Description Language, namely Auction Description Language with a set of functions FB (ADL[FB]). ADL[FB] is expressive enough to represent different kinds of protocols and enables reasoning about auction properties, including playability, termination, and budget-balance. We also study the complexity of model-checking ADL[FB].

KR Conference 2023 Conference Paper

Strategic Abilities of Forgetful Agents in Stochastic Environments

• Francesco Belardinelli
• Wojciech Jamroga
• Munyque Mittelmann
• Aniello Murano

In this paper, we investigate the probabilistic variants of the strategy logics ATL and ATL* under imperfect information. Specifically, we present novel decidability and complexity results when both the model transitions and the strategies played by agents are stochastic. That is, the semantics of the logics are based on multi-agent, stochastic transition systems with imperfect information, which combine two sources of uncertainty, namely, the partial observability agents have on the environment, and the likelihood of transitions to occur from a system state. Since the model checking problem is undecidable in general in this setting, we restrict our attention to agents with memoryless (positional) strategies. The resulting setting captures the situation in which agents have qualitative uncertainty of the local state and quantitative uncertainty about the occurrence of future events. We illustrate the usefulness of this setting with meaningful examples.

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.

AAMAS Conference 2022 Conference Paper

Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions

• Francesco Belardinelli
• Wojtek Jamroga
• Vadim Malvone
• Munyque Mittelmann
• Aniello Murano
• Laurent Perrussel

In online advertising, search engines sell ad placements for keywords continuously through auctions. This problem can be seen as an infinitely repeated game since the auction is executed whenever a user performs a query with the keyword. As advertisers may frequently change their bids, the game will have a large set of equilibria with potentially complex strategies. In this paper, we propose the use of natural strategies for reasoning in such setting as they are processable by artificial agents with limited memory and/or computational power as well as understandable by human users. To reach this goal, we introduce a quantitative version of Strategy Logic with natural strategies in the setting of imperfect information. In a first step, we show how to model strategies for repeated keyword auctions and take advantage of the model for proving properties evaluating this game. In a second step, we study the logic in relation to the distinguishing power, expressivity, and model-checking complexity for strategies with and without recall.

JAAMAS Journal 2022 Journal Article

Representing and reasoning about auctions

• Munyque Mittelmann
• Sylvain Bouveret
• Laurent Perrussel

Abstract The goal of this paper is to propose a framework for representing and reasoning about the rules of auction-based protocols. Such a framework is of interest for building digital marketplaces based on this type of mechanism. Hence the framework should fulfill two requirements: (i) it should enable bidders to express their preferences over combinations of items and (ii) it should allow the mechanism designer to describe the rules governing the market, namely the legality of bids, the allocative choice, and the payment rule. To do so, we define a logical language in the spirit of the Game Description Language, namely Auction Description Language with a set of functions \(\mathcal {F}_{\mathcal {B}}\) ( ADL \([\mathcal {F}_{\mathcal {B}}]\) ). ADL \([\mathcal {F}_{\mathcal {B}}]\) is the first language for describing auctions in a logical framework. With our approach, each stage in a protocol is seen as an independent direct revelation mechanism. Our contribution is three-fold: first, we illustrate the general dimension by representing different kinds of protocols. Second, we show how this machine-processable language enables reasoning about auction properties, including playability, termination, and classical conditions from mechanism design (e. g. , budget-balance and individual rationality). Finally, we develop a model-checking algorithm for ADL \([\mathcal {F}_{\mathcal {B}}]\), with complexity in PTIME when the functions in \(\mathcal {F}_{\mathcal {B}}\) can be computed in polynomial time.

LAMAS&SR Workshop 2022 Workshop Paper

Strategic Reasoning in Automated Mechanism Design

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

AAMAS Conference 2021 Conference Paper

A General Framework for the Logical Representation of Combinatorial Exchange Protocols

• Munyque Mittelmann
• Sylvain Bouveret
• Laurent Perrussel

The goal of this work is to propose a framework for representing and reasoning about the rules governing a combinatorial exchange. Such a framework is at first interest as long as we want to build up digital marketplaces based on auction, a widely used mechanism for automated transactions. Hence the framework should fulfill two requirements: (i) it should enable bidders to express their bids on combinations of goods and (ii) it should allow describing the rules governing some market, namely the legal bids, the allocation and payment rules. To do so, we define a logical language in the spirit of the Game Description Language: the Combinatorial Exchange Description Language is the first language for describing combinatorial exchange in a logical framework. The contribution is two-fold: first, we illustrate the general dimension by representing different kinds of protocols, and second, we show how to reason about auction properties in this machine-processable language.

LAMAS&SR Workshop 2021 Workshop Paper

Epistemic Reasoning about Rationality and Bids in Auctions

• Munyque Mittelmann
• Andreas Herzig
• Laurent Perrussel

The goal of this work is to investigate strategic reasoning in the context of auctions. More precisely, we establish an explicit link between the agents’ choice of bidding actions and bounded rationality. To do so, we extend the Auction Description Language with an epistemic operator and a choice operator and use it to represent a classical auction where agents have imperfect information about other bidders’ valuations. We formalize bounded rationality concepts in iterative protocols and show how to use them to reason about the players’ actions. Finally, we provide a model checking algorithm.

JELIA Conference 2021 Conference Paper

Epistemic Reasoning About Rationality and Bids in Auctions

• Munyque Mittelmann
• Andreas Herzig
• Laurent Perrussel

Abstract In this paper, we investigate strategic reasoning in the context of auctions. More precisely, we establish an explicit link between bidding actions and bounded rationality. To do so, we extend the Auction Description Language with an epistemic operator and an action choice operator and use it to represent a classical auction where agents have imperfect information about other agents’ valuations. We formalize bounded rationality concepts in iterative protocols and show how to use them to reason about the players’ actions. Finally, we provide a model checking algorithm.

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.

ECAI Conference 2020 Conference Paper

Auction Description Language (ADL): General Framework for Representing Auction-Based Markets

• Munyque Mittelmann
• Laurent Perrussel

The goal of this paper is to propose a language for representing and reasoning about the rules governing an auction-based market. Such language is at first interest as long as we want to build up digital market places based on auction, a widely used framework for automated transactions. Auctions may differ in several aspects: single or double-side, ascending or descending, single or multi-unit, open cry or sealed-bid, and so on. This variety prevents an agent to easily switch between different (auction-based) markets. The first requirement for building such agents is to have a general language for describing auction-based markets. Second, this language should also allow the reasoning about the key issues of a specific market, namely the allocation and payment rules. To do so, we define a language in the spirit of the Game Description Language (GDL): the Auction Description Language (ADL) is the first language for describing auctions in a logical framework. In this paper, we illustrate this general dimension by representing two different types of well-known auctions: an English Auction and a Multi-Unit Vickrey Auction. We show the benefit of ADL by deriving properties about these two auction protocols. It also enables us to show in an explicit way what should be assumed about the behavior of a rational bidder.