# zbMATH — the first resource for mathematics

When are timed automata weakly timed bisimilar to time Petri nets? (English) Zbl 1158.68029
Summary: We compare Timed Automata (TA) and Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is strictly included in the class of TA. It is thus natural to try and identify the subclass $$\mathcal{TA}^{wtb}$$ of TA equivalent to some TPN for the weak timed bisimulation relation. We give a characterization of this subclass and we show that the membership problem and the reachability problem for $$\mathcal{TA}^{wtb}$$ are PSPACE-complete. Furthermore we show that for a TA in $$\mathcal{TA}^{wtb}$$ with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential with respect to the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.

##### MSC:
 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) 68Q45 Formal languages and automata
##### Keywords:
time Petri nets; timed automata; weak timed bisimilarity
##### Software:
Kronos; Romeo; TINA; Uppaal2k
Full Text: