Model checking as constraint solving

被引：0
|
作者：
Podelski, A [1 ]
机构：
[1] Max Planck Inst Informat, D-66123 Saarbrucken, Germany
来源：
STATIC ANALYSIS | 2000年 / 1824卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We show how model checking procedures for different kinds of infinite-state systems can be formalized as a generic constraint-solving procedure, viz. the saturation under a parametric set of inference rules. The procedures can be classified by the solved form they are to compute. This solved form is a recursive (automaton-like) definition of the set of states satisfying the given temporal property in the case of systems over stacks or other symbolic data.
引用
收藏
页码：22 / 37
页数：16
相关论文
共 50 条
  • [1] From Model-Checking to Temporal Logic Constraint Solving
    Fages, Francois
    Rizk, Aurelien
    [J]. PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING, 2009, 5732 : 319 - 334
  • [2] Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
    Alex Groce
    Klaus Havelund
    Gerard Holzmann
    Rajeev Joshi
    Ru-Gang Xu
    [J]. Annals of Mathematics and Artificial Intelligence, 2014, 70 : 315 - 349
  • [3] Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
    Groce, Alex
    Havelund, Klaus
    Holzmann, Gerard
    Joshi, Rajeev
    Xu, Ru-Gang
    [J]. ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2014, 70 (04) : 315 - 349
  • [4] Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints
    Chan, W
    Anderson, R
    Beame, P
    Notkin, D
    [J]. COMPUTER AIDED VERIFICATION, 1997, 1254 : 316 - 327
  • [5] Model checking for the concurrent constraint paradigm
    Villanueva, A
    [J]. AI COMMUNICATIONS, 2004, 17 (02) : 93 - 94
  • [6] A Symbolic Approach Based on Model Checking and Constraint Solving Techniques for Reverse Engineering of Thomas Networks Parameters
    Gallet, Emmanuelle
    Manceny, Matthieu
    Le Gall, Pascale
    Ballarini, Paolo
    [J]. COMPUTATIONAL METHODS IN SYSTEMS BIOLOGY, 2013, 8130 : 240 - +
  • [7] Checking Sequence Generation for Symbolic Input/Output FSMs by Constraint Solving
    Timo, Omer Nguena
    Petrenko, Alexandre
    Ramesh, S.
    [J]. THEORETICAL ASPECTS OF COMPUTING - ICTAC 2018, 2018, 11187 : 354 - 375
  • [8] Improving the efficiency of forward checking algorithm for solving constraint satisfaction problems
    Farhang, Yusef
    Meybodi, M. R.
    Hatamlou, A. R.
    [J]. ISDA 2008: EIGHTH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS DESIGN AND APPLICATIONS, VOL 1, PROCEEDINGS, 2008, : 240 - +
  • [9] Model checking LTL using constraint programming
    Esparza, J
    Melzer, S
    [J]. APPLICATION AND THEORY OF PETRI NETS 1997, 1997, 1248 : 1 - 20
  • [10] Constraint logic programming applied to model checking
    Fribourg, L
    [J]. LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, PROCEEDINGS, 2000, 1817 : 30 - 41
12345