Labelled free choice petri nets, finite product Automata, and Expressions[HBNI Th83]

Abstract

Petri nets are a formal model of concurrent systems. They were first defined by Petri in his thesis [Pet62] and were presented at the IFIP 1962 congress in Munich [Pet63]. Nets are widely used in modelling various aspects of distributed systems. There are several different notions of acceptance to define languages for labelled Petri nets [Pet76, Hac76, Gra81, GR92] with general markings, depending on restrictions on labelling and “final” markings. Some of these are studied by Peterson [Pet76] and in a survey article by Jantzen [Jan86]. Grabowski [Gra81] defined expressions matching the regular languages accepted by labelled 1-bounded nets. Mazurkiewicz [Maz77] considers P-type languages of 1-bounded nets [Pet76, Jan86], labelled with a concurrent alphabet. Ochma´nski [Och85] defines c-rational expressions and sets up a correspondence between them and regular trace languages. An algebraic characterization in terms of recognition by finite partially commutative monoids is also discussed by Mazurkiewicz [Maz86] and described in this book. However this has not been used so far for characterizing subclasses of nets as has been done in automata theory. In this thesis, our focus is on producing expressions which exactly describe various subclasses of trace-labelled 1-bounded free choice nets, equipped with an initial marking and a set of final markings, so that the L-type Mazurkiewicz trace languages of both formalisms are the same. To get these expressions for nets, we use product systems in between. For that we explore the question of direct product representation of labelled 1-bounded nets.