In: J.W. de Bakker, et al.: Lecture Notes in Computer Science, Vol. 430; Proceedings of the REX Workshop on Stepwise Refinement, 1989, Mook, The Netherlands, pages 641-668. Berin, Germany: Springer-Verlag, 1990.
Abstract: The paper presents a notion of preorder with related equivalence between concurrent systems which supports functional abstraction and refinement. Concurrent systems are considered as modelled by contact-free Elementary Net systems in which some states are observable (S-labelled systems). The proposed preorder, called State Transformation (ST) preorder, is defined on the basis of morphisms between the OLST-algebras associated to the compared systems. OLST-algebras describe the state space of S-labelled systems. The paper presents the construction of the unique canonical representative of each ST-equivalence class of S-observable systems.
Keywords: refinement; local state transformation; functional abstraction (and) refinement; elementary net system; observable state.