3-ValuedAbstractionMorePrecisionatLessCost-Technion.PDFVIP

3-Valued Abstraction: More Precision at Less Cost Sharon Shoham Orna Grumberg Computer Science Department, Technion, Haifa, Israel E-mail: {sharonsh,orna}@cs.technion.ac.il Abstract formula is interpreted w.r.t. a 3-valued semantics [1]. This semantics evaluates a formula to either true,false or indefi- This paper investigates both the precision and the model nite. Abstract models can then be designed to be conserva- checking efficiency of abstract models designed to preserve tive for both true and false . Only if the value of a formula branching time logics w.r.t. a 3-valued semantics. Current in the abstract model is indefinite, its value in the concrete abstract models use ordinary transitions to over approxi- model is unknown. We follow this approach. mate the concrete transitions, while they use hyper transi- The logic specifications we consider in this paper are for- tions to under approximate the concrete transitions. In this mulas of the modal µ-calculus [15]. The modal µ-calculus work we refer to precision measured w.r.t. the choice of is a powerful formalism for expressing properties of transi- abstract states, independently of the formalism used to de- tion systems using fixpoint operators. In particular, it com- scribe abstract models. We show that current abstract mod- bines both existential and universal properties. As such, two els do not allow maximal precision. We suggest a new class transition relations are needed in an abstract model for it to of models and a construction of an