Decidability Problems in Petri Nets with Names and Replication

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

Abstrakty

EN

In this paper we study decidability of several extensions of P/T nets with name creation and/or replication. In particular, we study how to restrict the models of RN systems (P/T nets extended with replication, for which reachability is undecidable) and í-RN systems (RN extendedwith name creation, which are Turing-complete, so that coverability is undecidable), in order to obtain decidability of reachability and coverability, respectively. We prove that if we forbid synchronizations between the different components in a RN system, then reachability is still decidable. Similarly, if we forbid name communication between the different components in a &nuRN system, or restrict communication so that it is allowed only for a given finite set of names, we obtain decidability of coverability. Finally, we consider a polyadic version of ν-PN (P/T nets extended with name creation), that we call pν-PN, in which tokens are tuples of names. We prove that pν-PN are Turing complete, and discuss how the results obtained for ν-RN systems can be translated to them.

Słowa kluczowe

EN

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

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 105, nr 3
• Strony: 291--317
• Opis fizyczny: Bibliogr. 35 poz., wykr.

Twórcy

autor

Rosa-Velardo F.

autor

Frutos-Escrig D. de

• Facultad de Informatica. C\Prof. José Garcýa Santesmases, s/n - 28040 Madrid, Spain,

Bibliografia

• [1] P. A. Abdulla, and B. Jonsson. Verifying Programs with Unreliable Channels. Information and Computation, 127(2):91-101, 1996.
• [2] P. A. Abdulla, K. Cerans, B. Jonsson, and Y. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160:109-127. Academic Press Inc., 2000.
• [3] P. A. Abdulla, G. Delzanno, and L. Van Begin. Comparing the Expressive Power ofWell-Structured Transition Systems. 21st Int. Workshop on Computer Science Logic. Lecture Notes in Computer Science vol. 4646, pp. 99-114. Springer, 2007.
• [4] A. Bouajjani,M.Müller, and T. Touili. Regular symbolic analysis of dynamic networks of pushdown systems. In Proc. of CONCUR'05, LNCS vol. 3653, pp. 473-487. Springer, 2005.
• [5] D. Dahmani, J-M. Ilié, and M. Boukala. Reachability analysis for Recursive Petri Nets with shared places. Int. Workshop on Abstractions for Petri Nets and Other Models of Concurrency, APNOC'09.
• [6] G. Delzanno, J.-F. Raskin, and L. Van Begin. Towards the automated verification of multithreaded java programs. In TACAS 2007, LNCS. vol. 2280, pp. 173-187. Springer, 2002.
• [7] G. Decker, and M. Weske. Instance Isolation Analysis for Service-Oriented Architectures. In Proceedings of the 2008 IEEE International Conference on Services (SCC'08), pp. 249-256. IEE Computer Society, 2008.
• [8] 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. Electronic Notes in Theoretical Computer Science vol. 76. Elsevier, 2002.
• [9] R. Dietze, M. Kudlek, and O. Kummer. Decidability Problems of a Basic Class of Object Nets. Fundamenta Informaticae 79(2007) 295-302. IOS Press.
• [10] C. Dufourd, A. Finkel, and Ph. Schnoebelen. Reset Nets Between Decidability and Undecidability. 25th Int. Automata, Languages and Programming Colloquium, ICALP'98. LNCS vol. 1443. Springer (1998) 103-115.
• [11] J. Esparza andM. Nielsen. Decidability issues for Petri Nets-a survey. Bulletin of EATCS 52:244-262(1994).
• [12] J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In Proc. of LICS'99, pp. 352-359. IEEE Computer Society, 1999.
• [13] A. Finkel, and P. Schnoebelen. Well-Structured Transition Systems Everywhere! Theoretical Computer Science 256(1-2):63-92 (2001).
• [14] G. Geeraerts, J-F. Raskin, and L. Van Begin. Well-structured languages. Acta Informatica 44(3-4): 249-288 (2007)
• [15] A. Gordon. Notes on Nominal Calculi for Security and Mobility. Foundations of Security Analysis and Design, FOSAD'00. Lecture Notes in Computer Science vol. 2171, pp. 262-330. Springer, 2001.
• [16] S. Haddad, and D. Poitrenaud. Recursive Petri Nets. Acta Informatica 44(7-8):463-508, 2007.
• [17] S. Haddad, and D. Poitrenaud. Modelling and Analyzing Systems with Recursive Petri Nets. Proceedings of the 5thWorkshop on Discrete Event Systems,WODES'00, pp. 449-458.Kluwer Academic Publishers, 2000.
• [18] K.M. van Hee, N. Sidorova, M. Voorhoeve, and J.M. van derWer. Generation of Database Transactions with Petri Nets. Fundamenta Informaticae 93(1-3):171-184 (2009)
• [19] M. Köhler, and H. Rölke. Properties of Object Petri Nets. 25th Int. Conf. on Petri Nets, ICATPN'04. LNCS vol. 3099, pp. 278-297. Springer, 2004.
• [20] M. Köhler. Reachable markings of object Petri nets. Fundamenta Informaticae 79(3-4):401-413 (2007)
• [21] M. Köhler, and F. Heitmann. On the expressiveness of communication channels for object nets. Fundamenta Informaticae 93(13):205-219 (2009)
• [22] O. Kummer. Undecidability in object-oriented Petri nets. Petri Net Newsletter, 59:18-23, 2000.
• [23] O. Kummer, F. Wienberg, M. Duvigneau, J. Schumacher, M. Köhler, D. Moldt, H. Rölke, and R. Valk. An Extensible Editor and Simulation Engine for Petri Nets: Renew. In 25th Int. Conf. on Petri Nets, ICATPN'04. LNCS vol. 3099, pp. 484-493. Springer, 2004.
• [24] R. Lazic, T.C. Newcomb, J. Ouaknine, A.W. Roscoe, and J. Worrell. Nets with Tokens Which Carry Data. Fundamenta Informaticae 88(3):251-274. IOS Press, 2008.
• [25] I. Lomazova. Nested Petri nets - a formalism for specification and verification of multi-agent distributed systems. Fundamenta Informaticae 43(1-4):195-214. IOS Press, 2000.
• [26] I. Lomazova, and Ph. Schnoebelen. Some Decidability Results for Nested Petri Nets. 3rd Int. Andrei Ershov Memorial Conf. on Perspectives of System Informatics, PSI'99. LNCS vol.1755, pp. 208-220. Springer,2000.
• [27] R. Meyer. On Boundedness in depth in the π-Calculus. In IFIP Int. Federation for Information Processing, Volume 273; Fifth IFIP Int. Conference on Theoretical Computer Science, pp 477-489. Springer, 2008.
• [28] R.M. Needham. Names.Distributed Systems, pp. 89-101. Addison-Wesley, 1989.
• [29] F. Rosa-Velardo, D. de 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 180(1):77-94. Elsevier, 2007.
• [30] F. Rosa-Velardo, and D. de 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, ATPN'07, LNCS vol. 4546, pp. 402-422. Springer, 2007.
• [31] F. Rosa-Velardo, and D. de Frutos-Escrig. Name Creation vs. Replication in Petri Net Systems. Fundamenta Informaticae 88(3):329-356. Special issue on Selected Papers from ATPN'07. IOS Press, 2008.
• [32] F. Rosa-Velardo, and D. de Frutos-Escrig. Decidability results for restricted models of Petri nets with name creation and replication. 30th Int. Conf. on Applications and Theory of Petri Nets and other models of concurrency, ATPN'09, LNCS vol. 5606, pp. 63-82. Springer, 2009.
• [33] R. Valk. Nets in Computer Organisation. Advances in Petri Nets, LNCS vol. 255, pp. 218-233. Springer, 1987.
• [34] R. Valk. Petri Nets as Dynamical Objects. 16th Int. Conf. on Application and Theory of Petri Nets.Workshop proceedings, 1995.
• [35] R. Valk. Petri Nets as Token Objects - An Introduction to Elementary Object Nets. 19th Int. Conf. on Applications and Theory of Petri Nets, ICATPN'98, LNCS vol. 1420, pp. 1-25. Springer, 1998.