From trace sets to modal-transition systems by stepwise abstract interpretation

Following and expanding upon the philosophy set down by Cousot and Cousot, this tutorial paper uses stepwise abstract interpretation to transform a system’s naive trace-set semantics into a format that is readily analyzable by temporal logic. The abstraction interpretations first transform a concrete trace-set semantics, where the traces are characterized by a state-transition relation, into an abstracted trace-set semantics that uses abstracted states such that linear-time properties are soundly (and in some cases, completely) preserved. Conditions under which universally and existentially quantified linear-time properties are preserved are also stated, and these conditions motivate the universal and existential abstractions of the abstracted trace-set semantics into state-set semantics upon which quantified properties can be soundly and completely checked, producing simple branching-time logics. Finally, the combination of universal and existential quantification in a single logic motivates mixed and modal transition systems, where a concrete system is abstracted by two transition relations, one that abstracts universal behaviors and one that abstracts existential behaviors. The definitions, constructions, and technical results are illustrated by examples.