Bounded model checking for the universal fragment of CTL

被引：0
|
作者：
Penczek, W
Wozna, B
Zbrzezny, A
机构：
[1] Polish Acad Sci, Inst Comp Sci, PL-01237 Warsaw, Poland
[2] Podlasie Acad, PL-08110 Siedlce, Poland
[3] PU, Inst Math & Comp Sci, PL-42200 Czestochowa, Poland
来源：
FUNDAMENTA INFORMATICAE | 2002年 / 51卷 / 1-2期
关键词：
bounded model checking; logic ACTL (ECTL); bounded semantics; translation to SAT; Elementary Net Systems; system verification;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Bounded Model Checking (BMC) has been recently introduced as an efficient verification method for reactive systems. BMC based on SAT methods consists in searching for a counterexample of a particular length and generating a propositional formula that is satisfiable iff such a counterexample exists. This new technique has been introduced by E. Clarke et a]. for model checking of linear time temporal logic (LTL). Our paper shows how the concept of bounded model checking can be extended to ACTL (the universal fragment of CTL). The implementation of the algorithm for Elementary Net Systems is described together with the experimental results.
引用
收藏
页码：135 / 156
页数：22
相关论文
共 50 条
  • [21] The model checking fingerprints of CTL operators
    Andreas Krebs
    Arne Meier
    Martin Mundhenk
    Acta Informatica, 2019, 56 : 487 - 519
  • [22] CTL Model Checking in Deduction Modulo
    Ji, Kailiang
    AUTOMATED DEDUCTION - CADE-25, 2015, 9195 : 295 - 310
  • [23] Quantified CTL: Expressiveness and Model Checking
    Da Costa, Arnaud
    Laroussinie, Francois
    Markey, Nicolas
    CONCUR 2012 - CONCURRENCY THEORY, 2012, 7454 : 177 - 192
  • [24] The model checking fingerprints of CTL operators
    Krebs, Andreas
    Meier, Arne
    Mundhenk, Martin
    2015 22ND INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING (TIME), 2015, : 101 - 110
  • [25] The model checking fingerprints of CTL operators
    Krebs, Andreas
    Meier, Arne
    Mundhenk, Martin
    ACTA INFORMATICA, 2019, 56 (06) : 487 - 519
  • [26] An Approximate CTL Model Checking Approach
    Zhu, Weijun
    Feng, Pan
    Deng, Miaolei
    PROCEEDINGS OF 2019 IEEE 10TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS 2019), 2019, : 646 - 648
  • [27] CTL model checking for Boolean program
    Lee, Taehoon
    Kwon, Gihwon
    Han, Hyuksoo
    COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2006, PT 4, 2006, 3983 : 1081 - 1089
  • [28] Bounded model checking for the existential fragment of TCTL-G and diagonal timed automata
    Wozna, Bozena
    Zbrzezny, Andrzej
    FUNDAMENTA INFORMATICAE, 2007, 79 (1-2) : 229 - 256
  • [29] Bounded Model Checking for LLVM
    Priya, Siddharth
    Su, Yusen
    Bao, Yuyan
    Zhou, Xiang
    Vizel, Yakir
    Gurfinkel, Arie
    2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD, 2022, 3 : 214 - 224
  • [30] Bounded model checking with QBF
    Dershowitz, N
    Hanna, Z
    Katz, J
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS, 2005, 3569 : 408 - 414
12345