Parametric model-checking of stopwatch Petri nets

MaRDI QIDQ4929342zbMATH OpenFDO

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

Publication date 22 September 2010

Full work available at URL http://www.jucs.org/jucs_15_17/parametric_model_checking_of

zbMATH Keywords

model-checkingparametersstate-class graphstopwatchestime Petri nets

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 Time Petri Nets with Stopwatches Using the State-Class Graph
• Cost problems for parametric time Petri nets
• Symbolic unfolding of parametric stopwatch Petri nets
• Bounded parametric verification for distributed time Petri nets with discrete-time semantics
• scientific article; zbMATH DE number 6708300

Cited in

(23)

• Post and pre-initialized stopwatch Petri nets: formal semantics and state space computation
• Parametric verification: an introduction
• Symbolic unfolding of parametric stopwatch Petri nets
• Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques
• Parametric model checking with VerICS
• Bounded parametric verification for distributed time Petri nets with discrete-time semantics
• Formalising concurrent UML state machines using coloured Petri nets
• FAST verification of the class of stop-and-wait protocols modelled by coloured Petri nets
• Expressiveness of Petri Nets with Stopwatches. Dense-time Part
• Parametric Language Analysis of the Class of Stop-and-Wait Protocols
• Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph
• Shrinking of time Petri nets
• Parameter synthesis for hierarchical concurrent real-time systems
• Symbolic unfolding of parametric stopwatch Petri nets
• Parametric schedulability analysis of a launcher flight control system under reactivity constraints
• Cost problems for parametric time Petri nets
• Reachability and liveness in parametric timed automata
• Parametric verification of weighted systems
• Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets
• Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving
• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
• On-the-fly TCTL model checking for time Petri nets
• \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability

Describes a project that uses

Uses Software

• HyTech

This page was built for publication: Parametric model-checking of stopwatch Petri nets

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