Theory of regions

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 ${\displaystyle (S,\Lambda ,\rightarrow )}$ is a mapping assigning to each state ${\displaystyle s\in S}$ a number ${\displaystyle \sigma (s)}$ (natural number for P/T nets, binary for ENS) and to each transition label a number ${\displaystyle \tau (\ell )}$ such that consistency conditions ${\displaystyle \sigma (s')=\sigma (s)+\tau (\ell )}$ holds whenever ${\displaystyle (s,\ell ,s')\in \rightarrow }$. ^[1]

Intuitive explanation

Each region represents a potential place of a Petri net.

Mukund: event/state separation property, state separation property. ^[2]

References

1. "Madhavan Mukund".
2. Mukund, Madhavan (1992-12-01). "Petri nets and step transition systems" . International Journal of Foundations of Computer Science. 03 (4): 443–478. doi:10.1142/S0129054192000231. ISSN   0129-0541.

• Badouel, Eric; Darondeau, Philippe (1998), Reisig, Wolfgang; Rozenberg, Grzegorz (eds.), "Theory of regions", 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