Source-linked AI summary
The Complexity of Coverability-Like Problems in Elementary Object Systems: Data-Nets to the Rescue
Francesco Di Cosmo, Soumodev Mal, Tephilla Prince
TL;DR
The complexity of coverability, termination, and boundedness for conservative Elementary Object Systems was unclear. The paper reduces these problems to equivalent problems on data-net models and proves that coverability is F_ω2-complete, while termination and boundedness are non-primitive recursive.
Problem
The complexity of coverability, termination, and boundedness for conservative Elementary Object Systems was unclear.
Method
The paper inter-reduces conservative Elementary Object Systems and νPN-based data nets through channel-νPNs, using polynomial constructions to capture nesting and data.
Results
F_ω2-completeness holds for cEOS coverability, while cEOS termination and boundedness are non-primitive recursive.
Takeaways & Limitations
The results place conservative nested-net verification within the hierarchy of data nets, specifically between νPNs and Unordered Data Nets.
Takeaways & Limitations
The analysis is restricted to two nesting levels, while formal definitions and corresponding reductions for deeper object-system nesting remain open.
Abstract
from arXiv · showhide
Elementary Object Systems (EOSs) are a model in the nets-within-nets (NWNs) paradigm, where tokens in turn can host standard Petri nets. We study the complexity of coverability-like problems, including termination and boundedness, over EOSs. Since coverability and boundedness are undecidable in general on EOSs, we focus on the relevant fragment of conservative EOSs (cEOSs). Our technique interprets cEOSs into the framework of data nets, whose tokens carry data from an infinite domain, thus bridging the nesting and the data-aware paradigms. Specifically, we show that cEOS coverability-like problems are equivalent to the coverability-like problems over an interesting fragment, called channel-$ν$PNs (c-$ν$PNs), of data nets that extends $ν$PN (featuring globally fresh name creation) with restricted forms of transfers with renaming. c-$ν$PNs remain less expressive than Unordered Data Nets, which feature lossy name creation as well as powerful forms of whole-place operations and broadcasts. These reductions allow us to analyze cEOS coverability taking advantage of known results on data nets. We conclude that the complexity of cEOS coverability is double-Ackermanian, $\mathcal{F}_{ω2}$-complete, while termination and boundedness are non-primitive recursive.
1. Introduction
The paper studies coverability, termination, and boundedness for conservative Elementary Object Systems (cEOSs), where Petri-net tokens can themselves carry Petri nets. Its central approach bridges nesting with data extensions by reducing cEOS problems to νPN-related models, yielding a complexity characterization for coverability and addressing termination and boundedness.
- Motivation: cEOSs are one-level Nets Within Nets models in which tokens carry Petri nets, motivating verification for systems whose agents may suffer token losses.Prior work studied reachability and coverability for EOSs in the NWN paradigm.
- Problem: The paper investigates cEOS coverability, termination, and boundedness, whose relationship and complexity are unclear despite coinciding for ordinary Petri nets.Termination asks whether an infinite run exists, while boundedness asks whether finitely many configurations are reachable from an initial configuration.
- Approach: The central method bridges nesting with data-aware Petri nets, showing that cEOS coverability-like problems match corresponding νPN problems through reductions involving whole-place operations.Nesting is captured using whole-place operations on νPNs, which can be abstracted away for coverability-like problems via a polynomial reduction from cEOS to νPN.
- Contributions: It additionally introduces a novel example showing how cEOS nesting semantics can model real scenarios and addresses termination and boundedness.These contributions complement the coverability result by demonstrating an application of the model and treating the two additional verification problems.
- Contributions: The paper provides a complete proof that cEOS coverability is Fω2-complete, extends the technical development, and systematically analyzes whole-place operations.The revised development also introduces c-νPNs, a νPN form with selected whole-place operations in the style of Unordered Data Nets.
2. Preliminaries
This section defines configuration graphs and the abstract coverability, termination, and boundedness problems, then introduces Petri nets, νPNs, and Elementary Object Systems as the main models. It also records known νPN complexity results used later.
- Configuration graphs: A quasi-ordered normed configuration graph consists of a directed configuration graph equipped with a quasi-order and a natural-valued size norm.Runs are sequences of steps in the graph.
- Configuration-graph problems: The abstract problems ask whether a target is coverable, whether an initial configuration has an infinite run, and whether its reachable set is finite.Coverability requires reaching a configuration above the target in the quasi-order.
- Petri Nets: A Petri net uses finite places and transitions with natural-valued flow, while its configuration graph uses markings, transition firings, component-wise order, and token count as norm.A transition fires when its precondition is bounded by the marking and updates the marking using pre- and postconditions.
- νPN: A νPN extends Petri nets by associating tokens with data values and allowing transitions to test data equality or inequality using standard and fresh variables.Firing consumes and transforms selected tuples according to a mode and adds markings for fresh variables.
- νPN: νPN-coverability is F_ω2-complete, while νPN-termination and νPN-boundedness are non-primitive recursive [15, 16].These results concern the νPN problems defined over configurations ordered by injective component-wise embedding.
- Elementary Object Systems: An Elementary Object System is a Petri net whose tokens are themselves Petri nets, with firings occurring asynchronously in either layer or synchronously in both.The system net types object nets, and nested tokens carry an internal marking.
3. Channel νPN
This section introduces channel-νPNs (c-νPNs), extending νPNs with restricted whole-place transfers that rename tokens. Their semantics serialize standard preconditions, transfers, and postconditions, while channels provide a graphical representation of these operations.
- Definition and motivation: c-νPNs extend νPNs with special transitions performing restricted whole-place transfers with renaming, inspired by UDNs and affine nets.These operations encode nested-paradigm behavior in the data-aware setting.
- Definition and motivation: The transfer function G assigns place-to-place matrices subject to constraints that prevent duplication and restrict each variable’s transfer destinations.Each matrix entry contains at most one transferred token, and non-identity transfers exclude competing destinations for the same source variable.
- Graphical representation: Channels graphically represent transfers as decorated pre- and post-arrows, and a transition is special exactly when it has at least one channel.A channel transfers tokens taken from a precondition tuple to the tuple instantiating the corresponding postcondition variables, with renaming.
- Relationship to Petri nets: Every ordinary Petri net embeds as a c-νPN with identity mappings and no special transitions, preserving the same graphical representation.For each variable, the self-mapping is the identity and all other mappings are zero.
- Operational semantics: Firing a special transition serializes its standard preconditions, transfers, and postconditions, while fresh ν variables create new tuples during the firing.The semantics separately accounts for unaffected tokens, fresh-tuple creation, standard preconditions, transfers, and final postconditions.
4. Phase Encodings
Phase encodings map source configurations injectively to target configurations while representing each source step by a target phase, possibly containing intermediate configurations. Under uniformity, phase-finiteness, and boundedness conditions, these encodings preserve coverability, termination, and boundedness across the relevant configuration-graph families.
- Phase Encodings: A phase encoding injectively maps configurations and requires every source step to correspond to a target phase between the encoded endpoints, while every finite target phase decodes to a source step.Phases may be finite or infinite, and only their start and finish configurations are encoding configurations in the finite case.
- Phase Encodings: For qonCGs, embeddings preserve the configuration order, uniform encodings ensure reachable configurations above encoded ones remain encoded, and phase-finite encodings require all phases to be finite.An f-perfect encoding combines embedding, uniformity, phase-finiteness, and f-boundedness.
- Preservation Results: Uniform phase encodings make coverability equivalent between the source family and its encoded target family.The encoded instance replaces the source system and distinguished configurations with their images under ξ.
- Preservation Results: Phase-finite phase encodings make termination equivalent, while f-bounded phase encodings preserve boundedness when the target configuration graph is finitary.The configuration graphs of νPNs, cEOSs, and c-νPNs are finitary because finitely many tokens permit only finitely many configurations.
5. From νPN to cEOS
The section gives a polynomial phase encoding from arbitrary νPNs to conservative EOSs using two object types, preserving coverability, termination, and boundedness. This reduction transfers νPN lower bounds, making cEOS coverability Fω2-hard and cEOS termination and boundedness non-primitive recursive.
- From νPN to cEOS: The construction uses two object types: ▲ controls event sequences, while ND captures νPN transitions split by variable.For each νPN configuration, tuples are stored as internal markings of ND objects.
- From νPN to cEOS: The configuration encoding is a phase encoding and is f-perfect for some polynomial function f.It is injective, supports adding markings through sim objects, and satisfies the phase-encoding properties.
- From νPN to cEOS: The encoding preserves coverability, termination, and boundedness because its phases are finite and polynomially bounded in length and event effects.Each phase has at most 2 max_t∈T |Var(t)| + 3 steps.
- From νPN to cEOS: A polynomial reduction maps νPN coverability, termination, and boundedness to the corresponding cEOS problems.The encoding of each νPN configuration uses dedicated ND objects in sim and one ▲ token in selectTran.
- From νPN to cEOS: cEOS-coverability is Fω2-hard, while cEOS-termination and cEOS-boundedness are non-primitive recursive, inherited from νPN lower bounds.νPN-coverability is Fω2-complete, and νPN-boundedness and termination are non-primitive recursive.
6. From cEOS to c-νPN
This section gives a polynomial-time construction translating every conservative EOS into a c-νPN that serializes merging, internal firing, and distribution. The encoding is phase-perfect and yields polynomial reductions for coverability, termination, and boundedness.
- Construction: Every cEOS E has a polynomial-time constructible c-νPN W that simulates each synchronous event by serializing merging, internal firing, and distribution.The construction assumes each system-net transition participates in exactly one event; multiple events are handled by copying transitions.
- Configuration encoding: The encoding represents hosted objects in disjoint net-place copies with identifier places, and remains injective even for empty objects.A dedicated identifier token witnesses an object whose internal marking is zero.
- Phase modules: The phase modules encode merging, internal firing, and distribution, including fresh identifier creation and token movement with renaming.The updating phase ensures all prescribed internal transitions are enabled at the phase start or detects failure, while distribution creates identifiers for newly created objects.
- Correctness: The encoding is a phase encoding and f-perfect for some polynomial f, preserving cEOS coverability, termination, and boundedness instances.For markings M and M′, an EOS event step corresponds exactly to a finite c-νPN run between their encodings.
- Consequences and limitation: Consequently, cEOS-coverability, cEOS-termination, and cEOS-boundedness each admit polynomial reductions to the corresponding c-νPN problem, whereas the construction does not extend to non-conservative EOSs.Non-conservative transitions may require zero-checking when destroying nonempty objects, which the merging module cannot enforce.
7. From c-νPN to νPN
The section encodes arbitrary c-νPNs into standard νPNs using auxiliary places and sequential transition gadgets, while handling potentially broken configurations through projection and repair arguments. This yields polynomial-time equivalence for coverability, termination, and boundedness, preserving their respective complexities.
- From c-νPN to νPN: The encoding simulates channel transfers with sequential firings that manipulate tokens one by one, but may leave leftovers that create irreversible broken configurations.Auxiliary places track stages, modes, active tuples, and broken configurations; t_firebase and rename-style transitions implement transfers incrementally.
- From c-νPN to νPN: c-νPN coverability, termination, and boundedness reduce in polynomial time to the corresponding νPN problems via the encoding ξ.Theorem 7.9 establishes yes-instance equivalence, and the constructed net and encoded instances are polynomial-time computable.
- Complexity consequences: The resulting reduction cycle makes cEOS and νPN complexities coincide: coverability is Fω2-complete, while termination and boundedness are non-primitive recursive.The cycle runs from νPNs to cEOSs to c-νPNs and back to νPNs, establishing constant complexity across the variants.
8. Conclusions
The conclusions establish complexity results for conservative elementary object systems through reductions to νPNs, while identifying finite nesting depth as a limitation and direction for generalization.
- Conclusions: Inter-reductions with νPN problems yield Fω2-completeness for cEOS-coverability and non-primitive recursive lower bounds for cEOS-termination and cEOS-boundedness.Only the reduction from c-νPNs to νPNs performs cheating steps.
- Limitations and future work: The study restricts object net systems to two nesting levels because formal definitions beyond depth 2 are absent from existing literature.The authors hypothesize that finite nesting levels can support a generalized reduction.
- Limitations and future work: The authors expect deeper but finite nesting to restrict verification complexity relative to object systems with several nesting layers.This expectation motivates generalizing the reduction framework to finite nesting depths.
A. Phase Encodings Invariance
Uniform phase-encodings preserve coverability, while phase-finite encodings preserve termination and suitably bounded encodings preserve boundedness. These equivalences follow by translating runs into consistent phases and reflecting them through injectivity and finiteness conditions.
- A. Phase Encodings Invariance: Uniform phase-encodings make each F1-coverability instance equivalent to its translated F2 instance.Embedding preserves the target relation, while uniformity and injectivity reconstruct a corresponding F1 run from consistent F2 phases.
- A. Phase Encodings Invariance: Phase-finite phase-encodings make each F1-termination instance equivalent to its translated F2 instance.An infinite F1 run expands into infinitely many finite phases, while phase-finiteness lets any infinite F2 run be partitioned into infinitely many encoding phases.
- A. Phase Encodings Invariance: F-bounded phase-encodings into finitary F2 systems make each F1-boundedness instance equivalent to its translated F2 instance.Bounded reachable encoding configurations and finitarity yield finitely many reachable F2 configurations; conversely, injectivity maps finite F2 encoding reachability back to F1.
B. Phase-encoding Proofs
The appendix proves that the configuration encodings used throughout the paper are phase-encodings, establishing correspondence between source-system steps and finite target-system phases. It covers encodings for νPN-related constructions, EOS-to-c-νPN constructions, and CGW-to-CGN translations.
- νPN-to-cEOS encoding: The appendix establishes that the configuration encoding ξ in Def.5.2 is a phase encoding, with every D-step corresponding to a finite E-phase and conversely.The reverse direction organizes each phase into selection, firing, and reporting blocks, then uses injectivity of ξ to recover the corresponding D-step.
- EOS-to-c-νPN encoding: The encoding ξ in Def.6.2 is proved to preserve exactly one EOS event step and mode as a finite phase in the constructed c-νPN, and vice versa.The proof assumes the event mode handles a single system-net type and simulates merging, updating, fresh-tuple creation, distribution, movement, and transfer modules.
- CGW-to-CGN encoding: The function ξ in Def.7.1 is proved to be a phase encoding from CGW into CGN.Standard transitions translate directly, while split transitions are simulated by a finite sequence involving mode selection, firing, stopping, renaming, and reset; the reverse direction is symmetric.