BRICS RS-97-11 Čerāns et al.: Timed Modal Specification — Theory and Tools BRICS

Basic Research in Computer Science

Timed Modal Specification

— Theory and Tools

Kārlis Čerāns Jens Chr. Godskesen Kim G. Larsen

BRICS Report Series RS-97-11

ISSN 0909-0878 April 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/97/11/

Timed Modal Specification — Theory and Tools^{∗}

Kārlis Čerāns^{†}, Jens Chr. Godskesen^{‡}and Kim G. Larsen^{§}

Abstract

In this paper we present the theory of Timed Modal Specifications (TMS) together with its implementation, the tool Epsilon. TMS and Epsilon are timed extensions of respectively Modal Specifications [Lar90, LT88] and the Tav system [GLZ89, BLS92].

The theory of TMS is an extension of real–timed process calculi with the specific aim of allowing loose or partial specifications. Looseness of specifications allows implementation details to be left out, thus allowing several and varying implementations. We achieve looseness of specifications by introducing two modalities to transitions of specifications: a may and a must modality. This allows us to define a notion of refinement, generalizing in a natural way the classical notion of bisimulation. Intuitively, the more must–transitions and the fewer may–transitions a specification has, the finer it is. Also, we introduce notions of refinements abstracting from time and/or internal computation.

TMS specifications may be combined with respect to the constructs of the real–time calculus [Wan90]. “Time–sensitive” notions of refinements that are preserved by these constructs are defined 1, thus enabling compositional verification.

Epsilon provides automatic tools for verifying refinements. We apply Epsilon to a compositional verification of a train crossing example.

1 Introduction

In this paper we present the theory of Timed Modal Specifications (TMS) together with its implementation, the tool Epsilon. TMS and Epsilon are timed extensions of respectively Modal Specifications [Lar90, BL90, LT88, HL89] and the Tav system [GLZ89, BLS92].

During the last few years various process calculi have been extended to include real–time in order to handle quantitative aspects of real–time systems, for instance that some critical event must not or should happen within a certain time period. We mention the calculi defined in [Wan90] and the ones defined in [NSY91] and [BB89]. Common to these real–time calculi is that time is represented by some dense time domain, e.g. the non–negative reals.

∗This work has been supported by the Danish National Science Research Council project DART and the ESPRIT Basic Research Action 7166, CONCUR2. For the first author part of this work was performed while on a post–doc leave at Chalmers University of Technology, Göteborg, Sweden.

†Adress: Inst. of Math. and Comp. Sc., University of Latvia., Rainis blvd. 29, LV–1459 Riga, Latvia. E–mail:

karlis@mii.lu.lv.

‡Address: Tele Danmark Research, Lyngsø Allé 2, DK–2970 Hørsholm, Denmark. E–mail: jcg@tdr.dk §Address: Dep. of Math. and Comp. Sc., Aalborg University, Fredrik Bajers Vej 7, 9220 Aalborg, Denmark. E–mail:

kgl@iesd.auc.dk.

1To be precise, when abstracting from internal composition refinement is not preserved by choice for the usual reasons.

As argued in [Lar90] process calculi are often too concrete in the sense that when a system has been specified the set of possible implementations are restricted to one and only one equivalence class of processes (e.g. the class of bisimulation [Mil89, Par81] equivalent processes). Moreover, as correctness is given by the equivalence, the set of possible implementations remains constant under refinement. Hence, stepwise development methodologies are not well supported in classical process calculi. As an example, using the notation from [Wan90], a disposable medium M_{d}^{a,b} with some delay d between input and output can be specified by

M_{d}^{a,b} =^{def} a.ϵ(d).\overline{b}

meaning that after input a the output \overline{b} is first enabled after d time units. But, as a specification this may be too precise and perhaps all that needs to be required of the medium is that it enables its output at some point in the time interval [e, f] after a message has been received. Hence, using a suggestive notation, a more loose specification like

M_{e,f}^{a,b} =^{def} a.ϵ[e, f].\overline{b}

is needed. Intuitively, we want M_{e,f}^{a,b} to mean that after input a the output \overline{b} may be enabled in the interval [e, f) but is first guaranteed to be enabled after f time units. It is however impossible to give a loose specification, like M_{e,f}^{a,b}, using process calculi.

The theory of TMS is an extension of real–timed process calculi with the specific aim of allowing loose or partial specifications. Looseness here means that a specification S can have various implementations because implementation details may be left out in S. For instance, as in the example above, we can be liberal as to how long a medium may delay before it can deliver. The looseness of specifications is achieved by introducing two modalities to transitions: a may and a must modality, denoted by indices ◇ and □ respectively on actions. Using modalities the loosely specified media above can be specified by

S_{e,f}^{a,b} =^{def} a_{□} .(ϵ(e).\overline{b}_{◇} + ϵ(f).\overline{b}_{□})

that is, S_{e,f}^{a,b} specifies disposable media that must input a. After e time units from reception, but not before, \overline{b} may be enabled but only after f time units the enabling of \overline{b} is required. Obviously we expect M_{d}^{a,b} to implement S_{e,f}^{a,b} whenever d ∈ [e, f].

Generalizing in a natural way the notion of bisimulation we introduce a refinement ordering ⊲ between timed modal specifications. As indicated above, a timed modal specification may specify a whole range of implementations or processes. Thus conceptually one may view a modal specification S as the set of processes satisfying S, and the refinement ordering attempts to capture the corresponding set inclusion between specifications. Intuitively, we expect a modal specification S to be a refinement of specification T when all transition allowed by S are also allowed by T, and, conversely, all transitions required by T are also required by S. As an example, we expect S_{e,f}^{a,b} ⊲ S_{g,h}^{a,b}, whenever g ≤ e and f ≤ h.

In practical applications it is often advantageous to abstract from certain aspects when analyzing a system. In particular, internal computation will normally be considered unobservable, and in a first analysis of a large combined system explicit timing information may be irrelevant. In the paper we therefore introduce notions of refinements abstracting from time and internal computation, and, of course, our tool Epsilon supports automatic verification based on the refinements presented. For total specifications, i.e. specifications with no looseness in the sense that all events are labelled with □–modalities, our refinements collapses into standard process calculi (bisimulation) equivalences. We therefore consider TMS a conservative extension of timed process calculi,

The automatic refinement checking for TMS can be performed through adopting the techniques for checking bisimulation equivalences between networks of timed regular processes, developed in [Č92b] for timed (time–sensitive) and [LW90] for time–abstracted cases (an alternative approach for deciding time– abstracted equivalences can be found in [ACH^{+}92]). We have implemented these technique in the tool Epsilon so indeed automatic refinement checking between TMS specifications is feasible. For untimed specifications the algorithms of Epsilon coincide with those of the Tav [GLZ89, BLS92] system^{2}.

We intend TMS and Epsilon to be useful during the process of design and implementation. In particular, we want to support system development through stepwise refinement. In a stepwise refinement development of a system the initial specification is rather abstract permitting a wide range of implementations. An idealized development now consists in a series of small and successive refinements, each restricting the set of permitted implementations, until eventually an implementation can be extracted directly. Each refinement can be relatively small, consisting typically in the replacement of a single component of the current specification with more concrete ones. To illustrate the first step of an idealized stepwise refinement development, suppose we have an initial specification of disposable media, say

S_{e,f}^{a,b}

required to deliver in the interval from e to f after it receives its input. A possible refinement step could be to replace S_{e,f}^{a,b} by the composed specifications

(M_{d}^{a,c} | S_{e−d,f−d}^{c,b})\c  (1)

That is, the initial specification has been refined to a more concrete specification demanding the implementation to consists of a medium with a fixed delay d (d ≤ e) together with some medium delivering between e − d to f − d time units after it received. The two components communicate via the internal channel c.^{3} The refined specification may be considered more concrete because structural information has been added to the specification. Obviously, we expect (1) to be a correct refinement of S_{e,f}^{a,b} since the total delay is still within the interval from e to f. Using the verification tool Epsilon we can automatically prove the correctness of this refinement step; more precisely, we can prove

(M_{d}^{a,c} | S_{e−d,f−d}^{c,b})\c ⊴ S_{e,f}^{a,b}

where ⊴ indicates a refinement abstracting from internal events.

In general we would like the correctness of a refinement step to be immediately implied by the correctness of the refinement of the replaced component by the one replacing it as this obviously will greatly simplify the task of verification. That is, we want to support compositional verification and hence the refinements to be preserved by composition as much as possible. As an example, we want to be able to infer that the combined medium

(M_{d}^{a,c} | M_{f−d}^{c,b})\c

is a correct implementation of S_{e,f}^{a,b} directly from (1) and the obvious fact that M_{f−d}^{c,b} ⊴ S_{e−d,f−d}^{c,b}. Clearly, this inference is possible provided the refinement ⊴ is preserved by parallel composition and restriction.

2Tav is a system for deciding various equivalences between CCS processes [Mil89].

3As usual we take S\c to mean S but restricted from c.

TMS and the various notions of refinements also makes our correctness proofs far more general than correctness proofs within standard (timed) process calculi. That is, a single correctness proof in TMS may capture a whole (possibly) infinite family of correctness proofs in process calculi. For instance, in the example above the correctness proof of (1) establishes in a single refinement the fact that (M_{d}^{a,c} | M)\c is a correct implementation of S_{e,f}^{a,b} whenever M is chosen from the infinite set {M_{g}^{c,b} | g ∈ [e − d, f − d]}.

Temporal logics with explicit time provides an alternative framework for expressing loose specifications of real–time systems. In fact there have been quite substantial work on model–checking with respect to such logics [ACD90], and automatic tools for carrying out the model–checking has been or are under implementation (e.g. [NSY92]). However, no results as to the composition of (timed) logical specifications has been offered so far, and compositional verification and stepwise refinement are therefore not supported. Rather the tools and techniques developed within the (timed) logical framework always compare a (final) implementation with the (initial) specification. In contrast, the theory of TMS and the Epsilon tool are intended to be used throughout the entire development process.

The remainder of this paper is organized as follows. The next section contains a brief outline of Modal Specifications. Section 3 gives the definition of TMS and provides an operational semantics for composition with respect to the constructs of TCCS. Various notions of abstracting refinements are introduced in Section 4. The theory underlying TMS and the tools of Epsilon are applied in Section 5 in the verification of a (classical) train crossing example. In Section 6 we propose a new refinement abstracting from internal events. The last section offers a compact outline of the actual refinement checking algorithms as carried out by Epsilon.

2 Modal Specifications

Modal Specifications (or Modal Transition Systems) were introduced in [LT88] in order to allow loose or partial specifications to be expressed in a process algebraic framework. Semantically, Modal Specifications are given an operational interpretation imposing restrictions on the transitions of possible implementations by telling which transitions are necessary and which are admissible. The transition systems for Modal Specifications therefore have two transition relations: ⟶_{□} describing the required transitions and ⟶_{◇} describing the allowed transitions.

Definition 2.1 A modal transition system is a structure M = (S, A, ⟶_{□} , ⟶_{◇} ), where S is a set of specifications, A is set of actions and ⟶_{□}, ⟶_{◇} ⊆ S × A × S, satisfying the condition ⟶_{□} ⊆⟶_{◇} .

The condition ⟶_{□} ⊆⟶_{◇} simply says that anything required is also allowed, thus ensuring consistency of any Modal Specification. Clearly, the more a specification allows and the less it requires the looser the specification is. This idea is formalized in the following notion of refinement Definition 2.2 A refinement R is a binary relation on S such that whenever SRT and a ∈ A then the following holds:

1. Whenever S ⟶_{◇}^{a} S′, then T ⟶_{◇}^{a} T′ for some T′ with S′RT′,

2. Whenever T ⟶_{□}^{a} T′, then S ⟶_{□}^{a} S′ for some S′ with S′RT′.

We say that S refines T whenever (S, T) is contained in some refinement R. In this case we write S ⊲ T.

The behaviour of processes themselves is assumed to be given in terms of a standard labelled transition system, which may be seen as a special case of Modal Specifications with all transitions being required (i.e. ⟶_{□} =⟶_{◇} ). In this case the new notion of refinement coincides with the classical notion of bisimulation.

3 Timed Modal Specifications

The language we use to describe timed processes is the real–time calculus TCCS of Wang [Wan90]. This calculus is essentially Milner’s CCS [Mil89] extended with a delay construct ϵ(d).P, which informally means ”wait for d units of time and then behave like the process P ”, where d ∈ R_{+} is a positive real.

