Giuseppe Perelli

JAAMAS Journal 2025 Journal Article

Behavioral QLTL

• Giuseppe De Giacomo
• Giuseppe Perelli

Abstract 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” (Abadi et al. , Realizable and Unrealizable Specifications of Reactive Systems, 1989 ). 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. As such 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.

KR Conference 2025 Conference Paper

LTL Synthesis Under Multi-Agent Environment Assumptions

• Benjamin Aminof
• Giuseppe De Giacomo
• Giuseppe Perelli
• Sasha Rubin

We investigate LTL synthesis under structured assumptions about the environment. In our setting, the environment is viewed by the protagonist as a collection of peer agents acting together in a shared world. In contrast to the symmetrical frameworks typically studied in multi-agent systems, we take a strikingly asymmetric first-person perspective in which the protagonist ascribes a specification to each of its peer agents and the world, capturing its understanding of their possible strategies. We show that in this setting, LTL synthesis has the same computational complexity as standard LTL synthesis, i. e. , 2EXPTIME-complete. We establish this via a sophisticated, yet fully implementable, argument that builds on the notion of traces compatible with strategies: we use the fact that if the basic specification of the world and of each agent is given in LTL then the sets of traces compatible with the strategies describing the behaviors of the agents are omega-regular. This enables the use of word-automata rather than the more complicated tree-automata.

IJCAI Conference 2024 Conference Paper

Endogenous Energy Reactive Modules Games: Modelling Side Payments among Resource-Bounded Agents

• Julian Gutierrez
• David Hyland
• Muhammad Najib
• Giuseppe Perelli
• Michael Wooldridge

We introduce Energy Reactive Modules Games (ERMGs), an extension of Reactive Modules Games (RMGs) in which actions incur an energy cost (which may be positive or negative), and the choices that players make are restricted by the energy available to them. In ERMGs, each action is associated with an energy level update, which determines how their energy level is affected by the performance of the action. In addition, agents are provided with an initial energy allowance. This allowance plays a crucial role in shaping an agent’s behaviour, as it must be taken into consideration when one is determining their strategy: agents may only perform actions if they have the requisite energy. We begin by studying rational verification for ERMGs and then introduce Endogenous ERMGs, where agents can choose to transfer their energy to other agents. This exchange may enable equilibria that are impossible to achieve without such transfers. We study the decision problem of whether a stable outcome exists under both the Nash equilibrium and Core solution concepts.

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.

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.

AAAI Conference 2024 Conference Paper

Pure-Past Action Masking

• Giovanni Varricchione
• Natasha Alechina
• Mehdi Dastani
• Giuseppe De Giacomo
• Brian Logan
• Giuseppe Perelli

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.

ECAI Conference 2024 Conference Paper

Synthesis of Reward Machines for Multi-Agent Equilibrium Design

• Muhammad Najib
• Giuseppe Perelli

Mechanism design is a well-established game-theoretic paradigm for designing games to achieve desired outcomes. This paper addresses a closely related but distinct concept, equilibrium design. Unlike mechanism design, the designer’s authority in equilibrium design is more constrained; she can only modify the incentive structures in a given game to achieve certain outcomes without the ability to create the game from scratch. We study the problem of equilibrium design using dynamic incentive structures, known as reward machines. We use weighted concurrent game structures for the game model, with goals (for the players and the designer) defined as mean-payoff objectives. We show how reward machines can be used to represent dynamic incentives that allocate rewards in a manner that optimises the designer’s goal. We also introduce the main decision problem within our framework, the payoff improvement problem. This problem essentially asks whether there exists a dynamic incentive (represented by some reward machine) that can improve the designer’s payoff by more than a given threshold value. We present two variants of the problem: strong and weak. We demonstrate that both can be solved in polynomial time using a Turing machine equipped with an NP oracle. Furthermore, we also establish that these variants are either NP-hard or coNP-hard. Finally, we show how to synthesise the corresponding reward machine if it exists.

EUMAS Conference 2023 Conference Paper

Behavioral QLTL

• Giuseppe De Giacomo
• Giuseppe Perelli

Abstract 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” [ 1 ]. 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.

ECAI Conference 2023 Conference Paper

Optimal Alignment of Temporal Knowledge Bases

• Oliver Fernández Gil
• Fabio Patrizi
• Giuseppe Perelli
• Anni-Yasmin Turhan

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.

PRL Workshop 2023 Workshop Paper

Preemptive Restraining Bolts

• Giovanni Varricchione
• Natasha Alechina
• Mehdi Dastani
• Giuseppe De Giacomo
• Brian Logan
• Giuseppe Perelli

