External behaviour equivalence between two petrinets

Abstract

This paper presents a behaviour equivalence between two intrinsically deterministic Petri nets. Each net may have specific transitions and observable transitions. We define a relation between the observable transitions of the two nets. The behaviour equivalence which preserves interleaving semantics, consists in allowing that corresponding observable transitions must be fired in the same order. The main interest of this paper is that we do not make any restriction on the nets nor on the relation between corresponding transitions. Thus, the external behaviour equivalence particularly fits protocol validation, where one net models the protocol from level N, the other one models the service that the protocol must provide to the level N+1, and the relation associates transitions of the two nets modelling communication primitives between level N and level N+1. Unobservable transitions allow the service and the protocol to use auxiliary treatments. After defining the external behaviour equivalence, we present an algorithm which verifies it. This algorithm is based on an extended merging of two nets, and on a comparison of the merged net behaviour and the two nets behaviour. Then, we apply our method to a connection-disconnection protocol.