Ph.D Thesis

Ph.D StudentBustan Doron
SubjectEquivalence-Based Reductions and Checking for Preorders
DepartmentDepartment of Computer Science
Supervisor PROFESSOR EMERITUS Orna Grumberg


Due to the fast development of the  hardware and software industry, there is a growing need for formal verification tools and techniques.

Two widely used formal verification methods are temporal logic model checking and sequential equivalence checking. Temporal logic model checking is a

method for verifying finite-state systems with respect to propositional temporal logic specifications. In sequential equivalence checking, two sequential hardware designs are compared for language equivalence, meaning that for every sequence of inputs, the two designs produce the same sequence of outputs. Both model checking and equivalence checking are fully automatic. However, they both suffer from the state explosion problem, that is, their space requirements are high and limit their applicability to large systems.

Many approaches for overcoming the state explosion problem have been suggested; most of them use abstraction. An abstract model of a verified system is a model, which describes a system that is similar to the verified system but is simpler. An abstraction is conservative if the results of verifying the abstract model are true for the verified system. Thus, the abstract model preserves the verified properties of the verified

system. There are two types of preservations:  We say that an abstraction strongly preserves a set of verified properties, if for every property in the set, the system satisfies the property if and only if the abstract model satisfies it. Sometimes we relax our requirements such that for every verified property, if the abstract model satisfies the property then the system satisfies it as well. In this case the abstraction  weakly preserves the verified properties.

Strong preservation with respect to a set of properties can also be seen as an equivalence relation: A system is equivalent to an abstract model if the set of properties that the system satisfies is equal to the set of properties that the abstract model satisfies. Similarly, weak preservation with respect to a set of verified properties can be seen as a preorder: An abstract model is greater than a system if the set of properties that the system satisfies contains the set of properties that the abstract model satisfies. 

In this work we investigate different equivalence relations and preorders and their usage for abstraction. We present an algorithm that given a

system constructs the smallest abstract model, which is simulation equivalent to the system.

Next, we compare different preorders, which reflect a weak preservation of infinite behaviors. Finally, we present an algorithm which exploits the modular structure of the system to be verified, to improve the construction of an abstract model.