CTL* model checking for time Petri nets

DOI10.1016/J.TCS.2005.11.002MaRDI QIDQ2368992zbMATH OpenOpenAlexFDO

Authors H. Boucheneb, Rachid Hadjidj

Publication date 28 April 2006

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2005.11.002

zbMATH Keywords

Model checkingTime Petri netsAtomic state class graphCTL* propertiesState class spacesStrong state class graph

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

• TCTL model checking of time Petri nets
• On-the-fly \(TCTL\) model checking for time Petri nets
• Model checking of time Petri nets using the state class timed automaton
• scientific article; zbMATH DE number 1439078
• A more efficient time Petri net state space abstraction useful to model checking timed linear properties

Cites work

• scientific article; zbMATH DE number 177824 (Why is no real title available?)
• scientific article; zbMATH DE number 3622958 (Why is no real title available?)
• scientific article; zbMATH DE number 1956600 (Why is no real title available?)
• scientific article; zbMATH DE number 1755141 (Why is no real title available?)
• scientific article; zbMATH DE number 1755150 (Why is no real title available?)
• Applications and Theory of Petri Nets 2004
• Contraction of the ITCPN state space
• HyTech: A model checker for hybrid systems
• Recoverability of Communication Protocols--Implications of a Theoretical Study

Cited in

(14)

• On-the-fly \(TCTL\) model checking for time Petri nets
• Reachability problems and abstract state spaces for time Petri nets with stopwatches
• Relevant Timed Schedules / Clock Valuations for Constructing Time Petri Net Reachability Graphs
• TCTL model checking of time Petri nets
• Delay-dependent partial order reduction technique for real time systems
• Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets
• A more efficient time Petri net state space abstraction useful to model checking timed linear properties
• Contraction of the ITCPN state space
• Covering steps graphs of time Petri nets
• Simplification of CTL formulae for efficient model checking of Petri nets
• Model Checking Bounded Prioritized Time Petri Nets
• Relevant timed schedules/clock vectors for constructing time Petri net reachability graphs
• scientific article; zbMATH DE number 1755150 (Why is no real title available?)
• Partial order reduction for checking soundness of time workflow nets

Describes a project that uses

Uses Software

• HyTech

This page was built for publication: CTL* model checking for time Petri nets

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