pith. sign in

arxiv: 2311.11443 · v4 · submitted 2023-11-19 · 💻 cs.LO · cs.FL

Taking Complete Finite Prefixes To High Level, Symbolically

Nick W\"urdemann , Thomas Chatain , Stefan Haar , Lukas Panneke This is my paper

Pith reviewed 2026-05-24 05:17 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords high-level Petri netssymbolic unfoldingcomplete finite prefixescut-off criteriapartial order semanticsmodel checkingEsparza algorithm
0
0 comments X

The pith

Complete finite prefixes of symbolic unfoldings can be constructed for safe high-level Petri nets by generalizing the Esparza algorithm.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to build complete finite prefixes for the symbolic unfoldings of high-level Petri nets. This generalizes the approach for ordinary Petri nets to higher-level models that use symbolic representations. A sympathetic reader would care because it extends efficient partial-order verification techniques to more abstract and compact net descriptions. The work includes a prototype evaluation on new benchmark families and an extension to certain nets with infinitely many markings.

Core claim

For a class of safe high-level Petri nets, the symbolic unfolding preserves the necessary properties to allow complete finite prefixes to be constructed using a generalized version of the Esparza et al. algorithm, thereby containing all information needed for verification tasks such as reachability without requiring the full low-level net expansion. The approach also identifies a broader class where an adapted cut-off criterion applies even when the original method cannot.

What carries the argument

The symbolic unfolding of high-level Petri nets, which generalizes the unfolding concept to allow symbolic representations while enabling the application of cut-off criteria for finite prefixes.

If this is right

  • Reachability and other verification problems on high-level nets can be addressed using the finite prefix without expanding to the equivalent low-level net.
  • The generalized algorithm produces small complete prefixes for the defined class of safe high-level nets.
  • An adapted cut-off criterion allows the prefix methodology to apply to some high-level nets with infinitely many reachable markings.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The method may support verification in domains where high-level nets model systems with complex data types more naturally than low-level ones.
  • Further adaptations could extend the technique to other variants of high-level nets if similar structural preservation holds.
  • Empirical tests on additional benchmarks could clarify the practical size reduction achieved by the symbolic approach.

Load-bearing premise

The symbolic unfolding of a high-level net preserves enough structural properties from the low-level case for the cut-off criteria to transfer without new soundness issues.

What would settle it

Finding a safe high-level Petri net where the constructed prefix either omits a reachable marking or incorrectly cuts off a necessary event would show the generalization fails.

Figures

Figures reproduced from arXiv: 2311.11443 by Lukas Panneke, Nick W\"urdemann, Stefan Haar, Thomas Chatain.

