Time Petri Nets introduce timing constraints on normal Petri Nets — not sharp constraints, intervals are given for each constraint.
- "boundedness" for TPNs undecidable
- "reachability" for bounded petri nets decidable
- SCG = ??
- region graph = ??
- untimed CTL* = ??
- reachability + time CTL model-checking is decidable (1994)
- so: talk on relation between the two models
- aim: structural translation; correctness proof — both achieved
- the translation permits use of existing efficient tools for analysing TAs, eg. uppaal
Future work: real case studies, perhaps with uppaal — and investigate expressiveness — can TAs be translated back to TPNs?