Most of the papers available from this list appear in print, and the corresponding copyright is held by the publisher. While the papers can be used for personal use, redistribution or reprinting for commercial purposes is prohibited. Preproceedings versions are available upon request.
2024
AAMAS-24
Playing Quantitative Games Against an Authority: On the Module Checking Problem.
Module checking is a decision problem to formalize the verification of (possibly multi-agent) 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 the complexity and expressivity results.
@inproceedings{C-JMMP24,author={Jamroga, Wojtek and Mittelmann, Munyque and Murano, Aniello and Perelli, Giuseppe},title={Playing Quantitative Games Against an Authority: On the Module Checking Problem.},booktitle={The 23rd International Conference on Autonomous Agents and Multi-Agent Systems, {AAMAS}},year={2024},note={To appear}}
We present Pure-Past Action Masking (PPAM), a lightweight approach to action masking for safe reinforcement learning. In PPAM, actions are disallowed ("masked") according to specifications expressed in Pure-Past Linear Temporal Logic (PPLTL). PPAM can enforce non-Markovian constraints, i.e.,
constraints based on the history of the system, rather than just the current state of the (possibly hidden) MDP. The features used in the safety constraint need not be the same as those used by the learning agent, allowing a clear separation of concerns between the safety constraints and reward specifications of the (learning) agent. We prove formally that an agent trained with PPAM can learn any optimal policy that satisfies the safety constraints, and that they are as expressive as shields, another approach to enforce non-Markovian constraints in RL. Finally, we provide empirical results showing how PPAM can guarantee constraint satisfaction in practice.
@inproceedings{C-ADDLPV24,author={Alechina, Natasha and Dastani, Mehdi and {De Giacomo}, Giuseppe and Logan, Brian and Perelli, Giuseppe and Varricchione, Giovanni},title={Pure-Past Action Masking.},booktitle={38th Annual AAAI Conference on Artificial Intelligence, {AAAI}},pages={21646--21655},publisher={{AAAI} Press},year={2024},}
2023
TOCL
Reasoning about Quality and Fuzziness of Strategic Behaviours.
Temporal logics are extensively used for the specification of on-going behaviors of computer systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviors in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalize concepts such as certainty or quality. In the first class, SL (Strategy Logic) is one of the most natural and expressive logics describing strategic behaviors. In the second class, a notable logic is LTL[F], which extends LTL with quality operators.
In this work we introduce and study SL[F], which enables the specification of quantitative strategic behaviors. 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 \FSL in quantitative reasoning about multi-agent systems, showing how it can express and measure concepts like stability in multi-agent systems, and how it generalizes some fuzzy temporal logics. We also provide a model-checking algorithm for SL[F], based on a quantitative extension of Quantified CTL*. Our algorithm provides the first decidability result for a quantitative extension of Strategy Logic. In addition, it can be used for synthesizing strategies that maximize the quality of the systems’ behavior.
@incollection{C-BKMMMP23,author={Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe},title={Reasoning about Quality and Fuzziness of Strategic Behaviours.},year={2023},booktitle={{ACM} Transaction on Computational Logic},volume={24},number={3},pages={21:1--21:38},}
Rational verification refers to the problem of checking which temporal logic properties hold of a concurrent/multiagent system, under the assumption that agents in the system choose strategies that form a game theoretic equilibrium. Rational verification can be understood as a counterpart to model checking for multiagent systems, but while classical model checking can be done in polynomial time for some temporal logic specification languages such as CTL, and polynomial space with LTL specifications, rational verification is much harder: the key decision problems for rational verification are 2EXPTIME-complete with LTL specifications, even when using explicit-state system representations. Against this background, our contributions in this paper are threefold. First, we show that the complexity of rational verification can be greatly reduced by restricting specifications to GR(1), a fragment of LTL that can represent a broad and practically useful class of response properties of reactive systems. In particular, we show that for a number of relevant settings, rational verification can be done in polynomial space and even in polynomial time. Second, we provide improved complexity results for rational verification when considering players’ goals given by mean-payoff utility functions—arguably the most widely used approach for quantitative objectives in concurrent and multiagent systems. Finally, we consider the problem of computing outcomes that satisfy social welfare constraints. To this end, we consider both utilitarian and egalitarian social welfare and show that computing such outcomes is either PSPACE-complete or NP-complete.
@incollection{J-GNPW23,author={Gutierrez, Julian and Najib, Muhammad and Perelli, Giuseppe and Wooldridge, Michael},title={On the Complexity of Rational Verification.},volume={91},number={4},pages={409--430},year={2023},booktitle={Annals of Mathematics and Artificial Intelligence},publisher={Springer International Publishing},}
This paper introduces Behavioral QLTL, a “behavioral” variant of Linear Temporal Logic (LTL) with second-order quantifiers. Behavioral QLTL is characterized by the fact that the functions that assign the truth value of the quantified propositions along the trace can only depend on the past. In other words, such functions must be “processes”. This gives the logic a strategic flavor that we usually associate with planning. Indeed we show that temporally extended planning in nondeterministic domains and LTL synthesis are expressed in Behavioral QLTL through formulas with a simple quantification alternation. While as this alternation increases, we get to forms of planning/synthesis in which contingent and conformant planning aspects get mixed. We study this logic from the computational point of view and compare it to the original QLTL (with non-behavioral semantics) and simpler forms of behavioral semantics.
@inproceedings{C-DP23,author={{De Giacomo}, Giuseppe and Perelli, Giuseppe},title={Behavioral QLTL.},booktitle={20th European Conference of Multi-Agents Systems, {EUMAS}},year={2023},volume={14282},pages={133--149},}
We introduce Strategy Repair, the problem of finding a minimal amount of modifications to turn a strategy for a reachability game from losing into winning. The problem is relevant for a number of settings in Planning and Synthesis, where solutions essentially correspond to winning strategies in a suitably defined reachability game. We show, via reduction from Vertex Cover, that Strategy Repair is NP-complete and devise two algorithms, one optimal and exponential and one polynomial but sub-optimal, which we compare experimentally. The reported experimentation includes some heuristics for strategy modification, which proved crucial in dramatically improving performance.
@inproceedings{C-GPP23,author={Gaillard, Pierre and Patrizi, Fabio and Perelli, Giuseppe},title={Strategy Repair in Reachability Games.},booktitle={26th European Conference on Artificial Intelligence, {ECAI}},volume={372},pages={780--787},publisher={{IOS} Press},year={2023},}
Answering temporal CQs over temporalized Description Logic knowledge bases (TKB) is a main technique to realize ontology-based situation recognition. In case the collected data in such a knowledge base is inaccurate, important query answers can be missed.
In this paper we introduce the TKB Alignment problem, which computes a variant of the TKB that minimally changes the TKB, but entails the given temporal CQ and is in that sense (cost-)optimal. We investigate this problem for ALC TKBs and conjunctive queries with LTL operators and devise a solution technique to compute (cost-optimal) alignments of TKBs that extends techniques for the alignment problem for propositional LTL over finite traces.
@inproceedings{C-FPPT23,author={Fernandez-Gil, Oliver and Patrizi, Fabio and Perelli, Giuseppe and Turhan, Anni-Yasmin},title={Optimal Alignment of Temporal Knowledge Bases.},booktitle={26th European Conference on Artificial Intelligence, {ECAI}},year={2023},volume={372},pages={708--715},publisher={{IOS} Press},}
Our aim is to develop a formal semantics for giving instructions to taskable agents, to investigate the complexity of decision problems relating to these semantics, and to explore the issues that these semantics raise. In the setting we consider, agents are given instructions in the form of Linear Temporal Logic (LTL) formulae; the intuitive interpretation of such an instruction is that the agent should act in such a way as to ensure the formula is satisfied. At the same time, agents are assumed to have inviolable and immutable background safety requirements, also specified as LTL formulae. Finally, the actions performed by an agent are assumed to have costs, and agents must act within a limited budget. For this setting, we present a range of interpretations of an instruction to achieve an LTL task Υ, intuitively ranging from “try to do this but only if you can do so with everything else remaining unchanged” up to "drop everything and get this done." For each case we present a formal pre-/post-condition semantics, and investigate the computational issues that they raise.
@inproceedings{C-GKPW22,author={Gutierrez, Julian and Kraus, Sarit and Perelli, Giuseppe and Wooldridge, Michael},title={Giving Instruction in Linear Temporal Logic.},booktitle={29th International Symposium on Temporal Representation and Reasoning, {TIME}},series={LIPIcs},volume={247},pages={15:1--15:14},year={2022},}
KR-22
Automatic Synthesis of Dynamic Norms for Multi-Agent Systems.
Norms have been widely proposed to coordinate and regulate behaviour in multi-agent systems (MAS). We consider the problem of synthesising and revising the set of norms in a normative MAS to satisfy a design objective expressed in Alternating Time Temporal Logic (ATL*). ATL* is a well-established language for strategic reasoning, which allows the specification of norms that constrain the strategic behaviour of agents. We focus on dynamic norms, that is, norms corresponding to Mealy machines, that allow us to place different constraints on the agents’ behaviour depending on the state of the norm and the state of the underlying MAS. We show that synthesising dynamic norms is (k + 1)-EXPTIME where k is the alternation depth of quantifiers in the ATL* specification. Note that for typical cases of interest, k is either 1 or 2. We also study the problem of removing existing norms to satisfy a new objective, which we show to be 2EXPTIME-complete.
@inproceedings{C-ADLP22,author={Alechina, Natasha and {De Giacomo}, Giuseppe and Logan, Brian and Perelli, Giuseppe},title={{Automatic Synthesis of Dynamic Norms for Multi-Agent Systems.}},booktitle={Proceedings of the Nineteenth International Conference on Principles of Knowledge Representation and Reasoning ({KR})},pages={12-21},year={2022},}
We provide a survey of the state of the art of rational verification: the problem of checking whether a given temporal logic formula φis satisfied in some or all game theoretic equilibrium computations of a multi-agent system – that is, whether the system will exhibit the behaviour φrepresents under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the overall framework of rational verification, we discuss key results obtained in the past few years as well as relevant related work in logic, AI, and Computer Science.
@incollection{J-AGHHKNPSW21,author={Abate, Alessandro and Gutierrez, Julian and Hammond, Lewis and Harrenstein, Paul and Kwiatkowska, Marta and Najib, Muhammad and Perelli, Giuseppe and Steeples, Thomas and Wooldridge, Michael},title={{Rational Verification: a Progress Report}},booktitle={Appl. Intell.},year={2021},}
ACTA Informatica
Equilibria for Games with Combined Qualitative and Quantitative Objectives.
The overall aim of our research is to develop techniques to reason about the equilibrium properties of multi-agent systems.
We model multi-agent systems as concurrent games, in which each player is a process that is assumed to act independently and strategically in pursuit of personal preferences.
In this article, we study these games in the context of finite-memory strategies, and we assume players’ preferences are defined by a qualitative
and a quantitative objective, which are related by a lexicographic order: a player first prefers to satisfy its qualitative objective (given as a
formula of Linear Temporal Logic) and then prefers to minimise costs (given by a mean-payoff function).
Our main result is that deciding the existence of a strict εNash equilibrium in such games is 2\textscExpTime-complete (and hence decidable), even if players’ deviations are implemented as infinite-memory strategies.
@incollection{J-GMPRSW21,author={Gutierrez, Julian and Murano, Aniello and Perelli, Giuseppe and Rubin, Sasha and Steeples, Thomas and Wooldridge, Michael},title={Equilibria for Games with Combined Qualitative and Quantitative Objectives.},year={2021},booktitle={ACTA Informatica},volume={58},number={6},pages={585--610},}
TOCL
Expressiveness and Nash Equilibrium in Iterated Boolean Games
We define and investigate a novel notion of expressiveness for temporal logics that is based on game theoretic equilibria of multi-agent systems. We use \emphiterated Boolean games as our abstract model of multi-agent systems. In such a game, each agent i has a goal \gamma_i, represented using (a fragment of) Linear Temporal Logic (LTL). The goal \gamma_i captures agent i’s preferences, in the sense that the models of \gamma_i represent system behaviours that would satisfy i. Each player controls a subset of Boolean variables \Phi_i, and at each round in the game, player i is at liberty to choose values for variables \Phi_i in any way that she sees fit. Play continues for an infinite sequence of rounds, and so as players act they collectively trace out a model for LTL, which for every player will either satisfy or fail to satisfy their goal. Players are assumed to act strategically, taking into account the goals of other players, in an attempt to bring about computations satisfying their goal. In this setting, we apply the standard game-theoretic concept of (pure) Nash equilibria. The (possibly empty) set of Nash equilibria of an iterated Boolean game can be understood as inducing a set of computations, each computation representing one way the system could evolve if players chose strategies that together constitute a Nash equilibrium. Such a set of equilibrium computations expresses a temporal property—which may or may not be expressible within a particular LTL fragment. The new notion of expressiveness that we formally define and investigate is then as follows: \emphwhat temporal properties are characterised by the Nash equilibria of games in which agent goals are expressed in fragments of LTL? We formally define and investigate this notion of expressiveness and related issues, for a range of LTL fragments. For example, a very natural question is the following. Suppose we have an iterated Boolean game in which every goal is represented using a particular fragment of LTL: then is it always the case that the equilibria of the game can be characterised within such fragment? We show that this is not true in general.
@incollection{J-GHPW21,author={Gutierrez, Julian and Harrenstein, Paul and Perelli, Giuseppe and Wooldridge, Michael},title={Expressiveness and Nash Equilibrium in Iterated Boolean Games},booktitle={{ACM} Transaction on Computational Logic},year={2021},}
Inf&Comp
Multi-Player Games with LDL Goals over Finite Traces.
Linear Dynamic Logic on finite traces (LDLF) is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems.
In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on LDLF.
This study builds upon a generalisation of Boolean games, a logic-based game model of multi-agent systems where players have goals succinctly represented in a logical way.
Because LDLF goals are considered, in the settings we study - Reactive Modules games and iterated Boolean games with goals over finite traces - players’ goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace.
In particular, using alternating automata, the paper investigates automata-theoretic approaches to the characterisation and verification of (pure strategy Nash) equilibria, shows that the set of Nash equilibria in multi-player games with LDLF objectives is regular, and provides complexity results for the associated automata constructions.
@incollection{J-GPW21,author={Gutierrez, Julian and Perelli, Giuseppe and Wooldridge, Michael},title={Multi-Player Games with LDL Goals over Finite Traces.},booktitle={Information and Computation},year={2021},}
We study the impact of the need for the agent to obligatorily instruct the action stop in her strategies. More specifically we consider synthesis (i.e., planning) for LTLf goals under LTL environment specifications in the case the agent must mandatorily stop at a certain point. We show that this obligation makes it impossible to exploit the liveness part of the LTL environment specifications to achieve her goal, effectively reducing the environment specifications to their safety part only. This has a deep impact on the efficiency of solving the synthesis, which can sidestep handling Büchi determinization associated to LTL synthesis, in favor of finite-state automata manipulation as in LTLf synthesis. Next, we add to the agent goal, expressed in LTLf, a safety goal, expressed in LTL. Safety goals must hold forever, even when the agent stops, since the environment can still continue its evolution. Hence the agent, before stopping, must ensure that her safety goal will be maintained even after she stops. To do synthesis in this case, we devise an effective approach that mixes a synthesis technique based on finite-state automata (as in the case of LTLf goals) and model-checking of nondeterministic Büchi automata. In this way, again, we sidestep Büchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.
@inproceedings{C-DDPZ21,author={{De Giacomo}, Giuseppe and {Di Stasio}, Antonio and Perelli, Giuseppe and Zhu, Shufang},title={Synthesis with Mandatory Stop Actions},booktitle={Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning ({KR})},pages={237--246},year={2021},}
KR-21
Timed Trace Alignment with Metric Temporal Logic over Finite Traces
Trace Alignment is a prominent problem in Declarative Business Process Management, which consists in identifying a minimal set of modifications that a log trace (produced by a system under execution) requires in order to be made compliant with a temporal specification. In its simplest form, log traces are sequences of events from a finite alphabet and specifications are written in D ECLARE, a strict sublanguage of linear-time temporal logic over finite traces ( LTLf ). The best approach for trace alignment has been developed in AI, using cost-optimal planning, and handles the whole LTLf . In this paper, we study the timed version of trace alignment, where events are paired with timestamps and specifications are provided in metric temporal logic over finite traces (MTLf ), essentially a superlanguage of LTL f . Due to the infiniteness of timestamps, this variant is substantially more challenging than the basic version, as the structures involved in the search are (uncountably) infinite-state, and calls for a more sophisticated machinery based on alternating (timed) automata, as opposed to the standard finite-state automata sufficient for the untimed version. The main contribution of the paper is a provably correct, effective technique for Timed Trace Alignment that takes advantage of results on MTL f decidability as well as on reachability for well-structured transition systems.
@inproceedings{C-DMPP21,author={{De Giacomo}, Giuseppe and Murano, Aniello and Patrizi, Fabio and Perelli, Giuseppe},title={Timed Trace Alignment with Metric Temporal Logic over Finite Traces},booktitle={Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning ({KR})},pages={227--236},year={2021},}
IJCAI-21
HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs
In recent years, there has been an increasing interest in temporal logics over finite traces, to express and verify properties of systems whose execution have an unbounded, but finite, length. This is relevant in a number of settings, such as planning, business process management, and in general the analysis of system logs. However, these logics consider one trace at the time, while sometimes it is of interest to consider multiple traces (i.e., the entire log) at once. In the infinite-trace setting a specific logic, HyperLTL, has been proposed to express properties of sets of traces. In this paper, we study HyperLDLf, a logic that combines the features of HyperLTL with the expressiveness of linear dynamic logic over finite traces. We show decidability and complexity of the model checking problem in the relevant case where the set of traces is a regular language, and we discuss how this form of model checking on HyperLDLf properties can be used for checking security properties, instance-spanning constraints in business process management, and process mining.
@inproceedings{C-DFMP21,author={{De Giacomo}, Giuseppe and Felli, Paolo and Montali, Marco and Perelli, Giuseppe},title={{HyperLDLf}: a Logic for Checking Properties of Finite Traces Process Logs},booktitle={Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence ({IJCAI})},pages={1859--1865},year={2021},}
Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions. In this paper, we contribute to research on cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is PSPACE-complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.
@incollection{J-BMPS20,author={Bozzelli, Laura and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana},title={Hierarchical Cost-Parity Games.},booktitle={Theoretical Computer Science},year={2020},}
AIJ
Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games.
In the context of multi-agent systems, the \textitrational verification problem is concerned with checking which temporal logic properties will hold in a system when its constituent agents are assumed to behave rationally and strategically in pursuit of individual objectives.
Typically, those objectives are expressed as temporal logic formulae which the relevant agent desires to see satisfied.
Unfortunately, rational verification is computationally complex, and requires specialised techniques in order to obtain practically useable implementations.
In this paper, we present such a technique.
This technique relies on a reduction of the rational verification problem to the solution of a collection of parity games.
Our approach has been implemented in the \emphEquilibrium \emphVerification \emphEnvironment (EVE) system. The EVE system takes as input a model of a concurrent/multi-agent system represented using the Simple Reactive Modules Language (SRML), where agent goals are represented as Linear Temporal Logic (LTL) formulae, together with a claim about the equilibrium behaviour of the system, also expressed as an LTL formula.
EVE can then check whether the LTL claim holds on some (or every) computation of the system that could arise through agents choosing Nash equilibrium
strategies; it can also check whether a system has a Nash equilibrium, and synthesise individual strategies for players in the multi-player game.
After presenting our basic framework, we describe our new technique and prove its correctness.
We then describe our implementation in the EVE system, and present experimental results which show that EVE performs favourably in comparison to other existing tools that support rational verification.
@incollection{J-GNPW20,author={Gutierrez, Julian and Najib, Muhammad and Perelli, Giuseppe and Wooldridge, Michael},title={Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games.},booktitle={Artificial Intelligence},year={2020},}
ECAI-20
Reasoning About Quality and Fuzziness of Strategic Behaviours
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 our logic, based on a quantitative extension of Quantified CTL*.
@inproceedings{C-BKMMMP20,author={Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe},title={Reasoning About Quality and Fuzziness of Strategic Behaviours},booktitle={24th European Conference on Artificial Intelligence, {ECAI'20}, Santiago de Compostela, Spain, August 29 - September 8},series={Frontiers in Artificial Intelligence and Applications},volume={325},pages={2887--2888},year={2020},}
We propose a formalism to model and reason about multi-agent systems. We allow agents to interact and communicate in different modes so that they can pursue joint tasks; agents may dynamically synchronize, exchange data, adapt their behaviour, and reconfigure their communication interfaces. The formalism defines a local behaviour based on shared variables and a global one based on message passing. We extend LTL to be able to reason explicitly about the intentions of the different agents and their interaction protocols. We also study the complexity of satisfiability and model-checking of this extension.
@inproceedings{C-APP20,author={{Abd Alrahman}, Yehia and Perelli, Giuseppe and Piterman, Nir},title={Reconfigurable Interaction for MAS Modelling},booktitle={Proceedings of the 19th International Conference on Autonomous Agents and MultiAgent Systems, {AAMAS} '20, Auckland, New Zealand, May 09-13},year={2020},pages={7--15},}
Game theory provides a well-established framework for the analysis of concurrent and multi-agent systems. The basic idea is that concurrent processes (agents) can be understood as corresponding to players in a game; plays represent the possible computation runs of the system; and strategies define the behaviour of agents. Typically, strategies are modelled as functions from sequences of system states to player actions. Analysing a system in such a setting involves computing the set of (Nash) equilibria in the concurrent game. However, we show that, with respect to the above model of strategies (arguably, the "standard" model in the computer science literature), bisimilarity does not preserve the existence of Nash equilibria. Thus, two concurrent games which are behaviourally equivalent from a semantic perspective, and which from a logical perspective satisfy the same temporal logic formulae, may nevertheless have fundamentally different properties (solutions) from a game theoretic perspective. Our aim in this paper is to explore the issues raised by this discovery. After illustrating the issue by way of a motivating example, we present three models of strategies with respect to which the existence of Nash equilibria is preserved under bisimilarity. We use some of these models of strategies to provide new semantic foundations for logics for strategic reasoning, and investigate restricted scenarios where bisimilarity can be shown to preserve the existence of Nash equilibria with respect to the conventional model of strategies in the computer science literature.
@incollection{J-GHPW19,author={Gutierrez, Julian and Harrenstein, Paul and Perelli, Giuseppe and Wooldridge, Michael},title={Nash Equilibrium and Bisimulation Invariance.},booktitle={Logical Methods in Computer Science},journal={Logical Methods in Computer Science},volume={15, issue 3},year={2019},}
In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we study the design of incentives so that a desirable equilibrium is obtained, for instance, an equilibrium satisfying a given temporal logic property - a problem that we call equilibrium design. We base our study on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players’ goals as mean-payoff objectives. In particular, we consider system specifications given by LTL and GR(1) formulae, and show that implementing a mechanism to ensure that a given temporal logic property is satisfied on some/every Nash equilibrium of the game, whenever such a mechanism exists, can be done in PSPACE for LTL properties and in NP/Sigma^P_2 for GR(1) specifications. We also study the complexity of various related decision and optimisation problems, such as optimality and uniqueness of solutions, and show that the complexities of all such problems lie within the polynomial hierarchy. As an application, equilibrium design can be used as an alternative solution to the rational synthesis and verification problems for concurrent games with mean-payoff objectives whenever no solution exists, or as a technique to repair, whenever possible, concurrent games with undesirable rational outcomes (Nash equilibria) in an optimal way.
@inproceedings{C-GNPW19b,author={Gutierrez, Julian and Najib, Muhammad and Perelli, Giuseppe and Wooldridge, Michael},title={Equilibrium Design for Concurrent Games},booktitle={30th International Conference on Concurrency Theory, {CONCUR} 2019, August 27-30, 2019, Amsterdam, the Netherlands.},pages={22:1--22:16},year={2019},}
IJCAI-19
Reasoning about Quality and Fuzziness of Strategic Behaviours.
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 our logic, based on a quantitative extension of Quantified CTL*.
@inproceedings{C-BKMMMP19,author={Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe},title={Reasoning about Quality and Fuzziness of Strategic Behaviours.},booktitle={Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, {IJCAI} 2019, Macao, China, August 10-16, 2019},pages={1588--1594},year={2019},}
AAMAS-19
Enforcing Equilibria in Multi-Agent Systems.
Perelli, Giuseppe
In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS ’19, Montreal, QC, Canada, May 13-17, 2019 2019
We introduce and investigate Normative Synthesis: a new class of problems for the equilibrium verification that counters the absence of equilibria by purposely constraining multi-agent systems. We show that norms are powerful enough to ensure a positive answer to every instance of the equilibrium verification problem. Subsequently, we focus on two optimization versions, that aim at providing a solution in compliance with implementation costs. We show that the complexities of our procedures range between 2ExpTime and 3ExpTime, thus that the problems are no harder than the corresponding equilibrium verification ones.
@inproceedings{C-Per19,author={Perelli, Giuseppe},title={Enforcing Equilibria in Multi-Agent Systems.},booktitle={Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, {AAMAS} '19, Montreal, QC, Canada, May 13-17, 2019},pages={188--196},year={2019},}
We introduce Cycle-CTL*, an extension of CTL* with cycle quantifications that are able to predicate over cycles. The introduced logic turns out to be very expressive. Indeed, we prove that it strictly extends CTL* and is orthogonal to μ-Calculus. We also give an evidence of its usefulness by providing few examples involving non-regular properties. We extensively investigate both the model-checking and satisfiability problems for Cycle-CTL* and some of its variants/fragments.
@incollection{J-FMMPS18,author={Fontaine, Gaelle and Mogavero, Fabio and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana},title={Cycle Detection in Computation Tree Logic.},booktitle={Information and Computation},volume={262},number={Part},pages={265--279},year={2018},}
Reactive Modules is a high-level modelling language for concurrent, distributed, and multi-agent systems, which is used in a number of practical model checking tools. Reactive Modules Games are a game-theoretic extension of Reactive Modules, in which system components are assumed to act strategically in an attempt to satisfy a temporal logic formula representing their individual goal. Reactive Modules Games with perfect information have been extensively studied, and the complexity of game theoretic decision problems relating to such games (such as the existence of Nash equilibria) have been comprehensively classified. In this article, we study Reactive Modules Games in which agents have only partial visibility of their environment.
@incollection{J-GPW18,author={Gutierrez, Julian and Perelli, Giuseppe and Wooldridge, Michael},title={Imperfect Information in Reactive Modules Games.},booktitle={Information and Computation},volume={261},number={Part},pages={650--675},year={2018},}
In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings 2018
We present EVE (Equilibrium Verification Environment), a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems. In EVE, systems are modelled using the Simple Reactive Module Language (SRML) as a collection of independent system components (players/agents in a game) and players’ goals are expressed using Linear Temporal Logic (LTL) formulae. EVE can be used to automatically check the existence of pure strategy Nash equilibria in such concurrent and multi-agent systems and to verify which temporal logic properties are satisfied in the equilibria.
@inproceedings{C-GNPW18,author={Gutierrez, Julian and Najib, Muhammad and Perelli, Giuseppe and Wooldridge, Michael},title={EVE: A Tool for Temporal Equilibrium Analysis.},booktitle={Automated Technology for Verification and Analysis - 16th International Symposium, {ATVA} 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings},year={2018},pages={551--557},}
IJCAI-18
Synthesis of Controllable Nash Equilibria in Games with Quantitative Objectives.
In Rational Synthesis, we consider a multi-agent system in which some of the agents are controllable and some are not. All agents have objectives, and the goal is to synthesize strategies for the controllable agents so that their objectives are satisfied, assuming rationality of the uncontrollable agents. Previous work on rational synthesis considers objectives in LTL, namely ones that describe on-going behaviors, and in Objective-LTL, which allows ranking of LTL formulas. In this paper, we extend rational synthesis to LTL[F] – an extension of LTL by quality operators. The satisfaction value of an LTL[F] formula is a real value in [0,1], where the higher the value is, the higher is the quality in which the computation satisfies the specification. The extension significantly strengthens the framework of rational synthesis and enables a study its game- and social-choice theoretic aspects. In particular, we study the price of stability and price of anarchy of the rational-synthesis game and use them to explain the cooperative and non-cooperative settings of rational synthesis. Our algorithms make use of strategy logic and decision procedures for it. Thus, we are able to handle the richer quantitative setting using existing tools. In particular, we show that the cooperative and non-cooperative versions of quantitative rational synthesis are 2EXPTIME-complete and in 3EXPTIME, respectively – not harder than the complexity known for their Boolean analogues.
@inproceedings{C-AKP18,author={Almagor, Shaull and Kupferman, Orna and Perelli, Giuseppe},title={Synthesis of Controllable Nash Equilibria in Games with Quantitative Objectives.},booktitle={Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, {IJCAI} 2018, July 13-19, 2018, Stockholm, Sweden.},pages={35--41},year={2018},}
2017
LMCS
Reasoning about Strategies: On the Satisfiability Problem.
Strategy Logic (SL, for short) has been introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, subsuming all major previously studied modal logics for strategic reasoning, including ATL, ATL*, and the like. Unfortunately, due to its high expressiveness, SL has a non-elementarily decidable model-checking problem and the satisfiability question is undecidable, specifically Sigma_1^1. In order to obtain a decidable sublogic, we introduce and study here One-Goal Strategy Logic (SL[1G], for short). This is a syntactic fragment of SL, strictly subsuming ATL*, which encompasses formulas in prenex normal form having a single temporal goal at a time, for every strategy quantification of agents. We prove that, unlike SL, SL[1G] has the bounded tree-model property and its satisfiability problem is decidable in 2ExpTime, thus not harder than the one for ATL*.
@incollection{J-MMPV17,author={Mogavero, Fabio and Murano, Aniello and Perelli, Giuseppe and Vardi, Moshe},title={Reasoning about Strategies: On the Satisfiability Problem.},booktitle={Logical Methods in Computer Science},volume={13, issue 1},year={2017},}
Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions. In this paper, we contribute to research on Cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is PSpace-Complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.
@inproceedings{C-BMPS17,author={Bozzelli, Laura and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana},title={Hierarchical Cost-Parity Games.},booktitle={24th International Symposium on Temporal Representation and Reasoning, {TIME} 2017, October 16-18, 2017, Mons, Belgium},pages={6:1--6:17},year={2017},}
Game theory provides a well-established framework for the analysis of concurrent and multi-agent systems. The basic idea is that concurrent processes (agents) can be understood as corresponding to players in a game; plays represent the possible computation runs of the system; and strategies define the behaviour of agents. Typically, strategies are modelled as functions from sequences of system states to player actions. Analysing a system in such a way involves computing the set of (Nash) equilibria in the game. However, we show that, with respect to the above model of strategies—the standard model in the literature—bisimilarity does not preserve the existence of Nash equilibria. Thus, two concurrent games which are behaviourally equivalent from a semantic perspective, and which from a logical perspective satisfy the same temporal formulae, nevertheless have fundamentally different properties from a game theoretic perspective. In this paper we explore the issues raised by this discovery, and investigate three models of strategies with respect to which the existence of Nash equilibria is preserved under bisimilarity. We also use some of these models of strategies to provide new semantic foundations for logics for strategic reasoning, and investigate restricted scenarios where bisimilarity can be shown to preserve the existence of Nash equilibria with respect to the conventional model of strategies in the literature.
@inproceedings{C-GHPW17,author={Gutierrez, Julian and Harrenstein, Paul and Perelli, Giuseppe and Wooldridge, Michael},title={Nash Equilibrium and Bisimulation Invariance.},booktitle={28th International Conference on Concurrency Theory, {CONCUR} 2017, September 5-8, 2017, Berlin, Germany},pages={17:1--17:16},year={2017},}
IJCAI-17
Nash Equilibrium in Concurrent Games with Lexicographic Preferences.
In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017 2017
We study concurrent games with finite-memory strategies where players are given a Buchi and a mean-payoff objective, which are related by a lexicographic order: a player first prefers to satisfy its Buchi objective, and then prefers to minimise costs, which are given by a mean-payoff function. In particular, we show that deciding the existence of a strict Nash equilibrium in such games is decidable, even if players’ deviations are implemented as infinite memory strategies.
@inproceedings{C-GMPRW17,author={Gutierrez, Julian and Murano, Aniello and Perelli, Giuseppe and Rubin, Sasha and Wooldridge, Michael},title={Nash Equilibrium in Concurrent Games with Lexicographic Preferences.},booktitle={Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, {IJCAI} 2017, Melbourne, Australia, August 19-25, 2017},pages={1067--1073},year={2017},}
Linear Dynamic Logic on finite traces (LDL_f) is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on LDL_f. This study builds upon a generalisation of Boolean games, a logic-based game model of multi-agent systems where players have goals succinctly represented in a logical way. Because LDL_f goals are considered, in the setting we study—iterated Boolean games with goals over finite traces (iBG_f)—players’ goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace. In particular, using alternating automata, the paper investigates automata-theoretic approaches to the characterisation and verification of (pure strategy Nash) equilibria, shows that the set of Nash equilibria in games with LDL_f objectives is regular, and provides complexity results for the associated automata constructions.
@inproceedings{C-GPW17,author={Gutierrez, Julian and Perelli, Giuseppe and Wooldridge, Michael},title={Iterated Games with LDL Goals on Finite Traces.},booktitle={Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, {AAMAS} 2017, S{\~{a}}o Paulo, Brazil, May 8-12, 2017},pages={696--704},year={2017},}
Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g., a Kripke structure, and a formula specifying its expected behaviour, one can verify whether the system meets the behaviour by checking the formula against the model. Classically, system behaviour is expressed by a formula of a temporal logic, such as LTL and the like. These logics are “point-wise” interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those constraining the temporal relations between pairs of temporally extended events or involving temporal aggregations, which are inherently “interval-based”, and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham’s interval temporal logic HS over finite Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against finite Kripke structures is decidable by a suitable small model theorem, and we provide a lower bound to its computational complexity.
@incollection{J-MMMPP16,author={Molinari, Alberto and Montanari, Angelo and Murano, Aniello and Perelli, Giuseppe and Peron, Adriano},title={Checking Interval Properties of Computations.},year={2016},issn={0001-5903},booktitle={ACTA Informatica},publisher={Springer Berlin Heidelberg},pages={1-33},}
Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. The environment often consists of agents that have objectives of their own. Thus, it makes sense to soften the universal quantification on the behavior of the environment and take the objectives of its underlying agents into an account. Fisman et al. introduced rational synthesis: the problem of synthesis in the context of rational agents. The input to the problem consists of temporal logic formulas specifying the objectives of the system and the agents that constitute the environment, and a solution concept (e.g., Nash equilibrium). The output is a profile of strategies, for the system and the agents, such that the objective of the system is satisfied in the computation that is the outcome of the strategies, and the profile is stable according to the solution concept; that is, the agents that constitute the environment have no incentive to deviate from the strategies suggested to them. In this paper we continue to study rational synthesis. First, we suggest an alternative definition to rational synthesis, in which the agents are rational but not cooperative. We call such problem strong rational synthesis. In the strong rational synthesis setting, one cannot assume that the agents that constitute the environment take into account the strategies suggested to them. Accordingly, the output is a strategy for the system only, and the objective of the system has to be satisfied in all the compositions that are the outcome of a stable profile in which the system follows this strategy. We show that strong rational synthesis is 2EXPTIME-COMPLETE, thus it is not more complex than traditional synthesis or rational synthesis. Second, we study a richer specification formalism, where the objectives of the system and the agents are not Boolean but quantitative. In this setting, the objective of the system and the agents is to maximize their outcome. The quantitative setting significantly extends the scope of rational synthesis, making the game-theoretic approach much more relevant. Finally, we enrich the setting to one that allows coalitions of agents that constitute the system or the environment.
@incollection{J-KPV16,author={Kupferman, Orna and Perelli, Giuseppe and Vardi, Moshe},title={Synthesis with Rational Environments.},year={2016},booktitle={Annals of Mathematics and Artificial Intelligence},publisher={Springer International Publishing},isbn={978-3-319-17130-2},volume={8953},pages={219-235},series={Lecture Notes in Computer Science},}
In Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016. 2016
Temporal logic is a very powerful formalism deeply investigated and used in formal system design and verification. Its application usually reduces to solving specific decision problems such as model checking and satisfiability. In these kind of problems, the solution often requires detecting some specific properties over cycles. For instance, this happens when using classic techniques based on automata, game-theory, SCC decomposition, and the like. Surprisingly, no temporal logics have been considered so far with the explicit ability of talking about cycles.
In this paper we introduce Cycle-CTL*, an extension of the classical branching-time temporal logic CTL* along with cycle quantifications in order to predicate over cycles. This logic turns out to be very expressive. Indeed, we prove that it strictly extends CTL* and is orthogonal to mu-calculus. We also give an evidence of its usefulness by providing few examples involving non-regular properties.
We investigate the model checking problem for Cycle-CTL* and show that it is PSPACE-Complete as for CTL*. We also study the satisfiability problem for the existential-cycle fragment of the logic and show that it is solvable in 2ExpTime. This result makes use of an automata-theoretic approach along with novel ad-hoc definitions of bisimulation and tree-like unwinding.
@inproceedings{C-FMMPS16,author={Fontaine, Gaelle and Mogavero, Fabio and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana},title={Cycle Detection in Computation Tree Logic.},booktitle={Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016.},year={2016},pages={164--177},}
CIAA-16
Solving Parity Games by Using an Automata-Based Algorithm.
Parity games are abstract infinite-round games that take an important role in formal verification. In the basic setting, these games are two-player, turn-based, and played under perfect information on directed graphs, whose nodes are labeled with priorities. The winner of a play is determined according to the parities (even or odd) of the minimal priority occurring infinitely often in that play. The problem of finding a winning strategy in parity games is known to be in UPTime ∩ CoUPTime and deciding whether a polynomial time solution exists is a long-standing open question. In the last two decades, a variety of algorithms have been proposed. Many of them have been also implemented in a platform named PGSolver. This has enabled an empirical evaluation of these algorithms and a better understanding of their relative merits. \{In this paper, we further contribute to this subject by implementing, for the first time, an algorithm based on alternating automata. More precisely, we consider an algorithm introduced by Kupferman and Vardi that solves a parity game by solving the emptiness problem of a corresponding alternating parity automaton. Our empirical evaluation demonstrates that this algorithm outperforms other algorithms when the game has a small number of priorities relative to the size of the game. In many concrete applications, we do indeed end up with parity games where the number of priorities is relatively small. This makes the new algorithm quite useful in practice.
@inproceedings{C-DMPV16,author={{di Stasio}, Antonio and Murano, Aniello and Perelli, Giuseppe and Vardi, Moshe},title={Solving Parity Games by Using an Automata-Based Algorithm.},booktitle={Implementation and Application of Automata - 21st International Conference, {CIAA} 2016, Seoul, South Korea, July 19-22, 2016, Proceedings},pages={64--76},year={2016},}
AAMAS-16
Expressiveness and Nash Equilibrium in Iterated Boolean Games.
We introduce and investigate a novel notion of expressiveness for temporal logics that is based on game theoretic properties of multi-agent systems. We focus on iterated Boolean games, where each agent i has a goal γai, represented using (a fragment of) Linear Temporal Logic (LTL). The goal γai captures agent i’s preferences: the models of γi represent system behaviours that would satisfy i, and each player is assumed to act strategically, taking into account the goals of other players, in order to bring about computations satisfying their goal. In this setting, we apply the standard game-theoretic concept of Nash equilibria: the Nash equilibria of an iterated Boolean game can be understood as a (possibly empty) set of computations, each computation representing one way the system could evolve if players chose strategies in Nash equilibrium. Such an equilibrium set of computations can be understood as expressing a temporal property—which may or may not be expressible within a particular LTL fragment. The new notion of expressiveness that we study is then as follows: what LTL properties are characterised by the Nash equilibria of games in which agent goals are expressed in fragments of LTL? We formally define and investigate this notion of expressiveness and some related issues, for a range of LTL fragments.
@inproceedings{C-GHPW16,author={Gutierrez, Julian and Harrenstein, Paul and Perelli, Giuseppe and Wooldridge, Michael},title={Expressiveness and Nash Equilibrium in Iterated Boolean Games.},booktitle={Proceedings of the 2016 International Conference on Autonomous Agents {\&} Multiagent Systems, Singapore, May 9-13, 2016},pages={707--715},year={2016},}
In Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29, 2016. 2016
Reactive Modules is a high-level modelling language for concurrent, distributed, and multi-agent systems, which is used in a number of practical model checking tools. Reactive Modules Games are a game-theoretic extension of Reactive Modules, in which agents in a system are assumed to act strategically in an attempt to satisfy a temporal logic formula representing their individual goal. Reactive Modules Games with perfect information have been closely studied, and the complexity of game theoretic decision problems relating to such games have been comprehensively classified. However, to date, no work has considered the imperfect information case. In this paper we address this gap, investigating Reactive Modules Games in which agents have only partial visibility of their environment.
@inproceedings{C-GPW16,author={Gutierrez, Julian and Perelli, Giuseppe and Wooldridge, Michael},title={Imperfect Information in Reactive Module Games.},booktitle={Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, {KR} 2016, Cape Town, South Africa, April 25-29, 2016.},pages={390--400},year={2016},}
AAAI-16
Rational Verification: From Model Checking to Equilibrium Checking.
Rational verification is concerned with establishing whether a given temporal logic formula φ is satisfied in some or all equilibrium computations of a multi-agent system – that is, whether the system will exhibit the behaviour φ under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the framework of rational verification, we present formal models through which rational verification can be studied, and survey the complexity of key decision problems. We give an overview of a prototype software tool for rational verification, and conclude with a discussion and related work.
@inproceedings{C-WGHMPT16,author={Wooldridge, Michael and Gutierrez, Julian and Harrenstein, Paul and Marchioni, Enrico and Perelli, Giuseppe and Toumi, Alexis},title={Rational Verification: From Model Checking to Equilibrium Checking.},booktitle={Proceedings of the Thirtieth {AAAI} Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, {USA.}},pages={4184--4191},year={2016},}
2015
PRIMA-15
Multi-Agent Path Planning in Known Dynamic Environments.
We consider the problem of planning paths of multiple agents in a dynamic but predictable environment. Typical scenarios are evacuation, reconfiguration, and containment. We present a novel representation of abstract path-planning problems in which the stationary environment is explicitly coded as a graph (called the arena) while the dynamic environment is treated as just another agent. The complexity of planning using this representation is pspace-complete. The arena complexity (i.e., the complexity of the planning problem in which the graph is the only input, in particular, the number of agents is fixed) is np-hard. Thus, we provide structural restrictions that put the arena complexity of the planning problem into ptime(for any fixed number of agents). The importance of our work is that these structural conditions (and hence the complexity results) do not depend on graph-theoretic properties of the arena (such as clique- or tree-width), but rather on the abilities of the agents.
@inproceedings{C-MPR15,author={Murano, Aniello and Perelli, Giuseppe and Rubin, Sasha},title={Multi-Agent Path Planning in Known Dynamic Environments.},booktitle={{PRIMA} 2015: Principles and Practice of Multi-Agent Systems - 18th International Conference, Bertinoro, Italy, October 26-30, 2015, Proceedings},pages={218--231},year={2015},}
In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July25-31, 2015 2015
In this paper we investigate the model-checking problem of pushdown multi-agent systems for ATL* specifications.To this aim, we introduce pushdown game structures over which ATL* formulas are interpreted. We show an algorithm that solves the addressed model-checking problem in 3ExpTime. We also provide a 2ExpSpace lower bound by showing a reduction from the word acceptance problem for deterministic Turing machines with doubly exponential space.
@inproceedings{C-MP15a,author={Murano, Aniello and Perelli, Giuseppe},title={Pushdown Multi-Agent System Verification},booktitle={Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, {IJCAI} 2015, Buenos Aires, Argentina, July25-31, 2015},pages={1090--1097},year={2015},}
2014
TOCL
Reasoning about Strategies: On the Model-Checking Problem.
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multiagent games, such as Atl, Atl*, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by CHP-Sl, with the aim of getting a powerful framework for reasoning explicitly about strategies. CHP-Sl is obtained by using first-order quantifications over strategies and has been investigated in the very specific setting of two-agents turned-based games, where a nonelementary model-checking algorithm has been provided. While CHP-Sl is a very expressive logic, we claim that it does not fully capture the strategic aspects of multiagent systems. \{In this article, we introduce and study a more general strategy logic, denoted Sl, for reasoning about strategies in multiagent concurrent games. As a key aspect, strategies in Sl are not intrinsically glued to a specific agent, but an explicit binding operator allows an agent to bind to a strategy variable. This allows agents to share strategies or reuse one previously adopted. We prove that Sl strictly includes CHP-Sl, while maintaining a decidable model-checking problem. In particular, the algorithm we propose is computationally not harder than the best one known for CHP-Sl. Moreover, we prove that such a problem for Sl is NonElementary. This negative result has spurred us to investigate syntactic fragments of Sl, strictly subsuming Atl*, with the hope of obtaining an elementary model-checking problem. Among others, we introduce and study the sublogics Sl[ng], Sl[bg], and Sl[1g]. They encompass formulas in a special prenex normal form having, respectively, nested temporal goals, Boolean combinations of goals, and, a single goal at a time. Intuitively, for a goal, we mean a sequence of bindings, one for each agent, followed by an Ltl formula. We prove that the model-checking problem for Sl[1g] is 2ExpTime-complete, thus not harder than the one for Atl*. In contrast, Sl[ng] turns out to be NonElementary-hard, strengthening the corresponding result for Sl. Regarding Sl[bg], we show that it includes CHP-Sl and its model-checking is decidable with a 2ExpTimelower-bound.
It is worth enlightening that to achieve the positive results about Sl[1g], we introduce a fundamental property of the semantics of this logic, called behavioral, which allows to strongly simplify the reasoning about strategies. Indeed, in a nonbehavioral logic such as Sl[bg] and the subsuming ones, to satisfy a formula, one has to take into account that a move of an agent, at a given moment of a play, may depend on the moves taken by any agent in another counterfactual play.
@incollection{J-MMPV14,author={Mogavero, Fabio and Murano, Aniello and Perelli, Giuseppe and Vardi, Moshe},title={Reasoning about Strategies: On the Model-Checking Problem.},booktitle={{ACM} Transaction on Computational Logic},publisher={ACM Association for Computing Machinery},volume={15(4)},pages={34:1--34:47},year={2014},}
Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. The environment often consists of agents that have objectives of their own. Thus, it makes sense to soften the universal quantification on the behavior of the environment and take the objectives of its underlying agents into an account. Fisman et al. introduced rational synthesis: the problem of synthesis in the context of rational agents. The input to the problem consists of temporal-logic formulas specifying the objectives of the system and the agents that constitute the environment, and a solution concept (e.g., Nash equilibrium). The output is a profile of strategies, for the system and the agents, such that the objective of the system is satisfied in the computation that is the outcome of the strategies, and the profile is stable according to the solution concept; that is, the agents that constitute the environment have no incentive to deviate from the strategies suggested to them. \{In this paper we continue to study rational synthesis. First, we suggest an alternative definition to rational synthesis, in which the agents are rational but not cooperative. In the non-cooperative setting, one cannot assume that the agents that constitute the environment take into account the strategies suggested to them. Accordingly, the output is a strategy for the system only, and the objective of the system has to be satisfied in all the compositions that are the outcome of a stable profile in which the system follows this strategy. We show that rational synthesis in this setting is 2ExpTime-complete, thus it is not more complex than traditional synthesis or cooperative rational synthesis. Second, we study a richer specification formalism, where the objectives of the system and the agents are not Boolean but quantitative. In this setting, the goal of the system and the agents is to maximize their outcome. The quantitative setting significantly extends the scope of rational synthesis, making the game-theoretic approach much more relevant.
@inproceedings{C-KPV14,author={Kupferman, Orna and Perelli, Giuseppe and Vardi, Moshe},title={Synthesis with Rational Environments.},booktitle={Multi-Agent Systems - 12th European Conference, {EUMAS} 2014, Prague, Czech Republic, December 18-19, 2014, Revised Selected Papers},pages={219--235},year={2014},}
Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g. A Kripke structure, and a formula specifying its expected behavior, one can verify whether the system meets the behavior by checking the formula against the model. Classically, system behavior is given as a formula of a temporal logic, such as LTL and the like. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those involving temporal aggregations, which are inherently "interval-based", and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham’s interval temporal logic HS over Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against Kripke structures is decidable by a suitable small model theorem, and we outline a PSpace decision procedure for the meaningful fragments AAbarBBbar and AAbarEEbar.
@inproceedings{C-MMPP14,author={Montanari, Angelo and Murano, Aniello and Perelli, Giuseppe and Peron, Adriano},title={Checking Interval Properties of Computations.},booktitle={21st International Symposium on Temporal Representation and Reasoning, {TIME} 2014, Verona, Italy, September 8-10, 2014},pages={59--68},year={2014},}
2012
CONCUR-12
What Makes ATL* Decidable? A Decidable Fragment of Strategy Logic.
Strategy Logic (Sl, for short) has been recently introduced by Mogavero, Murano, and Vardi as a formalism for reasoning explicitly about strategies, as first-order objects, in multi-agent concurrent games. This logic turns out to be very powerful, strictly subsuming all major previously studied modal logics for strategic reasoning, including Atl, Atl*, and the like. The price that one has to pay for the expressiveness of Sl is the lack of important model-theoretic properties and an increased complexity of decision problems. In particular, Sl does not have the bounded-tree model property and the related satisfiability problem is highly undecidable while for Atl* it is 2ExpTime-complete. An obvious question that arises is then what makes Atl* decidable. Understanding this should enable us to identify decidable fragments of Sl. We focus, in this work, on the limitation of Atl* to allow only one temporal goal for each strategic assertion and study the fragment of Sl with the same restriction. Specifically, we introduce and study the syntactic fragment One-Goal Strategy Logic (Sl[1g], for short), which consists of formulas in prenex normal form having a single temporal goal at a time for every strategy quantification of agents. We show that Sl[1g] is strictly more expressive than Atl*. Our main result is that Sl[1g] has the bounded tree-model property and its satisfiability problem is 2ExpTime-complete, as it is for Atl*.
@inproceedings{C-MMPV12,author={Mogavero, Fabio and Murano, Aniello and Perelli, Giuseppe and Vardi, Moshe},title={What Makes ATL* Decidable? A Decidable Fragment of Strategy Logic.},booktitle={{CONCUR} 2012 - Concurrency Theory - 23rd International Conference, {CONCUR} 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings},series={LNCS 7454},publisher={Springer},year={2012},}