Dynamic Networks of Timed Petri Nets

  • María Martos-Salgado
  • Fernando Rosa-Velardo
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8489)


We study dynamic networks of infinite-state timed processes, modelled as unbounded Petri nets. These processes can evolve autono-mously, synchronize with each other (e.g., in order to gain access to some shared resources) and be created or become garbage dynamically. We introduce dense time in two different ways. First, we consider that each token in each process carries a real valued clock. We prove that this model can faithfully simulate Turing-complete formalisms and, in particular, safety properties are undecidable for them. Second, we consider locally-timed processes, where each process carries a single real valued clock. For them, we prove decidability of safety properties by a non-trivial instantiation of the framework of Well-Structured Transition Systems.


Transition System Dynamic Network Turing Machine Coverability Problem Critical Section 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1-2), 109–127 (2000)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Deneux, J., Mahata, P., Nylén, A.: Forward reachability analysis of timed Petri nets. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 343–362. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Abdulla, P.A., Jonsson, B.: Verifying networks of timed processes (Extended abstract). In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 298–312. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. 4.
    Abdulla, P.A., Mahata, P., Mayr, R.: Dense-timed Petri nets: Checking zenoness, token liveness and boundedness. Logical Methods in Computer Science 3(1) (2007)Google Scholar
  5. 5.
    Abdulla, P.A., Nylén, A.: Timed Petri Nets and BQOs. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53–70. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 162–177. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  7. 7.
    Bashkin, V.A., Lomazova, I.A., Novikova, Y.A.: Timed resource driven automata nets for distributed real-time systems modelling. In: Malyshkin, V. (ed.) PaCT 2013. LNCS, vol. 7979, pp. 13–25. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  8. 8.
    Boyer, M., Roux, O.H.: On the compared expressiveness of arc, place and transition time Petri nets. Fundam. Inform. 88(3), 225–249 (2008)MathSciNetzbMATHGoogle Scholar
  9. 9.
    de Frutos Escrig, D., Ruiz, V.V., Marroquín Alonso, O.: Decidability of properties of timed-arc Petri nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 187–206. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  10. 10.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Geeraerts, G., Heussner, A., Praveen, M., Raskin, J.-F.: ω-petri nets. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 49–69. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  12. 12.
    Haddad, S., Schmitz, S., Schnoebelen, P.: The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In: LICS, pp. 355–364. IEEE (2012)Google Scholar
  13. 13.
    Higman, G.: Ordering by Divisibility in Abstract Algebras. Proc. London Math. Soc. s3-2(1), 326–336 (1952)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Kleijn, J., Koutny, M.: Localities in systems with a/sync communication. Theoretical Computer Science 429, 185 (2012)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Lazic, R., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Inform. 88(3), 251–274 (2008)MathSciNetzbMATHGoogle Scholar
  16. 16.
    Martos-Salgado, M., Rosa-Velardo, F.: Dynamic networks of timed Petri nets. Technical Report 9/13, DSIC Universidad Complutense de Madrid (2013),
  17. 17.
    Martos-Salgado, M., Rosa-Velardo, F.: Expressiveness of dynamic networks of timed petri nets. In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 516–527. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  18. 18.
    Merlin, P., Farber, D.: Recoverability of communication protocols–implications of a theoretical study. IEEE Transactions on Comm. 24(9), 1036–1043 (1976)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Pezzè, M.: Time Petri nets. In: Proceedings of the Multi-Workshop on Formal Methods in Performance Evaluation and Applications (1999)Google Scholar
  20. 20.
    Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. Technical report, Cambridge, MA, USA (1974)Google Scholar
  21. 21.
    Razouk, R.R., Phelps, C.V.: Performance analysis using timed Petri nets. In: Yemini, Y., Strom, R.E., Yemini, S. (eds.) PSTV, pp. 561–576. North-Holland (1984)Google Scholar
  22. 22.
    Rosa-Velardo, F., de Frutos-Escrig, D.: Name creation vs. replication in Petri net systems. Fundam. Inform. 88(3), 329–356 (2008)MathSciNetzbMATHGoogle Scholar
  23. 23.
    Rosa-Velardo, F., de Frutos-Escrig, D.: Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci. 412(34), 4439–4451 (2011)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • María Martos-Salgado
    • 1
  • Fernando Rosa-Velardo
    • 1
  1. 1.Sistemas Informáticos y ComputaciónUniversidad Complutense de MadridSpain

Personalised recommendations