We present preemptive restraining bolts (PRBs), a new approach to safe reinforcement learning which uses non-Markovian action masking, i.e., actions are masked (disallowed) based on the history of the system, rather than just the current state. PRBs are expressed in Pure Past Linear Temporal Logic and have minimal overhead (linear in the size of the state) compared to Markovian action masking, while having the same expressive power as other non-Markovian approaches such as shields (that can express any safety Linear Temporal Logic property). As with restraining bolts, the language in which safety properties are expressed does not have to be the same as the language specifying the features of the state for the learning agent. Critically, PRBs can be applied in the learning process to learn an optimal safe policy while using only safe actions during learning. As a result, PRBs can be used to provide general safety guarantees, without compromising efficiency.

LAMAS&SR Workshop 2023 Workshop Paper

Strategy Repair in Reachability Games

• Pierre Gaillard
• Fabio Patrizi
• Giuseppe Perelli

ECAI Conference 2023 Conference Paper

Strategy Repair in Reachability Games

• Pierre Gaillard
• Fabio Patrizi
• Giuseppe Perelli

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.

KR Conference 2022 Conference Paper

Automatic Synthesis of Dynamic Norms for Multi-Agent Systems

• Natasha Alechina
• Giuseppe De Giacomo
• Brian Logan
• Giuseppe Perelli

Norms have been widely proposed to coordinate and regulate multi-agent systems (MAS) behaviour. 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.

TIME Conference 2022 Conference Paper

Giving Instructions in Linear Temporal Logic

• Julian Gutierrez 0001
• Sarit Kraus
• Giuseppe Perelli
• Michael J. Wooldridge

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.

Highlights Conference 2022 Conference Abstract

Timed Trace Alignment with Metric Temporal Logic over Finite Traces

• Giuseppe Perelli

Trace Alignment is a prominent problem in Declarative Process Mining, 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 DECLARE, 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 presentation, we introduce 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 LTLf. 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 more sophisticated machinery based on alternating (timed) automata, as opposed to the standard finite-state automata sufficient for the untimed version. The main contribution is a provably correct, effective technique for Timed Trace Alignment that takes advantage of results on MTLf decidability as well as on reachability for well-structured transition systems.

Highlights Conference 2021 Conference Abstract

Behavioral QLTL

• Giuseppe Perelli

We introduce Behavioral QLTL, which is a “behavioral” variant of linear-time temporal logic on infinite traces 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 to the logic a strategic flavor that we usually associate to planning. Indeed we show that temporally extended planning in nondeterministic domains, as well as 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 conditional 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 with simpler forms of behavioral semantics.

IJCAI Conference 2021 Conference Paper

HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs

• Giuseppe De Giacomo
• Paolo Felli
• Marco Montali
• Giuseppe Perelli

Temporal logics over finite traces, such as LTLf and its extension LDLf, have been adopted in several areas, including Business Process Management (BPM), to check properties of processes whose executions have an unbounded, but finite, length. These logics express properties of single traces in isolation, however, especially in BPM it is also of interest to express properties over the entire log, i. e. , properties that relate multiple traces of the log at once. In the case of infinite-traces, HyperLTL has been proposed to express these ``hyper'' properties. In this paper, motivated by BPM, we introduce HyperLDLf, a logic that extends LDLf with the hyper features of HyperLTL. We provide a sound, complete and computationally optimal technique, based on DFAs manipulation, for the model checking problem in the relevant case where the set of traces (i. e. , the log) is a regular language. We illustrate how this form of model checking can be used for verifying log of business processes and for advanced forms of process mining.

KR Conference 2021 Conference Paper

Synthesis with Mandatory Stop Actions

• Giuseppe De Giacomo
• Antonio Di Stasio
• Giuseppe Perelli
• Shufang Zhu

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 Buchi 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 Buchi automata. In this way, again, we sidestep Buchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.

KR Conference 2021 Conference Paper

Timed Trace Alignment with Metric Temporal Logic over Finite Traces

• Giuseppe De Giacomo
• Aniello Murano
• Fabio Patrizi
• Giuseppe Perelli

Trace Alignment is a prominent problem in Declarative Process Mining, 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 DECLARE, 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 LTLf. 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 MTLf decidability as well as on reachability for well-structured transition systems.

AIJ Journal 2020 Journal Article

Automated temporal equilibrium analysis: Verification and synthesis of multi-player games

• Julian Gutierrez
• Muhammad Najib
• Giuseppe Perelli
• Michael Wooldridge

TCS Journal 2020 Journal Article

Hierarchical cost-parity games

• Laura Bozzelli
• Aniello Murano
• Giuseppe Perelli
• Loredana Sorrentino

ECAI Conference 2020 Conference Paper

Reasoning About Quality and Fuzziness of Strategic Behaviours

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

AAMAS Conference 2019 Conference Paper

Enforcing Equilibria in Multi-Agent Systems

• Giuseppe Perelli

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.

IJCAI Conference 2019 Conference Paper

On Computational Tractability for Rational Verification

• Julian Gutierrez
• Muhammad Najib
• Giuseppe Perelli
• Michael Wooldridge

