Transition systems and testing preorders : an alternative to Petri Nets for systems specifications

The models of concurrency which have been proposed in the last ten years can be divided in two broad groups: models based on arbitrary interleavings and models based on partial orderings of elementary actions. Labelled Transition Systems and Petri Nets are two, widely used, representatives of these two groups. We discuss their relationships and their impact on formal specifications of systems and on proof of systems properties. In particular, we show how transition systems naturally support a theory of preorders which allows to prove whether a system is a satisfactory approximation of another, whether an implementation satisfies a specification and whether a subsystem can be substituted by another without affecting the overall behaviour.