Decidability and complexity of Petri nets with unordered data

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

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.

Recommendations

Cites work

Cited in

(36)

This page was built for publication: Decidability and complexity of Petri nets with unordered data

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q554219)