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 条
  • [41] Graded CTL Model Checking for Test Generation
    Napoli, Margherita
    Parente, Mimmo
    THEORY OF MODELING & SIMULATION: DEVS INTEGRATIVE M&S SYMPOSIUM 2011 (TMS-DEVS 2011) - 2011 SPRING SIMULATION, 2011, 43 (01): : 59 - 66
  • [42] Symbolic Causality Checking Using Bounded Model Checking
    Beer, Adrian
    Heidinger, Stephan
    Kuehne, Uwe
    Leitner-Fischer, Florian
    Leue, Stefan
    MODEL CHECKING SOFTWARE, SPIN 2015, 2015, 9232 : 203 - 221
  • [43] CTL model checking for labelled tree queries
    Halle, Sylvain
    Villemaire, Roger
    Cherkaoui, Omar
    TIME 2006: THIRTEENTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2006, : 27 - +
  • [44] First-order-CTL model checking
    Bohn, J
    Damm, W
    Grumberg, O
    Hungar, H
    Laster, K
    FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, 1998, 1530 : 283 - 294
  • [45] CTL formalized specification templates in model checking
    Chen, Z. (chenzhiyuan@hrbeu.edu.cn), 1600, Editorial Board of Journal of Harbin Engineering (34):
  • [46] A Bounded Semantics for Improving the Efficiency of Bounded Model Checking
    Zhang, Wenhui
    Gao, Ya
    2022 26TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2022), 2022, : 97 - 106
  • [47] Bounded Model Checking for Asynchronous Hyperproperties
    Hsu, Tzu-Han
    Bonakdarpour, Borzoo
    Finkbeiner, Bernd
    Sanchez, Cesar
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2023, 2023, 13993 : 29 - 46
  • [48] Simple bounded LTL model checking
    Latvala, T
    Biere, A
    Heljanko, K
    Junttila, T
    FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2004, 3312 : 186 - 200
  • [49] Bounded Model Checking of Contiki Applications
    Voertler, Thilo
    Ruelke, Steffen
    Hofstedt, Petra
    2012 IEEE 15TH INTERNATIONAL SYMPOSIUM ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS & SYSTEMS (DDECS), 2012, : 258 - 261
  • [50] Bounded model checking of compositional processes
    Sun, Jun
    Liu, Yang
    Dong, Jin Song
    Sun, Jing
    TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2008, : 23 - +
12345