Interval Order Synthesis of EN-Systems with Read and Mutex Arcs

Elementary net systems (EN-systems) are a fundamental Petri net model with simple markings and simple connections between places and transitions. To enhance their modelling power, a number of extensions have been proposed such as transition probabilities or inhibitor arcs. In this paper, we consider EN-systems extended with read and mutex arcs. The resulting ENRM-systems allow one to capture a wider range of computational/dynamic systems than the original EN-systems. The standard semantical models of EN-systems and their extensions are based on sequences of executed transitions (or total orders) or sequences of sets of transitions executed simultaneously (or stratified orders). The first kind of semantics does not capture simultaneity of executed transitions, and the second kind only allows a restrictive form of (transitive) simultaneity. In this paper, we introduce semantics of ENRM-systems based on interval (partial) orders which allows one to describe behaviours where transitions have non-atomic duration and the simultaneity of executed transitions does not need to be transitive. Assuming such a semantical model, we consider the net synthesis problem for ENRM-systems, and demonstrate that the standard notion of a region of a transition system (providing input to the synthesis procedure) can still be applied after suitable modifications.