Theory of regions explained

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, Λ , → ) 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') = \sigma(s) + \tau(\ell) holds whenever (s,\ell,s') \in → .^[1]

Intuitive explanation

Each region represents a potential place of a Petri net.

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

Notes and References

1. Web site: 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. 10.1142/S0129054192000231. 0129-0541.