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