Name Creation vs. Replication in Petri Net Systems

• Autorzy: Rosa-Velardo F. , de Frutos-Escrig D.
• Języki publikacji: EN

Abstrakty

EN

We study the relationship between name creation and replication in a setting of infinitestate 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.

Słowa kluczowe

EN

Petri net; pure names; infinite state systems; decidability; multithreading; security; choreography

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 88, nr 3
• Strony: 329--356
• Opis fizyczny: bibliogr. 28 poz., wykr.

Twórcy

autor

Rosa-Velardo F.

autor

de Frutos-Escrig D.

• Facultad de Ciencias Matem´aticas. Plaza de las Ciencias, 3-28040 Madrid, Spain,

Bibliografia

• [1] P.A. Abdulla, G. Delzanno, and L. Van Begin. Comparing the Expressive Power of Well-Structured Transition Systems. 21st Int.Workshop on Computer Science Logic, CSL'07, LNCS vol. 4646, pp. 99-114. Springer, 2007.
• [2] P.A. Abdulla, and G. Delzanno. On the coverability problem for constrained multiset rewriting. In: AVIS 2006, an ETAPS Workshop, 2006.
• [3] T. Ball, S. Chaki, and S.K. Rajamani. Parameterized Verification of Multithreaded Software Libraries. 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'01. LNCS vol. 2031, pp. 158-173. Springer, 2001.
• [4] A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'03. ACM SIGPLAN 38(1):62-73. ACM, 2003.
• [5] A. Bouajjani, J. Esparza, and T. Touili. Reachability Analysis of Synchronized PA Systems. 6th Int. Workshop on Verification of Infinite-State Systems, INFINITY'04. ENTCS vol. 138(2), pp. 153-178. Elsevier, 2005.
• [6] N. Busi, and G. Zavattaro. Deciding Reachability in Mobile Ambients. 14th European Symposium on Programming Languages and Systems, ETAPS'05. LNCS vol. 3444, pp. 248-262. Springer, 2005.
• [7] L. Cardelli, and A.D. Gordon. Mobile Ambients. 1st Int. Conf. on Foundations of Software Sciences and Computation Structures, FOSSACS'98. LNCS vol. 1387, pp. 140-155. Springer, 1998.
• [8] L. Cardelli, G. Ghelli, and A.D. Gordon. Types for the Ambient Calculus. Information and Computation 177(2): 160-194 (2002).
• [9] G. Cécé, A. Finkel, and S.P. Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation 124(1):20-31, 1996.
• [10] G. Delzanno. An overview of MSR(C): A CLP-based Framework for the Symbolic Verification of Parameterized Concurrent Systems. 11th Int. Workshop on Functional and Logic Programming, WFLP'02. ENTCS vol. 76. Elsevier, 2002.
• [11] G. Delzanno. Constraint-based Automatic Verification of Abstract Models of Multitreaded Programs. To appear in the Journal of Theory and Practice of Logic Programming, 2006.
• [12] N.A. Durgin, P.D. Lincoln, J.C. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. Proc. Workshop on Formal Methods and Security Protocols (FMSP'99).
• [13] A.Finkel, and P.Schnoebelen. Well-Structured Transition Systems Everywhere! Theoretical Computer Science 256(1-2):63-92 (2001).
• [14] D. Frutos-Escrig, O.Marroquin-Alonso and F. Rosa-Velardo. Ubiquitous Systems and Petri Nets. Ubiquitous Web Systems and Intelligence, LNCS vol.3841. Springer, 2005.
• [15] A. Gordon. Notes on Nominal Calculi for Security and Mobility. Foundations of Security Analysis and Design, FOSAD'00. LNCS vol. 2171, pp. 262-330. Springer, 2001.
• [16] O. Kummer. Undecidability in object-oriented Petri nets. Petri Net Newsletter, 59:18-23, 2000.
• [17] R. Lazic, T.C. Newcomb, J. Ouaknine, A.W. Roscoe and J. Worrell. Nets with Tokens Which Carry Data. 28th Int. Conf. on Applications and Theory of Petri Nets and other models of concurrency, ICATPN'07, LNCS vol. 4546, pp. 301-320. Springer, 2007.
• [18] R.Milner, J. Parrow, and D.Walker. A Calculus ofMobile Processes, I. Information and Computation 100(1): 1-40 (1992).
• [19] R.M. Needham. Names. Distributed systems, ed. S. Mullender, 2nd ed., Reading, MA: Addison-Wesley, 1993, 315-326 and 531- 541.
• [20] F. Nielson, R.R. Hansen, and H.R. Nielson. Abstract interpretation of mobile ambients. Sci. Comput. Program. 47(2-3): 145-175 (2003).
• [21] G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2): 416-430 (2000).
• [22] M. Rinard. Analysis of multithreaded programs. 8th Static Analysis Symposium, SAS'01. LNCS 2126, pp. 1-19. Springer, 2001.
• [23] F. Rosa-Velardo, D. Frutos-Escrig, and O. Marroqu´ın-Alonso. Mobile Synchronizing Petri Nets: a choreographic approach for coordination in Ubiquitous Systems. 1st Int. Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, MTCoord'05. ENTCS vol.150(1). Elsevier, 2006.
• [24] F. Rosa-Velardo, D. Frutos-Escrig, and O.Marroqu´ın-Alonso. On the expressiveness of Mobile Synchronizing Petri Nets. 3rd Int. Workshop on Security Issues in Concurrency, SecCo'05. ENTCS vol. 180(1), pp. 77-94. Elsevier, 2007.
• [25] F. Rosa-Velardo. Coding Mobile Synchronizing Petri Nets into Rewriting Logic. 7th Int. Workshop on Rulebased Programming, RULE'06. ENTCS vol. 174(1), pp. 83-98. Elsevier 2007.
• [26] F. Rosa-Velardo, D. Frutos-Escrig, O. Marroqu´ın-Alonso. Replicated Ubiquitous Nets. UbiquitousWeb Systems and Intelligence, LNCS vol. 3983. Springer, 2006.
• [27] F. Rosa-Velardo, D. Frutos-Escrig. Name creation vs. Replication in Petri Net Systems. 28th int. Conf. On Applications and Theory of Petri Nets and other models of concurrency, ICATPN'07, LNCS vol. 4546, pp. 402-422. Springer, 2007.
• [28] P. Zimmer. On the Expressiveness of Pure Mobile Ambients. 7th Int.Workshop on Expressiveness in Concurrency, EXPRESS'00, ENTCS vol. 39(1). Elsevier, 2003.