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.
Cover of Studia Informatica Journal

Downloads

Published

23.12.2021

Issue

Vol. 25 No. 1-2 (2021): Studia Informatica. Systems and Information Technology

Section

Article

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