Deciding Reachability and the Covering Problem with Diagnostics for Sound Acyclic Free-Choice Workflow Nets
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917242407485440 |
|---|---|
| author | Prinz, Thomas M. Schwanen, Christopher T. van der Aalst, Wil M. P. |
| author_facet | Prinz, Thomas M. Schwanen, Christopher T. van der Aalst, Wil M. P. |
| contents | A central decision problem in Petri net theory is reachability asking whether a given marking can be reached from the initial marking. Related is the covering problem (or sub-marking reachbility), which decides whether there is a reachable marking covering at least the tokens in the given marking. For live and bounded free-choice nets as well as for sound free-choice workflow nets, both problems are polynomial in their computational complexity. This paper refines this complexity for the class of sound acyclic free-choice workflow nets to a quadratic polynomial, more specifically to $O(P^2 + T^2)$. Furthermore, this paper shows the feasibility of accurately explaining why a given marking is or is not reachable. This can be achieved by three new concepts: admissibility, maximum admissibility, and diverging transitions. Admissibility requires that all places in a given marking are pairwise concurrent. Maximum admissibility states that adding a marked place to an admissible marking would make it inadmissible. A diverging transition is a transition which originally "produces" the concurrent tokens that lead to a given marking. In this paper, we provide algorithms for all these concepts and explain their computation in detail by basing them on the concepts of concurrency and post-dominance frontiers - a well known concept from compiler construction. In doing this, we present straight-forward implementations for solving (sub-marking) reachability. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_02447 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Deciding Reachability and the Covering Problem with Diagnostics for Sound Acyclic Free-Choice Workflow Nets Prinz, Thomas M. Schwanen, Christopher T. van der Aalst, Wil M. P. Formal Languages and Automata Theory Data Structures and Algorithms A central decision problem in Petri net theory is reachability asking whether a given marking can be reached from the initial marking. Related is the covering problem (or sub-marking reachbility), which decides whether there is a reachable marking covering at least the tokens in the given marking. For live and bounded free-choice nets as well as for sound free-choice workflow nets, both problems are polynomial in their computational complexity. This paper refines this complexity for the class of sound acyclic free-choice workflow nets to a quadratic polynomial, more specifically to $O(P^2 + T^2)$. Furthermore, this paper shows the feasibility of accurately explaining why a given marking is or is not reachable. This can be achieved by three new concepts: admissibility, maximum admissibility, and diverging transitions. Admissibility requires that all places in a given marking are pairwise concurrent. Maximum admissibility states that adding a marked place to an admissible marking would make it inadmissible. A diverging transition is a transition which originally "produces" the concurrent tokens that lead to a given marking. In this paper, we provide algorithms for all these concepts and explain their computation in detail by basing them on the concepts of concurrency and post-dominance frontiers - a well known concept from compiler construction. In doing this, we present straight-forward implementations for solving (sub-marking) reachability. |
| title | Deciding Reachability and the Covering Problem with Diagnostics for Sound Acyclic Free-Choice Workflow Nets |
| topic | Formal Languages and Automata Theory Data Structures and Algorithms |
| url | https://arxiv.org/abs/2602.02447 |