Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph

DOI10.1007/978-3-540-85778-5_20MaRDI QIDQ3543304zbMATH OpenOpenAlexFDO

Authors Louis-Marie Traonouez, Didier Lime, Olivier H. Roux

Publication date 2 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85778-5_20

zbMATH Keywords

parametersmodel-checkingstate-class graphtime Petri netsstopwatches

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Parametric model-checking of stopwatch Petri nets
• Applications and Theory of Petri Nets 2004
• Symbolic unfolding of parametric stopwatch Petri nets
• Symbolic unfolding of parametric stopwatch Petri nets
• Reachability problems and abstract state spaces for time Petri nets with stopwatches

Cites work

• scientific article; zbMATH DE number 1701759 (Why is no real title available?)
• Applications and Theory of Petri Nets 2004
• HyTech: A model checker for hybrid systems
• Model-checking for real-time systems
• Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph
• Parametric real-time reasoning
• Parametric timing analysis for real-time systems
• Reachability problems and abstract state spaces for time Petri nets with stopwatches
• Real-Time Model-Checking: Parameters everywhere

Cited in

(11)

• Expressiveness of Petri Nets with Stopwatches. Dense-time Part
• Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph
• Mean-payoff optimization in continuous-time Markov chains with parametric alarms
• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
• Post and pre-initialized stopwatch Petri nets: formal semantics and state space computation
• Parametric model-checking of stopwatch Petri nets
• Time based deadlock prevention for Petri nets
• Symbolic unfolding of parametric stopwatch Petri nets
• Symbolic unfolding of parametric stopwatch Petri nets
• Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving
• Liveness enforcement for production systems modeled by time Petri nets

Describes a project that uses

Uses Software

• HyTech

This page was built for publication: Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph

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