loading...
Unbounded Model Checking for Alternating-Time Temporal Logic
New York City, New York, USA July 19-July 23
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/AAMAS.2004.10089Third International Joint Conference ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
M. Kacprzak, W. Penczek, "Unbounded Model Checking for Alternating-Time Temporal Logic," Autonomous Agents and Multiagent Systems, International Joint Conference on, vol. 2, pp. 646-653, Third International Joint Conference on Autonomous Agents and Multiagent Systems - Volume 2 (AAMAS'04), 2004.
 
 
BibTex
x
 
@article{ 10.1109/AAMAS.2004.10089,
author = {M. Kacprzak and W. Penczek},
title = {Unbounded Model Checking for Alternating-Time Temporal Logic},
journal ={Autonomous Agents and Multiagent Systems, International Joint Conference on},
volume = {2},
year = {2004},
isbn = {0-7695-2092-8},
pages = {646-653},
doi = {http://doi.ieeecomputersociety.org/10.1109/AAMAS.2004.10089},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Autonomous Agents and Multiagent Systems, International Joint Conference on
TI - Unbounded Model Checking for Alternating-Time Temporal Logic
SN - 0-7695-2092-8
SP646
EP653
A1 - M. Kacprzak,
A1 - W. Penczek,
PY - 2004
KW - null
VL - 2
JA - Autonomous Agents and Multiagent Systems, International Joint Conference on
ER -
 
M. Kacprzak, Bia?ystok University of Technology
W. Penczek, Institute of Computer Science, PAS and Podlasie Academy
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.
Citation:
M. Kacprzak, W. Penczek, "Unbounded Model Checking for Alternating-Time Temporal Logic," aamas, vol. 2, pp.646-653, Third International Joint Conference on Autonomous Agents and Multiagent Systems - Volume 2 (AAMAS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.