Tableaux like model checking on-the-fly for ATL+

2021/07/12 by Serenella Cerrito, Cerrito, Serenella
Computer Science · #F.3 #F.4 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.2107.05378

openalex publication_date 2021/07/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We propose a model checking algorithm to test properties of systems that are expressed in the multi-agent temporal logic ATL+. The specificities of this algorithm are: it is on-the-fly, generating states only when they are needed, and it works by constructing a candidate formal proof in an inference system inspired by tableau proof systems.

Citations

• Alternating-time temporal logic
• Depth-First Search and Linear Graph Algorithms

Related

• Practical Abstractions for Model Checking Continuous-Time Multi-Agent Systems
• ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems
• Game-Theoretic Semantics for ATL+ with Applications to Model Checking
• Soundness and Completeness of a Model-Checking Proof System for CTL
• On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions