Model checking of time Petri nets using the state class timed automaton

DOI10.1007/s10626-006-8133-9zbMath1113.68068OpenAlexW2129140418MaRDI QIDQ859736

Didier Lime, Olivier H. Roux

Publication date: 18 January 2007

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

Full work available at URL: https://doi.org/10.1007/s10626-006-8133-9

zbMATH Keywords

Timed automataModel-checkingDense-time systemsTime Petri nets

Mathematics Subject Classification ID

Related Items (14)

Formal verification of real-time systems with preemptive scheduling ⋮ Modeling, simulation, estimation and boundedness analysis of discrete event systems ⋮ Waiting nets ⋮ Reconfigurable timed graphs for the design of optimal scheduling in uncertain environments based on transition-timed Petri net ⋮ Waiting Nets: State Classes and Taxonomy ⋮ Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets ⋮ A concurrency-preserving translation from time Petri nets to networks of timed automata ⋮ Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets ⋮ Symbolic unfolding of parametric stopwatch Petri nets ⋮ Combining free choice and time in Petri nets ⋮ Realizability of Schedules by Stochastic Time Petri Nets with Blocking Semantics ⋮ Approximated timed reachability graphs for the robust control of discrete event systems ⋮ Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques ⋮ Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets

Uses Software

• SENAC
• Kronos
• Uppaal

Cites Work

• Model-checking in dense real-time
• Symbolic model checking for real-time systems
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• Compositional specification of timed systems
• Applications and Theory of Petri Nets 2004
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking of time Petri nets using the state class timed automaton