We study data nets, a generalisation of Petri nets in which tokens
carry data from linearly-ordered 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.
Proceedings of ICATPN 07, LNCS 4546, 2007. 20 pages.
PostScript /
PDF
© 2007
Springer-Verlag.