
doi: 10.1007/11603009_17
In this paper we consider the model of Time Petri Nets (TPN) where time is associated with transitions. We also consider Timed Automata (TA) as defined by Alur & Dill, and compare the expressiveness of the two models w.r.t. timed language acceptance and (weak) timed bisimilarity. We first prove that there exists a TA $\mathcal{A}$s.t. there is no TPN (even unbounded) that is (weakly) timed bisimilar to $\mathcal{A}$. We then propose a structural translation from TA to (1-safe) TPNs preserving timed language acceptance. Further on, we prove that the previous (slightly extended) translation also preserves weak timed bisimilarity for a syntactical subclass $\mathcal{T}_{syn}(\leq,\geq)$of TA. For the theory of TPNs, the consequences are: 1) TA, bounded TPNs and 1-safe TPNs are equally expressive w.r.t. timed language acceptance; 2) TA are strictly more expressive than bounded TPNs w.r.t. timed bisimilarity; 3) The subclass $\mathcal{T}_{syn}(\leq,\geq)$, bounded and 1-safe TPNs “a la Merlin” are equally expressive w.r.t. timed bisimilarity.
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 43 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
