Name
Title | ||
|---|---|---|
Comparing approaches for model-checking strategies under imperfect information and fairness constraints |
Abstract | ||
|---|---|---|
Starting from alternating-time temporal logic, many logics for reasoning about strategies in a system of agents have been proposed. Some of them consider the strategies that agents can play when they have partial information about the state of the system. \(ATLK_{irF}\) is such a logic to reason about uniform strategies under unconditional fairness constraints. While this kind of logics has been extensively studied, practical approaches for solving their model-checking problem appeared only recently. This paper considers three approaches for model-checking strategies under partial observability of the agents, applied to \(ATLK_{irF}\). These three approaches have been implemented in PyNuSMV, a Python library based on the state-of-the-art model checker NuSMV. Thanks to the experimental results obtained with this library and thanks to the comparison of the relative performance of the approaches, this paper provides indications and guidelines for the use of these verification techniques, showing that different approaches are needed in different situations. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1007/s10009-018-0505-6 | International Journal on Software Tools for Technology Transfer |
Keywords | Field | DocType |
Alternating-time temporal logic, Imperfect information, Fairness constraints, Model checking | Observability,Model checking,Computer science,Theoretical computer science,Alternating-time Temporal Logic,Temporal logic,Perfect information,Python (programming language) | Journal |
Volume | Issue | ISSN |
21 | 4 | 1433-2787 |
Citations | PageRank | References |
0 | 0.34 | 19 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Simon Busard | 1 | 40 | 3.91 |
| Charles Pecheur | 2 | 284 | 28.50 |
| Hongyang Qu | 3 | 2 | 1.38 |
| Franco Raimondi | 4 | 832 | 48.18 |