@inproceedings{GL93a,
title = { Program Verification using compositional Abstraction },
author = {Graf, Susanne and Loiseaux, Claire},
month = {apr},
year = {1993},
booktitle = {TAPSOFT 93, joint conference CAAP/FASE},
publisher = {LNCS 668, Springer Verlag},
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 ``interface specification'' 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 ``cuts off'' 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.},
}
