Plain, Bounded, Reversible, Persistent, and k-marked Petri Nets Have Marked Graph Reachability Graphs

  • Eike Best
  • Harro WimmelEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9899)


In workflow specifications, it is desirable that k customers can use a system interference-freely, so that no customer is disturbed by other activities on the same workflow. In a Petri net representation of a workflow, this corresponds to allowing initial k-markings, in which the number of tokens on each place is a multiple of k, and to require that every global activity is separable, that is, can be viewed as k individual activities, each acting as if the initial marking had one k’th of its values. In this paper, it is shown that, if \(k\ge 2\), if such a Petri net is plain, and if its reachability graph is finite, reversible, and persistent, then the latter is isomorphic to the reachability graph of a marked graph.

The problem has been mentioned as open in a paper by Best and Darondeau from 2011, and its resolution rests on a more recent (2014) characterisation of the reachability graphs of marked graph Petri nets. This characterisation involves the notion of backward persistence, i.e., persistence in the reverse reachability graph, as well as some other properties which are true in the given context. The technical contribution of this paper is to prove that backward persistence is implied by the properties of plainness, boundedness, reversibility and persistence, provided the greatest common divisor of the token counts in the initial state is greater than 1. The existence of a suitable marked graph then follows.


  1. 1.
    Best, E., Darondeau, P.: A decomposition theorem for finite persistent transition systems. Acta Informatica 46(3), 237–254 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Best, E., Darondeau, P.: Separability in persistent Petri nets. Fundam. Inform. 113(3–4), 179–203 (2011)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Best, E., Devillers, R.: Characterisation of the state spaces of marked graph Petri nets. To be published in Information and Computation (2016).
  4. 4.
    Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked directed graphs. J. Comput. Syst. Sci. 5(5), 511–523 (1971)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    van Glabbeek, R.J., Goltz, U., Schicke, J.-W.: On causal semantics of Petri nets. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 43–59. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    van Hee, K.M., Sidorova, N., Voorhoeve, M.: Soundness and separability of workflow nets in the stepwise refinement approach. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 337–356. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Keller, R.M.: A fundamental theorem of asynchronous parallel computation. In: Feng, T.Y. (ed.) Parallel Processing. LNCS, vol. 24, pp. 102–112. Springer, Heidelberg (1975)CrossRefGoogle Scholar
  8. 8.
    Landweber, L.H., Robertson, E.L.: Properties of conflict-free and persistent Petri nets. JACM 25(3), 352–364 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)CrossRefGoogle Scholar
  10. 10.

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Department of Computing ScienceCarl von Ossietzky Universität OldenburgOldenburgGermany

Personalised recommendations