Formal Reachability Analysis, Soundness Verification, and Cross-Object Deadlock Detection Engine for Object-Centric Petri Nets (OCPN) and 1-Safe Workflow Nets.
Verifies per object-type sub-net projection:
- Option to Complete: for all reachable markings M in [M_0>, [M_end] in [M>
- Proper Completion: for all M in [M_0>, sink in M implies M == [M_end]
- Absence of Dead Transitions: for all t in T, exists M in [M_0> such that M[t>
- 1-Safety: for all M in [M_0>, for all p in P, M(p) <= 1
Additionally performs cross-object global deadlock detection via Resource Allocation Graph (RAG) cycle detection — addressing the critical gap identified by Prof. Marco Montali: two sub-nets individually sound may globally deadlock if transition synchronization over multiple object types creates circular waits.
Emits explicit minimal counter-example trace sequences on violation.
Summary
Functions
Cross-Object Global Deadlock Detection via Resource Allocation Graph (RAG) Cycle Analysis.
Performs complete reachability state-space exploration on a single-object or projected Workflow Net to verify 1-safe soundness.
Functions
Cross-Object Global Deadlock Detection via Resource Allocation Graph (RAG) Cycle Analysis.
Addresses the critical theoretical gap identified in adversarial review: Two sub-nets individually verified as 1-safe sound may globally deadlock when transition synchronization over multiple object types creates circular waits.
A cross-object deadlock requires a cycle in which distinct transitions form a mutual circular wait: T1 holds OT_A and waits for OT_B, while T2 holds OT_B and waits for OT_A — i.e. a cycle of length >= 4 in the bipartite RAG.
A single transition consuming and producing the same object type is NOT a cycle; it is simply a token pass-through (sound by token conservation).
Performs complete reachability state-space exploration on a single-object or projected Workflow Net to verify 1-safe soundness.