The semantics of TCCS applies the ”two–phase functioning principle” outlined in [NSY91]. That is, the behaviour of a real–time system is divided into two phases: one phase in which the components of the system agrees to let time pass, and a second phase in which the system computes by performing (instantaneous) actions. In the operational semantics of TCCS this is reflected by having transitions labelled by either action names or delays being positive reals.

Similar to the Modal Specification extensions of classical Process Algebra (e.g. CCS), and for the very same reasons,^{4} we offer in the following a Modal Specification extension of the real–time calculus TCCS.

3.1 Informal Semantics

First consider the TCCS process term a.P. As a specification this term is quite specific, in that it requires an implementation at any moment to be able to perform the action a and implement P thereafter. This interpretation is formalized by the following required transitions for a.P

a.P ⟶_{□}^{a} P a.P ⟶_{□}^{ϵ(d)} a.P for all d > 0

In the following we shall adopt the notation a_{□} .P for a.P.

To obtain looseness^{5} we introduce a new may prefix construct a_{◇} .P. As a specification this term will at any moment allow (without requiring) an implementation to have an a–transition as long as the result of such a transition implements P. Formally this is reflected in the following transitions

a_{◇} .P ⟶_{◇}^{a} P a_{◇} .P ⟶_{□}^{ϵ(d)} a_{◇} .P for all d > 0

4I.e. to obtain looseness in specifications.

5and analogous with the Modal Specification extension of CCS.

Informally, it should be rather clear that a_{◇} .P is a fairly loose specification covering a range of different implementations. In particular, a_{◇} .P will contain as typical implementations the processes a.P, for obvious reasons; nil, which never enables any actions and therefore trivially satisfies P after any possible a–transition, and, for any d, ϵ(d).a.P, which possess no actions before having delayed d units after which any a–transition clearly will lead to a derivative implementing P. To formally verify that (say) ϵ(d).a.P is indeed an implementation (i.e. refines) a_{◇} .P, simply note that the relation

R = {(ϵ(d).a.P, a_{◇} .P) | d > 0} ∪ Id

is a refinement.

In order to support compositional verification we want the ability to combine Timed Modal Specifications with respect to the process constructs of TCCS, in particular with respect to that of parallel composition. Here we recall that the real–time calculus TCCS applies the maximal progress assumption: i.e. if a process is in a state in which it can perform internal (τ) computations then time is not allowed to pass. As an example consider the following combined Timed Modal Specification

(\overline{a}_{◇} .S | a_{◇} .T)\a  (2)

Implementations of (2) should essentially be of the form (P | Q)\a, where P implements \overline{a}_{◇} .S and Q implements a_{◇} .T. From the discussion above we already know three typical implementations of a may– prefixed term. Hence, typical implementations^{6} of (2) will be of the form

(ϵ(d).\overline{a}.P′ | ϵ(d′).a.Q′)\a  (3)

where P′ and Q′ implements S and T, respectively. Now, the operational semantics to be given to the combined Timed Modal Specification (2) should capture precisely these desired implementations. Choosing d = d′ = 0 in (3), we obtain a desired implementation which — due to the maximal progress assumption — can perform nothing but a τ–transition (in particular it cannot delay). Thus, it is clear that (\overline{a}_{◇} .S | a_{◇} .T)\a should (at least) allow τ–transitions, whereas delay–transitions can not be required. In general, however, implementations of the form (3) are not immediately able to perform a τ–transition; rather a delay of max\{d, d′\} time units must elapse. Hence, (\overline{a}_{◇} .S | a_{◇} .T)\a cannot insist on an immediate τ–transition, and should on the other hand allow implementations to delay. In summary, (\overline{a}_{◇} .S | a_{◇} .T)\a is given the following transitions

(\overline{a}_{◇} .S | a_{◇} .T)\a ⟶_{◇}^{τ} (S | T)\a

(\overline{a}_{◇} .S | a_{◇} .T)\a ⟶_{◇}^{ϵ(d)} (\overline{a}_{◇} .S | a_{◇} .T)\a

Now it is reasonable to expect that (\overline{a}_{◇} .S | a_{◇} .T)\a should be equivalent to the specification τ_{◇} .((S | T)\a). This means that the semantics of specifications of the form τ_{◇} .S should be given by the following two axioms

τ_{◇} .S ⟶_{◇}^{τ} S τ_{◇} .S ⟶_{◇}^{ϵ(d)} τ_{◇} .S

6besides nil.

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

\frac{S ⟶_{m}^{a} S′}{S\A ⟶_{m}^{a} S′\A} a, \overline{a} ∉ A  \frac{S ⟶_{m}^{a} S′}{S + T ⟶_{m}^{a} S′}  \frac{T ⟶_{m}^{a} T′}{S + T ⟶_{m}^{a} T′}

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

Table 1: Action Rules for TMS (m ∈ {□, ◇}).

3.2 Formal Syntax and Semantics

After the introductory discussion, we are now ready to formally present the syntax and semantics for TMS. As in CCS, we assume a set Λ = Δ ∪ Δ̄ with ¯ ᾱ = α for all α ∈ Λ, ranged over by α, β representing external actions, and a distinct symbol τ representing internal actions. We use Act to denote the set Λ ∪ {τ} ranged over by a, b representing both internal and external actions. Further, assume a set of process variables ranged over by X.

We adopt a two–phase syntax to describe networks of regular TMS. First, regular TMS expressions are generated by the following grammar

E ::= nil |ϵ(d).E | a_{◇} .E | a_{□} .E | E + E | X

where X ranges over a finite set of variables Var and d ranges over R_{+} (the positive reals). We shall assume that process variables are defined by a recursive equation system

E = {X =^{def} E_{X} | X ∈ Var}

where all variables in E_{X} are guarded in the sense that each variable occurrence is within the scope of an action or delay prefix. Networks of regular TMS’ are composite expressions of the form

(S_{1} | … | S_{n})\A

where S_{i} are regular TMS and | and \A denote CCS parallel composition and restriction respectively. We will use S and T to range over (networks of regular) Timed Modal Specifications.

We now offer a modal transition semantics for TMS. This semantics is a conservative extension of the semantics for TCCS developed in [Wan90]. We present the transition rules in two groups: rules for actions in Table 1 and rules for delays in Table 2.^{7} It should be rather clear from Table 1 and 2 that we indeed have defined a modal transition system, i.e. ⟶_{□} ⊆⟶_{◇} . As such, it can readily be seen that ⟶_{□} –transitions may be derived for a combined specification (S + T or S | T) only if ⟶_{□} –transitions can be inferred for the contributing components. That is, in the derivation of transitions for a combined specification, the transitions contributed by the components should agree with respect to modality.

The side condition for the delay rule of parallel composition is to guarantee that (parallel composed) specifications satisfy the following two maximal progress assumptions

7In Table 2, we use d to stand for a non-zero real; this implies that an ϵ(0)–transition can never be inferred by the inference rules. However, we shall apply the convention that S ⟶_{m}^{ϵ(0)} S for all S.

\frac{−}{nil ⟶_{m}^{ϵ(d)} nil}  \frac{−}{α_{n}.S ⟶_{m}^{ϵ(d)} α_{n}.S}  \frac{−}{τ_{◇} .S ⟶_{◇}^{ϵ(d)} τ_{◇} .S}

\frac{−}{ϵ(c + d).S ⟶_{m}^{ϵ(d)} ϵ(c).S}  \frac{S ⟶_{m}^{ϵ(d)} S′}{ϵ(c).S ⟶_{m}^{ϵ(c+d)} S′}  \frac{S ⟶_{m}^{ϵ(d)} S′}{S\A ⟶_{m}^{ϵ(d)} S′\A}

\frac{S ⟶_{m}^{ϵ(d)} S′  T ⟶_{m}^{ϵ(d)} T′}{S + T ⟶_{m}^{ϵ(d)} S′ + T′}  \frac{S ⟶_{m}^{ϵ(d)} S′}{X ⟶_{m}^{ϵ(d)} S′} [X =^{def} S] ∈ E

\frac{S ⟶_{m}^{ϵ(d)} S′ T ⟶_{m}^{ϵ(d)} T′}{S | T ⟶_{m}^{ϵ(d)} S′ | T′} Sort_{m^{c}}(d, S) ∩ \overline{Sort_{m^{c}}(d, T)} = ∅

Table 2: Delay Rules for TMS (m, n ∈ {□, ◇} and □^{c} = ◇, ◇^{c} = □).

• a timed specification will not allow delays if it requires an internal action τ.

• a timed specification will not require delays if it allows an internal action τ.

For timed processes (i.e. timed specifications with all transitions being required) these two assumptions coincide and reduce exactly to the notion of maximal progress for processes. The two conditions above are formalized by means of two functions Sort_{□} and Sort_{◇} defined (inductively) in Table 3. Intuitively, given a positive real d and a timed modal specification S, Sort_{□} (d, S) (Sort_{◇} (d, S)) includes all external actions that S requires (allows) an implementation to enable within d time units; hence the side condition Sort_{□} (d, S) ∩ \overline{Sort_{□} (d, T)} = ∅ (Sort_{◇} (d, S) ∩ \overline{Sort_{◇} (d, T)} = ∅) means that implementations of S and T will not necessarily (can not possibly) be able to communicate with each other within d time units.

Definition 3.1 Given a timed modal specification S, we define Sort_{□} (0, S) = Sort_{◇} (0, S) = ∅ and Sort_{□} (c, S) and Sort_{◇} (c, S) for c ≠ 0 to be the least sets satisfying the equations^{8} given in Table 3.

The following properties of timed specifications are obvious generalizations of central properties of timed processes in [Wan90]

Proposition 3.2

1. (Maximal progress) If S ⟶_{m}^{τ} S′ for some S′, then S ⟶^{ϵ(d)}_{m^{c}} S′′ for no d and S′′.

2. (Time determinism) Whenever S ⟶_{m}^{ϵ(d)} S′ and S ⟶_{m}^{ϵ(d)} S′′ then S′ = S′′.

3. (Persistence) If S ⟶_{m}^{ϵ(d)} S′ and S ⟶_{m}^{α} T for some S′ and T, then S′ ⟶_{m}^{α} T′ for some T′.

4. (Time continuity) For all c, d and S′′, S ⟶_{m}^{ϵ(c+d)} S′′ iff S ⟶_{m}^{ϵ(c)} S′ ⟶_{m}^{ϵ(d)} S′′ for some S′.

5. (Transition liveness) Either S ⟶_{m}^{τ} S′ for some S′ or S ⟶^{ϵ(d)}_{m^{c}} S′′ for some S′′ and d > 0.

8In Table 3, c− · d is defined to be c − d if c > d, 0 otherwise.

Sort_{m}(d, nil) = ∅
Sort_{□} (d, α_{□} .S) = {α}
Sort_{□} (d, α_{◇} .S) = ∅
Sort_{m}(d, τ_{n}.S) = ∅
Sort_{◇} (d, α_{m}.S) = {α}
Sort_{m}(d, ϵ(c).S) = Sort_{m}(d− · c, S)
Sort_{m}(d, S + T) = Sort_{m}(d, S) ∪ Sort_{m}(d, T)
Sort_{m}(d, S | T) = Sort_{m}(d, S) ∪ Sort_{m}(d, T)
Sort_{m}(d, S\A) = Sort_{m}(d, S) \ (A ∪ \overline{A})
Sort_{m}(d, X) = Sort_{m}(d, S), [X =^{def} S] ∈ E

Table 3: Definition of Sort_{□} and Sort_{◇} (m, n ∈ {□, ◇}).

4 Abstracting Refinements

As already mentioned, TMS together with the two modal transition relations ⟶_{□} and ⟶_{◇} defined in Table 1 and 2 constitutes a modal transition system. As such, we may readily apply the general notion of refinement from Definition 2.2 to TMS.

However, this refinement will often be too strong in practical applications. In particular, a refinement based directly on ⟶_{□} and ⟶_{◇} will be completely sensitive to internal computation. In contrast, practical applications often need to abstract away from internal computation of systems. Also, when reasoning about large combined real–time systems, explicit timing information may in a first analysis be unimportant, in which case a time–abstracting refinement will suffice. Though such a refinement yields no information about the timing behaviour of the overall system, it will demand proper interaction between the timing properties of the components of the system.

