@article{GLS96,
title = { Compositional Minimisation of Finite State Systems using Interface Specifications },
author = {Graf, Susanne and L\"uttgen, Gerald and Steffen, Bernhard},
year = {1996},
note = {appeared as Passauer Informatik Bericht MIP-9505},
journal = {Formal Aspects of Computation},
volume = {8},
team = {DCS},
abstract = {In this paper we describe a method for the obtention of
the minimal transition system, representing a communicating system
given by a set of parallel processes, avoiding the complexity of the
non minimal transition system. We consider minimization with respect
to observational equivalence, but the method may be adapted to any
other equivalence. An interesting method to achieve this goal is to
proceed by stepwise composition and minimization of the components of
the system. However, if no precautions are taken, the intermediate
state graphs generated by this method may contain a lot of transitions
which are impossible in the whole context. We give here a variant of
this method which allows to avoid these impossible transitions by
taking into account at each composition step a guess of the interface
behaviour of the context. This <i>interface specification</i> must be
provided by the user. The method is based on a <I>reduction
operator</I> for the composition of a subsystem with its interface
specification, which is similar to the parallel operator but
introduces <I>undefinedness</I> predicates whereever the interface
<i>cuts off</i> a transition. The parallel operator is defined in a
way that these undefinedness predicates disappear again in the full
context if and only if the corresponding transition is in fact
impossible in the whole system. The <I>efficiency</I> of the method
depends in fact on the accuracy with which the designer is able to
approximate the possible sequences of the context, but its
<I>correctness</I> does not. The proof of the correctness of the
method is based on a preorder relation similar to the one defined by
Walker. },
}
