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 条
  • [41] Model checking temporal logics of knowledge via OBDDs1
    Su, Kaile
    Sattar, Abdul
    Luo, Xiangyu
    COMPUTER JOURNAL, 2007, 50 (04): : 403 - 420
  • [42] Agents and roles: Refinement in alternating-time temporal logic
    Ryan, M
    Schobbens, PY
    INTELLIGENT AGENTS VIII: AGENT THEORIES, ARCHITECTURES, AND LANGUAGES, 2002, 2333 : 100 - 114
  • [43] On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
    Beutner, Raven
    Finkbeiner, Bernd
    THIRTY-EIGHTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOL 38 NO 16, 2024, : 17317 - 17326
  • [44] Interval temporal logics model checking
    Montanari, Angelo
    PROCEEDINGS 23RD INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING - TIME 2016, 2016, : 2 - 2
  • [45] Alternating automata: Unifying truth and validity checking for temporal logics
    Vardi, MY
    AUTOMATED DEDUCTION - CADE-14, 1997, 1249 : 191 - 206
  • [46] Alternating-time temporal logic with finite-memory strategies
    Vester, Steen
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (119): : 194 - 207
  • [47] Game-Theoretic Semantics for Alternating-Time Temporal Logic
    Goranko, Valentin
    Kuusisto, Antti
    Ronnholm, Raine
    AAMAS'16: PROCEEDINGS OF THE 2016 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, 2016, : 671 - 679
  • [48] Agents With Truly Perfect Recall in Alternating-Time Temporal Logic
    Bulling, Nils
    Jamroga, Wojciech
    Popovici, Matei
    AAMAS'14: PROCEEDINGS OF THE 2014 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, 2014, : 1561 - 1562
  • [49] Satisfiability of Alternating-Time Temporal Epistemic Logic Through Tableaux
    Belardinelli, Francesco
    FOURTEENTH INTERNATIONAL CONFERENCE ON THE PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2014, : 398 - 407
  • [50] Combined model checking for temporal, probabilistic, and real-time logics
    Konur, Savas
    Fisher, Michael
    Schewe, Sven
    THEORETICAL COMPUTER SCIENCE, 2013, 503 : 61 - 88