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 条
  • [31] Alternating-time temporal logic with resource bounds
    Hoang Nga Nguyen
    Alechina, Natasha
    Logan, Brian
    Rakib, Abdur
    JOURNAL OF LOGIC AND COMPUTATION, 2018, 28 (04) : 631 - 663
  • [32] Alternating-time Temporal Belief and Knowledge Logic in Multi-agent Systems
    Ning, Zhengyuan
    Lai, Xianwei
    Hu, Shanli
    Wang, Xiuli
    2008 3RD INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEM AND KNOWLEDGE ENGINEERING, VOLS 1 AND 2, 2008, : 1357 - +
  • [33] Alternating-time temporal dynamic epistemic logic
    de Lima, Tiago
    JOURNAL OF LOGIC AND COMPUTATION, 2014, 24 (06) : 1145 - 1178
  • [34] Alternating-time Temporal Logic on Finite Traces
    Belardinelli, Francesco
    Lomuscio, Alessio
    Murano, Aniello
    Rubin, Sasha
    PROCEEDINGS OF THE TWENTY-SEVENTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2018, : 77 - 83
  • [35] Complete axiomatization and decidability of Alternating-time temporal logic
    Goranko, V
    van Drimmelen, G
    THEORETICAL COMPUTER SCIENCE, 2006, 353 (1-3) : 93 - 117
  • [36] Refining strategic ability in alternating-time temporal logic
    Guelev, Dimitar P.
    INFORMATION AND COMPUTATION, 2017, 254 : 316 - 328
  • [37] Relentful Strategic Reasoning in Alternating-Time Temporal Logic
    Mogavero, Fabio
    Murano, Aniello
    Vardi, Moshe Y.
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING (LPAR-16), 2010, 6355 : 371 - 386
  • [38] Relentful strategic reasoning in alternating-time temporal logic
    1663, Oxford University Press (26):
  • [39] Model checking temporal logics of knowledge and its application in security verification
    Wu, LJ
    Su, KL
    Chen, QL
    COMPUTATIONAL INTELLIGENCE AND SECURITY, PT 1, PROCEEDINGS, 2005, 3801 : 349 - 354
  • [40] Relentful strategic reasoning in alternating-time temporal logic
    Mogavero, Fabio
    Murano, Aniello
    Vardi, Moshe Y.
    JOURNAL OF LOGIC AND COMPUTATION, 2016, 26 (05) : 1663 - 1695