Autori: F.L. Tiplea, A. Tiplea

Editorial: Springer-Verlag, Proceedings of 3rd International Workshop on "Verification, Model Checking and Abstract Interpretation", Lecture Notes in Computer SCience, vol. 2294, p.272-288, 2002.

Rezumat:

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.

Cuvinte cheie: verification. model-checking, abstraction

URL: http://www.springerlink.com/(xc2n2a45t1svb0455mhjwk45)/app/home/journal.asp?referrer=parent&backto=browsepublicationsresults,1012,1573;