Asynchronous communication of petri nets and the refinement of transitions

Abstract

In this paper we study nets whose boundaries in a context net consist of places only, i.e. nets that communicate asynchronously with their environment. Such nets are called equivalent, if exchanging them in any context preserves deadlock-freeness. We characterize this equivalence internally, i.e. without referring to all possible contexts. Since this equivalence is undecidable in general, we then define a subclass of nets that are to some degree deterministic. For nets from this subclass we can show that the equivalence is decidable and that the exchange of equivalent nets does not only preserve deadlock-freeness, but gives nets that are even bisimilar; these results especially apply to the behaviour preserving refinement of transitions.