In: A. Cortesi (Ed.): Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002, Venice, Italy, January 21-22, 2002. Revised Papers, pages 1-272pp. Springer Verlag, LNCS 2294, April 2002.
Abstract: We present a simulation preorder for reactive systems modeled by fair Kripke structures whose transition relation is divided into two parts, internal and external. The first one models the internal behaviour of the system, while the second one is used to model the interaction with an environment. We show that our simulation preorder preserves a substantial subset of (forall CTL*). Then, we present an abstraction technique for systems composed by multiple modules and we show that each such system is smaller in the simulation preorder than its ``augmented'' components. We illustrate our abstraction methodology by applying it to Petri net reactive systems.