Rational verification in multi-agent systems by Najib, M

Subjects: “…Multi-Agent Systems…”

Rational verification: game-theoretic verification of multi-agent systems by Abate, A, Gutierrez, J, Hammond, L, Harrenstein, P, Kwiatkowska, M, Najib, M, Perelli, G, Steeples, T, Wooldridge, M

“…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 equilibria of a multi-agent system – that is, whether the system will exhibit the behavior ϕ represents under the assumption that agents within the system act rationally in pursuit of their preferences. …”

EVE: A tool for temporal equilibrium analysis by Gutierrez, J, Najib, M, Perelli, G, Wooldridge, M

“…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.…”

Local equilibria in logic-based multi-player games by Gutierrez, J, Harrenstein, B, Steeples, T, Wooldridge, M

“…Game theory provides a well-established framework for the analysis and verification of concurrent and multi-agent systems. Typically, the analysis of a multi-agent system involves computing the set of equilibria in the associated multi-player game representing the behaviour of the system. …”

Iterated games with LDL goals over finite traces by Gutierrez, J, Perelli, G, Wooldridge, M

“…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. …”

Iterated games with LDL goals by Gutierrez, J, Perelli, G, Wooldridge, M

“…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. …”

Multi-player games with LDL goals over finite traces by Gutierrez, J, Perelli, G, Wooldridge, M

“…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. …”

Iterated Boolean games for rational verification by Gutierrez, J, Gao, T, Wooldridge, M

“…Rational verification is the problem of understanding what temporal logic properties hold of a multi-agent system when agents are modelled as players in a game, each acting rationally in pursuit of personal preferences. …”

Expressiveness and Nash equilibrium in iterated Boolean games by Gutierrez, J, Harrenstein, P, Perelli, G, Wooldridge, M

“…We introduce and investigate a novel notion of expressiveness related to temporal logics and game theoretic properties of multi-agent systems. We focus on iterated Boolean games, where each agent …”

Expressiveness and Nash equilibrium in iterated Boolean games by Gutierrez, J, Harrenstein, P, Perelli, G, Wooldridge, M

“…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 iterated Boolean games as our abstract model of multi-agent systems [Gutierrez et al. 2013, 2015a]. …”

Imperfect information in Reactive Modules games by Gutierrez, J, Perelli, G, Wooldridge, M

“…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. …”

Imperfect information in reactive modules games by Gutierrez, J, Perelli, G, Wooldridge, M

“…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. …”

Mean-payoff games with ω-regular specifications by Gutierrez, J, Steeples, T, Wooldridge, M

“…Multi-player mean-payoff games are a natural formalism for modelling the behaviour of concurrent and multi-agent systems with self-interested players. Players in such a game traverse a graph, while attempting to maximise a (mean-)payoff function that depends on the play generated. …”

Nash equilibrium and bisimulation invariance by Gutierrez, J, Harrenstein, P, Perelli, G, Wooldridge, M

“…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. …”

A tool for the automated verification of Nash equilibria in concurrent games by Toumi, A, Gutierrez, J, Wooldridge, M

“…Reactive Modules is a high-level specification language for concurrent and multi-agent systems, used in a number of practical model checking tools. …”

On fixpoint logics and equivalences for processes with restricted nondeterminism by Gutierrez, J

“…More specifically, we study the impact that nondeterminism can have on some fixpoint modal logics and bisimulation equivalences for concurrent and multi-agent systems, when it is systematically restricted within the four kinds of behaviours mentioned above. …”

Nash equilibrium and bisimulation invariance by Gutierrez, J, Harrenstein, B, Perelli, G, Wooldridge, M

“…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. …”

Automated temporal equilibrium analysis: Verification and synthesis of multi-player games by Gutierrez, J, Najib, M, Perelli, G, Wooldridge, M

“…In the context of multi-agent systems, the rational 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. …”

From model checking to equilibrium checking: reactive modules for rational verification by Gutierrez, J, Harrenstein, B, Wooldridge, M

“…Equilibrium checking is relevant for multi-agent systems in which system components (agents) are assumed to be acting rationally in pursuit of delegated goals, and is concerned with understanding what temporal properties hold of such systems under the assumption that agents select strategies in equilibrium. …”

Rational verification: from model checking to equilibrium checking by Wooldridge, M, Gutierrez, J, Harrenstein, P, Marchioni, E, Perelli, G, Toumi, A

“…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. …”