Abstracting refinements with the above properties will be obtained through the definition of similarly abstracting versions of the modal transition relations ⟶_{□} and ⟶_{◇} . The abstracting transition relations will in all cases be generated by an abstraction function Φ on labels.^{9} Now, recall that the modal transitions for TMS are labeled by elements of the following set

L = Act ∪ Delay

where

Delay = {ϵ(d) | d > 0}

An abstraction function Φ maps sequences of (concrete) labels into a single (abstract) label. More precisely, an abstraction function Φ is a partial function of the following type

9This is strongly inspired by the notion of observation criterion in AUTO [SV89].

Φ : L^{∗} ↪ L ∪ {ε}

The partiality of Φ indicates that not all sequences of (concrete) labels makes sense as abstract actions. Also, Φ(s) = ε signifies that s is unobservable when viewed through the abstraction given by Φ.

Given an abstraction function we can now define abstracting transition relations.

Definition 4.1 Let Φ be an abstraction function. Then the abstracting transitions relations ⟶_{□}^{Φ} and ⟶_{◇}^{Φ} are defined as (m ranges over □ and ◇)

• S⟶^{σ}_{m}^{Φ} S′ whenever S ⟶_{m}^{μ_{1}} ⋯ ⟶_{m}^{μ_{n}} S′ with Φ(μ_{1} … μ_{n}) ≃ σ for some μ_{1}, …, μ_{n}, σ. ^{10}

Now it is easy to verify that TMS equipped with any abstracting transition relations ⟶_{□}^{Φ} and ⟶_{◇}^{Φ} does indeed constitute a modal transition system in the sense of Definition 2.1. Hence, we may apply the notion of refinement from Definition 2.2

Notation 4.2 If S refines T with respect to the Φ–abstracting transition relations ⟶_{□}^{Φ} and ⟶_{◇}^{Φ}, we say that S refines T with respect to the abstraction function Φ.

We now present the abstraction functions which will induce the desired τ– and time–abstracting refinements.

Definition 4.3 The τ–abstracting function Φ_{τ} is defined as follows

Φ_{τ}(τ^{k}) = ε; k ≥ 0
Φ_{τ}(τ^{k_{0}}ϵ(d_{1})τ^{k_{1}} … ϵ(d_{n})τ^{k_{n}}) = ϵ(d_{1} + … + d_{n}) ; k_{j} ≥ 0
Φ_{τ}(τ^{k}ατ^{j}) = α; k, j ≥ 0

Whenever S refines T with respect to Φ_{τ} we say that S weakly refines T. We write S ⊴ T in this case.

In the following we shall use also a more standard process algebraic notation S ⟹^{μ}_{m} S′ for S⟶^{μ}_{m}^{Φ_{τ}} S′ for any admissible label μ ∈ {ε} ∪ Λ ∪ Delay.

Following the proofs for timed equivalence in [Wan90] it can be shown ([God94]) that the non–abstracting refinement ⊲ is preserved by all constructs of TMS. For the weak refinement ⊴ a certain very natural syntactic conditions on specifications can be defined (see Section 6.1) which ensure also it to be preserved by all TMS constructs except summation (as usual for τ-abstracted process algebraic constructs). We study the (general lack of) compositionality of ⊴ in more detail in Section 6, where we also propose a new τ–abstracting refinement that is preserved by parallel composition.

The two following functions abstract from time (and internal computation)

Definition 4.4 The time–abstracting function Φ_{ϵ} is defined as follows

\begin{matrix}Φ_{ϵ}(s) = ε; s ∈ Delay^{∗} \\ Φ_{ϵ}(s_{1}as_{2}) = a; s_{1}, s_{2} ∈ Delay^{∗} \end{matrix}

Whenever S refines T with respect to Φ_{ϵ} we say that S is a time–abstracted refinement of T. We write S ⊲^{•} T in this case.

10For expressions e_{1} and e_{2}, e_{1} ≃ e_{2} holds if both expressions are defined and have the same value.

Definition 4.5 The τ– and time–abstracting function Φ_{τϵ} is defined as follows

\begin{matrix}Φ_{τϵ}(s) = ε; s ∈ (Delay ∪ \{τ\})^{∗} \\ Φ_{τϵ}(s_{1}αs_{2}) = α; s_{1}, s_{2} ∈ (Delay ∪ \{τ\})^{∗} \end{matrix}

Whenever S refines T with respect to Φ_{τϵ} we say that S is a weak time–abstracted refinement of T. We write S ⊴^{•} T in this case.

The two time–abstracting refinements are not preserved by the constructs of TMS (in particularly not parallel composition). However, the full abstractness result for time abstracted equivalences proved in [LW90] extends to ⊲^{•}. That is, the largest pre–order contained in ⊲^{•} which is also preserved by parallel composition will be ⊲. The proof can be found in [God94].

[figure: ⊲; ⊴; ⊲^{•}; ⊴^{•}]

Figure 1: Ordering refinements.

In Figure 1 we illustrate the relationship between the four refinements introduced. The arrows between, ⊲ and ⊲^{•} say, represents the set inclusion ⊲⊆⊲^{•}. The proof of these inclusions, that they are strict and also the only inclusions among the four refinements are straightforward. Also, it is easy to prove that the refinements, when restricted to timed processes, coincide with the corresponding equivalences studied at length in [LW90].

Example 4.6 Recall the combined media specification (1) from the introduction

(M_{d}^{a,c} | S_{e−d,f−d}^{c,b})\c

where ^{11}

M_{x}^{a,b} =^{def} a_{□} .ϵ(x).\overline{b}_{□} .
S_{x,y}^{a,b} =^{def} a_{□} .(ϵ(x).\overline{b}_{◇} . + ϵ(y).\overline{b}_{□} .)

Then the following abstracting refinements may be deduced

(M_{d}^{a,c} | S_{e−d,f−d}^{c,b})\c ⊴ S_{e,f}^{a,b}
(M_{d}^{a,c} | S_{e−d,f−d}^{c,b})\c ⊴^{•} S_{0,0}^{a,b}

i.e. the combined media weakly refines a media with delay between e and f and is a weak time–abstracted refinement of a medium which enables its output immediately after reception of its input.

11We omit trailing nil’s; i.e. a_{m} abbreviates a_{m}.nil.

[figure: app; close; open; enter; exit; inside; outside; down; up; Ct; G; Cr; T]

Figure 2: The Train Crossing.

The verification tool Epsilon supports automatic verification for all four types of refinements we have considered so far. In fact, all instances of the weak and time–abstracted refinements in the above example can be automatically checked using Epsilon. To be precise, the tool Epsilon supports automatic refinement checking for a slightly restricted class of TMS, namely, for those specifications which are initially integral timed (also called simply integral timed and abbreviated IT) according to the following definition.

Definition 4.7 S is initially integral timed iff every delay prefix ϵ(d) occurring in S has the delay d ∈ N.

Actually, the algorithms would apply also for specifications with delays being positive rationals, as we may simply multiply all delays with some rational q in order to end up with a comparison of initially integral processes. It should also be noted that an IT TMS specification still can perform delays of arbitrary real length^{12}, as well as all instances of TMS specifications naturally appearing in the considered Train Crossing example (see Section 5) are initially integral timed.

In the next section of this paper, we shall demonstrate the tools of Epsilon on a somewhat larger and more complex example.

5 The Train Crossing

In this section we demonstrate the applicability of the TMS theory and the tool Epsilon to a small example of a train crossing. Similar examples can be found elsewhere in the literature, e.g. [AD91].

The Train Crossing (see Figure 2) is a small idealized example of a real world train crossing. It consists of four components: the crossing (Cr), a train (T), the gate (G) and the controller (Ct). When a train approaches the crossing it sends a signal to the controller. Having received the signal, after some delay the controller starts closing the gate. Then, after some more delay the controller starts opening the gate. The train is assumed to have moved through the crossing while the gate was closed.

The external events of our model system will be down and up meant to occur when the gate is becoming closed or open, as well as inside and outside representing the moments of the train actually entering and leaving the crossing.

The TMS specification of the crossing is given in Figure 3 by TrainCrossing(X,A,B,C,U,V). It consists of four parallel components, namely the crossing, the gate, a train and the controller. We have made

12For instance, ϵ(1).a_{□} .nil ⟶^{ϵ(0.34)} ϵ(0.66).a_{□} .nil.

      Crossing :=:  in(enter);inside!Crossing With Train
      Crossing With Train :=:  in(exit);outside!Crossing
      Gate(X) :=:  in(close);ϵ[0,X].tau;down!Gate Closed(X)
      Gate Closed(X) :=:  in(open);ϵ[0,X].tau;up!Gate(X))
      Train(A,B,C) :=:  out(app)?Train To Enter(A,B,C)
      Train To Enter(A,B,C) :=: ϵ[A,B].out(enter);Train In(A,B,C)
      Train In(A,B,C) :=: ϵ[0,C].out(exit);Train(A,B,C)
      Controller(U,V) :=:  in(app);Contr Close(U,V)
      Contr Close(U,V) :=: ϵ[0,U].out(close);Contr Open(U,V)
      Contr Open(U,V) :=: ϵ(V);out(open);Controller(U,V)
      TrainCrossing(X,A,B,C,U,V) :=:
      (Crossing/Gate(X)/Train(A,B,C)/Controller(U,V))\[enter,exit,close,open,app]

Figure 3: Specification of the train crossing in Epsilon.

the specification explicitly dependent on a number of time parameters to illustrate the effect of their modification on the properties of the specified system.

In the specification we have introduced some (possibly generally useful) derived language constructs, namely,

• ϵ[d, e].a.S is a shorthand for ϵ(d).a_{◇} .S + ϵ(e).a_{□} .S (it means that the transition with the action a, leading to S may be enabled after d time units, but it must be enabled after e time units (usually d < e)), and

• a!S abbreviates T =^{def} a_{□} .S + τ_{□} .T (it is a kind of “time-lock” operation: the τ_{□} –loop around T ensures that the time is not allowed to pass due to the maximal progress assumption, so the only behaviour what such a specification allows is doing the a immedilately. This is the way, how immediate (urgent) actions are modelled in TMS.).

In Epsilon :=: is used for declarations binding the left hand side identifier to the right hand side, ; denotes the must modality and ? the may modality. in(a) and out(a) are used to represent an action and its corresponding co–action and restriction from actions is defined by \L where L is a list of actions.

The first of the four components, the Crossing is simply keeping track of whether there is a train in it, or not, and at any time when a train either enters or leaves, it gives an immediate signal inside or outside to the external observer.

The Gate is either open or closed. It is receiving signals open and close from the controller. After receiving a signal, say close, it takes for the gate some time in the range of [0, X] to actually become closed. When the gate becomes closed (open), a corresponding external output signal (down or up) is signalled immedilately.

                 Spec1 :=:  down?inside?outside?up?Spec1
                 Spec2(D) :=:  Spec2a(D)/Admit Urgency
                 Spec2a(D) :=:  down?ϵ(D);inside?outside?up?Spec2a(D)
                 Spec3(M,N) :=:  DownUp(M,N)/Uni([inside,outside])
                 Spec4(M,N) :=:  DownUp(M,N)/InOut/Admit Urgency
                 DownUp(M,N) :=:  down?ϵ[M,N].up;DownUp(M,N)
                 InOut :=:  inside?outside?InOut
                 Admit Urgency :=:  tau?Admit Urgency
                 Spec5(P) :=:  Down(P)/Uni([inside,outside,up])
                 Down(P) :=:  down?P;Down(P)

Figure 4: Specifications.

The Train initially may send a signal to the controller about its approaching^{13}. The train is then supposed to enter the crossing within the interval from A to B. Further on, it will necessarily leave the crossing no later than C time units after it entered.

In the initial state the Controller waits for the approaching of a train. If a train approaches he starts closing the gate no later than U time units after the approaching was signalled. Then he waits for V time units before opening the gate.

Figure 4 contains a few properties (specifications) against which the considered train crossing model can be analyzed.

First, a natural safety property for the train crossing to satisfy would be the occurrence of its external events in the order, as prescribed by Spec1. We express this fact in the theory by the weak time abstracted refinement between TrainCrossing(X,A,B,C,U,V) and Spec1. Using Epsilon it can be found out that, for instance,

                           TrainCrossing(1,3,4,1,1,6) ⊴^{•} Spec1

