On-the-fly TCTL model checking for Time Petri Nets using state class graphs

This paper shows how to efficiently model check a subclass of TCTL properties for the TPN model, using the so called state class method. The idea is to put the TPN model under analysis in parallel with a special TPN to capture relevant time events to verify a timed property. The special TPN, we call...

Full description

Saved in:
Bibliographic Details
Main Authors: Hadjidj, R., Boucheneb, H.
Format: Conference Proceeding
Language:English
Subjects:
Automata
Clocks
Explosions
Fires
Logic
Petri nets
Real time systems
Safety
State-space methods
Timing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper shows how to efficiently model check a subclass of TCTL properties for the TPN model, using the so called state class method. The idea is to put the TPN model under analysis in parallel with a special TPN to capture relevant time events to verify a timed property. The special TPN, we call alarm-clock, has two transitions, with special firing priorities, which can be set to fire at special moments. The verification of a timed property is based on a forward on-the-fly exploration technique, augmented with an abstraction by inclusion to further attenuate the state explosion problem. We prove the decidability of our verification technique for bounded TPN models and give some experimental results to show the effectiveness of our verification technique
ISSN:1550-4808
2374-8567
DOI:10.1109/ACSD.2006.18