Compositional Minimization of Finite State Systems

S. Graf, B. Steffen

	   In this paper we develop a compositional method for the
	   construction of the minimal transition system that represents
	   the semantics of a given reactive system.  The point of
	   this method is that it exploits structural properties of the
	   reactive system in order to avoid the consideration of large
	   intermediate representations.  Central is the use of {\em
	   interface specifications} here, which express constraints on
	   the components' communication behaviour, and therefore to
	   control the state explosion caused by the interleavings of
	   actions of communicating parallel components.

	   The {\em effect} of the method, which is developed for
	   bisimulation semantics here, depends on the structure of
	   the reactive system under consideration, in particular on
	   the accuracy of the interface specifications.  However, its
	   {\em correctness} does not: every `successful' construction
	   is guaranteed to yield the desired minimal transition
	   system, independently of the correctness of the interface
	   specifications provided by the designer.