Rational verification: from model checking to equilibrium checking

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

Rational verification: from model checking to equilibrium checking

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

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

Abstract

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.

Original language	English
Title of host publication	Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence
Editors	Dale Schuurmans, Michael Wellman
Place of Publication	Palo Alto CA USA
Publisher	Association for the Advancement of Artificial Intelligence (AAAI)
Pages	4184-4190
Number of pages	7
ISBN (Electronic)	9781577357605
Publication status	Published - 2016
Externally published	Yes
Event	AAAI Conference on Artificial Intelligence 2016 - Phoenix Convention Center, Phoenix, United States of America Duration: 12 Feb 2016 → 17 Feb 2016 Conference number: 30th http://www.aaai.org/Conferences/AAAI/aaai16.php

Conference

Conference	AAAI Conference on Artificial Intelligence 2016
Abbreviated title	AAAI 2016
Country/Territory	United States of America
City	Phoenix
Period	12/02/16 → 17/02/16
Internet address	http://www.aaai.org/Conferences/AAAI/aaai16.php

Keywords

multi-agent systems
game theory
temporal logic
model checking
equilibrium checking
rational verification
synthesis

Access to Document

301533077-oaFinal published version, 773 KB

https://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12268

Cite this

Wooldridge, M., Gutierrez, J., Harrenstein, P., Marchioni, E., Perelli, G., & Toumi, A. (2016). Rational verification: from model checking to equilibrium checking. In D. Schuurmans, & M. Wellman (Eds.), Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (pp. 4184-4190). Association for the Advancement of Artificial Intelligence (AAAI). https://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12268

@inproceedings{2dd7fb5ef2ca46ec807a45beb598a0ba,

title = "Rational verification: from model checking to equilibrium checking",

abstract = "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.",

keywords = "multi-agent systems, game theory, temporal logic, model checking, equilibrium checking, rational verification, synthesis",

author = "Michael Wooldridge and Julian Gutierrez and Paul Harrenstein and Enrico Marchioni and Giuseppe Perelli and Alexis Toumi",

year = "2016",

language = "English",

pages = "4184--4190",

editor = "Schuurmans, \{Dale \} and Wellman, \{Michael \}",

booktitle = "Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence",

publisher = "Association for the Advancement of Artificial Intelligence (AAAI)",

address = "United States of America",

note = "AAAI Conference on Artificial Intelligence 2016, AAAI 2016 ; Conference date: 12-02-2016 Through 17-02-2016",

url = "http://www.aaai.org/Conferences/AAAI/aaai16.php",

}

Wooldridge, M, Gutierrez, J, Harrenstein, P, Marchioni, E, Perelli, G & Toumi, A 2016, Rational verification: from model checking to equilibrium checking. in D Schuurmans & M Wellman (eds), Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence . Association for the Advancement of Artificial Intelligence (AAAI), Palo Alto CA USA, pp. 4184-4190, AAAI Conference on Artificial Intelligence 2016, Phoenix, Arizona, United States of America, 12/02/16. <https://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12268>

Rational verification: from model checking to equilibrium checking. / Wooldridge, Michael; Gutierrez, Julian; Harrenstein, Paul et al.
Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence . ed. / Dale Schuurmans; Michael Wellman. Palo Alto CA USA: Association for the Advancement of Artificial Intelligence (AAAI), 2016. p. 4184-4190.

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Rational verification

T2 - AAAI Conference on Artificial Intelligence 2016

AU - Wooldridge, Michael

AU - Gutierrez, Julian

AU - Harrenstein, Paul

AU - Marchioni, Enrico

AU - Perelli, Giuseppe

AU - Toumi, Alexis

N1 - Conference code: 30th

PY - 2016

Y1 - 2016

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

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

KW - multi-agent systems

KW - game theory

KW - temporal logic

KW - model checking

KW - equilibrium checking

KW - rational verification

KW - synthesis

UR - http://www.scopus.com/inward/record.url?scp=84999735256&partnerID=8YFLogxK

M3 - Conference Paper

AN - SCOPUS:84999735256

SP - 4184

EP - 4190

BT - Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence

A2 - Schuurmans, Dale

A2 - Wellman, Michael

PB - Association for the Advancement of Artificial Intelligence (AAAI)

CY - Palo Alto CA USA

Y2 - 12 February 2016 through 17 February 2016

ER -

Rational verification: from model checking to equilibrium checking

Abstract

Conference

Keywords

Access to Document

Other files and links

From model checking to equilibrium checking: reactive modules for rational verification

Cite this