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

*Kontaktforfatter

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

27 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 an 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 modeling 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.
OriginalsprogEngelsk
TitelProceedings af the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023)
Antal sider16
Vol/bind390
UdgivelsesstedItalien
ForlagOpen Publishing Association
Publikationsdato30 sep. 2023
Sider99-114
Kapitel7
DOI
StatusUdgivet - 30 sep. 2023
BegivenhedFourteenth International Symposium on Games, Automata, Logics, and Formal Verification - Università degli Studi di Udine, Palazzo Antonini-Cernazai, Udine, Italien
Varighed: 18 sep. 202320 sep. 2023
Konferencens nummer: 14
https://gandalf23.uniud.it/

Konference

KonferenceFourteenth International Symposium on Games, Automata, Logics, and Formal Verification
Nummer14
LokationUniversità degli Studi di Udine, Palazzo Antonini-Cernazai
Land/OmrådeItalien
ByUdine
Periode18/09/202320/09/2023
Internetadresse
NavnElectronic Proceedings in Theoretical Computer Science
ISSN2075-2180

Bibliografisk note

Asger Geel Weirsøe is a former student of Aalborg University

Emneord

  • ATL logic
  • dependency graphs
  • on-the-fly
  • heuristics
  • distributed algorithm

Fingeraftryk

Dyk ned i forskningsemnerne om 'CGAAL: Distributed On-The-Fly ATL Model Checker with Heuristics'. Sammen danner de et unikt fingeraftryk.

Citationsformater