Unbounded Model Checking for Alternating-Time Temporal Logic

M. Kacprzak; W. Penczek

doi:10.1109/AAMAS.2004.10089

Autonomous Agents and Multiagent Systems, International Joint Conference on

Unbounded Model Checking for Alternating-Time Temporal Logic

Year: 2004, Volume: 3, Pages: 646-653

DOI Bookmark: 10.1109/AAMAS.2004.10089

Authors

M. Kacprzak, Bia?ystok University of Technology
W. Penczek, Institute of Computer Science, PAS and Podlasie Academy

Abstract

This paper deals with the problem of verification of game-like structures by means of symbolic model checking. Alternating-time Temporal Logic (ATL) is used for expressing properties of multi-agent systems represented by concurrent game structures. Unbounded model checking (a SAT based technique) is applied for the first time for verifi- cation of ATL. An example is given to show an application of the technique.

Like what you’re reading?

Already a member?

Get this article FREE with a new membership!

Infinite State AMC-Model Checking for Cryptographic Protocols
2007 22nd Annual IEEE Symposium on Logic in Computer Science
Satisfiability in Alternating-time Temporal Logic
Logic in Computer Science, Symposium on
Unbounded model checking for alternating-time temporal logic
Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, 2004. AAMAS 2004.
SAT-Based Unbounded Symbolic Model Checking
Design Automation Conference
Modeling Cooperative Problem Solving Process with Extended Alternating-time Temporal Logic
Eighth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing (SNPD 2007)
Coalitional Planning in Game-like Domains via ATL Model Checking
2009 21st IEEE International Conference on Tools with Artificial Intelligence
Temporal Logic Query Checking
Proceedings 16th Annual IEEE Symposium on Logic in Computer Science
Focus Game for Projection Temporal Logic
2011 Fifth International Conference on Theoretical Aspects of Software Engineering
Alternating-time Temporal Logic
Proceedings 38th Annual Symposium on Foundations of Computer Science
Low complexity and large interactions are possible in Strategy logic
2019 International Symposium on Theoretical Aspects of Software Engineering (TASE)

Unbounded Model Checking for Alternating-Time Temporal Logic

Authors

Abstract

Related Articles