An Algebraic Semantics for Hierarchical P/T Nets

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...

• Type: Conference
• Year: 1995
• Where: APN
• Authors: Twan Basten, Marc Voorhoeve
• Keywords: Algebraic Semantics, APN 1995, Artificial Intelligence, Hierarchical P/t Nets, P/T Nets