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 条
  • [21] Symbolic Causality Checking Using Bounded Model Checking
    Beer, Adrian
    Heidinger, Stephan
    Kuehne, Uwe
    Leitner-Fischer, Florian
    Leue, Stefan
    [J]. MODEL CHECKING SOFTWARE, SPIN 2015, 2015, 9232 : 203 - 221
  • [22] Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking
    Igawa, Nao
    Yokogawa, Tomoyuki
    Amasaki, Sousuke
    Kondo, Masafumi
    Sato, Yoichiro
    Arimoto, Kazutami
    [J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2020, E103D (03) : 702 - 705
  • [23] CEGAR based bounded model checking of discrete time hybrid systems
    Mari, Federico
    Tronci, Enrico
    [J]. HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2007, 4416 : 399 - +
  • [24] Statistical probabilistic model checking with a focus on time-bounded properties
    Younes, Hakan L. S.
    Simmons, Reid G.
    [J]. INFORMATION AND COMPUTATION, 2006, 204 (09) : 1368 - 1409
  • [25] Model checking knowledge and linear time: PSPACE cases
    Engelhardt, Kai
    Gammie, Peter
    van der Meyden, Ron
    [J]. LOGICAL FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 2007, 4514 : 195 - +
  • [26] Bounded model checking of Time Petri Nets using SAT solver
    Yokogawa, Tomoyuki
    Kondo, Masafumi
    Miyazaki, Hisashi
    Amasaki, Sousuke
    Sato, Yoichiro
    Arimoto, Kazutami
    [J]. IEICE ELECTRONICS EXPRESS, 2015, 12 (02):
  • [27] A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems
    Kwon, YoungMin
    Kim, Eunhee
    Agha, Gul
    [J]. QUANTITATIVE EVALUATION OF SYSTEMS, QEST 2023, 2023, 14287 : 65 - 81
  • [28] Update and abstraction in model checking of knowledge and branching time
    Shilov, N. V.
    Garanina, N. O.
    Choe, K. -M.
    [J]. FUNDAMENTA INFORMATICAE, 2006, 72 (1-3) : 347 - 361
  • [29] Compositional Abstraction in Real-Time Model Checking
    Berendsen, Jasper
    Vaandrager, Frits
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS, 2008, 5215 : 233 - 249
  • [30] Correctness of efficient real-time model checking
    Reif, W
    Schellhorn, G
    Vollmer, T
    Ruf, J
    [J]. JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2001, 7 (02) : 194 - 209
12345