CGAAL: Distributed On-The-Fly ATL Model Checker with Heuristics

Falke Bjernemose Øtker Carlsen*, Lars Bo Park Frydenskov, Nicolaj Østerby Jensen*, Jacob Jenner Rasmussen, Mathias Mehl Sørensen, Ager Geel Weirsøe, Mathias Claus Jensen, Kim Guldstrand Larsen

*Corresponding author for this work

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

17 Downloads (Pure)

Abstract

We present CGAAL, our efficient on-the-fly model checker for alternating-time temporal logic (ATL) on concurrent game structures (CGS). We present how our tool encodes ATL as extended dependency graphs with negation edges and employs the distributed on-the-fly algorithm by Dalsgaard et al. Our tool offers multiple novel search strategies for the algorithm, including DHS which is inspired by PageRank and uses the in-degree of configurations as a heuristic, IHS which estimates instability of assignment values, and LPS which estimates the distance to a state satisfying the constituent property using linear programming. CGS are input using our modelling language LCGS, where composition and synchronisation are easily described. We prove the correctness of our encoding, and our experiments show that our tool CGAAL is often one to three orders of magnitude faster than the popular tool PRISM-games on case studies from PRISM’s documentation and among case studies we have developed. In our evaluation, we also compare and evaluate our search strategies, and find that our custom search strategies are often significantly faster than the usual breadth-first and depth-first search strategies.

Original languageEnglish
Title of host publicationProceedings af the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023)
Number of pages16
Volume390
Place of PublicationItalien
PublisherOpen Publishing Association
Publication date30 Sept 2023
Pages99-114
Chapter7
DOIs
Publication statusPublished - 30 Sept 2023
EventFourteenth International Symposium on Games, Automata, Logics, and Formal Verification - Università degli Studi di Udine, Palazzo Antonini-Cernazai, Udine, Italy
Duration: 18 Sept 202320 Sept 2023
Conference number: 14
https://gandalf23.uniud.it/

Conference

ConferenceFourteenth International Symposium on Games, Automata, Logics, and Formal Verification
Number14
LocationUniversità degli Studi di Udine, Palazzo Antonini-Cernazai
Country/TerritoryItaly
CityUdine
Period18/09/202320/09/2023
Internet address
SeriesElectronic Proceedings in Theoretical Computer Science
ISSN2075-2180

Fingerprint

Dive into the research topics of 'CGAAL: Distributed On-The-Fly ATL Model Checker with Heuristics'. Together they form a unique fingerprint.

Cite this