Accelerations for the Coverability Set of Petri Nets with Names

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

Abstrakty

EN

Pure names are identifiers with no relation between them, except equality and inequality. In previous works we have extended P/T nets with the capability of creating and managing pure names, obtaining -PNs and proved that they are strictly well structured (WSTS), so that coverability and boundedness are decidable. Here we use the framework recently developed by Finkel and Goubault-Larrecq for forward analysis for WSTS, in the case of -PNs, to compute the cover, that gives a good over approximation of the set of reachable markings. We prove that the least complete domain containing the set of markings is effectively representable. Moreover, we prove that in the completion we can compute least upper bounds of simple loops. Therefore, a forward Karp-Miller procedure that computes the cover is applicable. However, we prove that in general the cover is not computable, so that the procedure is non-terminating in general. As a corollary, we obtain the analogous result for Transfer Data nets and Data Nets. Finally, we show that a slight modification of the forward analysis yields decidability of a weak form of boundedness called width-boundedness, and identify a subclass of -PN that we call dw-bounded v-PN, for which the cover is computable.

Słowa kluczowe

EN

Petri net; pure names; infinite state systems; decidability; well structured transition system; forward analysis; accelerations

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 113, nr 3/4
• Strony: 313--341
• Opis fizyczny: Bibliogr. 24 poz.

Twórcy

autor

Rosa-Velardo F.

autor

Martos-Salgado M.

autor

Frutos-Escrig D. de

• Facultad de Informatica. C\Prof. Jose Garcia Santesmases, s/n - 28040 Madrid, Spain,

Bibliografia

• [1] P.A. Abdulla, K. Cerans, B. Jonsson, and Y. Tsay. Algorithmic Analysis of Programs with Well Quasiordered Domains. Inf. and Comp. 160(1-2):109-127 (2000)
• [2] P.A. Abdulla, and A. Nylén. Better is Better than Well: On Efficient Verification of Infinite-State Systems. 15th Annual IEEE Symp. on Logic in Computer Science, LICS'00 (2000) 132-140.
• [3] P.A. Abdulla, A. Collomb-Annichini, A. Bouajjani, and B. Jonsson. Using Forward Reachability Analysis for Verification of Lossy Channel Systems. Formal Methods in System Design 25(1): 39-65 (2004)
• [4] S. Bardin, A. Finkel, J. Leroux, and Ph. Schnoebelen. Flat Acceleration in Symbolic Model Checking. 3rd Int. Symposium on Automated Technology for Verification and Analysis, ATVA'05. LNCS vol. 3707. Springer (2005) 474-488.
• [5] R. Dietze,M. Kudlek, and O. Kummer. Decidability Problems of a Basic Class of Object Nets. Fundamenta Informaticae 79. IOS Press (2007) 295-302.
• [6] G. Decker, and M. Weske. Instance Isolation Analysis for Service-Oriented Architectures. Int. Conference on Services Computing, SCC'08, IEEE Computer Society (2008) 249-256.
• [7] 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.
• [8] J. Esparza and M. Nielsen. Decidability issues for Petri Nets - a survey. Bulletin of the EATCS 52:244-262 (1994).
• [9] A. Finkel, and Ph. Schnoebelen. Fundamental Structures in Well-Structured Infinite Transition Systems. In 3rd Latin American Symposium on Theoretical Informatics, LATIN'98. LNCS vol. 1380. Springer (1998) 102-118.
• [10] A. Finkel and P. Schnoebelen. Well-Structured Transition Systems Everywhere! Theoretical Computer Science 256(1-2):63-92 (2001)
• [11] A. Finkel and J.Goubault-Larrecq. Forward analysis forWSTS, Part I: Completions. In Proceedings of the 26th International Symposium on Theoretical Aspects of Computer Science, STACS'09 (2009) 433-444.
• [12] A. Finkel and J.Goubault-Larrecq. Forward analysis for WSTS, Part II: Complete WSTS. In 36th International Colloquium on Automata, Languages and Programming, ICALP'09. LNCS vol. 5556. Springer (2009) 188-199.
• [13] G. Geeraerts, J.-F. Raskin, and L. van Begin. Expand, enlarge and check: New algorithms for the coverability problem of WSTS. J.Comp. Sys. Sci.,72(1):180-203 (2006)
• [14] A. Gordon. Notes on Nominal Calculi for Security and Mobility. Foundations of Security Analysis and Design, FOSAD'00. LNCS vol. 2171. Springer (2001) 262-330.
• [15] J. Goubault-Larrecq. On Noetherian spaces. 22nd IEEE Symposium on Logic in Computer Science, LICS'07. IEEE Computer Society (2007) 453-462.
• [16] P. Janˇcar. A note on well quasi-orderings for powersets. Information Processing Letters 72(5-6):155-160 (1999)
• [17] R. Lazic, T. Newcomb, J. Ouaknine, A. W. Roscoe, and J. Worrell. Nets with Tokens which Carry Data. Fundamenta Informaticae 88(3):251-274. IOS Press (2008)
• [18] E.C. Milner. Basic WQO- and BQO-theory. In I. Rival (ed.). Graphs and Order. The Role of Graphs in the Theory of Ordered Sets and Its Applications. D. Reidel Publishing Co.. pp. 487-502.
• [19] F. Rosa-Velardo, D. de Frutos-Escrig, and O. Marroqu´ın-Alonso. On the expressiveness of Mobile Synchronizing Petri Nets. In 3rd InternationalWorkshop on Security Issues in Concurrency, SecCo'05. ENTCS 180(1). Elsevier (2007) 77-94.
• [20] F. Rosa-Velardo and D. de Frutos-Escrig. Name creation vs. replication in Petri Net systems. Fundamenta Informaticae 88(3). IOS Press (2008) 329-356.
• [21] F. Rosa-Velardo and D. de Frutos-Escrig. Name creation vs. replication in Petri Net systems. ATPN'07. LNCS vol. 4546. Springer (2007) 402-422.
• [22] F. Rosa-Velardo and D. de Frutos-Escrig. Forward analysis for Petri Nets with Name Creation. PETRI NETS 2010. LNCS vol. 6128. Springer (2010) 185-205.
• [23] F. Rosa-Velardo and D. de Frutos-Escrig. Decidability and Complexity of Petri Nets with Unordered Data. Theoretical Computer Science 412(34): 4439-4451 (2011).
• [24] Ph. Schnoebelen. Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5) (2002) 251-261.