Model Checking Alternating-time Temporal Logics of Knowledge

被引:0
|
作者
Long Shigong [1 ]
Luo Wenjun [1 ]
机构
[1] Guizhou Univ, Dept Comp Sci, Guiyang 550025, Peoples R China
关键词
Formal methods; Wireless protocol; ATL of knowledge; Algorithm; Model checking;
D O I
暂无
中图分类号
TN [电子技术、通信技术];
学科分类号
0809 ;
摘要
A wireless security protocol can be modeled as a Kripke structure M. The model checking problem for a logic L is : given a formula phi is an element of L 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.
引用
收藏
页码:5424 / 5426
页数:3
相关论文
共 50 条
  • [21] Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables
    Rybakov, Mikhail
    Shkatov, Dmitry
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2018, 2018, 11187 : 396 - 414
  • [22] Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications
    Wiebe van der Hoek
    Michael Wooldridge
    Studia Logica, 2003, 75 (1) : 125 - 157
  • [23] Satisfiability in alternating-time temporal logic
    van Drimmelen, G
    18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2003, : 208 - 217
  • [24] Alternating-Time Temporal Announcement Logic
    de Lima, Tiago
    COMPUTATIONAL LOGIC IN MULTI-AGENT SYSTEMS, 2011, 6814 : 105 - 121
  • [25] Graded Alternating-Time Temporal Logic
    Faella, Marco
    Napoli, Margherita
    Parente, Mimmo
    FUNDAMENTA INFORMATICAE, 2010, 105 (1-2) : 189 - 210
  • [26] Model checking temporal logics of knowledge in distributed systems
    Su, K
    PROCEEDING OF THE NINETEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE AND THE SIXTEENTH CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE, 2004, : 98 - 103
  • [27] Graded Alternating-Time Temporal Logic
    Faella, Marco
    Napoli, Margherita
    Parente, Mimmo
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING (LPAR-16), 2010, 6355 : 192 - 211
  • [28] Timed alternating-time temporal logic
    Henzinger, Thomas A.
    Prabhu, Vinayak S.
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2006, 4202 : 1 - 17
  • [29] Robust Alternating-Time Temporal Logic
    Murano, Aniello
    Neider, Daniel
    Zimmermann, Martin
    LOGICS IN ARTIFICIAL INTELLIGENCE, JELIA 2023, 2023, 14281 : 796 - 813
  • [30] Model checking temporal logics of knowledge via OBDDs
    Su, Kaile
    Sattar, Abdul
    Luo, Xiangyu
    Computer Journal, 2007, 50 (04): : 403 - 420