A Decidability Result for the Model Checking of Infinite-State Systems

被引：0

作者：

Zucchelli, Daniele ^{[2
]}

Nicolini, Enrica ^{[1
,3
]}

机构：

[1] LORIA, F-54602 Villers Les Nancy, France

[2] Univ Milan, Dipartimento Sci Informaz, I-20135 Milan, Italy

[3] INRIA Nancy Grand Est, F-54602 Villers Les Nancy, France

来源：

JOURNAL OF AUTOMATED REASONING | 2012年 / 48卷 / 01期

关键词：

Model checking; Combination methods; Satisfiability problems; Infinite-state systems; INTERPOLATION;

D O I：

10.1007/s10817-010-9192-z

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present a decidability result for the model checking of a certain class of properties that can be conveniently expressed as ground formulae of a first-order temporal fragment. The decidability result is obtained by importing into the context of model-checking problems some techniques developed for the combination of decision procedures for the satisfiability of constraints. The general decidability result is then specialized for checking properties of particular interest, such as liveness and safety, and, for the latter case, a more optimized algorithm has been proposed.

引用

页码：1 / 42

页数：42

共 50 条

[21] STAMINA 2.0: Improving Scalability of Infinite-State Stochastic Model Checking
Roberts, Riley
Neupane, Thakur
Buecherl, Lukas
Myers, Chris J.
Zhang, Zhen
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2022, 2022, 13182 : 319 - 331
[22] Infinite-state high-level MSCs: Model-checking and realizability
Genest, Blaise
Muscholl, Anca
Seidl, Helmut
Zeitoun, Marc
JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2006, 72 (04) : 617 - 647
[23] Infinite-state high-level MSCs: Model-checking and realizability
Genest, B
Muscholl, A
Seidl, H
Zeitoun, M
AUTOMATA, LANGUAGES AND PROGRAMMING, 2002, 2380 : 657 - 668
[24] Extensible Proof Systems for Infinite-State Systems
Cleaveland, Rance
Keiren, Jeroen J. A.
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2024, 25 (01)
[25] LTL falsification in infinite-state systems
Cimatti, Alessandro
Griggio, Alberto
Magnago, Enrico
INFORMATION AND COMPUTATION, 2022, 289
[26] SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems
Draeger, Klaus
Kupriyanov, Audrey
Finkbeiner, Bernd
Wehrheim, Heike
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2010, 6015 : 271 - +
[27] Decidability of infinite-state timed CCP processes and first-order LTL
Valencia, FD
THEORETICAL COMPUTER SCIENCE, 2005, 330 (03) : 577 - 607
[28] Bounded model checking of infinite state systems
Tobias Schuele
Klaus Schneider
Formal Methods in System Design, 2007, 30 : 51 - 81
[29] Bounded model checking of infinite state systems
Schuele, Tobias
Schneider, Klaus
FORMAL METHODS IN SYSTEM DESIGN, 2007, 30 (01) : 51 - 81
[30] Model checking procedures for infinite state systems
Bogunovic, Nikola
Pek, Edgar
13TH ANNUAL IEEE INTERNATIONAL SYMPOSIUM AND WORKSHOP ON ENGINEERING OF COMPUTER BASED SYSTEMS, PROCEEDINGS: MASTERING THE COMPLEXITY OF COMPUTER-BASED SYSTEMS, 2006, : 419 - +

← 1 2 3 4 5 →