Unbounded Model Checking for Alternating-Time Temporal Logic

	This Article
	Subscribers, please Login Purchase article: $19 PDF RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by M. Kacprzak Articles by W. Penczek

Third International Joint Conference on Autonomous Agents and Multiagent Systems - Volume 2 (AAMAS'04)

New York City, New York, USA

July 19-July 23

ISBN: 0-7695-2092-8

	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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/AAMAS.2004.10089

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

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.