A Calculus of Timed Refinement^{∗}

Extended Abstract

Kārlis Čerāns

Institute of Mathematics and Computer Science, University of Latvia

                     E-mail: karlis@mii.lu.lv

1 Introduction

This paper presents CTR - a process algebraic framework for loose specification of time quantity sensitive operational behaviour of reactive systems.

The necessity and role of quantitative time information in reactive (open) system descriptions is nowadays quite appreciated^{1}, and there are already quite many specification formalisms, which alongside with system structural and/or behaviour event ordering specification permits to specify quantitative time information characterizing the valid behaviours (see e.g. [MF76, CC89, AD90, Wan91, GMMP89] as a few examples of such formalisms).

Quite naturally, many of the existing “timed” specification formalisms do allow in certain natural sense “loose” specifications of time information (it would be not that natural to determine at early system design stage exactly what are the time quantities between specific events going to be^{2}), at least [MF76, AD90, Che92, Dan92, CGL93] to be mentioned.

The calculus CTR^{3} presented in this paper is also designed to follow this tradition. Specifically, its aim is to provide a framework with mathematically precise and semantically justified notion of timed specification refinement (when one specification can be termed to be “more precise” than the other), concentrating on external behaviour specifications and branching time semantics. The model closest to CTR among those already present in the literature certainly is that of Timed Modal Specifications (TMS) introduced in [CGL93, CGL94]. We discuss in Section 5 in detail, what subset of CTR corresponds to a slight semantic reformulation^{4} of TMS.

∗The full version to be published as a technical report LU-IMCS-TRCS-94-??, Institute of Mathematics and Computer Science, University of Latvia, Riga 1994

1Even if the observer of a system is not directly concerned about the actual time quantities between externally observable events, it could be relevant for him/her to put some timing information in the specifications of the system components in order to ensure the correct qualitative ordering of the whole system output events.

2It may appear impossible even on the level of implementations due to various unpredictable execution environment fluctuations.

3A Calculus of Timed Refinement.

4Achieving, moreover, more intuitive properties of the specification refinement.

In essence, CTR is obtained by adding to the Milner’s CCS [Mil89] the contruct of time interval prefix [a, b].P, where a, b are nonnegative real numbers, 0 ≤ a ≤ b, possibly b = ∞. Such a specification is intended to describe all processes which first delay for some quantity d ∈ [a, b], and then behave accordingly to some behaviour prescribed by P. (CTR can be seen as a generalization of Timed CCS due to Wang Yi in its version of [Wan90], where only delay prefixes of the form [d, d].P were considered and denoted by ϵ(d).P).

We define an operational semantics for CTR specification terms as a labelled transition system (each transition label denotes either some control action (externally visible or invisible), or it specifies some amount of time passage). Based on this semantics the relations of specification refinement ≤ and equivalence ≈^{·} are defined in a bisimulation - like fashion^{5}.

The CTR specification equivalence and refinement relations are shown to obey the algebraic properties of equivalence/preorder and substitutivity (congruence/pre-congruence). On Timed CCS terms ≤ induces a so-called divergence refinement relation, which is a slightly stronger property than the weak bisimulation ≈ of [Wan90]. ≈^{·} and ≤ are also decidable for finite control specifications^{6} (these include, for instance, networks of regular specifications).

Pragmatically, the CTR refinement relation ≤ is based on the intuition of resolving underspecification of timing information. So, [e, f].S ≤ [d, g].T whenever d ≤ e ≤ f ≤ g and S ≤ T ^{7} (the tighter the delay interval is, the finer is the specification). On the extreme, the term [0, ∞].S covers any specification of the form [d, e].S, together with the “empty” specification nil which never exhibits any observable behaviour but waiting. In fact, the term [0, ∞].S would specify just the possibility of the system to exhibit the behaviour prescribed by S after some (possibly none) initial delay^{8}. This is the only way of achieving in CTR looseness of “non-timed” transition behaviour of specifications.

On the other hand, the CTR refinement relation ≤ admits abstraction from internal transitions of specifications and is focusing just on the externally observable behaviour. As an example, we have

(a.[d, e].\overline{b} | b.[f, g].\overline{c})\b ≤ a.[d + f, e + g].\overline{c}.

Here on the right hand side we have a specification of all media which after recieving a message on the channel a wait for some time amount δ ∈ [d+f, e+g], after what a message on the channel c is delivered. On the left hand side we have decomposed such a general message transmission specification into more detailed one, where the transmission is done in two stages - first from the channel a to the internal channel b, then from b to c. For each stage the looseness of the delay specification is maintained. Observing the substitutivity property of ≤, one can during further stages of the design make further refinements of the components responsible for both transmission stages^{9} still ensuring that the resulting system^{10} will be a refinement of the initial general specification a.[d + f, e + g].\overline{c}.

5As largest relations in the set of all specification terms, satisfying certain local “closeness”

properties.

6To be precise, the decidability results hold for specifications whose initial delay bounds are given by integers (or at least rational numbers). In practice this is not a real restriction.

7This includes the case when S = T, due to the reflexivity of ≤.

8In the notation of TMS the term [0, ∞].a.S (observe the action label a necessary here) is written as a_{◇} .S and is read semantically as “a transition a leading to S may be enabled”.

This example illustrates how CTR is conceptually suitable for formal topdown system development by stepwise refinement. One can start with a general and very loose specificaton which captures only a few essential features of the system being designed. The stepwise refinement process allows, in a formal manner, to incorporate into the specification additional design decisions, both of structural and timing nature, each refinement step possibly being done locally in some component of the system^{11}.

One should note, however, that there are a lot of different notions of specification refinement (or, specification/implementation relations, for that matter), using rather different mathematical models, one could look at, say, [BW94, Lam91, Dil89]. The refinement aspect inherent in CTR is that of time information strenghening in external communication ability specifications, and no claim is being made about any “superiority” of this refinement aspect to others.

In the rest of the paper, after introducing the CTR model in Section 2, in Section 3 we consider the definition and properties of the refinement relation. Sections 4 and 5 are devoted to study of some semantic variations of CTR.

2 CTR: Syntax and Semantics

We start with defining the syntax of CTR specification terms.

Let Λ = Δ ∪ \overline{Δ} with \overline{\overline{α}} = α for all α ∈ Λ be a set of external actions, ranged over by α, β, and let τ be a distinct symbol representing the internal actions. Act = Λ ∪ {τ} is a set of all actions, ranged over by a, b.

Let Var be a finite set of process variables, ranged over by X. Then the set of regular CTR expressions over Var is defined by the following grammar:

E ::= nil | X | [c, e].E | ]c, e].E | a.E | E + E,

where c ∈ R^{+0}, e ∈ R^{+0} ∪ {∞}, c ≤ e. Here besides the standard process algebraic constructs nil, action prefix a.E, choice E + E and variable (see [Mil89]) we have introduced two kinds of delay interval prefix (left-closed and left-open). We let also ϵ(d).E to be another notation for [d, d].E.

We assume furthermore that for every X ∈ Var we are given a regular CTR expression E_{X} (over Var) that contains variable occurrences only guarded either by action or some delay interval prefix^{12}. We let E = {X =^{def} E_{X}|X ∈ Var} and call it a system of variable defining equations.

Given such a system E we call any regular CTR expresion over Var a regular CTR specification over Var and E (possibly not mentioning Var and E, if they are clear from the context).

9As a trivial possibility, one could tighten the message delivery delay intervals.

10Any system (S|T)\b, where S ≤ a.[d, e].\overline{b} and T ≤ b.[f, g].\overline{c}.

11Notice that the decidability of the refinement relation provides with (at least principal)

possibility for automatic formal verification of the validity of every performed refinement step.

12In other words, all variable occurrences in E_{X} are allowed only within subterms of the form a.E, [c, e].E or ]c, e].E. Moreover, a delay prefix counts as a valid guard, only if c > 0.

Let G(Var, E) be a set of all regular CTR specifications over Var and E, ranged over by G. We define the set S = S(Var, E) of CTR networks (CTR specifications), over Var and E, by the grammar:

S ::= G | S|S | S\A | S[f],

where A ⊆ Δ and f : Δ → Δ is a bijection, extended to Λ → Λ by f(\overline{α})) = \overline{f(α)} and f(τ) = τ. We let S and T to range over the set of CTR networks.

We define for CTR specifications an operational semantics. Following the design of a standard timed process calculi TCCS [Wan90], we base it on the transition relations S ⟶^{a} T, meaning that S can execute a control transition a ∈ Act and afterwards exhibit a behaviour prescribed by T, and S ⟶^{ϵ(d)} T meaning that S can become T just by delaying for d time units (d ∈ R^{>0}).

The new point is in defining the semantics for delay interval prefix. Our choice is to admit the ability of [c, e].S to exhibit the behaviour prescribed by S after any d ∈ [c, e] time units, the actual value of d to be chosen nondeterministically every time this construct is executed^{13}. However, to facilitate the compositionality of the CTR framework, we are to define also what [c, e].S is going to become (can become) after waiting for some smaller time amount (e.g., d < c). At least three possible variants initially come into mind, depending on actually when during the delay the nondeterminism is being resolved. These variants correspond to (i) choosing in the beginning (early choice), (ii) choosing gradually during the execution (inline choice), and (iii) choosing when to leave (late choice). We shall work out in most detail (iii). (ii) is considered in Section 4 (showing also its relation to the late choice semantics), while (i) can be argued to be not suitable as a basis of timed refinement framework^{14}.

So, the execution of [c, e].S in time begins with a deterministic and syn-

chronous decreasing of both its higher and lower time bounds: [c, e].S ⟶^{ϵ(d)} [c−d, e−d].S for d ≤ c. When [0, e].S is reached, the choice comes in. We still

let [0, e].S ⟶^{ϵ(d)} [0, e − d].S for d ≤ e, however, now we want the specification to be able to choose to exhibit the behaviour prescribed by S immedilately. The design decision taken in CTR is to introduce a special new kind of internal transition ⟶^{i} whose effect is to “leave the delay prefix”: [0, e].S ⟶^{i} S. This construction materializes the principle of letting the specification itself to make all time nondeterministic choice without any influence from the environment.

Formally, we require i ∉ Act and let Act^{+} = Act ∪ {i} to be ranged over by a^{+}. The whole operational semantics of CTR is given in Table 1 and Table 2 (we assume f(i) = i for any relabelling function f). x ˙−y means max{x − y, 0} and ]•[ stands for any kind of left end of the interval (] or [). In the delay rules

for ⟶^{ϵ(d)} we require d ∈ R^{>0}. ν stands for either a^{+}, or ϵ(d).

For parallel composition, the sorts Sort(d, S) ⊆ Λ in the side condition of the delay rule are computed in a standard way, as follows:

13This would amount to having [c, e].S ⟶^{ϵ(d)} S for all d ∈ [c, e]. As we shall see soon, a proper description of this property in CTR would be [c, e].S⟶^{ϵ(d)}_{I}S.

14In a sense, it requires the choice in the model to be done before the choice is performed in the real modelled system. We discuss this issue more precisely in Section 3.

\frac{−−}{nil ⟶^{ϵ(d)} nil} \frac{−−}{a.S ⟶^{a} S} \frac{−−}{α.S ⟶^{ϵ(d)} α.S} \frac{S ⟶^{ν} S′}{X ⟶^{ν} S′} [X =^{def} S] ∈ E

\frac{S ⟶^{a} S′}{S + T ⟶^{a} S′} \frac{T ⟶^{a} T′}{S + T ⟶^{a} T′} \frac{S ⟶^{i} S′}{S + T ⟶^{i} S′ + T} \frac{T ⟶^{i} T′}{S + T ⟶^{i} S + T′}

\frac{S ⟶^{ϵ(d)} S′ T ⟶^{ϵ(d)} T′}{S + T ⟶^{ϵ(d)} S′ + T′} \frac{S ⟶^{a^{+}} S′}{S|T ⟶^{a^{+}} S′|T} \frac{T ⟶^{a^{+}} T′}{S|T ⟶^{a^{+}} S|T′} \frac{S ⟶^{α} S′ T ⟶^{\overline{α}} T′}{S|T ⟶^{τ} S′|T′}

\frac{S ⟶^{ϵ(d)} S′ T ⟶^{ϵ(d)} T′}{S|T ⟶^{ϵ(d)} S′|T′} [Sort(d, S) ∩ \overline{Sort(d, T)} = ∅] \frac{S ⟶^{a^{+}} S′}{S\A ⟶^{a^{+}} S′\A}[a, \overline{a} ∉ A]

\frac{S ⟶^{ϵ(d)} S′}{S\A ⟶^{ϵ(d)} S′\A} \frac{S ⟶^{a^{+}} S′}{S[f] ⟶^{f(a^{+})} S′[f]} \frac{S ⟶^{ϵ(d)} S′}{S[f] ⟶^{ϵ(d)} S′[f]}

Table 1: Transition rules for standard process algebraic constructions

\frac{− − [d ≤ e]}{[c, e].S ⟶^{ϵ(d)} [c ˙−d, e−d].S} \frac{−−}{[0, e].S ⟶^{i} S} \frac{S ⟶^{a^{+}} S′}{[0, 0].S ⟶^{a^{+}} S′} \frac{S ⟶^{ϵ(d)} S′}{]•[c, e].S ⟶^{ϵ(d+e)} S′}

\frac{− − [d ≤ c]}{]c, e].S ⟶^{ϵ(d)}]c−d, e−d].S}  \frac{− − [c < d ≤ e]}{]c, e].S ⟶^{ϵ(d)} [0, e−d].S}

Table 2: Transition rules for delay prefix

• Sort(d, α.S) = {α}, Sort(d, τ.S) = Sort(d, nil) = ∅,

• Sort(d, [c, e].S) = Sort(d ˙−e, S),

• Sort(d, X) = Sort(d, S), where [X =^{def} S] ∈ E

• Sort(d, S + T) = Sort(d, S|T) = Sort(d, S) ∪ Sort(d, T)

• Sort(d, S[f]) = f(Sort(d, S) and Sort(d, S\A) = Sort(d, A) \ (A ∪ \overline{A}).

Following the design of Timed CCS, we have incorporated in our framework the principle of maximal progress, saying that an enabled internal τ transition has to be executed before the time progresses further^{15}.

In the semantics one should observe that unlike the ⟶^{τ} transitions, ⟶^{i} does not resolve the nondeterministic choice S + T (as do not the delay transitions). It is to be observed also that a specification of the form [0, 0].S does not need to have any ⟶^{i} transitions in order to “leave” the delay prefix. Intuitively this reflects the idea that ⟶^{i} corresponds to an active choice, but in case of [0, 0].S no (timed) choice has been left.

15There are no delay transitions for the τ.S terms, also the above side condition with sorts in parallel composition delay rule is just for this reason - a time can pass only until the point where a synchronization between componets is enabled. Note that this does not apply to ⟶^{i}.

Using the notation ϵ(d).S for [d, d].S we can interpret all Timed CCS (network) terms of [Wan90] as CTR terms. It can be seen that this embedding preserves also the TCCS operational semantics (modulo ignoring ⟶^{i} transitions which for TCCS terms can be essentially only of the form S ⟶^{i} S).

3 Refinement and Equivalence

In this section the CTR specification refinement and equivalence relations are defined on the basis of their operational behaviour. We recall also that the refinement relation is going to embody the idea of resolving timed underspecification (what operationally appears as timed non-determinism).

For S being a refinement of T, S ≤ T, we first require that any transition sequence (behaviour) of S is to be matched by a corresponding transition sequence of T^{16}, the resulting states of these sequences also being in the relation ≤. In a sense, a more general specification needs to admit more behaviours.

However, our notion of the refinement is not just that of simulation. We require also that certain behaviours of T, namely those not involving ⟶^{i} transitions, and not involving also delays, should be matched appropriately on the side of S. Since the ⟶^{i} and delay transitions are the only ones possibly resolving the timed nondeterminism (⟶^{i} is doing that in an “active” way, while some delay transitions do that in a “passive” way), this requirement means that all behaviours not resolving timed nondeterminism are to be maintained (modulo the abstraction from ⟶^{τ}) during the refinement process.

Formally, let S ⟶^{a}_{∘} S′ denote S(⟶^{i})^{∗} ⟶^{a} (⟶^{i})^{∗}S′, S ⟹^{ε} S′ denote S ⟶^{τ}^{∗} S′ and S ⟹^{α} S′ stand for S ⟹^{ε}⟶^{α}⟹^{ε} S′. Moreover, let ⟹^{ε}_{∘}= (⟶^{τ}

∪ ⟶^{i})^{∗} and S ⟹^{α}_{∘} S′ mean S ⟹^{ε}_{∘}⟶^{α}⟹^{ε}_{∘} S′.

In what follows, we prepare for defining the matching of delay transitions. For S ∈ S and d ∈ R^{>0} we call any finite sequence ⟨S_{0}, d_{0}⟩, ⟨S_{1}, d_{1}⟩, …, ⟨S_{n}, d_{n}⟩ such that S ⟹^{ε}_{∘} S_{0}, d_{0} = 0, d_{n} = d and for every i = 1, …, n − 1 we have S_{i} ⟶^{ϵ(d_{i+1}−d_{i})} S′_{i} ⟹^{ε}_{∘} S_{i+1} a base sequence for an ⟨S, d⟩-trace. The ⟨S, d⟩-trace itself associated with this base sequence is defined to be the function f : [0, d] →

S such that f(d_{i} + δ) = S_{i} ⟶^{ϵ(δ)}, where i = 1, …, n and δ ∈ [0, d_{i+1} − d_{i}[ ^{17}. We

denote by S ⟹^{ϵ(d)}_{∘} the set of all ⟨S, d⟩-traces.

For f ∈ S ⟹^{ϵ(d)}_{∘} and g ∈ T ⟹^{ϵ(d)}_{∘}, given a relation R ⊆ S × S, we say that ⟨f, g⟩ ∈ R^{t} if and only if ⟨f(d′), g(d′)⟩ ∈ R for every d′ ∈ [0, d].

For S ∈ S we let S ⟶^{τ^{∞}}_{∘} to denote the fact of existence of infinite chain of ⟶^{τ}_{∘} transitions starting at S: S ⟶^{τ}_{∘} S_{1} ⟶^{τ}_{∘} S_{2} ⟶^{τ}_{∘} · · ·.

16This matching is abstracting from the externally non-observable transitions ⟶^{i} and ⟶^{τ}.

17By S ⟶^{ϵ(δ)} we have denoted the unique T such that S ⟶^{ϵ(δ)} T. In Section 4 it will be demonstrated, how a trace can be defined also in the absence of this unicity.

Let μ range over Λ ∪ {ε} (μ is either α, or ε).

Definition 3.1 A relation R ⊆ S × S is a refinement relation, if for any ⟨S, T ⟩ ∈ R

1. S ⟹^{μ}_{∘} S′ implies ∃T′. T ⟹^{μ}_{∘} T′ so that ⟨S′, T′⟩ ∈ R;

2. T ⟹^{μ} T′ implies ∃S′. S ⟹^{μ} S′ so that ⟨S′, T′⟩ ∈ R;

3. f ∈ S ⟹^{ϵ(d)}_{∘} implies existence of g ∈ T ⟹^{ϵ(d)}_{∘} such that ⟨f, g⟩ ∈ R^{t};

4. S ⟶^{τ^{∞}}_{∘} implies T ⟶^{τ^{∞}}_{∘}.

We say that S is a refinement of T, and write S ≤ T whenever there exists a refinement relation R containing ⟨S, T ⟩ (In other words, ≤ is the largest refinement relation).

Observational equivalence is a refinement whose inverse is also a refinement^{18}. A few further comments on the given definition are in order. The intuitive

explanation of the refinement given in the beginning of the section motivates only its first three requirements (observing the specific way of defining a matching for timed transitions). Without including the fourth clause in the definition we would have a so-called simple refinement relation, which we denote by <. It can be shown that < obeys the essential mathematical properties of transitivity and substitutivity. However, this relation is in a sense too large since S < T holds also in some cases, when it is semantically undesirable, for instance, when

T = a.nil and S =^{def} a.nil + τ.S ^{19}.

The fourth clause in the refinement definition is pragmatically meant to forbid such examples (at the same time not forbidding too much). Though this clause is not of the form of “matching requirement”, traditional for process algebraic equivalence and preorder relations, it is hoped that it would pragmatically fit well with the system refinement process.

To facilitate that we suggest a pragmatic requirement that a design in CTR should not admit “instantaneous” loops of internal transitions^{20}. As loops of internal transitions are usually essential in the process algebraic system design, this requirement would mean just that any such loop possibly occurring in the specification should have its delay being strictly greater than 0 (a ]0, d].S construct executed in every round of the loop would be sufficient) ^{21}.

18In this paper we do not further explore the notion of specification equivalence. However, it is clearly relevant for the theory.

19One most likely would not want the “time-blocking” specification S to be a refinement of a perfectly well defined specification willing to synchronize with its environment on a at the moment when the environment is ready to do so (and not necessarily “immedilately”).

The simple refinement relation would be satisfactory, however, if one managed to exclude the possibilities of writing “time-blocking” specifications at all. This does not seem feasible while following the process algebraic specification style, and sticking to the maximal progress principle.

20In a modelling methodology, where we do take into account the actual time quantities, it might be admitted that some bounded amount of transitions are performed “instantaneously”

(if that helps to simplify the model). However, for unbounded chains or loops of internal actions, it is no longer realistic that they could be executed within 0 units of time.

Yet another variation of the refinement notion could be obtained by extending the set of “necessary” behaviours which, when present in a specification, should be matched appropriately also on the side of implementation^{22}. A natural such extension is obtained by observing that some delay transitions of CTR specifications, namely those of [c, e].S waiting for d ≤ c time units, are not resolving any timed non-determinism, and are in one or other form to be present also in all refinements of this specification.

However, a refinement relation which in case of T refined by S would require all “necessary” delay transitions of T to be matched by similar transitions of S (also done in the necessary mode, to ensure the transitivity of the refinement) appears to be too strong. To see that, look at the valid CTR refinement

[1, 2].τ.[1, 2].\overline{c}.nil ≤ [2, 4].\overline{c}.nil,

what is just a transformed and instantiated version of the transmission media refinement example considered in the introduction^{23}. One can see that the right hand side is to delay for 2 time units in the “necessary mode”. However, while it is clear that the left hand side also will necessarily delay for at least 2 time units before offering \overline{c}, there is no single chain of delay transitions of length 2 (possibly interleaved with ⟶^{τ}) which could also be performed in the necessary mode, without any active or passive resolving of the time nondeterminism^{24}. Thus the requirement of simple matching the “necessary” delay transitions would invalidate the above refinement instance, what could seriosly question the pragmatical applicability of the whole refinement relation^{25} ^{26}.

21As can be clearly seen from the definition of ≤, this requirement has not been formally incorporated into the definition. All what has been said is, if the implementation (the stronger specification) admits such a loop for one or other reason, then also the more general specification has to have it admitted (it could be done as, for instance, in S =^{def} a.nil + τ.S). Sometimes indeed some “time-blocking” effects could be useful to say the fact that a certain action should be immediate (ideally, of course, one should have other direct means of expressing that), however, that has nothing in common with the situation when a real chain (loop) of internal transitions is to be executed.

22For ≤ these are just all behaviours not containing ⟶^{i}, and not containing delays.

23(a.[d, e].\overline{b} | b.[f, g].\overline{c})\b ≤ a.[d + f, e + g].\overline{c} with d = f = 1 and e = g = 2, here we consider the situation where the initial a has already been performed.

24Observe that already after 1 time unit of waiting the further performed delay of [1, 2] appears to be only in the possible mode due to the other existing alternative to take ⟶^{i} at that moment.

25The framework of TMS in [CGL93, CGL94] is based on this idea of requiring the matching of “necessary” delay transitions in the direction from the specification to the implementation. Therefore in that framework only a reduced version of the considered example was possible (one does get a valid refinement instance when either d = e, or f = g, that is, when one of the components is deterministic).

26The same example [1, 2].τ.[1, 2].\overline{c}.nil ≤ [2, 4].\overline{c}.nil can be used also to invalidate the “early choice” semantics for CTR, as discussed in Section 2 (provided we keep our schema of defining the refinement).

Indeed, as we want a delay transition of the implementation, say ⟶^{ϵ(0.1)}, leading to ϵ(1.3).τ.[1, 2].\overline{c}.nil, to be matched on the side of the specification, we need to determine at

We turn to the mathematical properties of ≤. Due to the space constraints their proofs are mainly postponed to the full version.

Fact 3.2 The relation ≤ is reflexive and transitive.

Lemma 3.3 ≤ is preserved by CTR parallel composition, restriction and relabelling operations.

Proof: We prove that for any refinement relation R refinement relations are also R^{+} = {⟨S|T, P |T ⟩|⟨S, P ⟩ ∈ R}, R_{rs}^{+} = {⟨S\A, P \A⟩|⟨S, P ⟩ ∈ R} and R_{rl}^{+} = {⟨S[f], P [f]⟩|⟨S, P ⟩ ∈ R}. The proof is a rather straightforward check, including the case of timed matching of parallel composition. □

Lemma 3.4 If T ⟶^{i} S, then S ≤ T.

Proof: We show that the relation {⟨S, T ⟩|S = T or T ⟶^{i} S}, is a refinement. The proof is a matter of combining definitions, given the following fact.

Fact 3.5 If T ⟶^{i} S and T ⟶^{a} T′, then either S ⟶^{a} T′, or there exists an S′ such that S ⟶^{a} S′ and T′ ⟶^{i} S′.

Proof: By analyzing, whether T ⟶^{i} S and T ⟶^{a} T′ are performed in distinct regular components of T, or in the same. □

In what follows we show what relation the CTR refinement ≤ induces in the set of time determinstic (“fully specified”) process algebraic terms (those of Timed CCS). Let P denote the set of all TCCS (network) processes (P ⊆ S).

Following [Wan90], a relation R ⊆ P × P is a (weak) bisimulation, if for all ν ∈ Act ∪ {ϵ(d)|d ∈ R^{>0}} and all ⟨P, Q⟩ ∈ R

• whenever P ⟹^{ν} P′ then ∃Q′.Q ⟹^{ν} Q′ so that ⟨P′, Q′⟩ ∈ R and

• whenever Q ⟹^{ν} Q′ then ∃P′.P ⟹^{ν} P′ so that ⟨P′, Q′⟩ ∈ R.

Here X ⟹^{ϵ(d)} Y is defined to mean X(⟶^{τ})^{∗} ⟶^{ϵ(d_{1})} (⟶^{τ})^{∗} ⋯ ⟶^{ϵ(d_{k})} (⟶^{τ})^{∗}Y, where

d_{1} + ⋯ + d_{k} = d. The largest TCCS weak bisimulation is denoted by ≈.

Fact 3.6 For P and Q being TCCS processes, P ≤ Q implies P ≈ Q.

To characterize the relation induced by ≤ on TCCS terms precisely, let a relation R ⊆ P × P be called a divergence refinement iff

• R is a weak bisimulation, and

• for any ⟨P, Q⟩ ∈ R whenever P ⟶^{τ^{∞}}, then also Q ⟶^{τ^{∞}}.

Let <_{D} be the largest divergence refinement for TCCS processes.

Theorem 1 For P and Q being TCCS processes, P ≤ Q if and only if P <_{D} Q.

this very moment, how long the actual delay of [2, 4] is going to be. Doing that, we clearly can not keep the further flexibility inherent in the second implementation’s [1, 2] construct.

To prove the theorem we first give an equivalent characterization of ≈ and <_{D} using the form of “continuous matching” for delays^{27}. Later on, a determinacy of ⟶^{ϵ(d)} transitions, together with the maximal progress and a few other CTR transition system properties are exploited.

4 Inline Choice Semantics

This section concerns defining alternative semantics for CTR terms following the idea of inline, or ongoing choice, where the “speed” of execution at every moment is contributing to when a specification is going to leave its delay interval prefix. Surprisingly enough, a refinement defined naturally on the basis of this really wildly nondeterministic transition system, coincides with the “standard” CTR refinement ≤. For the sake of simplicity of technical treatment we consider here only specifications in reduced CTR, where we disallow left-open delay interval prefixes ]c, e].

First we define the inline choice operational semantics as the transition relation ⟶_{I}. For that we can take all the rules defining the “standard” semantics ⟶ in Table 1 and Table 2 (with changing syntactically ⟶ to ⟶_{I}) except for two. First of those to be changed is the main rule for delay of the delay prefix, which is to read now as

[c, e].P ⟶^{ϵ(d)} [c′, e′].P whenever max(0, c − d) ≤ c′ ≤ e′ ≤ e − d.

Intuitively this rule means that during the delay of d time units the lower delay bound is reduced by no more than d, and the higher bound is reduced by not less than d. Any choice in between can be taken during the runtime.

To be able to define adequately the semantics of the delay rule of the parallel composition (we can not work just with the Sort function, as in case of ⟶),

we have to refine a bit the whole definition of the relation S⟶^{ϵ(d)}_{I}T by basing it not solely on the fact of existence of such transition, but rather on the explicit exhibition of the whole trace leading in d time units from S to T. Therefore we inductively define the proposition f ∈ S⟶^{ϵ(d)}_{I}T, where always f : [0, d] → S satisfying f(0) = S and f(d) = T. This definition is in full conformance to the

already established clauses of definition of S⟶^{ϵ(d)}_{I}T. For the sake of brevity, we show only two clauses (the others are more straightforward):

• Whenever max(0, c − d) ≤ c′ ≤ e′ ≤ e − d, we let f ∈ [c, e].P ⟶^{ϵ(d)}_{I}[c′, e′].P

iff f(x) = [cc(x), ee(x)].P for all x ∈ [0, d] and the functions cc and ee together with cc(0) = c, ee(0) = e, cc(d) = c′ and ee(d) = e′ for any x, y ∈ [0, d] such that δ = y − x ≥ 0 satisfy

max(0, cc(x) − δ) ≤ cc(y) ≤ ee(y) ≤ ee(x) − δ.

27As can be seen, in the definition of ≈ only the endpoints of delay transition are required to be matched.

• Whenever f ∈ S⟶^{ϵ(d)}_{I}S′ and g ∈ T ⟶^{ϵ(d)}_{I}T′, we have f|g ∈ S|T ⟶^{ϵ(d)}_{I}S′|T′

provided Sort(f(x)) ∩ \overline{Sort(g(x))} = ∅ for all x ∈ [0, d[^{28}.

We say that f ∈ S⟹^{ϵ(d)}_{Io}S′ iff f : [0, d] → S and f(d) = S′, as well as

S ⟹^{ε}_{∘} S_{1}⟶^{ϵ(d_{1})}_{I}S′_{1} ⟹^{ε}_{∘} ⋯ S_{k}⟶^{ϵ(d_{k})}_{I}S′_{k} ⟹^{ε}_{∘} S′

so that d_{1} + d_{2} + ⋯ + d_{k} = d and ∀i ≤ k. ∃g_{i} ∈ S_{i}⟶^{ϵ(d_{i})}_{I}S′_{i} such that ∀δ ∈

[0, d_{i}[. f(d_{1} + ⋯ + d_{i−1} + δ) = g_{i}(δ).

S⟹^{ϵ(d)}_{Io} is defined to be the union of S⟹^{ϵ(d)}_{Io}S′ for all reduced CTR specifications S′.

The refinement ≤_{I} now can be defined by a variant of Definition 3.1 for ≤, where ⟹^{ϵ(d)}_{Io} is substituted for ⟹^{ϵ(d)}_{∘}. The principal result of this section (to be proved in the full version) is the following.

Theorem 2 For any two (reduced) CTR terms S and T S ≤_{I} T if and only if S ≤ T.

5 (Another) Timed Modal Specifications

In this section we provide yet another semantic variation of (a subset of) CTR, which is based on explicit defining of “necessary” and “possible” modes of transitions, the idea originally appearing in [LT88].

The intuition of the specification refinement in the modal framework is very simple - the more possible and fewer necessary transitions a specification has, the more general it is. This idea has already been adopted to a timed specification formalism in [CGL93, CGL94] resulting in already several times mentioned framework of TMS. Though the TMS model is theoretically very appealing, it turns out that a few of pragmatic properties of the model are a bit unnatural. This applies both to some intuitively desirable refinement examples which are not valid in TMS^{29}, as well as to the lack of clear operational behaviour intuition due to the having modalities also on the timed transitions.

Here we provide a slight reformulation of the TMS framework (in the light of the developped CTR refinement relation) with the aim of fixing some of its undesirable properties. On the other hand, the theory of A-TMS, sketched in this section, provides yet another semantic variation of the CTR framework, which, as demonstrated by Theorem 3, is consistent with the “standard” development based on ≤ and explored in Section 3.

Syntactically the A-TMS terms are those of CTR in which every nondeterministic delay prefix is followed by a control action (A-TMS terms have a_{[c,e]},

28Here (f|g)(x) is defined to be f(x)|g(x) for all x and Sort(S) = Sort(0, S) for the twoargument Sort function defined in Section 2.

29See, for instance, the discussion in Section 3.

\frac{−−}{nil ⟶^{ϵ(d)} nil} \frac{−−}{a.S ⟶^{a}_{□} S} \frac{S ⟶^{a}_{m} S′}{X ⟶^{a}_{m} S′} [X =^{def} S] ∈ E \frac{S ⟶^{ϵ(d)} S′}{X ⟶^{ϵ(d)} S′} [X =^{def} S] ∈ E

\frac{−−}{α_{[c,e]}.S ⟶^{ϵ(d)} a_{[c ˙−d,e ˙−d]}.S} \frac{− − [d ≤ e]}{τ_{[c,e]}.S ⟶^{ϵ(d)} τ_{[c ˙−d,e−d]}.S} \frac{−−}{a_{[0,e]}.S ⟶^{a}_{◇} S}

\frac{S ⟶^{a}_{m} S′}{S + T ⟶^{a}_{m} S′}  \frac{T ⟶^{a}_{m} T′}{S + T ⟶^{a}_{m} T′}  \frac{S ⟶^{ϵ(d)} S′ T ⟶^{ϵ(d)} T′}{S + T ⟶^{ϵ(d)} S′ + T′}

\frac{S ⟶^{a}_{m} S′}{S|T ⟶^{a}_{m} S′|T} \frac{T ⟶^{a}_{m} T′}{S|T ⟶^{a}_{m} S|T′}  \frac{S ⟶^{α}_{m} S′ T ⟶^{\overline{α}}_{m} T′}{S|T ⟶^{τ}_{m} S′|T′}

\frac{S ⟶^{ϵ(d)} S′ T ⟶^{ϵ(d)} T′}{S|T ⟶^{ϵ(d)} S′|T′} [Sort(d, S) ∩ \overline{Sort(d, T)} = ∅]

Table 3: Transition rules for A-TMS, m ∈ {◇, □}

a_{]c,e]} and ϵ(d) instead of separate [c, e], ]c, e] and control action prefixes). We abbreviate a_{[0,0]}.E as a_{□}.E (written also as a.E) and a_{[0,∞]}.E as a_{◇}.E ^{30}.

The operational semantics of A-TMS is based on the necessary control tran-

sitions ⟶^{a}_{□}, possible control transitions ⟶^{a}_{◇} and delays ⟶^{ϵ(d)} ^{31} ^{32}. For a fragment of the framework the semantics is summarized in Table 3 (this fragment does not include ϵ(d) and a_{]c,e]} prefixes, neither restriction and relabelling are considered). The Sort function^{33} in the side condition for the parallel composition delay rule is computed, as for CTR terms, following the rules given in Section 2.

In order to define the A-TMS refinement relation let M be the set of all TMS specifications (over certain sets of specification variables and equations). Let the observational (τ-abstracting) modal transition relations ⟹^{μ}_{m} also be

defined in the usual way. The trace set S ⟹^{ϵ(d)}_{◇} consists of all traces starting at

S and containing interleaving of ⟶^{ϵ(d_{i})} and ⟶^{τ}_{◇} transitions, with the total delay amount being d ^{34}. Also, let μ range over Λ ∪ {ϵ} (μ is either α, or ϵ).

30In the original definition of TMS in [CGL93] the modal prefixes a_{□} .E and a_{◇} .E were taken as primitives, and a_{[c,e]}.E was defined as ϵ(c).a_{◇} .E + ϵ(e).a_{□} .E. The a_{]c,e]} prefix here is new, though theoretically it is not principal.

31The delays always are in a sense in the possible mode.

32A suggested physical interpretation of the necessary and possible transitions is that of transitions of a specification being enabled in a weak and strong sense. For a_{[c,e]}.S during the first c time units the a transition is not enabled. Afterwards, for the next c − e units this transition is enabled in a weak sense, after what (if it has not been carried out already), it becomes enabled in a strong sense.

33This function computes the transition availability in a strong sense.

34A formal definition can be given following the style of the trace definition in Section 3. In the same fashion also the relation R^{t} for R ⊆ M × M is defined.

Definition 5.1 A relation R ⊆ M × M is a(n) (observational) modal refinement relation, if for any ⟨S, T ⟩ ∈ R

1. S ⟹^{μ}_{◇} S′ implies ∃T′.T ⟹^{μ}_{◇} T′ so that ⟨S′, T′⟩ ∈ R;

2. T ⟹^{μ}_{□} T′ implies ∃S′.S ⟹^{μ}_{□} S′ so that ⟨S′, T′⟩ ∈ R;

3. f ∈ S ⟹^{ϵ(d)}_{◇} implies existence of g ∈ T ⟹^{ϵ(d)}_{◇} such that ⟨f, g⟩ ∈ R^{t};

4. S ⟶^{τ^{∞}}_{◇} implies T ⟶^{τ^{∞}}_{◇}.

We say that S is a modal refinement of T, and write S <_{M} T whenever there exists a refinement relation R containing ⟨S, T ⟩ (In other words, <_{M} is the largest modal refinement relation).

Let n : M → S be a function giving for any A-TMS term S the same term, viewed as a CTR term^{35}. The principal theorem of this section says:

Theorem 3 For any two modal specifications S and T we have S <_{M} T if and only if n(S) ≤ n(T).

Lemma 5.2 1. Whenever S ⟶^{a}_{◇} S′, then n(S) ⟶^{a}_{∘} n(S′).

2. Whenever T ⟶^{a}_{□} T′, then n(T) ⟶^{a} n(T′).

3. Whenever n(S)(⟶^{i})^{∗} ⟶^{a} (⟶^{i})^{∗}Y, then S ⟶^{a}_{◇} S′ so that Y ≤ n(S′).

4. Whenever n(T) ⟶^{a} X, then T ⟶^{a}_{□} T′ so that n(T′) = X.

To prove S <_{M} T ⇒ n(S) ≤ n(T) we show that a CTR refinement is the relation {⟨X, n(T)⟩|X ≤ n(S), S <_{M} T }.

The other direction n(S) ≤ n(T) ⇒ S <_{M} T goes simply by showing that a modal refinement is the relation {⟨S, T ⟩|n(S) ≤ n(T)}. In both directions we rely on Lemma 5.2. Details are to be supplied in the full version. □

6 Decidability

We call a CTR specification initially integral timed iff all its initial delay interval prefix bounds are given by integers^{36}.

Theorem 4 The refinement relation ≤ is decidable for initially integral timed CTR specifications.

The extension of the result of the theorem to allow arbitrary rational numbers as the initial delay bounds is straightforward^{37}. As a corollary of the theorem we get also the decidability of <_{M} for TMS.

The main constructions used in the deciding algorithm are those of timed region graph [AD90] and symbolic checking of timed bisimulation [Cer92a, Cer92b], for exposition see also [CGL94, Go94]. The full version will discuss this issue in more detail.

35n is an injective mapping of M into S, introduced for the sake of further convenience.

36This requirement is to be applied to the defining equations of all variables which the initial specification relies upon.

37Simply by adopting an initial scaling of the time axis.

7 Conclusions

In this paper a mathematically sound and rather general process algebraic framework for refinement of timed system specifications has been proposed, its further fate is to be determined by applicability in CASE studies.

The obtained mathematical results of the coincidence of the three refinement relations ≤, ≤_{I} and <_{M} show the robustness of the proposed refinement notion - resolving of timed underspecification (nondeterminism). This is a point in favour for trying the proposed calculi on practical examples. It gives an excellent chance for every system designer to understand/imagine the refinement notion in the way he/she likes it most, all choices described here (standard refinement, inline choice, modal specifications) leading to the same formal result.

Still, a somewhat experimental nature of the fourth clauses in all refinement definitions is to be admitted. However, both the theoretical refinement properties and the examples seen so far suggest that this may be a good choice.

A possibility for a further work is to look at incorporating of the introduced timed behaviour underspecification constructs into other process algebraic frameworks (considering disciplines of interprocess communication other than that of CCS may widen the practical applicability of the formalism). It is hoped that the principle of internality of delay nondeterminism, embodied in the semantics of CTR delay interval prefix, should facilitate the possibility of such incorporation.

Though a few comments on the suggested pragmatics of the use of CTR in the real time system design were considered here, there are a few more aspects worth discussing (one of them could be on the pragmatic role of left-open delay interval prefixes).

In a long run one could aim at incorporating both external behaviour and data type refinements into a single framework. For a possible notion of the data type refinement one could look into [BW94] (see also the references therein).

For making CTR a practical specification refinement framework one should work also on practically feasible algorithms for refinement deciding^{38}. A possible step into this direction could be a combining of the local validity checking and partition refinement methods for work on deciding “bisimulation - like” properties.

Acknowledgements The author wants to thank Bengt Jonsson from University of Uppsala and Kim Larsen from University of Aalborg for stimulating discussions and ideas on what a proper notion of operational refinement for timed systems should be.

Thanks are also to BRICS for sponsoring my travel to and attendance at the NWPT’6 conference in Aarhus.

38During later stages of the development of the refinement frameworks the possibilities of interactive refinement provers may be considered.

References

[AD90] R. Alur and D. Dill, Automata for Modelling Real-Time Systems, in Proceedings of ICALP’90, Lecture Notes in Computer Science No. 443, 1990.

[BW94] R. Back and J. von Wright, Trace Refinement of Action Systems in Proceedings of CONCUR’94, Lecture Notes in Computer Science No. 836, 1994.

[CC89] CCITT, Functional Specification and Description Language (SDL), Recommendations Z.100, 1989.

[Cer92a] K. Čerāns, Decidability of Bisimulation Equivalences for Parallel Timer Processes, in Proceedings of CAV’92, Lecture Notes in Computer Science No. 663, 1992.

[Cer92b] K. Čerāns, Algorithmic Problems in Analysis of Real Time System Specifications, Dr.sc.comp. theses, University of Latvia, 1992.

[CGL93] K. Čerāns, J.Chr. Godskesen and K.G. Larsen, Timed Modal Specification - Theory and Tools, in Proceedings of CAV’93, Lecture Notes in Computer Science No. 697, 1993.

[CGL94] K. Čerāns, J.Chr. Godskesen and K.G. Larsen, Timed Modal Specification - Theory and Tools, submitted to Formal Aspects of Computing, 1994.

[Che92] L. Chen, An Interleaving Model for Real Time Systems, in Proceedings of LFCS’92, Lecture Notes in Computer Science No. 620, 1992.

[Dan92] M. Daniels, Modelling Real-Time Behaviour with an Interval Time Calculus, in Proceedings of Conference on Formal Techniques in RT and FT Systems, Nijmegen, 1992

[Dil89] D. Dill, Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits, ACM Distinguished Dissertations, MIT Press, 1989.

[GMMP89] C. Ghezzi, D. Mandrioli, S. Morasca and M. Pezze A General Way To Put Time in Petri Nets, in ACM SIGSOFT Eng. Notes, Vol. 14, No. 3, 1989.

[Go94] J.Chr. Godskesen, Timed Modal Specifications - A Theory for Verification of Real-Time Concurrent Systems, Ph.D thesis, Aalborg University, 1994.

[Lam91] L. Lamport, The Temporal Logic of Actions, DEC SRC Technical report No. 79, 1991.

[LT88] K.G. Larsen and B. Thomsen, A Modal Process Logic, in Proceedings of the fifth IEEE Symposium on Logic in Computer Science, 1988.

[MF76] P. Merlin and D.J. Farber, Recoverability of Communication Protocols, IEEE Trans. on Communication Protocols, Vol. COM-24, No. 9, 1976.

[Mil89] R. Milner, Communication and Concurrency, Series in Computer Science, Prentice-Hall International, 1989.

[Wan90] Yi Wang, Real Time Behaviour of Asynchronous Agents, in Proceedings of CONCUR’90, Lecture Notes in Computer Science No. 458, 1990.

[Wan91] Yi Wang, CCS + Time = an Interleaving Model for Real Time Systems, in Proceedings of ICALP’91, Lecture Notes in Computer Science No. 510, 1991.