Rational verification involves checking which temporal logic properties hold of a concurrent and multiagent system, under the assumption that agents in the system choose strategies in game theoretic equilibrium. Rational verification can be understood as a counterpart of model checking for multiagent systems, but while 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 more intractable: it is 2EXPTIME-complete with LTL specifications, even when using explicit-state system representations. In this paper 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 most response properties of reactive systems. We also provide improved complexity results for rational verification when considering players' goals given by mean-payoff utility functions -- arguably the most widely used quantitative objective for agents in concurrent and multiagent systems. In particular, we show that for a number of relevant settings, rational verification can be done in polynomial space or even in polynomial time.

IJCAI Conference 2019 Conference Paper

Reasoning about Quality and Fuzziness of Strategic Behaviours

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

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

IJCAI Conference 2018 Conference Paper

Synthesis of Controllable Nash Equilibria in Quantitative Objective Game

• Shaull Almagor
• Orna Kupferman
• Giuseppe Perelli

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.

TIME Conference 2017 Conference Paper

Hierarchical Cost-Parity Games

• Laura Bozzelli
• Aniello Murano
• Giuseppe Perelli
• Loredana Sorrentino

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.

AAMAS Conference 2017 Conference Paper

Iterated Games with LDL Goals over Finite Traces

• Julian Gutierrez
• Giuseppe Perelli
• Michael Wooldridge

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 setting we study—iterated Boolean games with goals over finite traces (iBGF )—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 LDLF objectives is regular, and provides complexity results for the associated automata constructions. CCS Concepts •Computing methodologies → Multi-agent systems;

IJCAI Conference 2017 Conference Paper

Nash Equilibria in Concurrent Games with Lexicographic Preferences

• Julian Gutierrez
• Aniello Murano
• Giuseppe Perelli
• Sasha Rubin
• Michael Wooldridge

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.

GandALF Workshop 2016 Workshop Paper

Cycle Detection in Computation Tree Logic

• Gaëlle Fontaine
• Fabio Mogavero
• Aniello Murano
• Giuseppe Perelli
• Loredana Sorrentino

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.

AAMAS Conference 2016 Conference Paper

Expressiveness and Nash Equilibrium in Iterated Boolean Games

• Julian Gutierrez
• Paul Harrenstein
• Giuseppe Perelli
• Michael Wooldridge

We introduce and investigate a novel notion of expressiveness for temporal logics that is based on game theoretic properties of multiagent systems. We focus on iterated Boolean games, where each agent i has a goal γi, represented using (a fragment of) Linear Temporal Logic (LTL). The goal γi 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 gametheoretic 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.

KR Conference 2016 Conference Paper

ImperfectInformation in Reactive Modules Games

• Julian Gutierrez
• Giuseppe Perelli
• Michael Wooldridge

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.

AAAI Conference 2016 Conference Paper

Rational Verification: From Model Checking to Equilibrium Checking

• Michael Wooldridge
• Julian Gutierrez
• Paul Harrenstein
• Enrico Marchioni
• Giuseppe Perelli
• Alexis Toumi

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.

Highlights Conference 2016 Conference Abstract

Solving Parity Games Using An Automata-Based Algorithm

• joint with Aniello Murano
• Giuseppe Perelli
• Moshe Vardi

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 \cap 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 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. This is joint work with Aniello Murano, Giuseppe Perelli and Moshe Vardi. The paper has been accepted in the 21° International Conference on Implementation and Application of Automata, CIAA 2016.

CSL Conference 2015 Conference Paper

Binding Forms in First-Order Logic

• Fabio Mogavero
• Giuseppe Perelli

Aiming to pinpoint the reasons behind the decidability of some complex extensions of modal logic, we propose a new classification criterion for sentences of first-order logic, which is based on the kind of binding forms admitted in their expressions, i. e. , on the way the arguments of a relation can be bound to a variable. In particular, we describe a hierarchy of four fragments focused on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with several first-order limitations proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel model-theoretic technique, that our logic enjoys the finite-model property, Craig's interpolation, and Beth's definability. Furthermore, the associated model-checking and satisfiability problems are solvable in PTime and Sigma_3^P, respectively.

Highlights Conference 2015 Conference Abstract

Pushdown Multi-Agent System Verification

• Giuseppe Perelli

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

IJCAI Conference 2015 Conference Paper

Pushdown Multi-Agent System Verification

• Aniello Murano
• Giuseppe Perelli

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.

TIME Conference 2014 Conference Paper

Checking Interval Properties of Computations

• Angelo Montanari
• Aniello Murano
• Giuseppe Perelli
• Adriano Peron

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.

Highlights Conference 2014 Conference Abstract

Checking Interval Properties of Computations

• Giuseppe Perelli

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, such as Halpern and Shoham's modal logic of time intervals (HS, for short). In this talk, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of HS formulas over Kripke structures, which makes it possible 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 HS[AA̅BB̅] and HS[AA̅EE̅].

EUMAS Conference 2014 Conference Paper

Synthesis with Rational Environments

• Orna Kupferman
• Giuseppe Perelli
• Moshe Y. Vardi

Abstract 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 2 ExpTime - 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.