Theory of regions

Short description: Petri net synthesis approach

The Theory of regions is an approach for synthesizing a Petri net from a transition system. As such, it aims at recovering concurrent, independent behavior from transitions between global states. Theory of regions handles elementary net systems as well as P/T nets and other kinds of nets. An important point is that the approach is aimed at the synthesis of unlabeled Petri nets only.

Definition

A region of a transition system $(S,\mathrm{\Lambda },\to )$ is a mapping assigning to each state $s\in S$ a number $\sigma (s)$ (natural number for P/T nets, binary for ENS) and to each transition label a number $\tau (\ell )$ such that consistency conditions $\sigma (s^{\prime })=\sigma (s)+\tau (\ell )$ holds whenever $(s,\ell ,s^{\prime })\in \to$.

Intuitive explanation

Each region represents a potential place of a Petri net.

Mukund: event/state separation property, state separation property.

References

• Badouel, Eric; Darondeau, Philippe (1998), Reisig, Wolfgang; Rozenberg, Grzegorz, eds., "Theory of regions" (in en), Lectures on Petri Nets I: Basic Models: Advances in Petri Nets, Lecture Notes in Computer Science (Berlin, Heidelberg: Springer): pp. 529–586, doi:10.1007/3-540-65306-6_22, ISBN 978-3-540-49442-3