Open AccessUnbounded Model Checking for ATL
Author(s) -
Michał Kański,
Artur Niewiadomski,
Magdalena Kacprzak,
Wojciech Penczek,
Wojciech Nabiałek
Publication year - 2021
Publication title -
studia informatica system and information technology
Language(s) - English
Resource type - Journals
ISSN - 1731-2264
DOI - 10.34739/si.2021.25.01
Subject(s) - model checking , temporal logic , computer science , computation tree logic , logic model , programming language , theoretical computer science , symbolic trajectory evaluation , sociology , social science
In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom