pith. sign in

arxiv: 2211.10540 · v5 · submitted 2022-11-19 · 💻 cs.FL

Waiting Nets: State Classes and Taxonomy

Lo\"ic H\'elou\"et , Pranay Agrawal This is my paper

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

classification 💻 cs.FL
keywords waiting netstime Petri netsstate class graphreachabilitycoverabilitytimed language equivalenceexpressivenessbounded nets
0
0 comments X

The pith

Bounded waiting nets admit a finite state class graph that decides reachability and coverability while generating strictly more timed languages than time Petri nets.

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

Waiting nets modify time Petri nets so that a transition can begin measuring time as soon as any of its input places hold tokens, rather than only when the full preset is marked. The semantics also permit firing after an upper time bound even if some resources are still missing, provided the missing tokens arrive later. For any bounded waiting net the construction produces a finite state class graph that abstracts both control locations and time intervals. Reachability and coverability questions can therefore be answered by inspecting this graph. The same model is shown to recognize timed languages that no time Petri net can produce.

Core claim

Waiting nets decouple time measurement from full transition enabling and relax urgency when resources remain unavailable. For bounded instances the paper constructs a finite state class graph by tracking sets of enabled transitions together with symbolic time intervals that account for the waiting semantics. Inspection of this graph decides reachability and coverability. With respect to timed language equivalence the class of waiting nets strictly contains the class of time Petri nets.

What carries the argument

Finite state class graph obtained by symbolic abstraction of control states and time intervals under the waiting semantics that allow partial presets and delayed firing after upper bounds.

If this is right

  • Reachability is decidable for every bounded waiting net.
  • Coverability is decidable for every bounded waiting net.
  • Waiting nets can generate timed languages outside the expressive power of time Petri nets.
  • The finite-graph construction remains valid even though urgency is relaxed and time may start on incomplete presets.

Where Pith is reading between the lines

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

  • The waiting semantics may capture systems in which timers run independently of resource acquisition without immediately losing decidability.
  • Waiting nets occupy an intermediate position between time Petri nets and stopwatch extensions that are already known to be undecidable on bounded nets.
  • The expressiveness gap suggests that any complete taxonomy of timed Petri-net variants must place waiting nets strictly above ordinary time Petri nets.

Load-bearing premise

The waiting nets under consideration are bounded, that is, each place can hold only finitely many tokens.

What would settle it

A concrete bounded waiting net whose successive state classes keep producing new time intervals indefinitely, or a timed word accepted by some waiting net but rejected by every time Petri net.

Figures

Figures reproduced from arXiv: 2211.10540 by Lo\"ic H\'elou\"et, Pranay Agrawal.

