Refining and Compressing Abstract Model Checking

For verifying systems involving a wide number or even an infinite number of states, standard model checking needs approximating techniques to be tractable. Abstract interpretation offers an appropriate framework to approximate models of reactive systems in order to obtain simpler models, where properties of interest can be effectively checked. In this work we study the impact of domain refinements in abstract interpretation based model checking. We consider the universal fragment of the branching time temporal logic CTL∗ and we characterize the structure of temporal formulae that are verified in new abstract models obtained by refining an abstract domain by means of reduced product and disjunctive completion, or by simplifying the domain by their inverse operations of complementation and least disjunctive bases.