@article{af0b9212a07543cbaacfea0e28b55694,
title = "Rational verification: game-theoretic verification of multi-agent systems",
abstract = "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. 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.",
keywords = "Automated synthesis, Automated verification, Game theory, Model checking, Multi-agent systems",
author = "Alessandro Abate and Julian Gutierrez and Lewis Hammond and Paul Harrenstein and Marta Kwiatkowska and Muhammad Najib and Giuseppe Perelli and Thomas Steeples and Michael Wooldridge",
note = "Funding Information: Wooldridge, Gutierrez, Harrenstein, and Perelli acknowledge the support of the ERC under grant 291528 (“RACE”). Wooldridge and Harrenstein further acknowledge the support of the Alan Turing Institute, London. Kwiatkowska received funding from the European Research Council (ERC) under the European Union{\textquoteright}s Horizon 2020 research and innovation programme (grant 834115, “FUN2MODEL”) and the EPSRC Programme Grant on Mobile Autonomy (EP/M019918/1). Abate achknowledges the HICLASS project (113213), a partnership between the Aerospace Technology Institute (ATI), Department for Business, Energy & Industrial Strategy (BEIS) and Innovate UK. Hammond acknowledges the support of an EPSRC Doctoral Training Partnership studentship (Reference: 2218880). Harrenstein was furthermore supported by the ERC under grant 639945 (“ACCORD”). Steeples gratefully acknowledges the support of the EPSRC Centre for Doctoral Training in Autonomous Intelligent Machines and Systems EP/L015897/1 and the Ian Palmer Memorial Scholarship. Najib acknowledges the support of the ERC European Union{\textquoteright}s Horizon 2020 research and innovation programme (grant 759969). Funding Information: Wooldridge, Gutierrez, Harrenstein, and Perelli acknowledge the support of the ERC under grant 291528 (?RACE?). Wooldridge and Harrenstein further acknowledge the support of the Alan Turing Institute, London. Kwiatkowska received funding from the European Research Council (ERC) under the European Union?s Horizon 2020 research and innovation programme (grant 834115, ?FUN2MODEL?) and the EPSRC Programme Grant on Mobile Autonomy (EP/M019918/1). Abate achknowledges the HICLASS project (113213), a partnership between the Aerospace Technology Institute (ATI), Department for Business, Energy & Industrial Strategy (BEIS) and Innovate UK. Hammond acknowledges the support of an EPSRC Doctoral Training Partnership studentship (Reference: 2218880). Harrenstein was furthermore supported by the ERC under grant 639945 (?ACCORD?). Steeples gratefully acknowledges the support of the EPSRC Centre for Doctoral Training in Autonomous Intelligent Machines and Systems EP/L015897/1 and the Ian Palmer Memorial Scholarship. Najib acknowledges the support of the ERC European Union?s Horizon 2020 research and innovation programme (grant 759969). Publisher Copyright: {\textcopyright} 2021, The Author(s).",
year = "2021",
month = sep,
doi = "10.1007/s10489-021-02658-y",
language = "English",
volume = "51",
pages = "6569--6584",
journal = "Applied Intelligence",
issn = "0924-669X",
publisher = "Springer",
number = "9",
}