Rational Verification: From Model Checking to Equilibrium Checking

Authors

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

DOI:

https://doi.org/10.1609/aaai.v30i1.9878

Keywords:

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

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.

AAAI 2016 Proceedings Cover

Downloads

Published

2016-03-05

How to Cite

Wooldridge, M., Gutierrez, J., Harrenstein, P., Marchioni, E., Perelli, G., & Toumi, A. (2016). Rational Verification: From Model Checking to Equilibrium Checking. Proceedings of the AAAI Conference on Artificial Intelligence, 30(1). https://doi.org/10.1609/aaai.v30i1.9878

Issue

Vol. 30 No. 1 (2016): Thirtieth AAAI Conference on Artificial Intelligence

Section

Senior Member Summary Talks