eighty-twenty

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?