Free-choice Petri nets: the algebraic approach

In this paper, we show how a decomposition of a free choice Petri net into a `routing´ network and marked graph subnetworks (i.e. linear subnetworks in the [max,+] setting) leads to new methods and algorithms to test structural as well as temporal properties of the net. We show how this decomposition allows one to: (in the timed case) establish evolution equations which involve two linear systems, a (min,+)-linear system, and a quasi (+,×)-linear one; (in the stochastic case) check stability i.e. the fact that the marking remains bounded in probability. The main tools for proving these properties are graph theory, idempotent algebras and ergodic theory