• DocumentCode
    3448412
  • Title

    Model Checking Alternating-Time Temporal Logics of Knowledge

  • Author

    Long Shigong ; Luo Wenjun

  • Author_Institution
    Dept. of Comput. Sci., Guizhou Univ., Guiyang
  • fYear
    2008
  • fDate
    12-14 Oct. 2008
  • Firstpage
    1
  • Lastpage
    3
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • 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
  • Type

    conf

  • DOI
    10.1109/WiCom.2008.1293
  • Filename
    4679201
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3448412