Actually, TrainCrossing(X,A,B,C,U,V) will be a weak time abstracted refinement of Spec1 whenever U + X < A and B + C < V (and for any particular values of the time parameters the fact of the refinement can be established by Epsilon; in fact, alongside with a symbolic description of the contents of the refinement, see Section 7). It is to be observed also that, though the specification Spec1 is not explicitly mentioning time quantities at all, the correctness of the train crossing model against this specification is crucially dependent on the time quantities put in the description of various components of the model (intuitively, the internal timing properties of the model are precluding some order of the external events by requiring that some component is going always to produce its output faster than the other).

However, not all important properties of real time systems can be described solely in terms of the ordering of the system external event occurrences. In the case of the train crossing it might be very important to require that always there will be a certain delay of, say, D time units between the gate becoming closed and the following moment when the train enters the crossing^{14}. We express this fact in the TMS theory by TrainCrossing(X,A,B,C,U,V) being a weak timed refinement of Spec2(D), and we may find out (either reasoning theoretically, or just by applying Epsilon) that

13Note, that we do not require a train to approach the crossing. If no train will approach the crossing the whole system is inactive. In the theory this is reflected by nil ⊲ TrainCrossing(X,A,B,C,U,V) for any values of X, A, B, C, U and V.

    TrainCrossing(1,3,4,1,1,6) ⊴ Spec2(1), but TrainCrossing(1,3,4,1,1,6) ⋬ Spec2(2).

And indeed, there can be implementations of TrainCrossing(1,3,4,1,1,6) which do let less that 2 time units between the events down and inside^{15}.

Similarly, we could ask about the relationship between the time moments of the closing and the opening of the gate. For that purpose we define Spec3(M,N). Intuitively, Spec3(M,N) specifies that the opening of the gate is guaranteed to occur in the interval from M to N after it was lowered. Here we use another specification shorthand, namely, the very loose specification

Uni(L) =^{def} ∏_{a∈L∪{τ}} a_{◇} .Uni(L)

where Π denotes an n–ary parallel composition and L ⊆ Act. Uni(L) is a “universal specification” in the sense that S ⊲ Uni(L) for any timed modal specification S with sort contained in L ^{16}.

Whenever M ≤ 5 and N ≥ 7 it turns out, applying Epsilon, that

                        TrainCrossing(1,3,4,1,1,6) ⊴ Spec3(M,N)  (4)

Hence, due to the strongest of these specifications, Spec3(5,7), the gate must be opened no later than 7 time units after it was closed. Moreover, it is impossible to tigthen the interval between the opening and the lowering of the gate, e.g. Spec3(5,6) is shown by Epsilon not be weak refined by

TrainCrossing(1,3,4,1,1,6).

Actually, for the values of M and N mentioned above, we can prove that TrainCrossing(1,3,4,1,1,6) is a weak refinement of the even stronger property Spec4(M,N), that is, compared to Spec3(M,N) we furthermore require a specific ordering of the external events inside and outside.

Under the assumption that a proof of

                        TrainCrossing(1,3,4,1,1,6) ⊴ Spec4(M,N)

had already been given, a direct proof of (4) would not be needed. As ⊲ is preserved by parallel composition, we can obtain the result in an alternative manner exploiting the compositionality. We prove that

14In case if there is very little time between these two events, think of a car which has entered the crossing just before the gate was closed, and has broken there. If there were enough time, it would be at least possible for people to leave the car, even better, if the car could be taken out mechanically, or the train could be stopped.

15A note is to be added about the specification component Admit Urgency. When we are given a specification like a_{◇} .S (or a_{□} , for that matter), it does not admit the implementation a!S, nor does it admit ϵ(d).a!S + a_{□} .S for any d ≥ 0. This is because the specification is requiring (unlimited) delay ability from all its implementations (see the TMS delay semantics description in Table 2). The component Admit Urgency, when added to the specification, contributes by discarding the delay ability requirement by the specification both in its initial and in any of its (operational) derivative states (Admit Urgency only allows delays, without requiring them). As our example does contain immediate (urgent) actions (in fact, we have made all our external actions urgent), it can refine only specifications which does admit them. It is clear, however, that as a specification component the Admit Urgency is harmless since allowing the implementations to have immediate actions is the only effect which it has.

16Thus Uni(L) is the weakest specification with sort L. It does also admit urgent actions, in fact Admit Urgency = Uni(∅).

               FastContr :=:  in(app);out(close);6;out(open);FastContr
               SlowContr :=:  in(app);1;out(close);6;out(open);SlowContr

Figure 5: Implementations.

                      InOut/Admit Urgency ⊲ Uni([inside,outside])

(which obviously holds) to immediately conclude Spec4(M,N) ⊴ Spec3(M,N). The rest of the proof is due to the transitivity of ⊴.

Another interesting property is the frequency of the lowering of the gate. More precisely, we want to determine the values of P for which TrainCrossing(1,3,4,1,1,6) is a weak refinement of Spec5(P). Intuitively, Spec5(P) specifies that the frequency between two consecutive closing of the gate must be at least P time units. At a first glance one would expect the frequency to be at least 6 time units because the controller must wait exactly 6 time units between initializing the lowering and opening of the gate. However, using Epsilon we can find that

                         TrainCrossing(1,3,4,1,1,6)⋬ Spec5(6)

The reason for this is that it may take up to one time unit for the gate to close and later there is a possibility to open and afterwards close again immediately without performing any delay.

Instead, whenever P ≤ 5, we have

                        TrainCrossing(1,3,4,1,1,6) ⊴ Spec5(P)  (5)

We can either prove (5) directly in Epsilon or alternatively, for any P ≤ 5, we could prove instead that

                                Spec3(P,7) ⊴ Spec5(P)  (6)

and then take advantage of the transitivity of ⊴. Due to compositionality, (6) holds since

                           DownUp(P,7) ⊴ Down(P)/Uni([up])

for any P ≤ 5.

Implementations of the loosely specified train crossing of Figure 3 may now be found simply by substituting each of the four components with some timed process (strongly or weakly) refining the component. Due to the partiality (looseness) of the specification of the components^{17} each component will have several inequivalent implementations. For instance, as implementation of the controller one could choose one of the processes in Figure 5. Clearly FastContr and SlowContr are inequivalent and obviously both

FastContr and SlowContr refines Controller(1,6).

Finally, let us emphasize the generality of correctness proofs carried out within the framework of TMS. Indeed, no matter which implementation of the Train Crossing we will decide upon, it will be ensured, as a consequence of the compositionality of verification in TMS, that any of those is guaranteed to satisfy all the properties above refined by TrainCrossing(1,3,4,1,1,6).

17Except for the Crossing of course.

6 Achieving Congruicity

In this section we examine the general lack of compositionality of the weak refinement ⊴ in more detail, and show two possible ways of coping with this deficiency. The first possibility is obtained through a syntactic restriction and the second possibility consists of a redefinition of weak refinement. It should be noted although that for most practical examples we belive that the weak refinement is preserved by parallel composition.

To see that ⊴ can in general not be preserved by parallel composition, consider the following example:

Let C be defined by

C =^{def} τ_{□} .C + τ_{◇} .(\overline{b}_{□} + τ_{◇} .(\overline{a}_{□} + ϵ(1).c_{□}))

Then nil ⊴ (C | ϵ(1).a_{□})\a since

{(nil, (C | ϵ(1).a_{□})\a)}
∪\{(nil, ((\overline{a}_{□} + ϵ(1).c_{□}) | ϵ(d).a_{□})\a) | d < 1\}
∪\{(nil, ((\overline{a}_{□} + ϵ(e).c_{□}) | ϵ(d).a_{□})\a) | d < e < 1\}
∪\{(nil, ((\overline{a}_{□} + ϵ(d).c_{□}) | a_{□})\a) | d < 1\}
∪{(nil, (nil | nil)\a)}

constitutes a refinement wrt. Φ_{τ}. Now, let S =^{def} nil | b_{□} and let T =^{def} ((C | ϵ(1).a_{□})\a) | b_{□}. ^{18} Then one may prove that S ⋬ T. Intuitively, S ⋬ T because S allows a delay, say half a time unit, and this delay can only be matched by T in such a way that T cannot allow b or such that T after yet another half time unit requires c.

6.1 Syntactic Conditions

Following we present a syntactic condition under which the weak refinement ⊴ is preserved by parallel composition. It shall be noted, however, that the condition is far from being also necessary. Finding further even less restrictive conditions has not been included in the scope of this paper, as we believe that the work on those can benefit from the further case studies using TMS.

We first define the set of actions Sort_{m} as follows:

Definition 6.1 Define for any regular S the set Sort_{m} ⊆ Λ as the least set satisfying the equations in Table 4.

18Strictly speaking T is not a network according to the definition of networks in Section 3.2. However, it is immediate that T can easily be transformed to the TMS network ((C | ϵ(1).a_{□} ) | b_{□} )\a.

Sort_{m}(nil) = ∅

Sort_{m}(ϵ(d).S) = Sort_{m}(S)

Sort_{m}(a_{m}.S) = {a} ∪ Sort_{m}(S)

Sort_{m}(τ_{m}.S) = Sort_{m}(S)

Sort_{m}(μ_{m^{c}}.S) = Sort_{m}(S)

Sort_{m}(S + T) = Sort_{m}(S) ∪ Sort_{m}(d, T)

Sort_{m}(C) = Sort_{m}(S_{C}), C =^{def} S_{C}

Table 4: Definition of Sort_{m}(S).

Then the restriction we impose on a network S = (S_{1} | … | S_{n})\A is that S must not contain τ_{◇} and for all S_{i}

α ∈ Sort_{◇} (S_{i}) implies
∀j ≠ i. \overline{α} ∉ Sort_{◇} (S_{j}) ∪ Sort_{□} (S_{j})

The restriction on networks implies that any network satisfying the restriction cannot allow without also requiring an internal transition.

It can be proven that for networks satisfying the syntactic restriction ⊴ preserves parallel composition.

6.2 Trajectory Step Refinement

In this section we define an alternative τ-abstracted refinement relation for TMS, which proves to be semantically “better behaved” than ⊴ (though not as elegantly definable).

First, given two TMS T and T′, and d ∈ R_{>0} let us call any sequence (⟨T_{0}, d_{0}⟩, …, ⟨T_{n}, d_{n}⟩) such that

• T ⟹^{ε}_{◇} T_{0}, d_{0} = 0, T_{n} = T′, d_{n} = d and

• T_{i} ⟶_{◇}^{ϵ(δ_{i})} ⟹^{ε}_{◇} T_{i+1}, with δ_{i} = d_{i+1} − d_{i} for all i = 0, 1, …, n − 1

a step sequence for ⟨T, d, T′⟩ (or simply a ⟨T, d, T′⟩ - step sequence). Further, let S^{(d)} for a TMS S and d ≥ 0 denote the TMS S′ for which S ⟶_{◇}^{ϵ(d)} S′, if such S′ exists (due to the time determinacy property (see Proposition 3.2) such S′, if it exists, is unique).

Definition 6.2 A binary relation R ⊆ S × S is a trajectory step refinement if ⟨S, T ⟩ ∈ R implies

• S ⟶_{◇}^{a} S′ implies ∃T′. T ⟹^{a}_{◇} T′ and ⟨S′, T′⟩ ∈ R,

• T ⟶_{□}^{a} T′ implies ∃S′. S ⟹^{a}_{□} S′ and ⟨S′, T′⟩ ∈ R,

• S ⟶_{◇}^{ϵ(d)} S′ implies the existence of a ⟨T, d, T′⟩ - step sequence (⟨T_{0}, d_{0}⟩, …, ⟨T_{n}, d_{n}⟩) such that ⟨S^{(d_{i})}, T_{i}⟩ ∈ R for all i = 0, 1, …, n.

• T ⟶_{□}^{ϵ(d)} T′ implies ∃S′. S ⟹^{ϵ(d)}_{□} S′ and ⟨S′, T′⟩ ∈ R.

We denote by ⊲^{T} the largest trajectory step refinement. It is not difficult to establish that ⊲^{T} is a preorder (i.e., ⊲^{T} is reflexive and transitive) and that ⊲^{T} ⊆⊴. Moreover, ⊲^{T} is preserved by parallel composition (as well as all other TMS constructors except summation), the proof can be found in [God94].

Furthermore, one can prove rather easily that for TCCS processes (which are the implementations of the TMS specifications) the relation ⊲^{T} coincides with the TCCS weak bisimulation^{19} (as does also ⊴).

