Paper Info
Title
3-Valued abstraction: More precision at less cost
Abstract
This paper investigates both the precision and the model checking efficiency of abstract models designed to preserve branching time logics w.r.t. a 3-valued semantics. Current abstract models use ordinary transitions to over approximate the concrete transitions, while they use hyper transitions to under approximate the concrete transitions. In this work, we refer to precision measured w.r.t. the choice of abstract states, independently of the formalism used to describe abstract models. We show that current abstract models do not allow maximal precision. We suggest a new class of models and a construction of an abstract model which is most precise w.r.t. any choice of abstract states. As before, the construction of such models might involve an exponential blowup, which is inherent by the use of hyper transitions. We therefore suggest an efficient algorithm in which the abstract model is constructed during model checking, by need. Our algorithm achieves maximal precision w.r.t. the given property while remaining quadratic in the number of abstract states. To complete the picture, we incorporate it into an abstraction-refinement framework.
Year
DOI
Venue
2008
10.1016/j.ic.2008.07.004
Information & Computation
Keywords
Field
DocType
maximal precision,model checking,concrete transition,current abstract model,abstract model,hyper transition,maximal precision w,precise w,model checking efficiency,3-valued abstraction,abstract state,computational complexity,refinement calculus,formal verification,finite state machines
Algebraic specification,Discrete mathematics,Model checking,Exponential function,Refinement calculus,Computer science,Quadratic equation,Algorithm,Finite-state machine,Computational complexity theory,Formal verification
Journal
Volume
Issue
ISSN
206
11
Information and Computation
Citations 
PageRank 
References 
21
0.76
30
Authors
2
Name
Order
Citations
PageRank
Sharon Shoham134226.67
Orna Grumberg24361351.99