ACP Semantics for Petri Nets

keywords: Petri nets, process algebra ACP, formal methods, semantics, specification, transformation
The paper deals with algebraic semantics for Petri nets, based on process algebra ACP. The semantics is defined by assigning a special variable to every place of given Petri net, expressing the process initiated in the place. Algebraic semantics of the Petri net is then defined as a parallel composition of all the variables, where corresponding places hold tokens within the initial marking. Resulting algebraic specification preserves operational behavior of the original net-based specification.
mathematics subject classification 2000: 68-Q85
reference: Vol. 37, 2018, No. 6, pp. 1464–1484