Structural Translation from Time Petri Nets to Timed Automata

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?