On-the-fly \(TCTL\) model checking for time Petri nets

DOI10.1016/j.tcs.2009.06.019zbMath1186.68292OpenAlexW2056081080MaRDI QIDQ732013

Rachid Hadjidj, Hanifa 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)

Related Items (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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• The power of reachability testing for timed automata
• Efficient verification of a class of time Petri nets using linear programming
• CTL* model checking for time Petri nets
• Timing Requirements for Time-Driven Systems Using Augmented Petri Nets
• Recoverability of Communication Protocols--Implications of a Theoretical Study
• Model-checking for real-time systems
• Lectures on Concurrency and Petri Nets
• Formal Modeling and Analysis of Timed Systems
• A space-efficient on-the-fly algorithm for real-time model checking

This page was built for publication: On-the-fly \(TCTL\) model checking for time Petri nets