Paper Info
Title
Abstraction and refinement in model checking
Abstract
In this paper we survey abstraction and refinement in model checking. We restrict the discussion to existential abstraction which over-approximates the behaviors of the concrete model. The logics preserved under this abstraction are the universal fragments of branching-time temporal logics as well as linear-time temporal logics. For simplicity of presentation, we also restrict the discussion to abstraction functions, rather then abstraction relations. Thus, every concrete state is represented by exactly one abstract state. An abstract state then represents a set of concrete states, which is disjoint from the sets represented by other abstract states.
Year
DOI
Venue
2005
10.1007/11804192_11
FMCO
Keywords
Field
DocType
concrete model,universal fragment,model checking,concrete state,branching-time temporal logic,linear-time temporal logic,abstraction relation,abstract state,temporal logic
Abstraction model checking,Model checking,Abstraction,Disjoint sets,Object-oriented programming,Computer science,Theoretical computer science,Abstraction inversion,Formal methods,restrict
Conference
Volume
ISSN
ISBN
4111
0302-9743
3-540-36749-7
Citations 
PageRank 
References 
3
0.46
38
Authors
1
Name
Order
Citations
PageRank
Orna Grumberg14361351.99