CTL* model checking for time Petri nets

DOI10.1016/J.TCS.2005.11.002zbMATH Open1088.68101OpenAlexW1997427041MaRDI QIDQ2368992FDOQ2368992

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

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

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)

Cites Work

• HyTech: A model checker for hybrid systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Recoverability of Communication Protocols--Implications of a Theoretical Study
• Applications and Theory of Petri Nets 2004
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Contraction of the ITCPN state space

Cited In (14)

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

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)