So, TMS with the refinement relations ⊲ and ⊲^{T} can be viewed as a conservative extension of Timed CCS with strong and weak bisimulation, being at the same time fully suitable for use in stepwise development process of real time systems.

Observe, though, that the definition of ⊲^{T} does not follow the general abstracting refinement definition pattern used in Section 4.

As all other refinemnet relations considered in this paper, also ⊲^{T} is decidable for (initially) integral timed TMS specifications. We outline the deciding algorithm in Section 7.5.

7 Algorithms for Refinement Checking

This section provides an outline of the algorithms for checking automatically whether two given (initially) integral timed modal specifications satisfy a given modal refinement relation (i.e. one of the relations ⊲, ⊴, ⊲^{•}, ⊴^{•} and ⊲^{T}). These algorithms are the basis for the verification tool Epsilon, in which ⊲, ⊴, ⊲^{•} and ⊴^{•} have been implemented.

Since the definitions of the considered refinement relations depend essentially on exploiting infinite transition systems defining semantics of TMS (in fact, these transition systems are in a certain sense even “continuous”, what is due to the density of the underlying time domain — non–negative reals), it is not possible to use them directly in the deciding algorithm. Instead, the algorithm uses a symbolic representation of TMS transition systems, based mainly on the region graph technique due to [AD90] and the following work in [Č92b] and [LW90] extending the region graph technique to work also for deciding timed and time abstracted bisimulation equivalences between timed processes.

The algorithms described in this section are theoretically rather direct generalizations of those described in [Č92b] and [LW90] for deciding corresponding (timed or time-abstracted) bisimulation equivalences, especially in the case of “timed” refinements (the strong and weak ones). The presentation of the refinement deciding algorithms in this section differs from the previous theoretical work mainly in

• being more concrete, with more detailed explanation of the used data structures, closely tied up with the basic design decisions implemented in the verification tool Epsilon;

• making use of explicitly compositional process algebraic style syntax of TMSs (this should be contrasted with the automata based model of Parallel Timer Processes for which the bisimulation equivalence problem was shown decidable in [Č92b]);

• providing uniform treatment in deciding time abstracted and time sensitive refinements.

19The proof relies on maximal progress and time determinism properties, which hold for TCCS (they hold also for TMS specifications).

Also a slightly novel point is the symbolic deciding procedure for trajectory step refinement in Section 7.5, what has not been considered before.

Yet for motivating the “correctness” of various parts of the developed algorithms we from time to time in the following refer to the basic theoretical papers [AD90], [Č92b] and [LW90].

7.1 Principal Schema of the Algorithms

Given two initially integral timed modal specifications S and T to be checked under some refinement relation ref (i.e. ⊲, ⊲^{•}, ⊴, ⊴^{•} of ⊲^{T}), the algorithm for deciding whether S is refined by T (i.e. if S ref T) can be thought as deciding some appropriate property over a certain finite symbolic transition system^{20}

T_{S,T} = ⟨X_{S,T} , L^{•}, ⟶, X_{0}⟩, where

• X_{S,T} is a set of symbolic states (each symbolic state X ∈ X_{S,T} is a representation of a certain (usually infinite) set of pairs ⟨S′, T′⟩ where S′ is a state of S and T′ is state of T);

• L^{•} is a set of symbolic labels (constructed from the actions a ∈ Act and some special actions used for representing delays);

• ⟶⊆ X_{S,T} × L^{•} × X_{S,T} is a symbolic transition relation; and

• X_{0} ∈ X_{S,T} is the initial state.

The property to be checked over T_{S,T} in each case is expressed as the existence of a state set X ⊆ X_{S,T} which is both containing X_{0} and satisfying a certain closeness property, such as, for instance, “for every

X ∈ X whenever X ⟶^{a} X′ for a ∈ L^{•}, then X′ ⟶^{a′} X′′ for some X′′ ∈ X ”.

More precisely, for every refinement relation ref a certain monotone functional F^{ref} on the powerset of X_{S,T} is defined (F^{ref} is mapping subsets of X_{S,T} to subsets of X_{S,T}), and the question to be answered about T_{S,T} (in order to decide, if S ref T) is formulated as

“Does there exist a set X ⊆ X_{S,T} such that X_{0} ∈ X and X ⊆ F^{ref}(X)?”

Equivalently, one can say that the algorithm is examining, whether X_{0} is contained in the greatest fixpoint of F^{ref}.

Having a monotone functional F over the finite symbolic transition system T_{S,T} there are a variety of ways how to check, if a certain state X_{0} of the system is contained in the greatest fixpoint of F. The tool Epsilon is based on the (efficient) local checking technique due to [Lar92], thus in constructing a state set X such that X ∈ F(X) we take initially X to contain only X_{0} and add elements as needed in order to obtain a set closed under the functional F. Though the local checking technique cannot be implemented without a limited amount of “backtracking” (since it is not possible to guess a priori which state should be included into X, if there are alternatives), the “storage” of already examined unsuccessful alternatives, as advocated in [Lar92], allows to avoid unnecessary recomputations. This gives for the considered local checking technique a polynomial worst-case time complexity (in size of the symbolic transition system). However, the main advantage of this technique is that it needs to explore only the reachable part of the symbolic system, which in “good” cases is considerably smaller than the system in whole. For more details of the method we refer to [Lar92].

20In fact, the transition systems T_{S,T} designed for solving S ref T are different for different refinement relations.

7.2 Main Symbolic Structures

In this section we define the main symbolic structures used in the refinement deciding algorithms, relevant for both deciding time abstracted and time sensitive refinements. After that the refinement deciding algorithms themselves (together with a few additional necessary constructs) are considered in Section 7.3 and Section 7.4 for time abstracted and time sensitive (⊲ and ⊴) refinements, respectively. The algorithm for deciding the trajectory step refinement ⊲^{T} is given in Section 7.5.

7.2.1 Representation of Regular TMS

We define the set of modal action prefixes Act^{m} = {a_{◇} , a_{□} |a ∈ Act} and let a_{•} possibly with some upper indices range over Act^{m}.

We say that a RTMS (= regular TMS) S_{1} is in Normal Expression Form (“NEF”, for short), if it is defined by an equation system

S_{1} =^{def} ϵ(d^{11}).a_{•}^{11}.S_{11} + … + ϵ(d^{1k_{1}}).a_{•}^{1k_{1}}.S_{1k_{1}},

. . . . . . . . .

S_{r} =^{def} ϵ(d^{r1}).a_{•}^{r1}.S_{r1} + … + ϵ(d^{rk_{r}}).a_{•}^{rk_{r}}.S_{rk_{r}},

where for every i ≤ r and j ≤ k_{i} we have d^{ij} ∈ N (possibly d^{ij} = 0), a_{•}^{ij} ∈ Act^{m} and S_{ij} = S_{u} for some u ≤ r (i.e. every S_{ij} appears as a left hand side of one of the expressions above).

In the following description of the refinement relation deciding algorithms we assume that every RTMS contained as a component in the given specifications S or T is given in a NEF. This assumption may be made without any loss of generality as any RTMS may be turned into NEF by rather straightforward equivalence preserving transformations.

For T being a RTMS, defined by the NEF equation

T =^{def} ϵ(d^{1}).a_{•}^{1}.T_{1} + … + ϵ(d^{k}).a_{•}^{k}.T_{k}

and d ≥ 0 being a non–negative real number we define a d-shift of T to be^{21}

T^{(d)} = ϵ(d^{1}− · d).a_{•}^{1}.T_{1} + … + ϵ(d^{k}− · d).a_{•}^{k}.T_{k}.

Observe that, if T ⟶^{ϵ(d)}_{m} T′ for some T′, then T′ = T^{(d)} ^{22}.

Let us further on denote the set of all initially integral timed regular TMS (RTMS) by I. Moreover, whenever a RTMS T can be obtained from some IT RTMS T_{0} ∈ I just by some time-shift T = T_{0}^{(d)}, where d ∈ R_{+0}, we call it well timed (and sometimes abbreviate this as w.t.). So,

T = ϵ(2.63).a_{□} .T_{1} + ϵ(4.63).b_{◇} .T_{2} + c_{□} .T_{3}

is well timed (take, for instance,

21For x, y being nonnegative reals, x− · y = max{x − y, 0}.

22However, the shift operation is defined purely syntactically, and it does assert nothing about the actual delay possibility T ⟶^{ϵ(d)}_{m} T′ for some T′. This delay can be impossible due to the maximal progress requirements, for instance, when T = ϵ(0).τ_{□} .S + ϵ(1).a_{•}.S′.

T_{0} = ϵ(3).a_{□} .T_{1} + ϵ(5).b_{◇} .T_{2} + c_{□} .T_{3} and d = 0.37),

while S = ϵ(2.63).a_{□} .T_{1} +ϵ(2.08).b_{◇} .T_{2} obviously is not. Clearly, any operational derivative of an initially integral timed regular TMS will be well timed.

