Formula-dependent abstraction for CTL model checking

被引：0

作者：

Qian, Junyan ^{[1
]}

Zhao, Lingzhong ^{[1
]}

Cai, Guoyong ^{[1
]}

Gu, Tianlong ^{[1
]}

机构：

[1] Guilin Univ Elect Technol, Dept Comp Sci & Technol, Guilin 541004, Peoples R China

来源：

COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2008, PT 2, PROCEEDINGS | 2008年 / 5073卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We present a state abstraction that is defined with respect to a given CTL formula. Since it does not attempt to preserve all ACTL formula, like simulation does, we can expect to compute coarser abstraction. Specifically, the abstraction is used to reduce the size of each Kripke structure, so that their product will be smaller. When the abstraction is too coarse, we show how refinement can be applied to produce a more precise abstract model. We also extend the notion of formula-dependent abstraction to Kripke structure with fairness, and define the coarsest abstraction that preserves the given CTL formula interpreted with respect to the fair paths. The method is exact and fully automatic, and handles full CTL.

引用

页码：1035 / 1048

页数：14

共 50 条

[31] Abstraction refinement for bounded model checking
Gupta, A
Strichman, O
COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2005, 3576 : 112 - 124
[32] Competent predicate abstraction in model checking
LI Li1
2Key Laboratory for Information System Security
3School of Software
4Department of ECE
ScienceChina(InformationSciences), 2011, 54 (02) : 258 - 267
[33] Bounded model checking for the universal fragment of CTL
Penczek, W
Wozna, B
Zbrzezny, A
FUNDAMENTA INFORMATICAE, 2002, 51 (1-2) : 135 - 156
[34] CTL Model Checking based on Probe Machine
Zhu, Weijun
Liu, Yichen
Li, En
PROCEEDINGS OF 2019 IEEE 10TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS 2019), 2019, : 518 - 522
[35] Model checking CTL properties of pushdown systems
Walukiewicz, I
FST TCS 2000: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2000, 1974 : 127 - 138
[36] On the Model Checking Problem for Some Extension of CTL*
A. R. Gnatenko
V. A. Zakharov
Automatic Control and Computer Sciences, 2021, 55 : 776 - 785
[37] CTL Model Checking of Self Modifying Code
Touili, Tayssir
Ye, Xin
2020 25TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2020), 2020, : 11 - 20
[38] Symbolic guided search for CTL model checking
Bloem, R
Ravi, K
Somenzi, F
37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 29 - 34
[39] On the Model Checking Problem for Some Extension of CTL*
Gnatenko, A. R.
Zakharov, V. A.
AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2021, 55 (07) : 776 - 785
[40] CTL Model-Checking with Graded Quantifiers
Ferrante, Alessandro
Napoli, Margherita
Parente, Mimmo
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2008, 5311 : 18 - 32

← 1 2 3 4 5 →