Name Creation vs. Replication in Petri Net Systems

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