Figure 1
Figure 1. Figure 1: A TPN a) a Timed Petri net b), and a Waiting net c) Consider the examples of [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: a) Decoupled time and control in a waiting net. b) ... with a timeout transition. The semantics of waiting nets associates clocks to transitions, and lets time elapse if their standard preset is filled. It allows firing of a transition t if the standard and the control preset of t is filled. Definition 3.2. (Enabled, Fully Enabled, Waiting transitions) • A transition t is enabled in marking M.N iff M ≥ ◦ (… view at source ↗
Figure 3
Figure 3. Figure 3: Operational semantics of Waiting Nets A timed move from a configuration (M.N, v) lets d ∈ R ≥0 time units elapse, but leaves the marking unchanged. We adopt an urgent semantics that considers differently fully enabled transitions and waiting transitions. First of all, elapsing of d time units from (M.N, v) is allowed only if, for every fully enabled transition t, v(t) + d ≤ β(t). If v(t) + d > β(t) then t … view at source ↗
Figure 4
Figure 4. Figure 4: A Waiting net, its initial domain, an equivalent DB [PITH_FULL_IMAGE:figures/full_fig_p014_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Upper bounds of transitions influence state classe [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: A non-deterministic state class graph for the wait [PITH_FULL_IMAGE:figures/full_fig_p019_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: A cyclic Waiting net The main idea of this example is to give control alternatively to transition t1 and t2, but measure enabled time for t2 when control allows firing of t1 and enabled time for t1 when control allows firing of t2. The timed word (t1, 1)(t1, 2)(tc3, 3)(t2, 3.2) is a possible behavior of this net. Notice that transition t2 becomes fully enabled after firing of t3, but was enabled from the b… view at source ↗
Figure 8
Figure 8. Figure 8: a) A timed automaton A1 b) An equivalent timed Petri net c) An equivalent TPN in T P Nǫ [PITH_FULL_IMAGE:figures/full_fig_p027_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: a) A waiting net W b) a part of TPN needed to encode L(W) c) An unbounded waiting net The above conditions are needed to ensure that L(N ) = L(W). We can now show that it is impossible to build a net N satisfying all these constraints. Since t1 must fire after t0 , N must contain a subnet of the form shown in figure 9-b, where p is an empty place preventing firing t1 before t0. Notice however that p forbid… view at source ↗
Figure 10
Figure 10. Figure 10: A TPN N2 with non-injective labeling. Corollary 5.11. BT P Ninj <L BW T P Ninj Proof: Inclusion BT P Ninj ≤L BW T P Ninj is straightforward from Definition 3.1. Now this inclusion is strict. Take the example of [PITH_FULL_IMAGE:figures/full_fig_p031_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Relation among net and automata classes, and fron [PITH_FULL_IMAGE:figures/full_fig_p032_11.png] view at source ↗
read the original abstract

In time Petri nets (TPNs), time and control are tightly connected: time measurement for a transition starts only when all resources needed to fire it are available. Further, upper bounds on duration of enabledness can force transitions to fire (this is called urgency). For many systems, one wants to decouple control and time, i.e. start measuring time as soon as a part of the preset of a transition is filled, and fire it after some delay \underline{and} when all needed resources are available. This paper considers an extension of TPN called waiting nets that dissociates time measurement and control. Their semantics allows time measurement to start with incomplete presets, and can ignore urgency when upper bounds of intervals are reached but all resources needed to fire are not yet available. Firing of a transition is then allowed as soon as missing resources are available. It is known that extending bounded TPNs with stopwatches leads to undecidability. Our extension is weaker, and we show how to compute a finite state class graph for bounded waiting nets, yielding decidability of reachability and coverability. We then compare expressiveness of waiting nets with that of other models w.r.t. timed language equivalence, and show that they are strictly more expressive than TPNs.

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

1 major / 0 minor

Summary. The paper claims that waiting nets, an extension of time Petri nets allowing time measurement to start with incomplete presets and ignoring urgency in certain cases, admit a finite state class graph when bounded, leading to decidability of reachability and coverability. It also claims strict expressiveness superiority over TPNs w.r.t. timed language equivalence.

Significance. If substantiated, the results would offer a decidable yet more expressive alternative to TPNs for modeling timed systems, positioned between TPNs and undecidable stopwatch TPNs. The state class graph would enable practical verification.

major comments (1)
  1. [Abstract] The finite state class graph construction for bounded waiting nets and the proof of strict timed-language expressiveness over TPNs are asserted without any construction details, proof sketches, or counter-examples provided in the visible text. These are load-bearing for the central claims of decidability and the taxonomy.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review. The major comment concerns the level of detail in the abstract; we clarify that the full manuscript contains the requested constructions and proofs, as summarized below.

read point-by-point responses

  1. Referee: [Abstract] The finite state class graph construction for bounded waiting nets and the proof of strict timed-language expressiveness over TPNs are asserted without any construction details, proof sketches, or counter-examples provided in the visible text. These are load-bearing for the central claims of decidability and the taxonomy.

    Authors: The abstract is a high-level summary; the finite state class graph construction (including the algorithm for computing classes and the proof that it remains finite for bounded waiting nets) is given in full in Section 3, with the decidability corollaries following directly. The strict expressiveness result over TPNs (via timed language equivalence) is established in Section 4 by exhibiting a concrete timed language accepted by a waiting net but not by any TPN, together with the formal proof. We can add one-sentence pointers to these sections in a revised abstract if the editor prefers. revision: partial

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines waiting nets via new semantics that decouple time measurement from control, then constructs a finite state class graph explicitly for the bounded case. Decidability of reachability/coverability follows as a direct consequence of that construction. The strict expressiveness claim over TPNs is obtained by exhibiting timed languages that waiting nets can realize but TPNs cannot. No equations reduce a claimed result to a fitted parameter or to a self-citation chain; the central arguments rest on the freshly stated operational rules and the standard state-class technique adapted to the new firing condition. The known undecidability of stopwatch extensions is invoked only as contrast and is not load-bearing for the positive results.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the newly introduced semantics of waiting nets and the explicit restriction to bounded nets. No numerical free parameters appear. The model itself is the main invented entity.

axioms (1)
  • domain assumption The waiting net is bounded
    The finite state-class graph and decidability statements are given only under this restriction.
invented entities (1)
  • Waiting net no independent evidence
    purpose: Timed Petri-net variant that decouples time measurement from full preset availability
    New model defined in the paper; no independent evidence supplied beyond the definition itself.

pith-pipeline@v0.9.0 · 5755 in / 1239 out tokens · 27195 ms · 2026-05-24T11:09:48.143692+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages

  1. [1]

    A Study of the Recoverability of Computing Sys tems

    Merlin PM. A Study of the Recoverability of Computing Sys tems. Ph.D. thesis, University of California, Irvine, CA, USA, 1974

    work page 1974

  2. [2]

    Elementary Net Systems

    Esparza J. Decidability and Complexity of Petri Net Prob lems - An Introduction. In: Proc. of Petri Nets, volume 1491 of LNCS. 1998 pp. 374–428. doi:10.1007/3-540-65306-6 20

    work page doi:10.1007/3-540-65306-6 1998

  3. [3]

    The Covering and Boundedness Problems for V ec tor Addition Systems

    Rackoff C. The Covering and Boundedness Problems for V ec tor Addition Systems. Theor . Comput. Sci.,

    work page

  4. [4]

    doi:10.1016/0304-3975(78)90036-1

    6(2):223–231. doi:10.1016/0304-3975(78)90036-1

    work page doi:10.1016/0304-3975(78)90036-1

  5. [5]

    An Algorithm for the General Petri Net Reachabili ty Problem

    Mayr E. An Algorithm for the General Petri Net Reachabili ty Problem. In: Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwa ukee, Wisconsin, USA. ACM, 1981 pp. 238–246. doi:10.1145/800076.802477

    work page doi:10.1145/800076.802477 1981

  6. [6]

    On Time Petri Nets

    Popova-Zeugmann L. On Time Petri Nets. J. Inf. Process. Cybern., 1991. 27(4):227–244

    work page 1991

  7. [7]

    Modeling and V erification of Time De pendent Systems Using Time Petri Nets

    Berthomieu B, Diaz M. Modeling and V erification of Time De pendent Systems Using Time Petri Nets. IEEE Trans. Software Eng., 1991. 17(3):259–273. doi:10.1109/32.75415

    work page doi:10.1109/32.75415 1991

  8. [8]

    Model Checking of Time Petri Nets Using the State Class Timed Automaton

    Lime D, Roux O. Model Checking of Time Petri Nets Using the State Class Timed Automaton. Discret. Event Dyn. Syst. , 2006. 16(2):179–205. doi:10.1007/s10626-006-8133-9

    work page doi:10.1007/s10626-006-8133-9 2006

  9. [9]

    Analysis of asynchronous concurrent sys tems by timed Petri nets

    Ramchandani C. Analysis of asynchronous concurrent sys tems by timed Petri nets. Ph.D. thesis, Mas- sachusetts Institute of Technology, 1974

    work page 1974

  10. [10]

    Timed Petri Nets and BQOs

    Abdulla P , Nyl´ en A. Timed Petri Nets and BQOs. In: ICA TPN. LNCS 2075, p.53-70, 2001

    work page 2075

  11. [11]

    Weak Time Petri Nets Strike Back! In: Proc

    Reynier P , Sangnier A. Weak Time Petri Nets Strike Back! In: Proc. of CONCUR 2009, volume 5710 of LNCS. 2009 pp. 557–571. doi:10.1007/978-3-642-04081-8 37

    work page doi:10.1007/978-3-642-04081-8 2009

  12. [12]

    On Non-Decidabili ty of Reachability for Timed-Arc Petri Nets

    Ruiz VV , Gomez FC, Frutos-Escrig Dd. On Non-Decidabili ty of Reachability for Timed-Arc Petri Nets. In: PNPM. IEEE Computer Society, 1999 pp. 188. doi:10.1109/ PNPM.1999.796565

    work page arXiv 1999

  13. [13]

    Decidable Classes of Un bounded Petri Nets with Time and Urgency

    Akshay S, Genest B, H´ elou¨ et L. Decidable Classes of Un bounded Petri Nets with Time and Urgency. In: Kordon F, Moldt D (eds.), Application and Theory of Petri Nets and Concurrency - 37th International Conference, Petri Nets 2016, Toru´ n, Poland, June 19-24, 20 16. Proceedings, volume 9698 of Lecture Notes in Computer Science . Springer, 2016 pp. 301–...

    work page doi:10.1007/978-3-319-3908 2016

  14. [14]

    V erification o f Timed-Arc Petri Nets

    Jacobsen L, Jacobsen M, Møller MH, Srba J. V erification o f Timed-Arc Petri Nets. In: SOFSEM’11. LNCS 6543, p.46-72, 2011 . doi:10.1007/978-3-642-18381-2 4

    work page doi:10.1007/978-3-642-18381-2 2011

  15. [15]

    Modelling time in Petri nets

    Bowden F. Modelling time in Petri nets. In: Proc. Second Australia-Japan Workshop on Stochastic Models. 1996

    work page 1996

  16. [16]

    Reachability P roblems and Abstract State Spaces for Time Petri Nets with Stopwatches

    Berthomieu B, Lime D, Roux O, V ernadat F. Reachability P roblems and Abstract State Spaces for Time Petri Nets with Stopwatches. Discret. Event Dyn. Syst. , 2007. 17(2):133–158. doi:10.1007/s10626-006- 0011-y

    work page doi:10.1007/s10626-006- 2007

  17. [17]

    Thegreatestcommondivisor:acasestudy for program extraction from classical proofs

    Cassez F, Larsen K. The Impressive Power of Stopwatches . In: Palamidessi C (ed.), CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, P A, USA, August 22-25, 2000, Pro- ceedings, volume 1877 of Lecture Notes in Computer Science. Springer, 2000 pp. 138–152. doi:10.1007/3- 540-44618-4 12

    work page doi:10.1007/3- 2000

  18. [18]

    Timed State Spac e Analysis of Real-Time Preemptive Systems

    Bucci G, Fedeli A, Sassoli L, Vicario E. Timed State Spac e Analysis of Real-Time Preemptive Systems. IEEE Trans. Software Eng., 2004. 30(2):97–111. doi:10.1109/TSE.2004.1265815. 96 L. H´ elou¨ et and P . Agrawal/ W aiting Nets: State Classes and Taxonomy

    work page doi:10.1109/tse.2004.1265815 2004

  19. [19]

    Timed Petri Nets with Reset fo r Pipelined Synchronous Circuit Design

    Parrot R, Briday M, Roux O. Timed Petri Nets with Reset fo r Pipelined Synchronous Circuit Design. In: Buchs D, Carmona J (eds.), Application and Theory of Petri Ne ts and Concurrency - 42nd International Conference, Petri Nets 2021, Virtual Event, June 23-25, 202 1, Proceedings, volume 12734 of Lecture Notes in Computer Science . Springer, 2021 pp. 55–75...

    work page doi:10.1007/978-3-030-76983- 2021

  20. [20]

    Complexity of Some Probl ems in Petri Nets

    Jones N, Landweber LH, Lien YE. Complexity of Some Probl ems in Petri Nets. Theor . Comput. Sci.,

    work page

  21. [21]

    doi:10.1016/0304-3975(77)90014-7

    4(3):277–299. doi:10.1016/0304-3975(77)90014-7

    work page doi:10.1016/0304-3975(77)90014-7

  22. [22]

    https://doi.org/10.1007/3-540-44988-4 3

    Frutos-Escrig Dd, Ruiz V , Marroqu´ ın Alonso O. Decidab ility of Properties of Timed-Arc Petri Nets. In: Nielsen M, Simpson D (eds.), Application and Theory of Petri Nets 2000, 21st International Conference, ICA TPN 2000, Aarhus, Denmark, June 26-30, 2000, Proceeding , volume 1825 of Lecture Notes in Com- puter Science. Springer, 2000 pp. 187–206. doi:10...

    work page doi:10.1007/3-540-44988-4 2000

  23. [23]

    Waiting Nets

    H´ elou¨ et L, Agrawal P . Waiting Nets. In: Bernardinello L, Petrucci L (eds.), Proc. of PETRI NETS 2022, volume 13288 of LNCS. 2022 pp. 67–89. doi:10.1007/978-3-031-06653-5 4

    work page doi:10.1007/978-3-031-06653-5 2022

  24. [24]

    Timing Assumptions and V erification of Finite-S tate Concurrent Systems

    Dill D. Timing Assumptions and V erification of Finite-S tate Concurrent Systems. In: Sifakis J (ed.), Automatic V erification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings, volume 407 of Lecture Notes in Computer Science. Springer, 1989 pp. 197–212. doi:10.1007/3-540-52148-8 17

    work page doi:10.1007/3-540-52148-8 1989

  25. [25]

    A Theory of Timed Automata

    Alur R, Dill D. A Theory of Timed Automata. Theor . Comput. Sci., 1994. 126(2):183–235

    work page 1994

  26. [26]

    Structural translation from Time Petr i Nets to Timed Automata

    Cassez F, Roux O. Structural translation from Time Petr i Nets to Timed Automata. Journal of Systems and Software, 2006. 79(10):1456–1468. doi:10.1016/j.jss.2005.12.021

    work page doi:10.1016/j.jss.2005.12.021 2006

  27. [27]

    The expres sive power of Time Petri nets

    B´ erard B, Cassez F, Haddad S, Lime D, Roux OH. The expres sive power of Time Petri nets. TCS, 2013. 474:1–20. doi:10.1016/j.tcs.2012.12.005

    work page doi:10.1016/j.tcs.2012.12.005 2013

  28. [28]

    Time Petri Nets for Analyzing and V erifying Time Dependent Commu- nication Protocols

    Menasche M, Berthomieu B. Time Petri Nets for Analyzing and V erifying Time Dependent Commu- nication Protocols. In: Rudin H, West CH (eds.), Protocol Sp ecification, Testing, and V erification, III, Proceedings of the IFIP WG 6.1 Third International Workshop on Protocol Specification, Testing and V er- ification, organized by IBM Research, R¨ uschlikon, Swit...

    work page 1983

  29. [29]

    Analyse des r´ eseaux de Petri temporis´ es e t Application aux syst` emes distribu´ es

    Menasche M. Analyse des r´ eseaux de Petri temporis´ es e t Application aux syst` emes distribu´ es. Ph.D. thesis, Univ. Paul Sabatier, Toulouse, 1982

    work page 1982

  30. [30]

    Timed Automata: Semantics, Algorith ms and Tools

    Bengtsson J, Yi W . Timed Automata: Semantics, Algorith ms and Tools. In: Desel J, Reisig W , Rozenberg G (eds.), Lectures on Concurrency and Petri Nets, Advances i n Petri Nets, volume 3098 of Lecture Notes in Computer Science . Springer, 2003 pp. 87–124. doi:10.1007/978-3-540-27755 -2 3

    work page doi:10.1007/978-3-540-27755 2003

  31. [31]

    Complexity Results for 1 -Safe Nets

    Cheng A, Esparza J, Palsberg J. Complexity Results for 1 -Safe Nets. Theor . Comput. Sci., 1995. 147(1- 2):117–136. doi:10.1016/0304-3975(94)00231-7

    work page doi:10.1016/0304-3975(94)00231-7 1995

  32. [32]

    Removing epsilon-Transit ions in Timed Automata

    Diekert V , Gastin P , Petit A. Removing epsilon-Transit ions in Timed Automata. In: Reischuk R, Morvan M (eds.), STACS 97, 14th Annual Symposium on Theoretical Asp ects of Computer Science, L¨ ubeck, Germany, February 27 - March 1, 1997, Proceedings, volume 12 00 of Lecture Notes in Computer Science. Springer, 1997 pp. 583–594. doi:10.1007/BFb0023491

    work page doi:10.1007/bfb0023491 1997

  33. [33]

    Combining free choiceand time in Petri nets

    Akshay S, H´ elou¨ et L, Phawade R. Combining free choiceand time in Petri nets. J. Log. Algebraic Methods Program., 2020. 110. doi:10.1016/j.jlamp.2018.11.006

    work page doi:10.1016/j.jlamp.2018.11.006 2020

  34. [34]

    Timed Petri-Nets for Modelling and Analysing Protocols with Real-Time Characteristics

    Walter B. Timed Petri-Nets for Modelling and Analysing Protocols with Real-Time Characteristics. In: Proc. of PSTV . 1983 pp. 149–159. https://dblp.org/rec/conf/ifip/Walter83.bib. L. H´ elou¨ et and P . Agrawal/ W aiting Nets: State Classes and Taxonomy 97

    work page 1983

  35. [35]

    Decidability Questions for Petri Nets

    Hack M. Decidability Questions for Petri Nets. Ph.D. th esis, M.I.T., MIT, CA, USA, 1976

    work page 1976

  36. [36]

    A Forward Reacha bility Algorithm for Bounded Timed-Arc Petri Nets

    David A, Jacobsen L, Jacobsen M, Srba J. A Forward Reacha bility Algorithm for Bounded Timed-Arc Petri Nets. In: SSV’12, volume 102 of EPTCS. 2012 pp. 125–140. doi:10.4204/EPTCS.102.12

    work page doi:10.4204/eptcs.102.12 2012

  37. [37]

    Fourier-Motzkin Elimination and I ts Dual

    Dantzig G, Eaves BC. Fourier-Motzkin Elimination and I ts Dual. J. Comb. Theory, Ser . A , 1973. 14(3):288–297. doi:10.1016/0097-3165(73)90004-6

    work page doi:10.1016/0097-3165(73)90004-6 1973

  38. [38]

    Comparison of the Expressiveness of Timed Automata and Time Petri Nets

    B´ erard B, Cassez F, Haddad S, Lime D, Roux O. Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In: FORMA TS, volume 3829 of Lecture Notes in Computer Science . 2005 pp. 211–225. doi:10.1007/11603009 17

    work page doi:10.1007/11603009 2005

  39. [39]

    Timed Petri nets and time d automata: On the discriminating power of Zeno sequences

    Bouyer P , Haddad S, Reynier P A. Timed Petri nets and time d automata: On the discriminating power of Zeno sequences. Inf. Comput., 2008. 206(1):73–107. doi:10.1016/j.ic.2007.10.004

    work page doi:10.1016/j.ic.2007.10.004 2008

  40. [40]

    When are ti med automata weakly timed bisimilar to time Petri nets ? Theoretical Computer Science, 2008

    B´ erard B, Cassez F, Haddad S, Lime D, Roux OH. When are ti med automata weakly timed bisimilar to time Petri nets ? Theoretical Computer Science, 2008. 403(2-3):202–220. doi:10.1016/j.tcs.2008.03.030

    work page doi:10.1016/j.tcs.2008.03.030 2008

  41. [41]

    Bridging the gap betw een timed automata and bounded Time Petri Nets

    Berthomieu B, Peres F, V ernadat F. Bridging the gap betw een timed automata and bounded Time Petri Nets. In: FORMA TS’06, volume 4202 of LNCS. 2006 pp. 82–97. doi:10.1007/11867340 7

    work page doi:10.1007/11867340 2006

  42. [42]

    Timed Petri Nets for Modelling and Analyzing P rotocols with Real-time Char- acteristics

    Walter B. Timed Petri Nets for Modelling and Analyzing P rotocols with Real-time Char- acteristics. In: Protocol Specification, Testing, and V eri fication, III. 1983 pp. 149–159. https://dblp.org/rec/conf/ifip/Walter83.bib. A. Fourier-Motzkin elimination Fourier-Motzkin Elimination [35] is a method to eliminate a set of variables V ⊆ X from a system of lin...

    work page 1983

  43. [43]

    N0), v′ 0(t) = min( v(t) + d1, β (t)) if t ∈ enabled(M0) \ FullyEnabled(M0) and v′ 0(t) = ⊥ otherwise

    where v′ 0(t) = v0(t) + d1 if t ∈ FullyEnabled(M0. N0), v′ 0(t) = min( v(t) + d1, β (t)) if t ∈ enabled(M0) \ FullyEnabled(M0) and v′ 0(t) = ⊥ otherwise. The valuation v1 is computed according to timed moves rules, which means that v1(t) =      0 if t ∈↑ enabled(M1, t 1) , v ′ 0(t) if t ∈ Enabled(M0) ∩ Enabled(M1) ⊥ otherwise Now, since ρ = ( M0.N 0,...

    work page