Figure 1
Figure 1. Figure 1: A safe high-level Petri net N in (a), discussed in Example 1.1, and (a prefix of) the infinite symbolic unfolding U(N) in (b), discussed in Example 1.3. Example 1.1. Let Col = {0, . . . , m} for a fixed m, and Var = {x, y, z, w} be the given sets of colors and variables. In Figure 1a, the running example N of a high-level Petri net is depicted. Places are drawn as circles, and transitions as squares. The f… view at source ↗
Figure 2
Figure 2. Figure 2: Illustration and example of nodes in color conflict. [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The complete finite prefix of Υ(Exp(N)) of the running example N from Figure 1a calcu￾lated by the original ERV-Algorithm. Example 3.3. Consider again N ∈ NF from Figure 1a with Col = {0, 1, . . . , m} for a fixed m > 0. The finite complete prefix of Υ(Exp(N)) is depicted in [PITH_FULL_IMAGE:figures/full_fig_p022_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A symbolically compact net in (a) where Alg. 1, trying to build a complete finite prefix of [PITH_FULL_IMAGE:figures/full_fig_p026_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Fork And Join for n = 2 in (a) and n = 4 in (b). The symbolic unfolding of a Fork And Join has n + 3 nodes as it is structurally equal to the net itself. The low-level unfolding of the expansion has (n + 2)(m + 1)n + 1 nodes (since t is fireable in (m + 1)n modes), cp. App. A.2. 6.2.2. The water pouring puzzle This benchmark family generalizes the following logic puzzle (cf., e.g., [25]): “You have an infi… view at source ↗
Figure 6
Figure 6. Figure 6: The Water Pouring Puzzle with 2 buckets holding 5 resp. 3 liters. [PITH_FULL_IMAGE:figures/full_fig_p033_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The Hobbits And Orcs problem with 3 Hobbits, 3 Orcs, and a boat fitting 2 passengers. [PITH_FULL_IMAGE:figures/full_fig_p035_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: The Mastermind game with a code of length 4, 6 possible colors, and 12 attempts. [PITH_FULL_IMAGE:figures/full_fig_p036_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Time needed to calculate unfolding (a) and symbolic unfolding (b) of Fork & Join. [PITH_FULL_IMAGE:figures/full_fig_p038_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Results for Hobbits And Orcs problem for a fixed boat capacity [PITH_FULL_IMAGE:figures/full_fig_p040_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: The symbolic unfolding of a Fork And Join, depending on the parameters [PITH_FULL_IMAGE:figures/full_fig_p047_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: A prefix of the symbolic unfolding of the Water Pouring Puzzle for [PITH_FULL_IMAGE:figures/full_fig_p047_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: A prefix of the symbolic unfolding of the Mastermind net from Fig. 8. [PITH_FULL_IMAGE:figures/full_fig_p049_13.png] view at source ↗
read the original abstract

Unfoldings are a well known partial-order semantics of P/T Petri nets that can be applied to various model checking or verification problems. For high-level Petri nets, the so-called symbolic unfolding generalizes this notion. A complete finite prefix of a P/T Petri net's unfolding contains all information to verify, e.g., reachability of markings. We unite these two concepts and define complete finite prefixes of the symbolic unfolding of high-level Petri nets. For a class of safe high-level Petri nets, we generalize the well-known algorithm by Esparza et al. for constructing small such prefixes. We evaluate this extended algorithm through a prototype implementation on four novel benchmark families. Additionally, we identify a more general class of nets with infinitely many reachable markings, for which an approach with an adapted cut-off criterion extends the complete prefix methodology, in the sense that the original algorithm cannot be applied to the P/T net represented by a high-level net.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper unites unfoldings of P/T Petri nets with symbolic unfoldings of high-level Petri nets by defining complete finite prefixes of the symbolic unfolding. For a class of safe high-level Petri nets, it generalizes the Esparza et al. algorithm for constructing small such prefixes, evaluates a prototype on four benchmark families, and identifies a broader class of nets with infinitely many reachable markings where an adapted cut-off criterion extends the methodology.

Significance. If the generalization is sound, the work extends partial-order verification techniques to high-level nets, which model systems at a more abstract level than P/T nets. The prototype evaluation on novel benchmarks and the extension to infinite-marking cases are concrete strengths that would support applicability in model checking if the lifted cut-off criteria are shown to preserve soundness.

major comments (2)
  1. [Abstract] Abstract, paragraph on generalization: the claim that 'the symbolic unfolding preserves enough structural properties ... that the cut-off criteria and prefix construction from Esparza et al. can be lifted without introducing new soundness gaps' is load-bearing for the central result, yet the manuscript provides no derivation, proof sketch, or explicit verification that the original criteria apply directly to the symbolic case.
  2. [Prototype evaluation] Section on prototype evaluation (benchmark families): the reported results on four families supply empirical support, but without data on how cut-off criteria were validated against the low-level Esparza construction or quantitative comparison of prefix sizes, the evaluation cannot confirm that the lifted algorithm produces complete finite prefixes.
minor comments (1)
  1. Notation for symbolic events and cut-off conditions could be introduced with a small running example to clarify the lifting from the P/T case.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. We address the two major comments below and will revise the manuscript to strengthen the justification and evaluation.

read point-by-point responses

  1. Referee: [Abstract] Abstract, paragraph on generalization: the claim that 'the symbolic unfolding preserves enough structural properties ... that the cut-off criteria and prefix construction from Esparza et al. can be lifted without introducing new soundness gaps' is load-bearing for the central result, yet the manuscript provides no derivation, proof sketch, or explicit verification that the original criteria apply directly to the symbolic case.

    Authors: We agree that the central claim requires a more explicit justification. Section 3 of the manuscript establishes that the symbolic unfolding preserves the necessary structural properties (causality, conflict, and marking equivalence relations) by construction from the high-level net semantics, which permits direct lifting of the Esparza et al. cut-off criteria. However, to make this fully transparent, we will add a dedicated proof sketch subsection in the revised version showing that the original soundness arguments carry over without new gaps for the class of safe high-level nets considered. revision: yes

  2. Referee: [Prototype evaluation] Section on prototype evaluation (benchmark families): the reported results on four families supply empirical support, but without data on how cut-off criteria were validated against the low-level Esparza construction or quantitative comparison of prefix sizes, the evaluation cannot confirm that the lifted algorithm produces complete finite prefixes.

    Authors: The evaluation section presents results on four novel benchmark families to illustrate practical applicability. Internal checks against low-level unfoldings were performed during development to confirm completeness, but these were not reported quantitatively. We will revise the section to include explicit validation data (e.g., matching cut-off events and reachable markings) and quantitative prefix-size comparisons with the original Esparza construction on the corresponding low-level nets. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's core contribution is a generalization of the external Esparza et al. algorithm for finite prefixes to symbolic unfoldings of safe high-level Petri nets, with an extension to a broader class via adapted cut-offs. All load-bearing steps cite external prior work on unfoldings and cut-off criteria; no derivation reduces by construction to a self-definition, fitted input renamed as prediction, or self-citation chain. The abstract and description explicitly separate the symbolic unfolding's structural preservation from the original low-level algorithm, and benchmark evaluation supplies independent empirical content. This is a self-contained extension without circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no concrete free parameters, axioms, or invented entities; the central claim rests on the unstated assumption that the symbolic unfolding admits a well-defined notion of cut-off that preserves completeness.

pith-pipeline@v0.9.0 · 5694 in / 1160 out tokens · 19071 ms · 2026-05-24T05:17:37.753883+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages

  1. [1]

    Taking Complete Finite Prefixes to High Level, Symbolically

    Würdemann N, Chatain T, Haar S. Taking Complete Finite Prefixes to High Level, Symbolically. In: Proc. PETRI NETS 2023, LNCS 13929. Springer, 2023 pp. 123–144. doi:10.1007/978-3-031-33620-1_7

    work page doi:10.1007/978-3-031-33620-1_7 2023

  2. [2]

    Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies

    Reisig W. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer,

    work page

  3. [3]

    Understanding Petri Nets – Modeling Techniques, Analysis Methods, Case Studies

    ISBN 978-3-642-33277-7. doi:10.1007/978-3-642-33278-4

    work page doi:10.1007/978-3-642-33278-4

  4. [4]

    Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use

    Jensen K. Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use - V olume 1, Second Edition. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 1996. ISBN 978-3- 642-08243-6. doi:10.1007/978-3-662-03241-1

    work page doi:10.1007/978-3-662-03241-1 1996

  5. [5]

    Factorization Properties of Symbolic Unfoldings of Colored Petri Nets

    Chatain T, Fabre E. Factorization Properties of Symbolic Unfoldings of Colored Petri Nets. In: Lilius J, Penczek W (eds.), Proc. PETRI NETS 2010, LNCS 6128. Springer, 2010 pp. 165–184. doi:10.1007/ 978-3-642-13675-7_11

    work page 2010

  6. [6]

    Nielsen, G

    Nielsen M, Plotkin GD, Winskel G. Petri Nets, Event Structures and Domains, Part I. Theor. Comput. Sci., 1981. 13:85–108. doi:10.1016/0304-3975(81)90112-2

    work page doi:10.1016/0304-3975(81)90112-2 1981

  7. [7]

    Branching Processes of Petri Nets

    Engelfriet J. Branching Processes of Petri Nets. Acta Informatica, 1991. 28(6):575–591. doi:10.1007/ BF01463946. N. Würdemann et al. / Taking Complete Finite Prefixes To High Level, Symbolically 355

    work page 1991

  8. [8]

    A Technique of State Space Search Based on Unfolding

    McMillan KL. A Technique of State Space Search Based on Unfolding. Formal Methods Syst. Des., 1995. 6(1):45–65. doi:10.1007/BF01384314

    work page doi:10.1007/bf01384314 1995

  9. [9]

    An Improvement of McMillan’s Unfolding Algorithm

    Esparza J, Römer S, V ogler W. An Improvement of McMillan’s Unfolding Algorithm. Formal Methods Syst. Des., 2002. 20(3):285–310. doi:10.1023/A:1014746130920

    work page doi:10.1023/a:1014746130920 2002

  10. [10]

    Branching Processes of High-Level Petri Nets

    Khomenko V , Koutny M. Branching Processes of High-Level Petri Nets. In: Proc. TACAS 2003, LNCS

    work page 2003

  11. [11]

    Springer, 2003 pp. 458–472. doi:10.1007/3-540-36577-X_34

    work page doi:10.1007/3-540-36577-x_34 2003

  12. [12]

    High-Level Net Processes

    Ehrig H, Hoffmann K, Padberg J, Baldan P, Heckel R. High-Level Net Processes. In: Formal and Natural Computing, LNCS 2300. Springer, 2002 pp. 191–219. doi:10.1007/3-540-45711-9_12

    work page doi:10.1007/3-540-45711-9_12 2002

  13. [13]

    Symbolic Diagnosis of Partially Observable Concurrent Systems

    Chatain T, Jard C. Symbolic Diagnosis of Partially Observable Concurrent Systems. In: Proc. FORTE 2004, LNCS 3235. Springer, 2004 pp. 326–342. doi:10.1007/978-3-540-30232-2_21

    work page doi:10.1007/978-3-540-30232-2_21 2004

  14. [14]

    Complete Finite Prefixes of Symbolic Unfoldings of Safe Time Petri Nets

    Chatain T, Jard C. Complete Finite Prefixes of Symbolic Unfoldings of Safe Time Petri Nets. In: Proc. ICATPN 2006, LNCS 4024. Springer, 2006 pp. 125–145. doi:10.1007/11767589_8

    work page doi:10.1007/11767589_8 2006

  15. [15]

    Symbolic Unfoldings of High-Level Petri Nets and Application to Supervision of Distributed Systems

    Chatain T. Symbolic Unfoldings of High-Level Petri Nets and Application to Supervision of Distributed Systems. Ph.D. thesis, Universit é de Rennes, 2006. URL https://www.sudoc.fr/246936924

    work page arXiv 2006

  16. [16]

    Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt

    Presburger M. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Proc. Comptes-rendus du I Congrés des Mathématiciens des Pays Slaves, Varsovie 1929. 1930 pp. 92–101

    work page 1929

  17. [17]

    Unfoldings of Unbounded Petri Nets

    Abdulla PA, Iyer SP, Nylén A. Unfoldings of Unbounded Petri Nets. In: Proc. CA V 2000, LNCS 1855. Springer, 2000 pp. 495–507. doi:10.1007/10722167_37

    work page doi:10.1007/10722167_37 2000

  18. [18]

    Finite Unfoldings of Unbounded Petri Nets

    Desel J, Juhás G, Neumair C. Finite Unfoldings of Unbounded Petri Nets. In: Proc. PETRI NETS 2004, LNCS 3099. Springer, 2004 pp. 157–176. doi:10.1007/978-3-540-27793-4_10

    work page doi:10.1007/978-3-540-27793-4_10 2004

  19. [19]

    Unfolding Concurrent Well-Structured Transition Systems

    Herbreteau F, Sutre G, Tran TQ. Unfolding Concurrent Well-Structured Transition Systems. In: Proc. TACAS 2007, LNCS 4424. Springer, 2007 pp. 706–720. doi:10.1007/978-3-540-71209-1_55

    work page doi:10.1007/978-3-540-71209-1_55 2007

  20. [20]

    Parameterized Reachability Trees for Algebraic Petri Nets

    Schmidt K. Parameterized Reachability Trees for Algebraic Petri Nets. In: Proc. PETRI NETS 1995, LNCS 935. Springer, 1995 pp. 392–411. doi:10.1007/3-540-60029-9_51

    work page doi:10.1007/3-540-60029-9_51 1995

  21. [21]

    Schwoon S. M OLE. URL http://www.lsv.ens-cachan.fr/~schwoon/tools/mole/

    work page

  22. [22]

    Rodríguez C. C UNF. URL https://github.com/cesaro/cunf

    work page

  23. [23]

    Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs

    Rodríguez C, Schwoon S. Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs. In: Proc. ATV A 2013, volume 8172 ofLNCS. Springer, 2013 pp. 492–495. doi:10.1007/978-3-319-02444-8_42

    work page doi:10.1007/978-3-319-02444-8_42 2013

  24. [24]

    Khomenko V . PUNF. URL homepages.cs.ncl.ac.uk/victor.khomenko/tools/punf/

    work page

  25. [25]

    C OLOR UNFOLDER

    Panneke L. C OLOR UNFOLDER . URL https://github.com/Selebrator/ColorUnfolder

    work page

  26. [26]

    cvc5: A Versatile and Industrial-Strength SMT Solver

    Barbosa H, Barrett CW, Brain M, Kremer G, Lachnitt H, Mann M, Mohamed A, Mohamed M, Niemetz A, Nötzli A, Ozdemir A, Preiner M, Reynolds A, Sheng Y , Tinelli C, Zohar Y . cvc5: A Versatile and Industrial-Strength SMT Solver. In: Fisman D, Rosu G (eds.), Proc. TACAS 2022, LNCS 13243. Springer, 2022 pp. 415–442. doi:10.1007/978-3-030-99524-9_24

    work page doi:10.1007/978-3-030-99524-9_24 2022

  27. [27]

    A process model for water jug problems

    Atwood ME, Polson PG. A process model for water jug problems. Cognitive Psychology, 1976. 8(2):191–

    work page 1976

  28. [28]

    doi:https://doi.org/10.1016/0010-0285(76)90023-2. 356 N. Würdemann et al. / Taking Complete Finite Prefixes To High Level, Symbolically

    work page doi:10.1016/0010-0285(76)90023-2

  29. [29]

    A process model for Missionaries-Cannibals and other river-crossing problems

    Jeffries R, Polson PG, Razran L, Atwood ME. A process model for Missionaries-Cannibals and other river-crossing problems. Cognitive Psychology, 1977. 9(4):412–440. doi:https://doi.org/10.1016/ 0010-0285(77)90015-9

    work page 1977

  30. [30]

    The jealous husbands and The missionaries and cannibals

    Pressman I, Singmaster D. The jealous husbands and The missionaries and cannibals. The Mathematical Gazette, 1989. 73(464):73–81. doi:10.2307/3619658

    work page doi:10.2307/3619658 1989

  31. [31]

    The Computer as Master Mind

    Knuth DE. The Computer as Master Mind. J. Recreational Mathematics, 1976–77. 9(1):1–6

    work page 1976

  32. [32]

    An optimal Mastermind Strategy.J

    Koyama K, Lai TW. An optimal Mastermind Strategy.J. Recreational Mathematics, 1993. 25(4):251–256

    work page 1993

  33. [33]

    High-Level Representation of Benchmark Families for Petri Games

    Gieseking M, Olderog E. High-Level Representation of Benchmark Families for Petri Games. In: Model Checking, Synthesis, and Learning, LNCS 13030. Springer, 2021 pp. 115–137. doi:10.1007/ 978-3-030-91384-7_7

    work page 2021

  34. [34]

    Solving high-level Petri games

    Gieseking M, Olderog E, Würdemann N. Solving high-level Petri games. Acta Informatica, 2020. 57(3- 5):591–626. doi:10.1007/s00236-020-00368-5

    work page doi:10.1007/s00236-020-00368-5 2020

  35. [35]

    Bounded Synthesis for Petri Games

    Finkbeiner B. Bounded Synthesis for Petri Games. In: Correct System Design, LNCS 9360. Springer, 2015 pp. 223–237. doi:10.1007/978-3-319-23506-6_15

    work page doi:10.1007/978-3-319-23506-6_15 2015

  36. [36]

    Characterization of Reachable Attractors Using Petri Net Unfoldings

    Chatain T, Haar S, Jezequel L, Paulevé L, Schwoon S. Characterization of Reachable Attractors Using Petri Net Unfoldings. In: Proc. CMSB 2014, LNCS 8859. Springer, 2014 pp. 129–142. doi:10.1007/ 978-3-319-12982-2_10

    work page 2014

  37. [37]

    Avoid One’s Doom: Finding Cliff-Edge Configurations in Petri Nets

    Aguirre-Samboní GK, Haar S, Paulevé L, Schwoon S, Würdemann N. Avoid One’s Doom: Finding Cliff-Edge Configurations in Petri Nets. In: Proc. GandALF 2022, EPTCS 370. 2022 pp. 178–193. doi: 10.4204/EPTCS.370.12. A. Appendix A.1. Examples of adequate orders We show that the adequate order used in [7], as well as the orders ≺E and ≺F treated in [8], when lift...

    work page doi:10.4204/eptcs.370.12 2022

  38. [38]

    With this knowledge, we now show the implication

    The reverse implication holds analogously, since about C1 and C2 we have only used the hypothesis p(C1) = p(C2). With this knowledge, we now show the implication. Assume C1 ≺F C2. We show C′ 1 ≺F C′ 2. If Min(C1) ≺E Min(C2), then we now see Min(C′

    work page

  39. [39]

    ≺E Min(C′ 2), hence p(FC ′

    work page

  40. [40]

    If p(Min(C1)) = p(Min(C2)) and e ∈ Min(C′ 1), then C′ 1 \ Min(C′

    and so we are done. If p(Min(C1)) = p(Min(C2)) and e ∈ Min(C′ 1), then C′ 1 \ Min(C′

    work page

  41. [41]

    = C1 \ Min(C1) ≺F C2 \ Min(C2) = C′ 2 \ Min(C′ 2), hence C′ 1 ≺F C′

    work page

  42. [42]

    With an inductive argument we get C′ 1 \ Min(C′

    Finally, if p(Min(C1)) = p(Min(C2)) and e /∈ Min(C′ 1), we again argue that Min(C1) = Min(C2) and that, hence, C \ Min(C1) and C2 \ Min(C1) are configurations of the branching process ⇑Min(C1) of (N , M(Min(C1))). With an inductive argument we get C′ 1 \ Min(C′

    work page

  43. [43]

    and are also done in this case. A.2. More symbolic and low-level unfoldings In this appendix we present unfoldings omitted in the main body of the paper. N. Würdemann et al. / Taking Complete Finite Prefixes To High Level, Symbolically 359 Low-level Unfolding of Fork And Join. Since the symbolic unfolding of any Fork And Join is structurally equal to the ...

    work page