Waiting Nets: State Classes and Taxonomy

DOI10.3233/FI-242167MaRDI QIDQ6189319zbMATH OpenOpenAlexWikidataFDO

Authors Loïc Hélouët, Pranay Agrawal

Publication date 8 February 2024

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2211.10540

zbMATH Keywords

Petri netsstate classestime

Mathematics Subject Classification ID

Computer science (68-XX)

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.

Cites work

• A theory of timed automata
• Bridging the Gap Between Timed Automata and Bounded Time Petri Nets
• Combining free choice and time in Petri nets
• Complexity of some problems in Petri nets
• Complexity results for 1-safe nets
• Decidable classes of unbounded Petri nets with time and urgency
• Formal Modeling and Analysis of Timed Systems
• Fourier-Motzkin elimination and its dual
• scientific article; zbMATH DE number 1696456 (Why is no real title available?)
• scientific article; zbMATH DE number 4209631 (Why is no real title available?)
• scientific article; zbMATH DE number 1302047 (Why is no real title available?)
• scientific article; zbMATH DE number 1755138 (Why is no real title available?)
• scientific article; zbMATH DE number 1759608 (Why is no real title available?)
• Model checking of time Petri nets using the state class timed automaton
• Reachability problems and abstract state spaces for time Petri nets with stopwatches
• Removing -transitions in timed automata
• The covering and boundedness problems for vector addition systems
• The expressive power of time Petri nets
• Timed Petri nets and timed automata: On the discriminating power of Zeno sequences
• Timed Petri nets with reset for pipelined synchronous circuit design
• Waiting nets
• Weak Time Petri Nets Strike Back!
• When are timed automata weakly timed bisimilar to time Petri nets?

This page was built for publication: Waiting Nets: State Classes and Taxonomy

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6189319)