An Algebraic Semantics for Hierarchical P/T Nets
(extended abstract)
The first part of this paper gives an algebraic semantics for
Place/Transition nets in terms of an algebra which is based on the
process algebra ACP. The algebraic semantics is such that a P/T net
and its term representation have the same operational behavior. As
opposed to other approaches in the literature, the actions in the
algebra do not correspond to the firing of a transition, but to the
consumption or production of tokens. Equality of P/T nets can be
determined in a purely equational way.
The second part of this paper extends the results to hierarchical
P/T nets. It gives a compositional algebraic semantics for both
their complete operational behavior and their high-level,
observable behavior. By means of a non-trivial example, the
Alternating-Bit Protocol, it is shown that the notions of
abstraction and verification in the process algebra ACP can be used
to verify in an equational way whether a hierarchical P/T net
satisfies some algebraic specification of its observable behavior.
Thus, the theory in this paper can be used to determine whether two
hierarchical P/T nets have the same observable behavior. As an
example, it is shown that the Alternating-Bit Protocol behaves as a
simple one-place buffer. The theory forms a basis for a modular,
top-down design methodology based on Petri nets.