Affiliations: Department of Computer Science, University of Warwick,
UK | Computing Laboratory, University of Oxford, UK
Note: [] Address for correspondence: Department of Computer Science,
University of Warwick, Coventry CV4 7AL, UK
Abstract: 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.
Keywords: Petri nets, infinite-state systems, program verification, computational complexity
