Model checking of time Petri nets using the state class timed automaton
From MaRDI portal
Recommendations
- State space computation and analysis of Time Petri Nets
- TCTL model checking of time Petri nets
- Structural translation from time Petri nets to timed automata
- On-the-fly TCTL model checking for time Petri nets
- Specification and model checking of temporal properties in time Petri nets and timed automata
Cites work
- Compositional specification of timed systems
- Decidability of properties of timed-arc Petri nets
- scientific article; zbMATH DE number 4209631 (Why is no real title available?)
- scientific article; zbMATH DE number 3177183 (Why is no real title available?)
- Kronos: A verification tool for real-time systems
- Model-checking in dense real-time
- Specification and model checking of temporal properties in time Petri nets and timed automata
- State class constructions for branching analysis of time Petri nets
- Symbolic model checking for real-time systems
- Timed Petri nets and BQOs
- Uppaal in a nutshell
Cited in
(34)- Modeling, simulation, estimation and boundedness analysis of discrete event systems
- Waiting nets
- A state class construction for computing the intersection of time Petri nets languages
- Symbolic unfolding of parametric stopwatch Petri nets
- Combining free choice and time in Petri nets
- Approximated timed reachability graphs for the robust control of discrete event systems
- Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques
- CTL* model checking for time Petri nets
- Interval timed coloured Petri net: efficient construction of its state class space preserving linear properties
- Realizability of schedules by stochastic time Petri nets with blocking semantics
- Structural translation from time Petri nets to timed automata
- Model Checking Bounded Prioritized Time Petri Nets
- scientific article; zbMATH DE number 5368984 (Why is no real title available?)
- Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets
- Towards building the state class graph of the TSPN model
- A more efficient time Petri net state space abstraction useful to model checking timed linear properties
- TCTL model checking of time Petri nets
- Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL}
- State class constructions for branching analysis of time Petri nets
- 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
- Timed aggregate graph: a finite graph preserving event- and state-based quantitative properties of time Petri nets
- Blending timed formal models with clock transition systems
- State space computation and analysis of Time Petri Nets
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
- Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets
- Specification and model checking of temporal properties in time Petri nets and timed automata
- Using zone graph method for computing the state space of a time Petri net
- Reconfigurable timed graphs for the design of optimal scheduling in uncertain environments based on transition-timed Petri net
- Waiting Nets: State Classes and Taxonomy
- A state class based controller synthesis approach for time Petri nets
- An extremum timed extended reachability graph for temporal analysis of time Petri nets
- On-the-fly TCTL model checking for time Petri nets
- Formal verification of real-time systems with preemptive scheduling
This page was built for publication: Model checking of time Petri nets using the state class timed automaton
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q859736)
