Title :
Model Checking Alternating-Time Temporal Logics of Knowledge
Author :
Long Shigong ; Luo Wenjun
Author_Institution :
Dept. of Comput. Sci., Guizhou Univ., Guiyang
Abstract :
A wireless security protocol can be modeled as a Kripke structure M. The model checking problem for a logic L is: given a formula phiisinL decide if phi holds in the states of M. The alternating time temporal logic (ATL) is expanded and the alternating time temporal logics of knowledge is considered. We propose an efficient algorithm to model-check ATL of knowledge properties.
Keywords :
formal verification; temporal logic; alternating time temporal logic; formal methods; model checking alternating-time temporal logics; wireless security protocol; Communication system security; Computer science; Logic; State-space methods; Wireless application protocol;
Conference_Titel :
Wireless Communications, Networking and Mobile Computing, 2008. WiCOM '08. 4th International Conference on
Conference_Location :
Dalian
Print_ISBN :
978-1-4244-2107-7
Electronic_ISBN :
978-1-4244-2108-4
DOI :
10.1109/WiCom.2008.1293
