Skip to main content
SpringerLink
Log in

Name Creation vs. Replication in Petri Net Systems

  • Conference paper
Petri Nets and Other Models of Concurrency – ICATPN 2007 (ICATPN 2007)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4546))

Included in the following conference series:

Abstract

We study the relationship between name creation and replication in a setting of infinite-state communicating automata. By name creation we mean the capacity of dynamically producing pure names, with no relation between them other than equality or inequality. By replication we understand the ability of systems of creating new parallel identical threads, that can synchronize with each other. We have developed our study in the framework of Petri nets, by considering several extensions of P/T nets. In particular, we prove that in this setting name creation and replication are equivalent, but only when a garbage collection mechanism is added for idle threads. However, when simultaneously considering both extensions the obtained model is, a bit surprisingly, Turing complete and therefore, more expressive than when considered separately.

Work partially supported by the Spanish projects DESAFIOS TIN2006-15660-C02-02, WEST TIN2006-15578-C02-01 and PROMESAS-CAM S-0505/TIC/0407.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Deneux, J., Mahata, P., Nylén, A.: Forward Reachability Analysis of Timed Petri Nets. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 343–362. Springer, Heidelberg (2004)

    Google Scholar 

  2. Ball, T., Chaki, S., Rajamani, S.K.: Parameterized Verification of Multithreaded Software Libraries. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 158–173. Springer, Heidelberg (2001)

    Google Scholar 

  3. Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’03. ACM SIGPLAN, vol. 38(1), pp. 62-73. ACM (2003)

    Google Scholar 

  4. Bouajjani, A., Esparza, J., Touili, T.: Reachability Analysis of Synchronized PA Systems. In: 6th Int. Workshop on Verification of Infinite-State Systems, INFINITY’04. ENTCS vol. 138(2), pp. 153-178. Elsevier, Amsterdam (2005)

    Google Scholar 

  5. Busi, N., Zavattaro, G.: Deciding Reachability in Mobile Ambients. In: Sagiv, M. (ed.) ESTAPS’05. LNCS, vol. 3444, pp. 248–262. Springer, Heidelberg (2005)

    Google Scholar 

  6. Cardelli, L., Gordon, A.D.: Mobile Ambients. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  7. Cardelli, L., Ghelli, G., Gordon, A.D.: Types for the Ambient Calculus. Information and Computation 177(2), 160–194 (2002)

    MATH  MathSciNet  Google Scholar 

  8. Delzanno, G.: An overview of MSR(C): A CLP-based Framework for the Symbolic Verification of Parameterized Concurrent Systems. In: 11th Int. Workshop on Functional and Logic Programming, WFLP’02. ENTCS, vol. 76, Elsevier, Amsterdam (2002)

    Google Scholar 

  9. Delzanno, G.: Constraint-based Automatic Verification of Abstract Models of Multitreaded Programs. To appear in the Journal of Theory and Practice of Logic Programming (2006)

    Google Scholar 

  10. Durgin, N.A., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: Undecidability of bounded security protocols. In: Proc. Workshop on Formal Methods and Security Protocols (FMSP’99)

    Google Scholar 

  11. Finkel, A., Schnoebelen, P.: Well-Structured Transition Systems Everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  12. Frutos-Escrig, D., Marroquín-Alonso, O., Rosa-Velardo, F.: Ubiquitous Systems and Petri Nets. In: Zhou, X., Li, J., Shen, H.T., Kitsuregawa, M., Zhang, Y. (eds.) APWeb 2006. LNCS, vol. 3841, Springer, Heidelberg (2005)

    Google Scholar 

  13. Gordon, A.: Notes on Nominal Calculi for Security and Mobility. In: Focardi, R., Gorrieri, R. (eds.) Foundations of Security Analysis and Design (FOSAD’00). LNCS, vol. 2171, pp. 262–330. Springer, Heidelberg (2001)

    Google Scholar 

  14. Kummer, O.: Undecidability in object-oriented Petri nets. Petri Net Newsletter 59, 18–23 (2000)

    Google Scholar 

  15. Lazic, R.: Decidability of Reachability for Polymorphic Systems with Arrays: A Complete Classification. ENTCS 138(3), 3–19 (2005)

    MathSciNet  Google Scholar 

  16. Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, I. Information and Computation 100(1), 1–40 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  17. Nielson, F., Hansen, R.R., Nielson, H.R.: Abstract interpretation of mobile ambients. Sci. Comput. Program 47(2-3), 145–175 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  18. Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)

    Article  Google Scholar 

  19. Ramanujam, R., Suresh, S.P.: Decidability of context-explicit security protocols. Journal of Computer Security 13(1), 135–165 (2005)

    Google Scholar 

  20. Ramanujam, R., Suresh, S.P.: Tagging makes secrecy decidable with unbounded nonces as well. In: Pandya, P.K., Radhakrishnan, J. (eds.) FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 2914, pp. 363–374. Springer, Heidelberg (2003)

    Google Scholar 

  21. Rinard, M.: Analysis of multithreaded programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 1–19. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. Rosa Velardo, F., Segura Díaz, C., de Frutos Escrig, D.: Tagged systems: a framework for the specification of history dependent properties. Fourth Spanish Conference on Programming and Computer Languages, PROLE’04. ENTCS vol. 137(1) (2005)

    Google Scholar 

  23. Rosa-Velardo, F., Frutos-Escrig, D., Marroquín-Alonso, O.: Mobile Synchronizing Petri Nets: a choreographic approach for coordination in Ubiquitous Systems. In: 1st Int. Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, MTCoord’05. ENTCS, vol. 150(1), Elsevier, Amsterdam (2006)

    Google Scholar 

  24. Rosa-Velardo, F., Frutos-Escrig, D., Marroquín-Alonso, O.: On the expressiveness of Mobile Synchronizing Petri Nets. In: 3rd Int. Workshop on Security Issues in Concurrency, SecCo’05. ENTCS (to appear)

    Google Scholar 

  25. Rosa-Velardo, F.: Coding Mobile Synchronizing Petri Nets into Rewriting Logic. 7th Int. Workshop on Rule-based Programming, RULE’06. ENTCS (to appear)

    Google Scholar 

  26. Rosa-Velardo, F., Frutos-Escrig, D., Marroquín-Alonso, O.: Replicated Ubiquitous Nets. In: Gavrilova, M., Gervasi, O., Kumar, V., Tan, C.J.K., Taniar, D., Laganà, A., Mun, Y., Choo, H. (eds.) ICCSA 2006. LNCS, vol. 3983, Springer, Heidelberg (2006)

    Google Scholar 

  27. Zimmer, P.: On the Expressiveness of Pure Mobile Ambients. In: 7th Int. Workshop on Expressiveness in Concurrency, EXPRESS’00. ENTCS, vol. 39(1), Elsevier, Amsterdam (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dpto. de Sistemas Informáticos y Programación, Universidad Complutense de Madrid,  

    Fernando Rosa-Velardo & David de Frutos-Escrig

Authors
  1. Fernando Rosa-Velardo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David de Frutos-Escrig
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jetty Kleijn Alex Yakovlev

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

Rosa-Velardo, F., de Frutos-Escrig, D. (2007). Name Creation vs. Replication in Petri Net Systems. In: Kleijn, J., Yakovlev, A. (eds) Petri Nets and Other Models of Concurrency – ICATPN 2007. ICATPN 2007. Lecture Notes in Computer Science, vol 4546. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73094-1_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-73094-1_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-73093-4

  • Online ISBN: 978-3-540-73094-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation