Several timed process calculi have been proposed in the literature, which mainly differ for the way in which delays are represented. In particular, a distinction is made between integrated-time calculi, in which actions are durational, and orthogonal-time calculi, in which actions are instantaneous and delays are expressed separately. To reconcile the two approaches, in a previous work an encoding from the integratedtime calculus CIPA to the orthogonal-time calculus TCCS was defined, which preserves timed bisimilarity. To complete the picture, in this paper we consider the reverse translation, by examining the modifications to the two calculi that are needed to make an encoding feasible, as well as the behavioral equivalence that is appropriate to preserve. We then introduce an encoding from modified TCCS to modified CIPA, and show that it can only preserve the weak variant of timed bisimilarity.
Computing systems are characterized not only by their functional behavior, but also by their quantitative features. In particular, timing aspects play a fundamental role, as they describe the temporal evolution of system activities. This is especially true for real-time systems, which are considered correct only if the execution of their activities fulfills certain temporal constraints.
When modeling these systems, time is represented through nonnegative numbers. In the following, we refer to abstract time, in the sense that we use time as a parameter for expressing constraints about instants of occurrences of actions. Unlike physical time, abstract time permits simplifications that are convenient, on the conceptual side, to obtain tractable models.
Many timed process calculi have appeared in the literature. Among them, we
mention temporal CCS [
Moreover, for timed process calculi, there are several different interpretations of action execution, in terms of whether and when it can be delayed, such as: – Eagerness : actions must be performed as soon as they become enabled, i.e., without any delay, thereby implying that they are urgent. – Laziness : after getting enabled, actions can be delayed arbitrarily long before they are executed. – Maximal progress : enabled actions can be delayed arbitrarily long unless they are involved in synchronizations, in which case they are urgent.
In this paper, we focus on two different timed process calculi obtained by
suitably combining the time-related options mentioned above. More precisely,
the first calculus, TCCS [
In [
In this paper, we complete the previous expressiveness study by considering
the reverse encoding from TCCS processes to CIPA processes, which may also be
exploited for checking bisimilarity of TCCS processes more efficiently. As pointed
out at the end of [
The rest of the paper is organized as follows. In Sect. 2, we recall TCCS and CIPA. In Sect. 3, we discuss the main design decisions behind the reverse encoding. In Sect. 4, we define the reverse encoding and show that it preserves weak timed bisimilarity. Finally, in Sect. 5 we provide some concluding remarks. 2 2.1
We denote by A a nonempty set of visible actions – ranged over by a, b – and by A¯ = {a¯ | a ∈ A} the set of corresponding coactions such that a¯¯ = a for all a ∈ A. We use Act = A ∪ A¯ ∪ {τ } to indicate the set of all actions – ranged over by α, β – where τ is the invisible action.
We denote by Rel a set of action relabeling functions. Each such function ϕ : Act → Act satisfies ϕ(τ ) = τ and ϕ(a) = ϕ(a¯) for all a ∈ Act \ {τ }.
We denote by T = (T, , v) a time domain such that T ∩ Act = ∅, which is equipped with an associative operation possessing neutral element and a total order relation v satisfying t1 v t2 iff there exists t0 ∈ T such that t1 t0 = t2. Typical choices are T = N and T = R≥0, with the usual + and ≤.
Finally, we denote by Var a nonempty set of process variables – ranged over by X, Y – whose occurrences can be free or bound by “rec”. 2.2
We recall from [
P ::= 0 | α.P | (t).P | P + P | P |P | P \L | P [ϕ] | X | rec X : P stopped process action prefix delay prefix alternative composition parallel composition restriction relabeling process variable recursion where α ∈ Act , t ∈ N>0, L ⊆ A, ϕ ∈ Rel , and X ∈ Var . We denote by PTCCS the set of closed and guarded process terms of PLTCCS.
Process 0 can neither proceed with any action, nor proceed through time. Process α.P can perform instantaneous action α and then evolves into process P ; action α is urgent, hence time cannot progress before α is executed. Process (t).P evolves into process P after a delay equal to t.
Process P1 + P2 represents a nondeterministic choice between processes P1 and P2, with the choice being resolved depending on whether an action of P1 or P2 is executed first. Time does not resolve choices, in the sense that any initial passage of time common to P1 and P2 must be allowed without making the choice. Process P1|P2 describes the parallel composition of processes P1 and P2, α P1 −−→ P10
α P1 + P2 −−→ P10
α P1 −−→ P10
α P1|P2 −−→ P10|P2
α P2 −−→ P20
α P1 + P2 −−→ P20
α P2 −−→ P20
α
P1|P2 −−→ P1|P20 a a¯ P1 −−→ P10 P2 −−→ P20
τ P1|P2 −−→ P10|P20 α ¯ P −−→ P 0 α ∈/ L ∪ L
α P \L −−→ P 0\L
α P −−→ P 0
ϕ(α) P [ϕ] −−→ P 0[ϕ]
α P {rec X : P ,→ X} −−→ P 0
α rec X : P −−→ P 0 t (t).P −; P t (t + t0).P −; (t0).P
t P −; P 0
t+t0 (t0).P −; P 0 t t P1 −; P10 P2 −; P20
t P1 + P2 −; P10 + P20
t t P1 −; P10 P2 −; P20
t P1|P2 −; P10|P20
t P −; P 0
t P \L −; P 0\L
t P −; P 0
t P [ϕ] −; P 0[ϕ]
t P {rec X : P ,→ X} −; P 0
t rec X : P −; P 0 where any two complementary actions may synchronize thereby resulting in a τ action; also in this case, any initial passage of time must be permitted.
Process P \L behaves as process P except for actions in L ∪ L¯, which are forbidden; this operator is useful to force synchronizations between complementary actions. Process P [ϕ] behaves as process P , with the difference that every performed action is transformed via ϕ; this operator allows processes with different actions to communicate. Finally, rec X : P represents a recursive process, which behaves as process P in which every free occurrence of X is replaced by rec X : P itself; the resulting process will be denoted by P {rec X : P ,→ X}.
Following [
A notion of weak bisimilarity for TCCS was studied in [
a – ==⇒ = ==⇒−−→==⇒.
αˆ αˆ α – ==⇒ = ==⇒ if α = τ , ==⇒ = ==⇒ if α 6= τ .
t t1 tn – ==⇒ = ==⇒−;==⇒ · · · ==⇒−;==⇒ where t = P1≤i≤n ti, n ∈ N≥1. Definition 2. A symmetric relation B over PTCCS is a weak timed bisimulation iff, whenever (P1, P2) ∈ B, then for all actions α ∈ Act and delays t ∈ N>0: – For each P1 −−α→ P10 there exists P2 ==αˆ⇒ P20 such that (P10, P20) ∈ B. – For each P1 −t; P10 there exists P2 ==t⇒ P20 such that (P10, P20) ∈ B. P1 ≈TCCS P2 iff (P1, P2) is contained in a weak timed bisimulation. 2.3
We recall from [
Q ::= nil | a.Q | wait t.Q | Q + Q | Q|Q | Q\L | Q[ϕ] | X | rec X : Q inactive process durational action prefix waiting prefix alternative composition parallel composition restriction relabeling process variable recursion where a ∈ Act \ {τ }, t ∈ N>0, L ⊆ A, ϕ ∈ Rel , and X ∈ Var . We denote by PCIPA the set of closed and guarded process terms of PLCIPA.
Process nil cannot proceed with any action, but can let time pass. Process a.Q can perform urgent action a and evolves into process Q after the execution of a has finished; all occurrences of an action are assumed to have the same duration, which is established by a function Δ : (Act \{τ }) → N>0 such that Δ(a¯) = Δ(a). Process wait t.Q waits for time t and then becomes process Q. All the other operators work as expected, with the additional constraints that each relabeling function ϕ must preserve durations, i.e., Δ(ϕ(a)) = Δ(a) for all a ∈ Act \ {τ }, and any pair of actions a and a¯ can synchronize only if they start at the same time, yielding a τ action with the same duration as the two original actions.
Following [
α@t K1|K2 −−→ K10|K2 d
α@t α0@t0 K2 −−→ K20 ¬(K1 −−→ K10 ∧ t0 < t) d d0
α@t K1 + K2 −−→ K20
d α@t α0@t0 K2 −−→ K20 ¬(K1 −−→ K10 ∧ t0 < t) d d0
α@t K1|K2 −−→ K1|K20
d
a¯@t K2 −−→ K20
d τ@t K1|K2 −−→ K10|K20 d
α@t ¯ K −−→ K0 α ∈/ L ∪ L d
α@t K\L −−→ K0\L
d
K0[ϕ]
α@t t ⇒ Q{rec X : Q ,→ X} −−→ K0
d α@t t ⇒ rec X : Q −−→ K0 d K ::= t ⇒ nil | t ⇒ a.Q | t ⇒ wait t0.Q | t ⇒ rec X : Q |
K + K | K|K | K\L | K[ϕ]
α@t
In this setting, any transition is of the form K −−→ K0, meaning that K ∈ KP
d
performs an action of name α ∈ Act that starts at time t ∈ N≥0 and has duration
d ∈ N>0, after which evolves to K0 ∈ KP. The transition relation is defined in
Table 2, where negative premises are present as in [
A notion of weak bisimilarity for CIPA was studied in [
K1 ≈CIPA K2 iff (K1, K2) is contained in a weak timed bisimulation. Moreover, Q1 ≈CIPA Q2 iff (0 ⇒ Q1, 0 ⇒ Q2) is contained in a weak timed bisimulation.
Although in the clause α = τ it may be t0 6= t and d0 6= d, possible subsequent visible actions must start at the same time in both processes for ≈CIPA to hold. 3
In [
The first issue is related to the range of values that can be used in CIPA to express action durations. In TCCS, it is possible to describe both timed processes and untimed ones. Consider for example the untimed TCCS process a.b.0. This cannot be translated into a reasonably corresponding CIPA process for the very simple reason that actions a and b are instantaneous, but CIPA does not allow zero durations. Moreover, due to instantaneous actions, TCCS processes may exhibit Zeno behaviors, which are not possible in CIPA. For instance, the timed TCCS process (t1).a.rec X : (b.X + c.(t2).0) may perform, after time t1 and action a, an arbitrary (even infinite) number of actions b at the same time. These problems can be straightforwardly solved by admitting zero durations in CIPA through an extended duration function Δ : (Act \ {τ }) → N.
The second issue that we address is timelock. In a TCCS process, time does not solve choices; indeed, the operational rules for alternative and parallel composition allow time to pass only if all the subprocesses do so. As a consequence, a local timelock always implies a global timelock, which may in turn determine a deadlock. By contrast, in CIPA timelock cannot occur unless there is a deadlock, because time passing is associated with action execution and explicit waiting. Consider the TCCS process 0+(t).0 and the ideally corresponding CIPA process nil + wait t.nil; the former process cannot let time pass, while the latter process can. The same would happen with (a.0)\{a} + (t).0 and (a.nil)\{a} + wait t.nil.
To avoid timelocks due to the stopped process 0, we replace it with the
inactive process 0 introduced in [
Note that this modification does not limit the expressive power of the calculi. Suppose that a process P is made out of three subprocesses P1, P2, P3 composed in parallel, such that P1 has action a and the other two have action a¯, but only P1 and P2 have to synchronize on a and a¯. Normally, one would write (P1|P2)\{a}|P3, but this is forbidden by the revised syntax. However, the same effect can be obtained through (P1[ϕ]|P2[ϕ]|P3)\{b}, where relabeling function ϕ maps a to a fresh action b not occurring in any of the three subprocesses. 3.2
One of the major design decisions about the translation of (modified) TCCS into (modified) CIPA is how to assign durations to actions. In principle, it is desirable to be able to associate a suitable nonzero duration with every visible action occurring in a TCCS process that is not untimed. Unfortunately, in most cases this is not possible, as we now show.
Consider the TCCS process a.(t1).b.(t2).0. In this case, it is natural to
interpret delay t1 as the duration of a and delay t2 as the duration of b, thus
considering the occurrence of an instantaneous visible action of TCCS as the beginning
of the corresponding durational action of CIPA (initial view ). In the TCCS
process (t1).a.(t2).b.0, the durations are as before, provided that the occurrence of
an instantaneous visible action is considered as the end of the corresponding
durational action (final view ). Notice that, if a = b but t1 6= t2, the translation
into a reasonably corresponding CIPA process would not be possible, unless, as
noted in [
Let us now examine the case in which there is not a precise pairing between actions and delays, like, e.g., in the TCCS process (t1).a.(t2).0. In this scenario, the duration of a can be either t1 or t2, but in any case a waiting is necessary to account for the delay that is not associated with a. The situation is even more complicated if we consider the TCCS process a.(t1).(t2).b.0. One option is to interpret t1 + t2 as the duration of a (initial view), with b having duration 0. The dual option is to interpret t1 + t2 as the duration of b (final view), with a having duration 0. In any case, the definition of the encoding would become technically involved, especially in the presence of recursion, due to the necessity of performing some lookahead. Moreover, there seems not to be any strong reason for choosing one option rather than the other.
Yet another option is to interpret t1 as the duration of a (initial view) and t2 as the duration of b (final view). This mixed option should be discarded because it disrupts equivalence preservation of the encoding. Indeed, the considered process is equivalent to the TCCS process a.(t2).(t1).b.0, while, under the assumption t1 6= t2, the two corresponding CIPA processes are not equivalent to each other, because the a-transition of duration t1 in the first CIPA process cannot be matched by the a-transition of duration t2 of the second CIPA process.
Summing up, on the one hand there are TCCS delays that cannot be associated with any visible action, and hence have to be translated into CIPA waitings. On the other hand, it is not always possible to assign a nonzero duration to every TCCS visible action. In particular, this is impossible in the case of untimed TCCS processes. In this respect, it is also worth reminding that the two untimed TCCS processes a.0|b.0 and a.b.0 + b.a.0 are always equivalent under the interleaving view of concurrency, while the two ideally corresponding CIPA processes a.nil|b.nil and a.b.nil + b.a.nil are equivalent to each other only if both a and b have duration zero.
As a consequence, for the sake of simplicity, uniformity, and semantics preservation, when encoding TCCS into CIPA we proceed as follows: – Every TCCS action a will be translated into a CIPA action a with Δ(a) = 0. – The TCCS action τ will be translated into a CIPA waiting of duration 0 by allowing for waitings of the form wait 0.Q in the modified syntax of CIPA. – Every TCCS delay t will be translated into a CIPA waiting of duration t. 3.3
While the encoding from CIPA to TCCS defined in [
Consider the two TCCS processes a.(t1).(t2).b.0 and a.(t1 + t2).b.0, which
are equivalent to each other according to the strong timed bisimilarity of [
It is however worth pointing out that the two former processes are equivalent according to ≈TCCS and, most importantly, the two latter processes are equivalent according to ≈CIPA. As a consequence, in this paper we have to restrict ourselves to weak timed bisimilarities when investigating semantics preservation for the reverse encoding. 4
In this section, we translate (modified) TCCS process terms into (modified) CIPA process terms and we show that the resulting encoding is fully abstract, in the sense that it preserves weak timed bisimilarity. The encoding is defined by induction on the syntactical structure of process terms.
Definition 5. The encoding [[ ]] : P0TCCS → P0CIPA is defined as follows: [[0]] = nil [[a.P ]] = a.[[P ]] [[τ.P ]] = wait 0.[[P ]] [[(t).P ]] = wait t.[[P ]] [[P1 + P2]] = [[P1]] + [[P2]] [[P1|P2]] = [[P1]]|[[P2]] [[P \L]] = [[P ]]\L [[P [ϕ]]] = [[P ]][ϕ]
[[X]] = X [[rec X : P ]] = rec X : [[P ]] with Δ(a) = 0 for all a ∈ Act \ {τ }.
The states of the labeled transition systems underlying a TCCS process P and the corresponding [[P ]] are strictly related. This relation is the key point that permits to show the main result of the paper stated in the forthcoming Thm. 1. Formally, to establish the relation, we need to add local clocks to [[P ]]. We let E [[P ]] ∈ KP denote the encoded P process where a clock 0 ⇒ has been added to each sequential component.
Consider as an example the process P0 = a.(1).b.0 | c.(2).(1).d.0, whose transition system is depicted in Fig. 1. The transition system of E [[P0]] is shown in Fig. 2. It easy to see that, as far as only visible actions and zero-valued local clocks are concerned, the correspondence is one-to-one: E [[Pi]] = Ki, for i = 0, 1, 2, 3. However, in CIPA the wait t waitings, which produce τ actions, can be executed independently by one of the sequential components, which moves its own clock forward in time. In the meanwhile, the other components still have to τ@0 execute actions “before” that time. This happens, for instance, in K1 −−→ K10; 1 note, anyway, that K10 can still perform the visible action c at time 0.
Processes P5, P6 and P7 are related by TCCS delay transitions. In the corresponding CIPA states, we can relate P5 with K5. The nil CIPA process lets any time pass for other sequential components. Thus, K5 can be considered equivalent (at least with respect to ≈CIPA) to K50 = 2 ⇒ nil | 2 ⇒ wait 1.d.nil. In this way, E [[P6]] = 0 ⇒ nil | 0 ⇒ wait 1.d.nil can be related to K50 by adjusting the clock values that are different in absolute value, but agree on the relative differences: 2 − 2 = 0 − 0 = 0. Similarly, process P7 can be related to process K60 = 3 ⇒ nil | 3 ⇒ d.nil obtained from K6.
Consider, finally, process P4, derived from P0. Its counterpart K4 cannot perform any τ , but E [[P4]] has clock values not corresponding to K4. Nevertheless, the b action is performed at the same time in both cases, i.e., with timestamp 1.
To formally treat the discrepancies mentioned above, it is convenient to define
a structural congruence ≡ over KP that permits to equate timed processes that
respect, in their sequential components, the following two equations:
m ⇒ wait n.P = m + n ⇒ P
n ⇒ nil = m ⇒ nil
where n, m ∈ N. It is easy to see that ≡ implies ≈CIPA. Moreover, following [
Using this notation, we get E [[P1]] = K1 = up(K1, 0) ≡ K10, i.e., P1 in Fig. 1 can be related to two timed states that are structural equivalent and, thus, ≈CIPA equivalent. Moreover, E [[P5]] = up(K5, 1), E [[P6]] = up(K50, 1 + 1 = 2) where K50 ≡ K5, E [[P7]] = up(K60, 2 + 1 = 3) where K60 ≡ K6. Note that the subsequent times n in up(·, n) reflect the TCCS delay transitions. Finally, E [[P4]] = 0 ⇒ b.nil | 0 ⇒ wait 1.wait 1.d.nil ≡ 0 ⇒ b.nil | 1 ⇒ wait 1.d.nil = up(K4, 1). Theorem 1. Let P1, P2 ∈ P0TCCS. Then P1 ≈TCCS P2 iff [[P1]] ≈CIPA [[P2]]. 5
In this paper, we have addressed the issues raised at the end of [
As future work, we want to investigate how to exploit our encoding of TCCS
into CIPA together with the notion of compact representation of CIPA timed
states introduced in [