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
来源：
2008 4TH INTERNATIONAL CONFERENCE ON WIRELESS COMMUNICATIONS, NETWORKING AND MOBILE COMPUTING, VOLS 1-31 | 2008年
关键词：
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 条
  • [1] Parameterised Model Checking for Alternating-Time Temporal Logic
    Kouvaros, Panagiotis
    Lomuscio, Alessio
    ECAI 2016: 22ND EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2016, 285 : 1230 - 1238
  • [2] On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems
    Vester, Steen
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 : 361 - 377
  • [3] Alternating-time temporal logics with linear past
    Bozzelli, Laura
    Murano, Aniello
    Sorrentino, Loredana
    THEORETICAL COMPUTER SCIENCE, 2020, 813 : 199 - 217
  • [4] Probabilistic alternating-time temporal logic and model checking algorithm
    Chen, Taolue
    Lu, Jian
    FOURTH INTERNATIONAL CONFERENCE ON FUZZY SYSTEMS AND KNOWLEDGE DISCOVERY, VOL 2, PROCEEDINGS, 2007, : 35 - +
  • [5] MODEL-CHECKING ALTERNATING-TIME TEMPORAL LOGIC WITH STRATEGIES BASED ON COMMON KNOWLEDGE IS UNDECIDABLE
    Diaconu, Raluca
    Dima, Catalin
    APPLIED ARTIFICIAL INTELLIGENCE, 2012, 26 (04) : 331 - 348
  • [6] Fully symbolic unbounded model checking for Alternating-time Temporal Logic
    Kacprzak, M
    Penczek, W
    AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS, 2005, 11 (01) : 69 - 89
  • [7] Action and Knowledge in Alternating-Time Temporal Logic
    Thomas Ågotnes
    Synthese, 2006, 149 : 375 - 407
  • [8] Action and knowledge in alternating-time temporal logic
    Ågotnes, T
    SYNTHESE, 2006, 149 (02) : 121 - 153
  • [9] Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
    Dima, Catalin
    Enea, Constantin
    Guelev, Dimitar
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (25): : 103 - 117
  • [10] Distributed synthesis for alternating-time logics
    Schewe, Sven
    Finkbeiner, Bernd
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 268 - +
12345