Abstract
Rational verification is the problem of understanding what temporal logic properties hold of a multiAgent system when agents are modelled as players in a game, each acting rationally in pursuit of personal preferences. More specifically, rational verification asks whether a given property, expressed as a temporal logic formula, is satisfied in a computation of the system that might be generated if agents within the system choose strategies for selecting actions that form a Nash equilibrium. We show that, when agents are modelled using the Simple Reactive Modules Language, a widelyused system modelling language for concurrent and multiAgent systems, this problem can be reduced to a simpler query: Whether some iterated gamein which players have control over a finite set of Boolean variables and goals expressed as Linear Temporal Logic (LTL) formulaehas a Nash equilibrium. To better understand the complexity of solving this kind of verification problem in practice, we then study the twoplayer case for various types of LTL goals, present some experimental results, and describe a general technique to implement rational verification using MCMAS, a model checking tool for the verification of concurrent and multiAgent systems.
Original language  English 

Title of host publication  Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems 
Editors  Sanmay Das, Ed Durfee 
Place of Publication  New York NY USA 
Publisher  Association for Computing Machinery (ACM) 
Pages  705713 
Number of pages  9 
ISBN (Electronic)  9781510855076 
Publication status  Published  2017 
Externally published  Yes 
Event  International Conference on Autonomous Agents and Multiagent Systems 2017  Sao Paulo, Brazil Duration: 8 May 2017 → 12 May 2017 Conference number: 16th https://dl.acm.org/doi/proceedings/10.5555/3091125 (Proceedings) 
Conference
Conference  International Conference on Autonomous Agents and Multiagent Systems 2017 

Abbreviated title  AAMAS 2017 
Country/Territory  Brazil 
City  Sao Paulo 
Period  8/05/17 → 12/05/17 
Internet address 

Keywords
 Formal verification
 Iterated boolean games
 Linear temporal logic
 MCMAS
 Nash equilibria
 Strategy logic