In: Proceedings of the 24th International Conference on Applications and Theory of Petri Nets (ICATPN 2003), Eindhoven, The Netherlands, June 23-27, 2003, pages 357-376. Volume 2679 of Lecture Notes in Computer Science / Wil M. P. van der Aalst and Eike Best (Eds.) --- Springer-Verlag, June 2003.
Abstract: n the paper we extend the algebraic description of Petri nets based on rewriting logic by introducing a partial synchronous operation in order to distinguish between synchronous and concurrent occurrences of transitions. In such an extension one first needs to generate steps of transitions using a partial operation of synchronous composition and then to use these steps to generate process terms using partial operations of concurrent and sequential composition. Further, we define which steps are true synchronous. In terms of causal relationships, such an extension corresponds to the approach described in [6,7,9], where two kinds of causalities are defined, first saying (as usual) which transitions cannot occur earlier than others, while the second indicating which transitions cannot occur later than others. We illustrate this claim by proving a one-to-one correspondence between such extended algebraic semantics of elementary nets with inhibitor arcs and causal semantics of elementary nets with inhibitor arcs presented in [7].