On-the-fly TCTL model checking for time Petri nets

DOI10.1016/J.TCS.2009.06.019MaRDI QIDQ732013zbMATH OpenOpenAlexFDO

Authors Rachid Hadjidj, H. Boucheneb

Publication date 9 October 2009

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

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

zbMATH Keywords

time Petri netsstate class methodstate space abstractionsTCTL model checking

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
• CTL* model checking for time Petri nets
• scientific article; zbMATH DE number 1439078
• Model checking of time Petri nets using the state class timed automaton
• Applications and Theory of Petri Nets 2004
• scientific article; zbMATH DE number 1361125
• Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL}
• Tools and Algorithms for the Construction and Analysis of Systems
• A CTL* Model Checker for Petri Nets

Cites work

• scientific article; zbMATH DE number 177824 (Why is no real title available?)
• scientific article; zbMATH DE number 1956600 (Why is no real title available?)
• scientific article; zbMATH DE number 1755138 (Why is no real title available?)
• scientific article; zbMATH DE number 1755150 (Why is no real title available?)
• A space-efficient on-the-fly algorithm for real-time model checking
• CTL* model checking for time Petri nets
• Efficient verification of a class of time Petri nets using linear programming
• Formal Modeling and Analysis of Timed Systems
• Lectures on Concurrency and Petri Nets
• Model-checking for real-time systems
• Model-checking in dense real-time
• Parametric model-checking of stopwatch Petri nets
• Recoverability of Communication Protocols--Implications of a Theoretical Study
• Structural translation from time Petri nets to timed automata
• The power of reachability testing for timed automata
• Timing Requirements for Time-Driven Systems Using Augmented Petri Nets

Cited in

(5)

• Relevant timed schedules/clock vectors for constructing time Petri net reachability graphs
• TCTL model checking of time Petri nets
• Model checking of time Petri nets using the state class timed automaton
• CTL* model checking for time Petri nets
• Timed aggregate graph: a finite graph preserving event- and state-based quantitative properties of time Petri nets

Describes a project that uses

Uses Software

• Uppaal

This page was built for publication: On-the-fly \(TCTL\) 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 Q732013)