Nets with Tokens which Carry Data

• Autorzy: Lazić R. , Newcomb T. , Ouaknine J. , Roscoe A.W. , Worrell J.
• Języki publikacji: EN

Abstrakty

EN

We study data nets, a generalisation of Petri nets in which tokens carry data from linearlyordered infinite domains and in which whole-place operations such as resets and transfers are possible. Data nets subsume several known classes of infinite-state systems, including multiset rewriting systems and polymorphic systems with arrays. We show that coverability and termination are decidable for arbitrary data nets, and that boundedness is decidable for data nets in which whole-place operations are restricted to transfers. By providing an encoding of lossy channel systems into data nets without whole-place operations, we establish that coverability, termination and boundedness for the latter class have non-primitive recursive complexity. The main result of the paper is that, even for unordered data domains (i.e., with only the equality predicate), each of the three verification problems for data nets without whole-place operations has non-elementary complexity.

Słowa kluczowe

EN

Petri net; infinite-state systems; program verification; computational complexity

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 88, nr 3
• Strony: 251--274
• Opis fizyczny: bibliogr. 24 poz.

Twórcy

autor

Lazić R.

autor

Newcomb T.

autor

Ouaknine J.

autor

Roscoe A.W.

autor

Worrell J.

• Department of Computer Science, University of Warwick, Coventry CV4 7AL, UK

Bibliografia

• [1] Abdulla, P. A., Delzanno, G.: Constrained Multiset Rewriting, AVIS '06, ENTCS, to appear.
• [2] Abdulla, P. A., Jonsson, B.: Verifying Programs with Unreliable Channels, Inf. Comput., 127(2), 1996, 91-101.
• [3] Abdulla, P. A., Jonsson, B.: Model checking of systems with many identical timed processes, Theor. Comput. Sci., 290(1), 2003, 241-264.
• [4] Abdulla, P. A., Nylén, A.: Timed Petri Nets and BQOs, ICATPN, number 2075 in LNCS, Springer, 2001.
• [5] Bozzano, M., Delzanno, G.: Automatic Verification of Invalidation-based Protocols, CAV, number 2404 in LNCS, Springer, 2002.
• [6] Bozzano, M., Delzanno, G.: Beyond Parameterized Verification, TACAS, number 2280 in LNCS, Springer, 2002.
• [7] Delzanno, G.: An Assertional Language for Systems Parametric in Several Dimensions, VEPAS, number 50 in ENTCS, 2001.
• [8] Delzanno, G.: Constraint Multiset Rewriting, Technical Report DISI-TR-05-08, Universit`a di Genova, 2005, Extends [7, 6, 5].
• [9] Dufourd, C., Finkel, A., Schnoebelen, P.: Reset Nets Between Decidability and Undecidability, ICALP, number 1443 in LNCS, Springer, 1998.
• [10] Esparza, J., Nielsen, M.: Decidability Issues for Petri Nets - a survey, Bull. EATCS, 52, 1994, 244-262.
• [11] Finkel, A., McKenzie, P., Picaronny, C.: A well-structured framework for analysing Petri net extensions, Inf. Comput., 195(1-2), 2004, 1-29.
• [12] Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!, Theor. Comput. Sci., 256(1-2), 2001, 63-92.
• [13] Girault, C., Valk, R., Eds.: Petri Nets for Systems Engineering, Springer, 2003.
• [14] Higman, G.: Ordering by divisibility in abstract algebras, Proc. London Math. Soc. (3), 2(7), 1952, 326-336.
• [15] Lazić, R.: Decidability of Reachability for Polymorphic Systems with Arrays: A Complete Classification, Infinity '04, number 138 in ENTCS, 2005.
• [16] Lazić, R., Newcomb, T. C., Roscoe, A. W.: Polymorphic Systems with Arrays, 2-Counter Machines and Multiset Rewriting, Infinity '04, number 138 in ENTCS, 2005.
• [17] Lipton, R. J.: The Reachability Problem Requires Exponential Space, Technical Report 62, Yale University, 1976.
• [18] Meyer, A. R.: Weak monadic second-order theory of successor is not elementary-recursive, Logic colloquium '72-73, number 453 in Lect. Not. Math., Springer, 1975.
• [19] Odifreddi, P.: Classical Recursion Theory II, Elsevier, 1999.
• [20] Rackoff, C.: The Covering and Boundedness Problems for Vector Addition Systems, Theor. Comput. Sci., 6,1978, 223-231.
• [21] Reisig, W.: Petri Nets: An Introduction, Springer, 1985.
• [22] Rosa Velardo, F., de Frutos Escrig, D., Marroqu´ın Alonso, O.: On the expressiveness of Mobile Synchronizing Petri nets, SecCo '05, number 180 in ENTCS, 2007.
• [23] Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity, Inf. Proc. Lett., 83(5), 2002, 251-261.
• [24] Valk, R., Jantzen, M.: The Residue of Vector Sets with Applications to Decidability Problems in Petri Nets, Acta Inf., 21, 1985, 643-674.