Translation from timed Petri nets with intervals on transitions to intervals on places (with urgency)
Marc Boyer · Electronic Notes in Theoretical Computer Science · 2002
stronger than the language inclusion 5 .The proof highlights a 1-bounded TLPN that could not be bisimulated by any TTPN 6 .Let us denote by the fact that a model is more powerful that another 7 .In [6], is is shown that ¬(TLPN TTPN).In [7], it is shown that the proof of [6] also gives ¬(TPPN TTPN).A construction from TTPN to TLPN gives TTPN TLPN, and a straightforward result is TPPN TLPN.That is to say, TLPN is the more powerful model, TTPN is not more powerful than TPPN, but the two could be incomparable.In this paper, we go a step further, showing that bounded TPPN are more powerful that 1-bounded TTPN, by building a translation from 1-bounded TTPN to TPPN 8 .The paper is organized as follows: Section 2 gives some definitions (multi-set, Petri net, timed bisimulation, TTPN and TPPN), Section 3 presents the translation, its core ideas (Subsection 3.1), some details (Subsection 3.2) and the bisimulation relation (Subsection 3.3).By lack of space, the proof itself is not given here.Then, Section 4 concludes. DefinitionsHere comes some definitions, on alphabets, multi-sets, Petri nets and statically timed Petri nets, their behaviors (expressed as a labeled timed transition systems) and weak timed bisimulation.Definition 2.1 (Alphabet) An alphabet A is a finite set such that, there exists a special (invisible) element λ ∈ A, and A ∩ R + = ∅ ( 9 ).Let A + def = A\ {λ} denote the set of visible actions.Definition 2.2 (Multi-set) Let X be a set, then µ : X → N is a multi-set over X, and X ⊕ denote the set of multi-sets over X.In this paper, we will only consider finite multi-sets, that is such that x∈X µ(x) is finite.On such sets, we could define |µ| = x∈X µ(x).As for sets, we can define x ∈ µ ⇐⇒ µ(x) = 0, the inclusion µ ⊂ µ ⇐⇒ ∀x : µ(x) ≤ µ (x), the union (µ ∪ µ )(x) = µ(x) + µ(x ), the intersection (µ ∩ µ )(x) = min(µ(x), µ (x)) and µ ⊂ µ ⇒ (µ\µ )(x) = µ(x)µ (x).If there exists an order ≤ on X, min(µ) def = min {i µ(i) = 0}.Finite multi-sets will