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

DOI10.1016/J.TCS.2009.06.019zbMATH Open1186.68292OpenAlexW2056081080MaRDI QIDQ732013FDOQ732013

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

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

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)

Cites Work

• Lectures on Concurrency and Petri Nets
• Model-checking in dense real-time
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Model-checking for real-time systems
• Recoverability of Communication Protocols--Implications of a Theoretical Study
• The power of reachability testing for timed automata
• CTL* model checking for time Petri nets
• Structural translation from time Petri nets to timed automata
• Formal Modeling and Analysis of Timed Systems
• Title not available (Why is that?)
• Efficient verification of a class of time Petri nets using linear programming
• Timing Requirements for Time-Driven Systems Using Augmented Petri Nets
• Title not available (Why is that?)
• A space-efficient on-the-fly algorithm for real-time model checking

Cited In (2)

• Relevant timed schedules/clock vectors for constructing time Petri net reachability graphs
• Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets

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)