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 条
  • [1] A Decidability Result for the Model Checking of Infinite-State Systems
    Daniele Zucchelli
    Enrica Nicolini
    Journal of Automated Reasoning, 2012, 48 : 1 - 42
  • [2] Decidability of model checking for infinite-state concurrent systems
    Javier Esparza
    Acta Informatica, 1997, 34 : 85 - 107
  • [3] Decidability of model checking for infinite-state concurrent systems
    Esparza, J
    ACTA INFORMATICA, 1997, 34 (02) : 85 - 107
  • [4] General decidability theorems for infinite-state systems
    Abdulla, PA
    Cerans, K
    Jonsson, B
    Tsay, YK
    11TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1996, : 313 - 321
  • [5] Global model-checking of infinite-state systems
    Piterman, N
    Vardi, MY
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 387 - 400
  • [6] On model checking for non-deterministic infinite-state systems
    Emerson, EA
    Namjoshi, KS
    THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1998, : 70 - 80
  • [7] Symbolic model checking of infinite-state systems using narrowing
    Escobar, Santiago
    Meseguer, Jose
    TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2007, 4533 : 153 - +
  • [8] Model checking infinite-state Markov chains
    Remke, A
    Haverkort, BR
    Cloth, L
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2005, 3440 : 237 - 252
  • [9] Selfless Interpolation for Infinite-State Model Checking
    Schindler, Tanja
    Jovanovic, Dejan
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2018), 2018, 10747 : 495 - 515
  • [10] Combination methods for satisfiability and model-checking of infinite-state systems
    Chilardi, Silvio
    Nicolini, Enrica
    Ranise, Silvio
    Zucchelli, Daniele
    AUTOMATED DEDUCTION - CADE-21, PROCEEDINGS, 2007, 4603 : 362 - +
12345