We define for any well timed RTMS T its integral part T_{0} = int(T) ∈ I and fractional part d = fr(T) ∈ [0, 1[ by T = T_{0}^{(d)} (since we require T_{0} ∈ I and d ∈ [0, 1[, such a decomposition of any w.t. T into its integral and fractional parts is unique).

We shall find it convenient to have the notions of integral and fractional parts of RTMS also generalized to tuples (or, vectors) of RTMS. So, for \overline{U} = ⟨U_{1}, …, U_{n}⟩ being a tuple (= a vector) of RTMSs, we define

\overline{int}(\overline{U}) = ⟨int(U_{1}), …, int(U_{n})⟩ and \overline{fr}(\overline{U}) = ⟨fr(U_{1}), …, fr(U_{n})⟩.

We call a RTMS T delay sensitive iff T^{(d)} differs from T for some d > 0. Equivalently, T is delay sensitive, iff its NEF main (top level) defining equation contains at least one non-zero delay prefix^{23}. It is not difficult to show that a w.t. RTMS is delay sensitive if and only if its integral part is.

For S ∈ I being defined in NEF over the variable set V ar we define the set of RTMSs possibly reachable from S to be re(S) = {V^{(d)}|V ∈ V ar, d ∈ R_{+0}}. Observe that for any RTMS S the set of IT RTMS S_{0} ∈ re(S) ∩ I is finite.

Finally, for a composite TMS S = (V_{1}| … |V_{k}) \ L we let ^{24}.

re(S) = {(U_{1}| … |U_{k}) \ L | U_{i} ∈ re(V_{i}), ∀i}.

A TMS (U_{1}| … |U_{k}) \ L is called well timed iff all its components U_{i} are.

7.2.2 Symbolic Characterization of RTMS Tuples

In this section we introduce some basic ingredients of the “region graph” construction (see e.g. [AD90]) serving as the main part of the symbolic representations of TMS specifications under analysis both in the time abstracted and time sensitive cases.

First, for any n-tuple of non-negative real numbers \overline{x} = ⟨x_{1}, x_{2}, …, x_{n}⟩ ∈ R_{+0}^{n} let us define its symbolic value c(\overline{x}) to be the ordering ≤_{•} of the n + 1–element set M_{n} = \{1, 2, …, n\} ∪ \{∗\} such that

• for i, j ∈ {1, 2, …, n} i ≤_{•} j iff x_{i} ≤ x_{j}, and

• for i ∈ {1, 2, …, n} i ≤_{•} ∗ iff x_{i} = 0, as well as

• ∗ ≤_{•} i for all i ∈ M_{n}.

We define =_{•} to be ≤_{•} ∩ ≤_{•}^{−1}, and i <_{•} j whenever i ≤_{•} j and not i =_{•} j.

It is easy to see that the set of all symbolic values c(\overline{x}) for \overline{x} ∈ R_{+0}^{n} precisely coincides with the set of all orderings ≤′_{•} of M_{n} which are well formed in a sense they are

• total (meaning i ≤′_{•} j or j ≤′_{•} i for all i, j ∈ M_{n}), • transitive, and

23So, τ_{□} .T_{1} + ϵ(2.15).a_{□} .T_{2} is delay sensitive (though the actual “semantical” delays of it are forbidden due to its first summand). On the contrary, a_{□} .T_{1} + b_{◇} .T_{2} is not delay sensitive, since it does not change by delaying.

24Observe that for a composite S the set re(S) most likely is an over-estimation of the set of TMSs reachable from S.

• having ∗ ≤′_{•} i for all i ∈ M_{n}.

We represent any well formed ordering ≤_{•} (and, so, any symbolic value c(\overline{x})) as a list [s_{1}, s_{2}, …, s_{u}], where {s_{1}, s_{2}, …, s_{u}} is a partitioning of M_{n} into non-empty sets such that

• i =_{•} j iff i and j belong to the same subset s_{r} of M_{n}, and

• for l < r ≤ u whenever i ∈ s_{l} and j ∈ s_{r}, then i <_{•} j (i, j ∈ M_{n})^{25}.

Further, let \overline{U} = ⟨U_{1}, U_{2}, …, U_{n}⟩ be an n-tuple of w.t. RTMS. We define the symbolic characterization of \overline{U} to be σ(\overline{U}) = ⟨\overline{int}(\overline{U}), c(\overline{fr}(\overline{U}))⟩ (observe that in the vector \overline{fr}(\overline{U}) every element is a nonnegative real, moreover it lies within the interval [0, 1[).

For a fixed n ∈ N we let Ω(n) denote the set of all pairs σ = ⟨\overline{V} , c⟩ where \overline{V} is an n-tuple of IT RTMS and c is a well formed ordering of M_{n}. Again, one can easily show that Ω(n) precisely coincides with the set of all symbolic characterizations σ(\overline{U}) for \overline{U} being an n-tuple of w.t. RTMS.

We call an element σ = ⟨\overline{V} , c⟩ ∈ Ω(n) boundary iff for some i ∈ M_{n} \ \{∗\} simultaneously i =_{•} ∗ and V_{i} is delay sensitive^{26} ^{27}. A symbolic value σ ∈ Ω(n) which is not boundary is called interior.

Up to now we have defined a “static” symbolic characterization of arbitrary n-tuple \overline{U} of RTMS. The next point is to introduce “transitions” between symbolic values in Ω(n), which we claim “represent” the actual delay transitions performed synchronously by all components of \overline{U} (see Lemma 7.1 below). To begin with, let next(T) for an integral timed RTMS T ∈ I denote T^{(1)} (clearly, always next(T) ∈ I).

Let σ = ⟨\overline{V} , c⟩ with c = [s_{1}, s_{2}, …, s_{u}]. We define succ(σ) = ⟨\overline{V}′, c′⟩:

• for σ being boundary

– \overline{V}′ = \overline{V} (i.e. no changes are occurring in the integral part vector), and

– c′ = [s_{1}^{A}, s_{1}^{B}, s_{2}, …, s_{u}], where s_{1}^{A} and s_{1}^{B} is the partitioning of s_{1} where i ∈ s_{1}^{B} whenever V_{i} is delay sensitive, and i ∈ s_{1}^{A} otherwise (∗ always stays in s_{1}^{A});

• for interior σ,

– if u > 1, then c′ = [s_{1} ∪ s_{u}, s_{2}, …, s_{u−1}]. As to V′, let V′_{i} = next(V_{i}), if i ∈ s_{u}, and V′_{i} = V_{i} otherwise;

– if u = 1, then succ(σ) = σ (this corresponds to the case when all components of \overline{V} have already exhausted all their delay prefixes).

Observe that for this definition of succ we will have succ(σ) well formed (= being a symbolic characterization of some \overline{U}) whenever σ is. Moreover, one can show the following result. We let \overline{U}^{(d)} = ⟨U_{1}^{(d)}, …, U_{n}^{(d)}⟩.

25For instance, if \overline{x} = ⟨5.1, 4.2, 0.7, 0, 4.2, 5.1⟩, then c(\overline{x}) = [\{∗, 4\}, \{3\}, \{2, 5\}, \{1, 6\}].

26Here and further on we use an obvious convention that \overline{V} = ⟨V_{1}, …, V_{n}⟩, \overline{V}′ = ⟨V′_{1}, …, V′_{n}⟩, etc. for an appropriate n.

27The intuition of a boundary symbolic value σ = σ(\overline{U}) is that no matter how small shift (delay) will be performed simultaneously by all U_{j}s, the resulting tuple of RTMSs will have another corresponding symbolic value - due to the component U_{i} which has integral initial delay prefixes (indicated by fr(U_{i}) = 0) and at least one of them not zero (indicated by the delay sensitiveness of U_{i}).

Lemma 7.1 If σ = σ(\overline{U}), then succ(σ) = σ(\overline{U}^{(d)}) for some d > 0. Reverse, for every d ≥ 0 we have σ(\overline{U}^{(d)}) = succ^{m}(σ(\overline{U})) for some m ≥ 0.

Proof sketch: For a RTMS vector \overline{U} such that σ(\overline{U}) = ⟨\overline{V} , c⟩ we define δ(\overline{U}) = 1 − fr(U_{i}), where i is one of indices in the last component of the list c. One can show that succ(σ(\overline{U})) = σ(\overline{U}^{(δ)}), where

• δ = δ(\overline{U}) whenever σ(\overline{U}) is interior, and

• δ ∈]0, δ(\overline{U})[, if σ(\overline{U}) is boundary.

This observation together with time determinacy and time continuity properties of RTMSs, taking into account also that for any d ∈ R_{+0} the symbolic value set \{σ(\overline{U}^{(d′)})|0 ≤ d′ ≤ d\} is finite, leads to the proof of the lemma in both directions.□

We illustrate the introduced constructions on a simple example. Let

\overline{U} = ⟨ϵ(3.53).a_{□} .S_{1}, ϵ(0.04).b_{□} .S_{2}, ϵ(1.53).c_{□} .S_{3}, ϵ(3.00).d_{□} .S_{4}, ϵ(0).e_{□} .S_{5}⟩.

Then σ(\overline{U}) = ⟨\overline{V} , c⟩, where c = [\{∗, 4, 5\}, \{1, 3\}, \{2\}]^{28} and \overline{V} is the vector of integral timed RTMS

\overline{V} = ⟨ϵ(4).a_{□} .S_{1}, ϵ(1).b_{□} .S_{2}, ϵ(2).c_{□} .S_{3}, ϵ(3).d_{□} .S_{4}, ϵ(0).e_{□} .S_{5}⟩

Observe that V_{4} = ϵ(3).d_{□} .S_{4} is delay sensitive, whereas V_{5} = ϵ(0).e_{□} .S_{5} is not. Since 4 =_{•} ∗, we conclude that σ is boundary. So, succ(σ(\overline{U})) = ⟨\overline{V}′, c′⟩ for \overline{V}′ = \overline{V} and c′ = [\{∗, 5\}, \{4\}, \{1, 3\} < \{2\}]. Synchronous delay of any length d ∈]0, 0.04[ of all components of \overline{U} would lead to a RTMS vector \overline{U}′ whose symbolic characterization σ(\overline{U}′) = succ(σ(\overline{U})). As can easily be seen, σ(\overline{U}′) is interior.

7.3 Time Abstracted Refinements

In this section we show some details of the algorithms for deciding the time abstracted refinement relations ⊲^{•} and ⊴^{•} between initially integral timed specifications.

Let S′ = (U_{1}| … |U_{k}) \ L be an arbitrary well timed TMS^{29}. We define the symbolic representation of S′ to be the triple ⟨⟨S′⟩⟩ = ⟨\overline{V} , c, L⟩ where ⟨\overline{V} , c⟩ = σ(\overline{U}) is the symbolic characterization of the RTMS vector \overline{U} = ⟨U_{1}, …, U_{k}⟩.

For a given IT TMS S we define the set of its symbolic states to be X_{S} = {⟨⟨S_{0}⟩⟩ | S_{0} ∈ re(S)}. It can be easily seen that X_{S} is finite for every S.

One can observe that two TMSs S_{1} and S_{2} which have the same symbolic representation (i.e. ⟨⟨S_{1}⟩⟩ = ⟨⟨S_{2}⟩⟩) have also identical “time abstracted” behaviours (whenever S_{1} may/must be able to do a real action becoming S′_{1}, this can be simulated by the same real action of S_{2} becoming S′_{2} such that ⟨⟨S′_{2}⟩⟩ = ⟨⟨S′_{1}⟩⟩, also if S_{1} ⟶^{ϵ(d)}_{m} S′_{1}, then S_{2} ⟶^{ϵ(d′)}_{m} S′_{2} for some d′, S′_{2}, again having ⟨⟨S′_{2}⟩⟩ = ⟨⟨S′_{1}⟩⟩). One can find this result proven for a similar case of timed processes (in place of TMSs) in [LW90].

28Indeed, the corresponding fractional part vector is ⟨0.47, 0.96, 0.47, 0, 0⟩. One needs to get slightly used to the fact that the RTMS itself has smaller waiting time than its integral part. This decision was taken to ensure that a RTMS is delay sensitive if and only if its integral part is.

29Recall that well timedness means consisting of RTMSs each of which can be obtained from IT RTMS by some delay.

We exploit this observation of (abstracted) behaviour coincidence of symbolically equally represented TMSs by reflecting these “equal” behaviours on the level of symbolic representations, what will lead directly to the needed refinement deciding algorithms.

More precisely, we define for a ∈ Act and m ∈ {◇, □} the transitions ⟶^{a}_{m} and ⟶^{W T}_{m} between the symbolic states of IT TMS in the following (abstract) way

\frac{S′ ⟶^{a}_{m} S′′}{⟨⟨S′⟩⟩ ⟶^{a}_{m} ⟨⟨S′′⟩⟩}, \frac{⟨⟨S′′⟩⟩ = succ_{m}⟨⟨S′⟩⟩}{⟨⟨S′⟩⟩ ⟶^{W T}_{m} ⟨⟨S′′⟩⟩},

where succ_{m} is a natural generalization of succ from RTMS vector symbolic characterizations to symbolic states of TMSs, taking into account also maximal progress requirements. More precisely,

• succ_{m}(⟨\overline{V} , c, L⟩) = ⟨\overline{V}′, c′, L⟩ for ⟨\overline{V}′, c′⟩ = succ(⟨\overline{V} , c⟩), if (V_{1}| … |V_{k}) \ L can not do a τ_{m^{c}} transition^{30},

• succ_{m}(⟨\overline{V} , c, L⟩) is undefined otherwise.

The real (non-delay) transitions between symbolic states are computed as follows (it is not difficult to see that these computations correspond to the more abstract definition given above):

• whenever a ∈ Act, then ⟨\overline{V} , c, L⟩ ⟶^{a}_{m} ⟨\overline{V}′, c′, L⟩ provided a ∉ L and for some i

– V_{i} ⟶^{a}_{m} V′_{i} (in the definition of V_{i} an appropriate summand must be contained);

– V′_{j} = V_{j} for all j ≠ i (all other components remain unchanged);

– c′ is obtained from c by moving the index i from its equivalence class to the class containing ∗ (followed by cleaning the list from empty elements - subsets of M_{n}).

• In addition, ⟨\overline{V} , c, L⟩ ⟶^{τ}_{m} ⟨\overline{V}′, c′, L⟩ whenever for some i ≠ j and some α ∈ Λ

– V_{i} ⟶^{α}_{m} V′_{i} and V_{j} ⟶^{ᾱ}_{m} V′_{j};

– V′_{s} = V_{s} for all s such that s ≠ i and s ≠ j;

– c′ is obtained from c by moving the indices i and j from their equivalence classes to the class containing ∗ (followed by cleaning the list from empty elements).

Let A ⟶^{W T^{∗}}_{m} B mean A(⟶^{W T}_{m})^{∗}B (i.e. the symbolic state B can be reached from A by zero or more succ_{m} operations. We also introduce “time abstracted” transitions of symbolic states by defining A ⟶^{a}_{m}^{W} B to

stand for A ⟶^{W T^{∗}}_{m}⟶^{a}_{m}⟶^{W T^{∗}}_{m} B.

Observing Lemma 7.1 and “equivalence” of TMSs corresponding to one symbolic state, it is not difficult to justify the correctness of the following deciding procedures for ⊲^{•} and ⊴^{•}.

For initially integral timed TMS S and T to check, if S ⊲^{•} T, we define first X_{S,T} = X_{S} × X_{T}. For any X ⊆ X_{S,T} we let F^{⊲^{•}}(X) to consist of all those pairs ⟨A, B⟩ for which

• whenever A ⟶^{a}_{◇} A′ then B ⟶^{a}_{◇}^{W} B′ for some B′ with ⟨A′, B′⟩ ∈ X,

30□^{c} = ◇, ◇^{c} = □.

• whenever B ⟶^{a}_{□} B′ then A ⟶^{a}_{□}^{W} A′ for some A′ with ⟨A′, B′⟩ ∈ X,

• whenever A ⟶^{W T}_{◇} A′ then B ⟶^{W T^{∗}}_{◇} B′ for some B′ with ⟨A′, B′⟩ ∈ X,

• whenever B ⟶^{W T}_{□} B′ then A ⟶^{W T^{∗}}_{□} A′ for some A′ with ⟨A′, B′⟩ ∈ X.

We have S ⊲^{•} T if and only if for some X both ⟨⟨⟨S⟩⟩, ⟨⟨T ⟩⟩⟩ ∈ X and X ⊆ F^{⊲^{•}}(X) (i.e. ⟨⟨⟨S⟩⟩, ⟨⟨T ⟩⟩⟩ is contained in the greatest fixpoint of F^{⊲^{•}}).

In the weak case we distinguish observable actions (denoted by α) and the internal computations τ and let ⟹^{ε}_{m} stand for (⟶^{τ}_{m} ∪ ⟶^{W T}_{m})^{∗}. It can be easily shown (similarly, as in the strong case) that S ⊴^{•} T if and only if ⟨⟨⟨S⟩⟩, ⟨⟨T ⟩⟩⟩ ∈ X ⊆ X_{S} × X_{T} for some X satisfying for every ⟨A, B⟩ ∈ X the following conditions

• whenever A ⟶^{τ}_{◇} A′ or A ⟶^{W T}_{◇} A′ then B ⟹^{ε}_{◇} B′ for some B′ with ⟨A′, B′⟩ ∈ X,

• whenever A ⟶^{α}_{◇} A′ then B ⟹^{ε}_{◇} ⟶^{α}_{◇} ⟹^{ε}_{◇} B′ for some B′ with ⟨A′, B′⟩ ∈ X,

• whenever B ⟶^{τ}_{□} B′ or B ⟶^{W T}_{□} B′ then A ⟹^{ε}_{□} A′ for some A′ with ⟨A′, B′⟩ ∈ X,

• whenever B ⟶^{α}_{□} B′ then A ⟹^{ε}_{□} ⟶^{α}_{□} ⟹^{ε}_{□} A′ for some A′ with ⟨A′, B′⟩ ∈ X.

7.4 Timed Refinements

To decide (strong or weak) time–sensitive refinements between two initially integral timed specifications S and T it is not in general possible to build finite partitionings of the state sets of S and T in which each element contains only “equivalent” states as we saw for the time–abstracted refinements (observe that any two TMSs^{31} which have a slightest difference in their initial delay prefixes usually are semantically different).

However, following the ideas of [Č92b], one can attribute a symbolic characterization (similar in its nature to the symbolic state considered before in the time abstracted case) to every pair of well timed TMSs, so achieving the property that, whenever ⟨⟨S′, T′⟩⟩ = ⟨⟨S′′, T′′⟩⟩, then either both S′ ⊲ T′ and S′′ ⊲ T′′, or none of these refinements hold^{32}. We follow this line in the following technical description of algorithms deciding timed refinement relations.

For S_{0} = (U_{1}| … |U_{k}) \ L and T_{0} = (U_{k+1}| … |U_{n}) \ M being well timed TMS we define a symbolic representation (a symbolic state) ⟨⟨S_{0}, T_{0}⟩⟩ of the pair ⟨S_{0}, T_{0}⟩ to be a 5-tuple ⟨\overline{V} , c, L, M, k⟩, where ⟨\overline{V} , c⟩ = σ(\overline{U}) for \overline{U} = ⟨U_{1}, …, U_{k}, U_{k+1}, …, U_{n}⟩ being a concatenation of component vectors ⟨U_{1}, …, U_{k}⟩ and ⟨U_{k+1}, …, U_{n}⟩ for both TMSs S_{0} and T_{0}^{33}.

For S and T being IT TMSs we define the symbolic state set X_{S,T} for characterizing their “joint behaviour” to be {⟨⟨S_{0}, T_{0}⟩⟩|S_{0} ∈ re(S), T_{0} ∈ re(T)}. One can show that X_{S,T} is finite for any S, T.

Similarly, as in time abstracted case, we define symbolic transitions between symbolic states. Here, however, we must distinguish between transitions which are done by “left” (i.e. “belonging” to S_{0}) components from those done by “ right” components (i.e. “belonging” to T_{0}). We do that by introducing an additional index 1 or 2 to the transition relation.

31One can consider also timed processes without modalities to observe the same effect.

32In other words, S′ ⊲ T′ implies S′′ ⊲ T′′. The same property is true also for ⊴, i.e. whenever ⟨⟨S′, T′⟩⟩ = ⟨⟨S′′, T′′⟩⟩, then S′ ⊴ T′ implies S′′ ⊴ T′′.

33The number k is carried into the symbolic state to separate the components of the joint vector into those which “belong”

to S_{0} and which to T_{0}.

Assuming m ∈ {◇, □}, a ∈ Act, we have first:

\frac{S ⟶^{a}_{m} S′}{⟨⟨S, T ⟩⟩ ⟶^{a}_{m,1} ⟨⟨S′, T ⟩⟩} \frac{T ⟶^{a}_{m} T′}{⟨⟨S, T ⟩⟩ ⟶^{a}_{m,2} ⟨⟨S, T′⟩⟩}.

We say that ⟨⟨R_{1}, R_{2}⟩⟩ ⟶^{W T}_{m,i} (without specifying the target of the transition) provided R_{i} ⟶^{ϵ(d)}_{m} for some d > 0 (due to the maximal progress and transition liveness properties the necessary and sufficient condition for such delays is the absence of R_{i} ⟶^{τ}_{m^{c}} transition possibility).

For X = ⟨\overline{V} , c, L, M, k⟩ such that X ⟶^{W T}_{m,1} and X ⟶^{W T}_{m,2} we define its “m-delay successor” to be succ_{m}(X) = ⟨\overline{V}′, c′, L, M, k⟩, where ⟨\overline{V}′, c′⟩ = succ(⟨\overline{V} , c⟩) (see Section 7.2.2 for definition of time successor succ for a symbolic characterization of a vector of RTMS)^{34}.

Given 5-tuple representations of the symbolic states, the computation of the transition relations ⟶^{a}_{m,i} between them in accordance with the given abstract definition is rather straightforward, so we show only an example:

• For a ∈ Act, if a ≠ τ, then ⟨\overline{V} , c, L, M, k⟩ ⟶^{a}_{m,1} ⟨\overline{V}′, c′, L′, M′, k′⟩ iff

– L′ = L, M′ = M and k′ = k, as well as a ∉ L;

– V_{i} ⟶^{a}_{m} V′_{i} for some i ≤ k; V′_{j} = V_{j} for all j ≠ i;

– c′ is obtained from c by moving i to the equivalence class containing ∗ (followed by cleaning the list from empty elements).

In the case of symbolic time transitions we perform the check if X ⟶^{W T}_{m,i} by checking the negation of

X ⟶^{τ}_{m^{c},i}.

The following algorithm of deciding (strong) timed refinement between IT TMS can be proven correct following very closely the arguments from [Č92b].

Given X ⊆ X_{S,T} we define F_{S,T}^{◁} (X) to consist of those and only those X ∈ X_{S,T} for which

• X ⟶^{a}_{◇,1} X_{1} implies X_{1} ⟶^{a}_{◇,2} X_{2} for X_{2} ∈ X,

• X ⟶^{a}_{□,2} X_{1} implies X_{1} ⟶^{a}_{□,1} X_{2} for X_{2} ∈ X,

• whenever X ⟶^{W T}_{◇,1} then succ_{◇} (X) ∈ X,

• whenever X ⟶^{W T}_{□,2} then succ_{□} (X) ∈ X.

We conclude that S ⊲ T iff ⟨⟨S, T ⟩⟩ is contained in the greatest fixpoint of F_{S,T}^{◁}.

In order to decide the weak refinement we let X ⟹^{τ}_{m,i} X′ mean X(⟶^{τ}_{m,i})^{∗}X′ and X ⟹^{α}_{m,i} X′ mean X ⟹^{τ}_{m,i}⟶^{α}_{m,i}⟹^{τ}_{m,i} X′. Let also a symbolic state X = ⟨\overline{V} , c, L, M, k⟩ be called boundary or interior in accordance with the pair ⟨\overline{V} , c⟩.

Let us recall that the definition of the weak (τ-abstracted) refinement in Section 4 in case of S ⊴ T allows to match a delay transition S ⟶_{◇}^{ϵ(d)} S′ in general by a chain of transitions

34Observe that for X = ⟨⟨S_{0}, T_{0}⟩⟩ succ_{m}(X), if defined, will be ⟨⟨S′_{0}, T′_{0}⟩⟩, where S′_{0} and T′_{0} are obtained by synchronous delaying of S_{0} and T_{0} for some time amount d > 0.

T (⟶_{◇}^{τ} )^{∗} ⟶_{◇}^{ϵ(d_{1})} (⟶_{◇}^{τ} )^{∗} ⋯ ⟶_{◇}^{ϵ(d_{k})} (⟶_{◇}^{τ} )^{∗}T′

so that d_{1} + … + d_{k} = d and S′ ⊴ T′ ( T ⟶_{□}^{ϵ(d)} T′ is to be matched by a similar appropriate chain from S). It turns out that in the deciding procedure below we need to consider symbolic transitions following the same general pattern, at least for matching the ⟶_{◇}^{ϵ(d)} transitions^{35}.

To describe the search for timed matching transitions on the symbolic level, first, if succ_{◇} (X) is defined, we let X ⟶^{0} X′ and X ⟶^{1} X′′, where

• X′ = succ_{◇} (X) and X′′ = succ_{◇} (succ_{◇} (X)) for X being boundary, and

• X′ = X and X′′ = succ_{◇} (X) for interior X.

One can say that ⟶^{0} is “waiting to become interior” and ⟶^{1} is “waiting to become boundary”. Semantically, if δ = δ(S, T) is the difference between 1 and the largest delay fractional part in S, T, then

⟨⟨S, T ⟩⟩ ⟶^{0} ⟨⟨S′, T′⟩⟩ and ⟨⟨S, T ⟩⟩ ⟶^{1} ⟨⟨S′′, T′′⟩⟩, where

• S ⟶_{◇}^{δ} S′′ and T ⟶_{◇}^{δ} T′′, as well as

• S ⟶_{◇}^{δ′} S′ and T ⟶_{◇}^{δ′} T′ with δ′ chosen to be any number within ]0, δ[.

Intuitively ⟶^{1} can be also explained as a symbolic move corresponding to the simultaneous waiting of TMSs until the first new timer fractional part becomes 0 (for what two succ_{◇} moves are necessary, if the pair of initial TMSs belonged to a boundary region).

Further, let ⟹^{0∗}= (⟹^{τ}_{◇,2} ∪ ⟶^{0})^{∗}. Observe that this relation comprises interleaving of “right” symbolic τ_{◇} -moves (we need to introduce this construction for only one direction) and elementary delay transitions. One can show, for instance, that ⟨⟨S_{0}, T_{0}⟩⟩ ⟹^{0∗} X implies that for some d ∈ [0, δ(S_{0}, T_{0})[^{36} both S_{0} ⟶^{ϵ(d)}_{◇} S′ and T_{0} ⟹^{ϵ(d)}_{◇} T′ so that X = ⟨⟨S′, T′⟩⟩ (observe the same d in both transition chains).

Following the ideas of [Č92b] and [Č92a] one can prove that S ⊴ T if and only if there exists X ⊆ X_{S,T} such that both ⟨⟨S, T ⟩⟩ ∈ X and for every X ∈ X:

• whenever X ⟶^{a}_{◇,1} X_{1} then X_{1} ⟹^{a}_{◇,2} X_{2} for X_{2} ∈ X,

• whenever X ⟶^{a}_{□,2} X_{1} then X_{1} ⟹^{a}_{□,1} X_{2} for X_{2} ∈ X,

• whenever X ⟶^{W T}_{□,2} then X ⟹^{τ}_{□,1} X_{1} for some X_{1} such that succ_{□} (X_{1}) ⟹^{τ}_{□,1} X_{2} for X_{2} ∈ X,

• whenever X ⟶^{W T}_{◇,1} then both

35Remarkably, the ⟶_{□} transition system of TMS satisfies the classical maximal progress property ([Wan90]), saying that for no TMS S it would be the case that both S ⟶_{□}^{τ} S′ and S ⟶_{□}^{ϵ(d)} S′′ for any d, S′, S′′. This implies that, if S ⟶^{ϵ(d)}_{□} for some d > 0, then for sufficiently small d′s we have S ⟹^{ϵ(d′)}_{□} S′ if and only if S ⟶^{ϵ(d′)}_{□} S′ (i.e. during some initial period the delay of S can not be interrupted by any internal transitions). One can show that this initial period is at least as long as the difference between 1 and the largest S component fractional part. Using this observation the “matching region”

construction in the □-timed cases can be taken to be substantially simpler (see the deciding procedure below). For ⟶_{◇} transition system the classical maximal progress property is not satisfied, for instance, on τ_{◇} .S for any S.

36In fact, d can be taken 0, if there were no ⟶^{0} transitions actually occurring within this ⟹^{0∗}, otherwise d can be taken to be any value from ]0, δ(S_{0}, T_{0})[. It can be noted that the following transitions could be possible (actually, only in somewhat degenerate cases) also for larger values of d.

– X ⟹^{0∗}⟶^{0}⟹^{τ}_{◇,2} X_{1} for some X_{1} ∈ X ^{37} and

– X ⟹^{0∗}⟶^{1}⟹^{τ}_{◇,2} X_{2} for X_{2} ∈ X ^{38}.

The most complicated X ⟶^{W T}_{◇,1} case in the above definition for a pair of TMSs ⟨S_{0}, T_{0}⟩ ∈ X ∈ X makes immediate guarantees that whenever S_{0} ⟶^{ϵ(d)}_{◇} S′ for some d ≤ δ(S_{0}, T_{0}), then T_{0} ⟹^{ϵ(d)}_{◇} T′ with X′ = ⟨⟨S′, T′⟩⟩ ∈ X ^{39}. The necessary extension to the case of arbitrary d ∈ R_{+0} is then done by induction over time moments when fractional parts of specification components become 0 ^{40} (precisely as in the another timed case of X ⟶^{W T}_{□,2} ). For more details of the correctness proof we refer to [Č92b, Č92a].

7.5 Trajectory Step Refinement

For the procedure deciding, if S ⊲^{T} T, we keep the notation introduced to describe symbolic deciding of ⊴. What is changing here, is just the symbolic clause for matching the ⟶_{◇}^{ϵ(d)} moves of S, precisely to reflect the requirement taken from the definition of S ⊲^{T} T that all regions corresponding to the points in the step sequence of T ⟹^{ϵ(d)}_{◇} T′ should be “matching”.

So, it can be proven that S ⊲^{T} T if and only if there exists X ⊆ X_{S,T} such that both ⟨⟨S, T ⟩⟩ ∈ X and for every X ∈ X:

37Observe that this case reduces to triviality, if X is interior and X ⟶^{W T}_{◇,2} , by letting X_{1} = X.

38In fact this is a slight simplification. Actually one needs to make sure (for the given algorithm to work properly) that during the ⟹^{0∗} transitions the last component of “fractional part list” of X is not lost. This is implemented by adding into this last class an extra dummy element (so X becomes some X^{+}) to be removed later (when X^{+} has become X_{2}^{+}, we keep just X_{2}). In theory this construction corresponds to an extra clock, and is elaborated for a very similar situation in [Č92a].

39Recall that δ(S_{0}, T_{0}) is the distance from the largest fractional part of components of either S_{0} or T_{0} to 1.

40It can be shown that there can not be more than a finite amount of those within any finite time interval.

• whenever X ⟶^{a}_{◇,1} X_{1} then X_{1} ⟹^{a}_{◇,2} X_{2} for X_{2} ∈ X,

• whenever X ⟶^{a}_{□,2} X_{1} then X_{1} ⟹^{a}_{□,1} X_{2} for X_{2} ∈ X,

• whenever X ⟶^{W T}_{□,2} then X ⟹^{τ}_{□,1} X_{1} for some X_{1} such that succ_{□} (X_{1}) ⟹^{τ}_{□,1} X_{2} for X_{2} ∈ X,

• whenever X ⟶^{W T}_{◇,1} then both

– X ⟹^{τ}_{◇,2} X_{0} ⟶^{0}⟹^{τ}_{◇,2} X_{1} so that X_{i} ∈ X for i = 0, 1, and

– X ⟹^{τ}_{◇,2} X′_{0} ⟶^{0}⟹^{τ}_{◇,2} X′_{1} … ⟶^{0}⟹^{τ}_{◇,2} X′_{m} ⟶^{1}⟹^{τ}_{◇,2} X′_{m+1} so that X′_{i} ∈ X for all i =

0, 1, …, m + 1, m ≥ 0 ^{41}.

We shall not be concerned here with discussions on the efficiency of checking ⊲^{T}, however, let us make the obvious observation that both parts of the matching requirement in the last clause (when X ⟶^{W T}_{◇,1} ) could usually be easily fulfilled by a single region sequence, namely X ⟹^{τ}_{◇,2} X′_{0} ⟶^{0}⟹^{τ}_{◇,2} X′_{1} … ⟶^{0}⟹^{τ}_{◇,2}

X′_{m} ⟶^{1}⟹^{τ}_{◇,2} X′_{m+1}, where m ≥ 1.

8 Conclusions

In this paper we have presented the theory of TMS together with the automatic refinement checking tool Epsilon. The theory TMS is an extension of real–time process calculi with the specific aim of allowing loose or partial specifications. Looseness of specifications was achieved by introducing two modalities to transitions of specifications: a may and a must modality. As a natural consequence of having two kinds of transitions we generalized in a direct way various notions of process equivalences (strong equivalence, τ–abstracted equivalence, time–abstracted equivalence and τ– and time–abstracted equivalence) and introduced corresponding refinement orderings between specifications.

We showed how the notion of refinement allows for generality in the theory, that is, a single correctness proof in TMS may capture a whole (possibly) infinite family of correctness proofs in process calculi. Further, it turned out that the theory is compositional to a large extent; in particular the non time–abstracted refinements are preserved (at least) by parallel composition. Together, generality and compositionality makes TMS a useful formalism for stepwise refinement development. In a stepwise refinement development of a system the initial specification is rather abstract and permits a wide range of implementations. In each refinement step the set of possible implementation is reduced while still maintaining correctness with respect to the initial specification. Eventually an implementation is reached.

We consider (and this may be stated in a formal manner) TMS to be a theory in between timed process algebras and timed logics. TMS possesses both the compositional strength of algebras and is like logics a theory for expressing loose specifications of real–time systems. However, in contrast to (real–time) logics where compositional verification so far has not been offered, TMS supports compositional verification.

TMS and its automatic refinement checking tool has been successfully applied to a not completely trivial example of a train crossing. In particular we outlined how compositionality can be taken advantage of during refinement checking.

Epsilon, however is a prototype tool and we have ideas of how to improve the time and space performance of the tool. One possible idea is to investigate combinations of the kernel of Epsilon (that is, the local model checking technique of [Lar92]) with the state space partitioning algorithms that has proven successful for verification of real–timed systems (e.g. the temporal logic model checking partitioning algorithm presented in [ACH^{+}92]). Other performance improving ideas include utilizing algebraic laws while performing the correctness checking.

41Here we should also be concerned with keeping the last component of X fractional part list, precisely as in similar situation when deciding ⊴.

The idea of introducing looseness by allowing two modalities on transitions is completely orthogonal to process algebra. Hence, another topic of research interest is that of introducing looseness to other kinds of real–time theories, for instance timed graphs [Dil89].

References

[ACD90] Rajeev Alur, Costas Courcoubetis, and David Dill. Model–checking for real–time systems. In Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, 1990.

[ACH^{+}92] R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of timed transition systems. In CONCUR’92, volume 630 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

[AD90] R. Alur and D. Dill. Automata for modelling real–time systems. In ICALP’90, volume 443 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

[AD91] R. Alur and D. Dill. The theory of timed automata. In Real–Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, 1991.

[BB89] J.C.M. Baeten and J.A. Bergstra. Real time process algebra. Technical Report P8916, University of Amsterdam, 1989.

[BL90] G. Boudol and K.G. Larsen. Graphical versus logical specifications. In Proceedings of CAAP’90, volume 431 of Lecture Notes in Computer Science, 1990.

[BLS92] A. Børjesson, K.G. Larsen, and A. Skou. Generality in design and compositional verification using tav. In Proceedings of FORTE’92, 1992.

[Dil89] D.L. Dill. Timing assumptions and verification of finite–state concurrent systems. Lecture Notes in Computer Science, 407, 1989.

[GLZ89] J.C. Godskesen, K.G. Larsen, and M. Zeeberg. TAV (tools for automatic verification) — users manual. Technical report, University of Aalborg, Denmark, 1989.

[God94] Jens Chr. Godskesen. Timed Modal Specifications — A Theory for Verification of Real–Time Concurrent Systems. Ph.d. thesis, University of Aalborg, Denmark, 1994.

[HL89] H. Hüttel and K.G. Larsen. The use of static constructs in a modal process logic. In Proceedings of Logic at Botik’89, volume 363 of Lecture Notes in Computer Science. Springer-Verlag, 1989.

[Lar90] K.G. Larsen. Modal specifications. In Proceedings of Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, 1990.

[Lar92] K.G. Larsen. Efficient local correctness checking. In Proceedings of CAV’92, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

[LT88] K.G. Larsen and B. Thomsen. A modal process logic. In Proceedings LICS’88, 1988.

[LW90] K.G. Larsen and Y. Wang. Time abstracted bisimulation: Implicit specifications and decidability. In Proceedings of MFPS’93, Lecture Notes in Computer Science. Springer-Verlag, 1990.

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

[NSY91] X. Nicollin, J. Sifakis, and S. Yovine. From ATP to timed graphs and hybrid systems. In Real– Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, 1991.

[NSY92] X. Nicollin, J. Sifakis, and S. Yovine. Compiling real–time specifications into extended automata. IEEE TSE Special Issue on Real–Time Systems, September 1992.

[Par81] D. Park. Concurrency and automata on infinite sequences. In 5th GI Conference, volume 104 of Lecture Notes in Computer Science, 1981.

[SV89] R. De Simone and D. Vergamini. Aboard AUTO. Technical Report 111, INRIA, Sofia–Antipolis, 1989.

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

[Č92b] K. Čerāns. Decidability of bisimulation equivalences for processes with parallel timers. In Proceedings of CAV’92, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

[Wan90] Y. Wang. Real–time behaviour of asynchronous agents. In Proceedings of CONCUR’90, volume 458 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

Recent BRICS Report Series Publications

RS-97-11 Kārlis Čerāns, Jens Chr. Godskesen, and Kim G. Larsen. Timed Modal Specification — Theory and Tools. April 1997. 32 pp.

RS-97-10 Thomas Troels Hildebrandt and Vladimiro Sassone. Transition Systems with Independence and Multi-Arcs. April 1997. 20 pp. Appears in Peled, Pratt and Holzmann, editors, DIMACS Workshop on Partial Order Methods in Verification, POMIV ’96, pages 273–288.

RS-97-9 Jesper G. Henriksen and P. S. Thiagarajan. A Product Version of Dynamic Linear Time Temporal Logic. April 1997. 18 pp. To appear in Concurrency Theory: 7th International Conference, CONCUR ’97 Proceedings, LNCS, 1997.

RS-97-8 Jesper G. Henriksen and P. S. Thiagarajan. Dynamic Linear Time Temporal Logic. April 1997. 33 pp.

RS-97-7 John Hatcliff and Olivier Danvy. Thunks and the λ-Calculus (Extended Version). March 1997. 55 pp. Extended version of article to appear in the Journal of Functional Programming.

RS-97-6 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. March 1997. 53 pp. Extended version of an article to appear in the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’97), Amsterdam, The Netherlands, June 1997.

RS-97-5 Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. March 1997. 18 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-97-4 Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for Labelled Markov Processes. March 1997. 48 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-97-3 Carsten Butz and Ieke Moerdijk. A Definability Theorem for First Order Logic. March 1997. 10 pp.

RS-97-2 David A. Schmidt. Abstract Interpretation in the Operational Semantics Hierarchy. March 1997. 33 pp.