Concurrent Regular Expressions and their Relationship to Petri Nets

We define algebraic systems called concurrent regular expressions which provide a modular description of languages of Petri nets. Concurrent regular expressions are extension of regular expressions with four operators - interleaving, interleaving closure, synchronous composition and renaming. This alternative characterization of Petri net languages gives us a flexible way of specifying concurrent systems. Concurrent regular expressions are modular and hence easier to use for specification. The proof of equivalence also provides a natural decomposition method for Petri nets. 1 Introduction Formal models proposed for specification and analysis of concurrent systems can be categorized roughly into two groups: algebra based and transition based. The algebra based models specify all possible behaviors of concurrent systems by means of expressions that consist of algebraic operators and primitive behaviors. Examples of such models are path expressions[3], behavior expressions[21] and extend..