Abstract
Reactive Modules is a high-level specification language for concurrent and multi-agent systems, used in a number of practical model checking tools. Reactive Modules Games is a game-theoretic extension of Reactive Modules, in which concurrent agents in the system are assumed to act strategically in an attempt to satisfy a temporal logic formula representing their individual goal. The basic analytical concept for Reactive Modules Games is Nash equilibrium. In this paper, we describe a tool through which we can automatically verify Nash equilibrium strategies for Reactive Modules Games. Our tool takes as input a system, specified in the Reactive Modules language, a representation of players’ goals (expressed as CTL formulae), and a representation of players strategies; it then checks whether these strategies form a Nash equilibrium of the Reactive Modules Game passed as input. The tool makes extensive use of conventional temporal logic satisfiability and model checking techniques. We first give an overview of the theory underpinning the tool, briefly describe its structure and implementation, and conclude by presenting a worked example analysed using the tool.
Original language | English |
---|---|
Title of host publication | Theoretical Aspects of Computing – ICTAC 2015 |
Subtitle of host publication | 12th International Colloquium Cali, Colombia, October 29–31, 2015 Proceedings |
Editors | Martin Leucker, Camilo Rueda, Frank D. Valencia |
Place of Publication | Cham Switzerland |
Publisher | Springer |
Pages | 583-594 |
Number of pages | 12 |
ISBN (Electronic) | 9783319251509 |
ISBN (Print) | 9783319251493 |
DOIs | |
Publication status | Published - 2015 |
Externally published | Yes |
Event | International Colloquium on Theoretical Aspects of Computing 2015 - Cali, Colombia Duration: 29 Oct 2015 → 31 Oct 2015 Conference number: 12th http://www.ictac2015.co |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 9399 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | International Colloquium on Theoretical Aspects of Computing 2015 |
---|---|
Abbreviated title | ICTAC 2015 |
Country/Territory | Colombia |
City | Cali |
Period | 29/10/15 → 31/10/15 |
Internet address |