Bounded model checking for knowledge and real time

被引：20
|
作者：
Lomuscio, Alessio [1 ]
Penczek, Wojciech [2 ,3 ]
Wozna, Boiena [4 ]
机构：
[1] Imperial Coll London, Dept Computing, London SW7 2BZ, England
[2] Polish Acad Sci, Inst Comp Sci, PL-01237 Warsaw, Poland
[3] Podlasie Acad, Inst Informat, Siedlce, Poland
[4] Jan Dlugosz Univ, Inst Math & Comp Sci, PL-42200 Czestochowa, Poland
来源：
ARTIFICIAL INTELLIGENCE | 2007年 / 171卷 / 16-17期
基金：
英国工程与自然科学研究理事会;
关键词：
temporal epistemic logics; model checking; interpreted systems; real time systems;
D O I：
10.1016/j.artint.2007.05.005
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present TECTLK, a logic to specify knowledge and real time in multi-agent systems. We show that the TECTLK model checking problem is decidable, and we present an algorithm for bounded model checking based on a discretisation method. We exemplify the use of the technique by means of the "Railroad Crossing System", a popular example in the multi-agent systems literature. (c) 2007 Elsevier B.V All rights reserved.
引用
收藏
页码：1011 / 1038
页数：28
相关论文
共 50 条
  • [1] Bounded Model Checking for the Existential Part of Real-Time CTL and Knowledge
    Wozna-Szczesniak, Bozena
    [J]. ADVANCES IN SOFTWARE ENGINEERING TECHNIQUES, 2012, 7054 : 164 - 178
  • [2] Bounded model checking for GSMP models of stochastic real-time systems
    Alur, Rajeev
    Bernadsky, Mikhail
    [J]. HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2006, 3927 : 19 - 33
  • [3] SMT-based Bounded Model Checking for Real-time Systems
    Xu, Liang
    [J]. QSIC 2008: PROCEEDINGS OF THE EIGHTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, 2008, : 120 - 125
  • [4] Model checking knowledge and time
    van der Hoek, W
    Wooldridge, M
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2002, 2318 : 95 - 111
  • [5] Abstraction In Model Checking Real-Time Temporal Logic of Knowledge
    Zhou, CongHua
    Sun, Bo
    [J]. JOURNAL OF COMPUTERS, 2012, 7 (02) : 362 - 370
  • [6] The Complexity of Model Checking Knowledge and Time
    Bozzelli, Laura
    Maubert, Bastien
    Murano, Aniello
    [J]. PROCEEDINGS OF THE TWENTY-EIGHTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2019, : 1595 - 1601
  • [7] On the Complexity of Model Checking Knowledge and Time
    Bozzelli, Laura
    Maubert, Bastien
    Murano, Aniello
    [J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2024, 25 (01)
  • [8] Model checking Bounded Prioritized Time Petri Nets
    Berthomieu, Bernard
    Peres, Florent
    Vernadat, Francois
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 523 - +
  • [9] Bounded Model Checking
    Biere, A
    Cimatti, A
    Clarke, EM
    Strichman, O
    Zhu, YS
    [J]. ADVANCES IN COMPUTERS, VOL 58: HIGHLY DEPENDABLE SOFTWARE, 2003, 58 : 117 - 148
  • [10] A new approach to bounded model checking for branching time logics
    Oshman, Rotem
    Grumberg, Orna
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 410 - +
12345