Decidability and complexity of Petri nets with unordered data (Q554219): Difference between revisions

P/T-nets are a fundamental class of Petri nets (models of concurrent and distributed computing systems) for which a number of key behavioural properties, including reachability and boundedness, are decidable. Reachability is concerned with establishing whether a given marking (or state) can be derived from the initial marking of a P/T-net. Boundedness is concerned with establishing whether the set of markings which can be derived from the initial marking (i.e. reachable markings) is finite. Extending P/T-nets with additional modelling features, such as inhibitor arcs testing for the absence of tokens in places, often renders reachability and/or boundedness undecidable. The paper is concerned with an extension of P/T-nets, called \(\nu\)-PN, in which tokens (resources) have identities that can be compared for equality, and in this way they can influence the dynamic behaviour of a net. New names can be created dynamically, and \(\nu\)-PN can be used to model systems in different application areas, such as mobility and security. The paper proves several decidability and undecidability results for \(\nu\)-PN. The first is a simple proof of the undecidability of reachability which is obtained by reducing reachability in P/T-nets with inhibitor arcs to reachability in \(\nu\)-PN. This also means that, unlike P/T-nets, \(\nu\)-PN are Turing powerful. The paper then encodes \(\nu\)-PN in terms of Petri data nets for which coverability, termination (concerned with establishing whether there exists an infinite run) and boundedness are decidable properties. Moreover, Ackermann-hardness results for all three decidable decision problems are obtained. Unboundedness in a \(\nu\)-PN can be due to an unbounded number of different names in reachable markings (width-unboundedness), or due to an unbounded number of instances of an individual name in reachable markings (depth-unboundedness). Width-boundedness was known to be decidable, and the paper proves that its complexity is non-primitive recursive. It is also shown that depth-boundedness is undecidable. Finally, the paper proves that the corresponding `place versions' of all the boundedness problems (for example, the place version of boundedness is concerned with establishing whether a given place can hold an unbounded number of tokens in reachable markings) are undecidable for \(\nu\)-PN. These results carry over to Petri data nets.