In: Petri Net Technology for Communication-Based Systems, pages 430-454. Volume 2472 of Lecture Notes in Computer Science / Hartmut Ehrig, Wolfgang Reisig, Grzegorz Rozenberg and Herbert Weber (Eds.) --- Springer-Verlag, November 2003.
Abstract: We suggest a new notion of behaviour preserving transition refinement based on partial order semantics. This notion is called transition refinement. We introduced transition refinement for elementary (low-level) Petri Nets earlier. For modelling and verifying complex distributed algorithms, high-level (Algebraic) Petri nets are usually used. In this paper, we define transition refinement for Algebraic Petri Nets. This notion is more powerful than transition refinement for elementary Petri nets because it corresponds to the simultaneous refinement of several transitions in an elementary Petri net. Transition refinement is particularly suitable for refinement steps that increase the degree of distribution of an algorithm, e.g. when synchronous communication is replaced by asynchronous message passing. We study how to prove that a replacement of a transition is a transition refinement.
Keywords: Distributed Algorithms; Concurrency; Action Refinement; Partial Order Semantics; Verification; Algebraic Petri Nets.