Unbounded Model Checking for ATL

Michał Kański; Artur Niewiadomski; Magdalena Kacprzak; Wojciech Penczek; Wojciech Nabiałek

doi:10.34739/si.2021.25.01

Unbounded Model Checking for ATL

Authors

Michał Kański
Artur Niewiadomski
Magdalena Kacprzak
Wojciech Penczek
Wojciech Nabiałek

DOI:

https://doi.org/10.34739/si.2021.25.01

Abstract

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.

Downloads

Download data is not yet available.

Downloads

PDF File

Published

2021-12-23

How to Cite

Kański, M., Niewiadomski, A., Kacprzak, M., Penczek, W., & Nabiałek, W. (2021). Unbounded Model Checking for ATL. Studia Informatica. System and Information Technology, 25(1-2), 5–22. https://doi.org/10.34739/si.2021.25.01