## Abstract

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. 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 mod-elled using the Simple Reactive Modules Language, a widely-used system modelling language for concurrent and multi-Agent systems, this problem can be reduced to a simpler query: Whether some iterated game-in which players have control over a finite set of Boolean variables and goals expressed as Linear Temporal Logic (LTL) formulae-has a Nash equilibrium. To better understand the complexity of solving this kind of verification problem in practice, we then study the two-player 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 multi-Agent 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 | 705-713 |

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 http://www.ifaamas.org/Proceedings/aamas2017/forms/index.htm |

### Conference

Conference | International Conference on Autonomous Agents and Multiagent Systems 2017 |
---|---|

Abbreviated title | AAMAS 2017 |

Country | 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