Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Waiting Nets: State Classes and Taxonomy

Loïc Hélouët, Pranay Agrawal

TL;DR

Waiting nets decouple time measurement from control in time Petri nets by introducing a separate control layer and clocks attached to transitions. The authors define a precise semantics, prove that bounded waiting nets admit a finite state class graph (SCG), and show reachability and coverability are decidable (PSPACE-complete) for bounded nets. They establish that waiting nets are strictly more expressive than standard TPNs and compare them to timed automata and other time-Petri-net variants, including results with non-injective labeling and silent transitions. The work provides a solid abstraction framework (domains and canonical forms) that preserves timing information while enabling finite-state analysis, with implications for modeling and verifying cyber-physical systems under timing constraints.

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.

Waiting Nets: State Classes and Taxonomy

TL;DR

Waiting nets decouple time measurement from control in time Petri nets by introducing a separate control layer and clocks attached to transitions. The authors define a precise semantics, prove that bounded waiting nets admit a finite state class graph (SCG), and show reachability and coverability are decidable (PSPACE-complete) for bounded nets. They establish that waiting nets are strictly more expressive than standard TPNs and compare them to timed automata and other time-Petri-net variants, including results with non-injective labeling and silent transitions. The work provides a solid abstraction framework (domains and canonical forms) that preserves timing information while enabling finite-state analysis, with implications for modeling and verifying cyber-physical systems under timing constraints.

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.
Paper Structure (15 sections, 20 theorems, 18 equations, 10 figures, 1 table, 1 algorithm)

This paper contains 15 sections, 20 theorems, 18 equations, 10 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Waiting nets
  4. Reachability
  5. 1) Time progress:
  6. 2) Firing condition:
  7. 3) Substitution of variables:
  8. 4) Variable Elimination:
  9. 5) Addition of new constraints :
  10. Expressiveness
  11. Conclusion
  12. Fourier-Motzkin elimination
  13. Canonical forms : the Floyd-Warshall algorithm
  14. Difference Bound Matrices
  15. Proofs for Section \ref{['sec:reachability']}

Key Result

Proposition 4.8

For every run $\rho=(M_0.N_0,v_0) \dots (M_k.N_k,v_k)$ of $\mathcal{W}$ there exists a path $\pi$ of $SCG(\mathcal{W})$ such that $\rho$ and $\pi$ coincide.

Figures (10)

  • Figure 1: A TPN $a)$ a Timed Petri net $b)$, and a Waiting net $c)$
  • Figure 2: $a)$ Decoupled time and control in a waiting net. $b)$ ... with a timeout transition.
  • Figure 3: Operational semantics of Waiting Nets
  • Figure 4: A Waiting net, its initial domain, an equivalent DBM representation, and its constraint graph.
  • Figure 5: Upper bounds of transitions influence state classes of waiting Nets
  • ...and 5 more figures

Theorems & Definitions (40)

  • Definition 2.1: Timed Automaton
  • Definition 3.1
  • Definition 3.2: Enabled, Fully Enabled, Waiting transitions
  • Definition 3.3: Transition Firing
  • Definition 3.4: Configuration
  • Definition 3.5
  • Remark 3.6
  • Definition 4.1: State Class, Domain
  • Definition 4.2: Canonical Form
  • Definition 4.3: Projection
  • ...and 30 more