DocumentCode
2209898
Title
Unbounded model checking for alternating-time temporal logic
Author
Kacprzak, M. ; Penczek, Wojciech
Author_Institution
Bialystok University of Technology
fYear
2004
fDate
23-23 July 2004
Firstpage
646
Lastpage
653
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 verification of ATL. An example is given to show an application of the technique.
Keywords
Binary decision diagrams; Boolean functions; Data structures; Electronic mail; Logic; Mathematics; Multiagent systems; Permission; Physics; Power system modeling;
fLanguage
English
Publisher
ieee
Conference_Titel
Autonomous Agents and Multiagent Systems, 2004. AAMAS 2004. Proceedings of the Third International Joint Conference on
Conference_Location
New York, NY, USA
Print_ISBN
1-58113-864-4
Type
conf
Filename
1373533
Link To Document