Reachability problems and abstract state spaces for time Petri nets with stopwatches

DOI10.1007/s10626-006-0011-yzbMath1134.93369OpenAlexW2021391928MaRDI QIDQ884758

Bernard Berthomieu, Olivier H. Roux, Didier Lime, François Vernadat

Publication date: 7 June 2007

Published in: Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10626-006-0011-y

zbMATH Keywords

ApproximationDecidabilityReachabilityReal-time systems modeling and verificationState classesStopwatchesTime Petri Nets

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65) Attainable sets, reachability (93B03)

Related Items (16)

Interpreted synchronous extension of time Petri nets. Definition, semantics and formal analysis ⋮ Formal verification of real-time systems with preemptive scheduling ⋮ Spatial determinism for a freeZ²-action ⋮ Waiting nets ⋮ Shrinking of time Petri nets ⋮ Time distance-based computation of the \textit{DBM} over-approximation of preemptive real-time systems ⋮ Symbolic State Space of Stopwatch Petri Nets with Discrete-Time Semantics (Theory Paper) ⋮ Waiting Nets: State Classes and Taxonomy ⋮ Growth-type invariants for \(\mathbb Z^{d}\) subshifts of finite type and arithmetical classes of real numbers ⋮ Zero entropy systems ⋮ Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph ⋮ Symbolic unfolding of parametric stopwatch Petri nets ⋮ “Metric” complexity for weakly chaotic systems ⋮ Topological pressure dimension for almost additive potentials ⋮ Post and pre-initialized stopwatch Petri nets: formal semantics and state space computation ⋮ A game approach to the parametric control of real-time systems

Uses Software

• Romeo
• TINA
• NewPolka

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• Complexity of some problems in Petri nets
• CTL* model checking for time Petri nets
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Applications and Theory of Petri Nets 2004
• Computer Aided Verification

This page was built for publication: Reachability problems and abstract state spaces for time Petri nets with stopwatches