BRICS RS-00-23 Aceto et al.: Characteristic Formulae for Timed Automata BRICS

Basic Research in Computer Science

Characteristic Formulae for Timed Automata

Luca Aceto Anna Ingólfsdóttir Mikkel Lykke Pedersen Jan Poulsen

BRICS Report Series RS-00-23

ISSN 0909-0878 September 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Luca Aceto & Anna Ingólfsdóttir &

Mikkel Lykke Pedersen & Jan Poulsen. 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/00/23/

Characteristic Formulae for Timed Automata

Luca Aceto Anna Ingólfsdóttir Mikkel Lykke Pedersen Jan Poulsen

BRICS^{∗}, Department of Computer Science, Aalborg University Fr. Bajersvej 7E, 9220 Aalborg Ø, Denmark

Abstract

This paper offers characteristic formula constructions in the realtime logic L_{ν} for several behavioural relations between (states of) timed automata. The behavioural relations studied in this work are timed (bi)similarity, timed ready simulation, faster-than bisimilarity and timed trace inclusion. The characteristic formulae delivered by our constructions have size which is linear in that of the timed automaton they logically describe. This also applies to the characteristic formula for timed bisimulation equivalence, for which an exponential space construction was previously offered by Laroussinie, Larsen and Weise.

1 Introduction

There are two main methodologies for the formal verification of reactive systems, viz. model checking and implementation verification. In the model checking approach [8], one establishes the correctness of a system with respect to a given specification by checking whether a state-transition graph that models the program satisfies a temporal logic formula expressing the desired specification of the system’s behaviour. In implementation verification, both a system and the specification of its desired behaviour are expressed as state-transition graphs. Establishing that a system is correct with respect to its specification then amounts to checking whether the behaviours of the two state-transition graphs are related in some formal sense. In the classic, untimed setting, this correlation between the behaviours of two state-transition graphs is usually expressed in terms of a behavioural relation in the linear time-branching time spectrum [12].

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation

One of the bridges between these two approaches to verification is provided by the notion of characteristic formula [13, 15, 26]. A characteristic formula is a formula in a temporal logic that completely characterizes the behaviour of a (state in a) state-transition graph modulo a chosen notion of behavioural relation. Using it, checking whether two state-transition graphs A and B are related with respect to a behavioural relation can be reduced to checking whether, say, A is a model of the characteristic formula for B.

The approach to (automated) verification where the problem of checking behavioral relations between finite Labelled Transition Systems (LTSs) [16] is reduced to model checking is advocated by Cleaveland and Steffen in [9, 10]. In their approach, the language being model checked is a logic equivalent in expressive power to the alternation-free fragment of the modal μ-calculus [17]. The efficiency of this approach hinges on the following two facts:

1. the characteristic formula associated with a finite labelled transition system has size that is linear in that of the original LTS, and

2. the time complexity of determining whether a process satisfies a formula is proportional to the product of the sizes of the process and the formula.

The resulting algorithm offered in [9] is still considered to be one of the most efficient for checking behavioural preorders.

In the setting of modelling and verification for real time systems, a characteristic formula construction for timed bisimulation equivalence over timed automata [2] has been offered in [19]. In op. cit., Laroussinie, Larsen and Weise have proposed the logic L_{ν}—a real-time version of Hennessy-Milner Logic [14] with greatest fixed-points—, and have shown that its associated model checking problem is decidable, and that this logic is sufficiently expressive for representing any timed automaton as a single characteristic L_{ν} formula. Such a formula uniquely characterizes the timed automaton up to timed bisimilarity.

The characteristic formula construction presented in [19], together with a model checking algorithm for the logic L_{ν}, yields an algorithm for checking whether two timed automata are timed bisimilar, which may be seen as the implementation of the approach advocated in [9] in a real-time setting. Unfortunately, however, the characteristic formula construction for timed automata proposed in [19] produces formulae whose size is exponential in that of the original automaton, and this makes its use in checking timed bisimilarity for timed automata infeasible. The exponential blow-up involved in the characteristic formula construction from op. cit. is due to the fact that the formula is essentially constructed by applying the standard, untimed construction developed by Ingólfsdóttir, Godskesen and Zeeberg [15] to the region graph associated with the timed automaton [2]. As shown by Alur and Dill [2], the size of the region graph is exponential in that of the original timed automaton.

This study offers characteristic formula constructions for timed automata using the logic L_{ν} that, like those in the untimed setting and unlike that offered in [19], yield formulae whose size is linear with respect to that of the timed automaton they characterize. We present characteristic formula constructions for timed bisimilarity [28], timed versions of the simulation [21] and ready simulation [5, 20] preorders and for the faster-than preorder [23]. In particular, the characteristic formula construction for timed bisimilarity improves upon that offered in [19]. In addition, since, if B is a deterministic timed automaton, checking whether the set of timed traces afforded by a timed automaton A is included in that of B is equivalent to establishing that B simulates A, the characteristic formula construction for timed simulation can also be applied to checking timed trace inclusion [2].

The constructions we propose constitute a first step towards the application of the model checking approach to implementation verification in the timed setting. A prototype tool based on the theory we present in this study is described in [25].

Further Related Work Characteristic formulae were introduced in [13] to relate equational reasoning about processes to reasoning in a modal logic, and therefore to allow proofs about processes to be carried out in a logical framework. The initial research within characteristic formulae concerned terminating processes and bisimulation equivalences, but extensions to this theory have included finite processes and further equivalences. The unpublished master’s thesis [15] presents, amongst other things, characteristic formulae for finite LTSs with respect to bisimulation, and is the precursor of most of the papers on the subject that followed, including ours. In [26] Ingólfsdóttir and Steffen show how to extend these results to cover bisimulation-like preorders which are sensitive to liveness properties. Their work demonstrates the expressive power of intuitionistically interpreted Hennessy Milner Logic with greatest fixed-points, and builds the theoretical basis for a uniform and efficient method to automatically verify bisimulation-like relations between processes by means of model checking. As previously mentioned, this approach to checking behavioural relations has been advocated by Cleaveland and Steffen in a series of papers (see, e.g., [9]).

All the aforementioned papers use some form of Hennessy-Milner Logic with greatest fixed-points as the logical counterpart of automata. This is, however, by no means the only option pursued in the literature. For example, Browne, Clarke and Grümberg [6] have shown how to characterize Kripke structures in the logic CTL [7] up to bisimilarity.

Roadmap of the Paper After a brief review of background material on timed automata and the logic L_{ν} (Sect. 2), we present the timed behavioural relations for which we offer characteristic formula constructions (Sect. 3). The constructions of the characteristic formulae are the topic of Sect. 4, where their correctness is also proven. The paper concludes with a discussion of the use of characteristic formulae for checking timed trace inclusion between timed automata in a setting in which the specification automaton is deterministic (Sect. 5).

2 Preliminaries

We begin by briefly reviewing the timed automaton model proposed by Alur and Dill [2] and the logic L_{ν} [19] that will be used in this study.

Timed Labelled Transition Systems Let Act be a finite set of actions, ranged over by a, b, and let ℕ and ℝ_{≥0} denote the sets of natural and nonnegative real numbers, respectively. We use D to denote the set of delay actions {ϵ(d) | d ∈ ℝ_{≥0}}, and L to stand for the union of Act and D. The meta-variable α will range over L.

Definition 2.1 A timed labelled transition system (TLTS) is a structure T = (S, L, s^{0}, ⟶) where S is a set of states, s^{0} ∈ S is the initial state, and ⟶⊆ S × L × S is a transition relation satisfying the following properties:

• (Time Determinism) for every s, s′, s′′ ∈ S and d ∈ ℝ_{≥0}, if s →^{ϵ(d)} s′

and s →^{ϵ(d)} s′′, then s′ = s′′;

• (Time Additivity) for every s, s′′ ∈ S and d_{1}, d_{2} ∈ ℝ_{≥0}, s →^{ϵ(d_{1}+d_{2})} s′′

iff s →^{ϵ(d_{1})} s′ →^{ϵ(d_{2})} s′′, for some s′ ∈ S;

• (0-Delay) for every s, s′ ∈ S, s →^{ϵ(0)} s′ iff s = s′.

As usual, we write s →^{α} to mean that there is some state s′ such that s →^{α} s′.

The axioms of time determinism, time additivity and 0-delay are standard in the literature on Yi’s TCCS (see, e.g., [28]).

Timed Automata Let C be a set of clocks. We use B(C) to denote the set of boolean expressions over atomic formulae of the form x ⋈ p and x − y ⋈ p, with x, y ∈ C, p ∈ ℕ, and ⋈∈ {<, >, =}. Expressions in B(C) are interpreted over the collection of time assignments. A time assignment, or valuation, v for C is a function from C to ℝ_{≥0}. Given an expression g ∈ B(C) and a time assignment v, we write v ⊧ g if v satisfies g. Note that B(C) is closed under negation. For every time assignment v and d ∈ ℝ_{≥0}, we use v + d to denote the time assignment which maps each clock x ∈ C to the value v(x) + d. Two assignments u and v are said to agree on the set of clocks C′ iff they assign the same real number to every clock in C′. For every subset C′ of clocks, v[C′ ↦ 0] denotes the assignment for C which maps each clock in C′ to the value 0 and agrees with v over C\C′.

Definition 2.2 A timed automaton is a quintuple A = (Act, N, n_{0}, C, E) where N is a finite set of nodes, n_{0} is the initial node, C is a finite set of clocks, and E ⊆ N × N × Act × 2^{C} × B(C) is a set of edges. The quintuple e = (n, n_{e}, a, r_{e}, g_{e}) ∈ E stands for an edge from node n to node n_{e} (the target of e) with action a, where r_{e} denotes the set of clocks to be reset to 0 and g_{e} is the enabling condition (or guard) over the clocks of A.

A state of a timed automaton A is a pair (n, v) where n is a node of A and v is a time assignment for C. The initial state of A is (n_{0}, [C ↦ 0]) where n_{0} is the initial node of A, and [C ↦ 0] is the time assignment mapping all clocks in C to 0.

The operational semantics of a timed automaton A is given by the TLTS T_{A} = (S_{A}, L, s_{A}^{0}, ⟶), where S_{A} is the set of states of A, s_{A}^{0} is the initial state of A, and ⟶ is the transition relation defined as follows:

\begin{matrix}(n, v) →^{a} (n′, v′) & iff ∃e = (n, n′, a, r_{e}, g_{e}) ∈ E. v ⊧ g_{e} ∧ v′ = v[r_{e} ↦ 0] \\ (n, v) →^{ϵ(d)} (n′, v′) & iff n = n′ and v′ = v + d , \end{matrix}

where a ∈ Act and ϵ(d) ∈ D.

The Logic L_{ν} The logic L_{ν} is a real-time version of Hennessy-Milner Logic with greatest fixed-points that stems from [19]. We now briefly review its syntax and semantics for the sake of completeness.

Definition 2.3 (Syntax of L_{ν}) Let K be a finite set of formula clocks, Id a finite set of identifiers and k a non-negative integer. The set L_{ν} of formulae over K, Id and largest constant k is generated by the abstract syntax below, with φ and ψ ranging over L_{ν}:

φ ::= tt | ff | φ ∧ ψ | φ ∨ ψ | ∃∃φ | ∀∀φ | ⟨a⟩φ | [a]φ |
x \underline{in} φ | x ⋈ p | x + p ⋈ y + q | Z

where a ∈ Act, x, y ∈ K, p, q ∈ {0, …, k}, ⋈∈ {=, <, ≤, >, ≥} and Z ∈ Id.

The logic L_{ν} allows for the recursive definition of formulae by including a finite set Id of identifiers. The formula associated with each of the identifiers is specified by a declaration D, i.e. D assigns a formula of L_{ν} to each identifier. For an identifier Z we let Z =^{def} φ denote D(Z) = φ. Intuitively Z will stand for the largest solution of the equation Z =^{def} φ. We refer the interested reader to [19] for more information on L_{ν}.

Given a timed automaton A, whose set of clocks C is disjoint from K, we interpret the formulae in L_{ν} over extended states. An extended state of A is a pair (n, vu), where (n, v) is a state of A, u is a time assignment for K, and we use vu for the assignment over C ∪ K that agrees with v over C and with u over K. Definition 2.4 (Semantics of L_{ν}) Let A be a timed automaton and D a declaration. The satisfaction relation ⊧_{D} is the largest relation satisfying the following implications:

(n, vu) ⊧_{D} tt ⇒ true
(n, vu) ⊧_{D} ff ⇒ false
(n, vu) ⊧_{D} φ ∧ ψ ⇒ (n, vu) ⊧_{D} φ and (n, vu) ⊧_{D} ψ
(n, vu) ⊧_{D} φ ∨ ψ ⇒ (n, vu) ⊧_{D} φ or (n, vu) ⊧_{D} ψ
(n, vu) ⊧_{D} ∃∃φ ⇒ ∃d ∈ ℝ_{≥0}.(n, (v + d)(u + d)) ⊧_{D} φ
(n, vu) ⊧_{D} ∀∀φ ⇒ ∀d ∈ ℝ_{≥0}.(n, (v + d)(u + d)) ⊧_{D} φ
(n, vu) ⊧_{D} ⟨a⟩φ ⇒ ∃(n′, v′).(n, v) →^{a} (n′, v′) and (n′, v′u) ⊧_{D} φ
(n, vu) ⊧_{D} [a]φ ⇒ ∀(n′, v′).(n, v) →^{a} (n′, v′) implies (n′, v′u) ⊧_{D} φ
(n, vu) ⊧_{D} x ⋈ p ⇒ u(x) ⋈ p
(n, vu) ⊧_{D} x + p ⋈ y + q ⇒ u(x) + p ⋈ u(y) + q
(n, vu) ⊧_{D} x \underline{in} φ ⇒ (n, vu′) ⊧_{D} φ where u′ = u[\{x\} ↦ 0]
(n, vu) ⊧_{D} Z ⇒ (n, vu) ⊧_{D} D(Z) .

Any relation satisfying the above implications is referred to as a satisfiability relation. From standard fixed-point theory [27] we have that ⊧_{D} is the union of all satisfiability relations.

3 Timed Behavioural Relations

In the untimed setting various behavioral relations over processes have been proposed (see, e.g., [12] for an encyclopaedic treatment and detailed references to the original literature), and some of them (e.g. bisimulation and trace equivalence) have later been adapted to a timed setting. However, the timed setting also provides specific time-dependent behavioral relations. One such relation is the faster-than bisimulation from [23], which explicitly requires one process to execute at least as fast as another, while having the same functional behaviour. (See [3] for a similar proposal in the more classic setting of CCS [22].)

We now proceed to review the timed behavioural relations over TLTSs studied in this paper. The notion of timed bisimulation stems from [28]. It is the obvious adaptation to the timed setting of the classic definition due to Park [24].

Definition 3.1 Let T = (S, L, s^{0}, ⟶) be a TLTS. A timed simulation is a relation R ⊆ S × S such that whenever s_{1}Rs_{2} and α ∈ L, then:

- If s_{1} →^{α} s′_{1} then s_{2} →^{α} s′_{2} for some s′_{2} such that s′_{1}Rs′_{2}.

A timed bisimulation is a symmetric timed simulation.

For states s_{1}, s_{2}, we write s_{1} ⊏_{∼}_{S} s_{2} (resp. s_{1} ∼ s_{2}) iff there exists a timed simulation (resp. a timed bisimulation) R with s_{1}Rs_{2}.

In the untimed setting, the notion of ready simulation stems from [5, 20]. In [5], the ready simulation preorder was characterized as the largest congruence with respect to the GSOS format of operational rules included in completed trace inclusion.

Definition 3.2 Let T = (S, L, s^{0}, ⟶) be a TLTS. A timed ready simulation is a relation R ⊆ S × S such that whenever s_{1}Rs_{2}, a ∈ Act and α ∈ L then:

- If s_{1} →^{α} s′_{1} then s_{2} →^{α} s′_{2} for some s′_{2} such that s′_{1}Rs′_{2};

- If s_{2} →^{a} then s_{1} →^{a}.

For states s_{1}, s_{2}, we write s_{1} ⊏_{∼}_{RS} s_{2} iff there exists a timed ready simulation R with s_{1}Rs_{2}.

Moller and Tofts [23] have proposed a preorder on processes that distinguishes functionally behaviourally equivalent processes which operate at different speed. Their original proposal applied to their calculus TCCS, but it is simple enough to adapt it to the setting of TLTSs.

Definition 3.3 Let T = (S, L, s^{0}, ⟶) be a TLTS. A faster-than bisimulation is a relation R ⊆ S ×S such that whenever s_{1}Rs_{2}, a ∈ Act and d ∈ ℝ_{≥0} then:

1. if s_{1} →^{a} s′_{1} then there are d ∈ ℝ_{≥0}, s′′_{1}, s′_{2} and s′′_{2} such that s′_{1} →^{ϵ(d)} s′′_{1},

s_{2} →^{ϵ(d)} s′_{2} →^{a} s′′_{2}, and s′_{1} R s′_{2};

2. If s_{2} →^{a} s′_{2} then s_{1} →^{a} s′_{1} for some s′_{1} such that s′_{1} R s′_{2};

3. If s_{1} →^{ϵ(d)} s′_{1} then s_{2} →^{ϵ(d)} s′_{2} for some s′_{2} such that s′_{1} R s′_{2};

4. If s_{2} →^{ϵ(d)} s′_{2} then s_{1} →^{ϵ(d)} s′_{1} for some s′_{1} such that and s′_{1} R s′_{2}.

For states s_{1}, s_{2}, we write s_{1} ⊏_{∼}_{F T} s_{2} iff there exists a faster-than bisimulation R with s_{1}Rs_{2}.

It is well-known that ⊏_{∼}_{∗} (∗ ∈ {S, RS, F T }) is a preorder. Moreover ⊏_{∼}_{S} is the largest timed simulation, ⊏_{∼}_{RS} is the largest timed ready simulation, and ⊏_{∼}_{F T} is the largest faster-than bisimulation. Similarly, ∼ is an equivalence relation, and is the largest timed bisimulation.

All of the previously defined behavioural relations can be lifted to the setting of timed automata thus:

Definition 3.4 Let A, B be two timed automata. Then, for every relation R∈ {⊏_{∼}_{S}, ⊏_{∼}_{RS}, ⊏_{∼}_{F T} , ∼}, we write A R B iff s_{A}^{0} R s_{B}^{0} in the TLTS that results by taking the disjoint union of T_{A} and T_{B}.

In what follows, we shall always use the behavioural relations defined above to compare (states of) timed automata.

4 Characteristic Formula Constructions

We now offer general characteristic formula constructions in terms of L_{ν} for each of the timed behavioral relations introduced in Sect. 3. The constructions associate with each timed automaton a set of propositional equations (one equation per node of the automaton) that characterizes it up to the given timed behavioural relation.

To increase the readability of the characteristic formulae we make use of some derived constructs in the logic L_{ν}. These we now present for the sake of clarity.

For a reset set r = \{x_{1}, …, x_{k}\}, we use the abbreviation r \underline{in} φ to stand for the formula inductively defined thus:

∅ \underline{in} φ =^{def} φ
\{x_{1}, …, x_{k}\} \underline{in} φ =^{def} x_{1} \underline{in} (\{x_{2}, …, x_{k}\} \underline{in} φ)  (k ≥ 1) .

Note that the order of the clocks is arbitrary because x \underline{in} (y \underline{in} φ) is logically equivalent to y \underline{in} (x \underline{in} φ).

The expression g ⇒ φ will stand for \overline{g} ∨ φ, where \overline{g} is the negation of the guard g. This is a formula in L_{ν} because the collection of guards is closed under negation.

Given a node n in a timed automaton A, and action a, we define:

enabled(n, a) =^{def} ⋁_{e∈E(n,a)}g_{e} ,  (1)

where e = (n, n_{e}, a, r_{e}, g_{e}) is an edge, and E(n, a) denotes the set of alabelled edges from node n. Intuitively, the formula enabled(n, a) describes when action a can be performed from a state of the form (n, v). The negation of the expression enabled(n, a) will be used in the characteristic formula construction for timed ready simulation. Note that, since the collection of guards is closed under negation, the negation of enabled(n, a) can also be expressed in L_{ν}. Finally, we recall that, as usual, an empty disjunction stands for ff and an empty conjunction is equivalent to tt.

In the remainder of this section, we shall implicitly assume a given timed automaton A, for which all the characteristic formulae will be defined.

Characteristic Formula for Timed Bisimulation Equivalence For this relation we define the characteristic formula describing the properties presented in Defn. 3.1. A formula characterizing a node of a timed automaton up to timed bisimulation should offer a description of:

1. all the actions that are enabled in the node,

2. which node is entered by taking a given transition, together with the resets associated with it, and

3. the maximal delay that is allowed in the node.

The resulting characteristic formula is presented below. It consists of three sets of conjuncts, each associated to one of the above properties, for each node n of a timed automaton A:

Φ^{∼}(n) =^{def} ( ⋀_{a∈Act} ⋀_{e∈E(n,a)}g_{e} ⇒ (⟨a⟩ r_{e} \underline{in} Φ^{∼}(n_{e}))) ∧

⋀_{a∈Act} [a]( ⋁_{e∈E(n,a)} g_{e} ∧ (r_{e} \underline{in} Φ^{∼}(n_{e}))) ∧

∀∀Φ^{∼}(n)

where n is a node of A, e = (n, n_{e}, a, r_{e}, g_{e}), and we recall that E(n, a) denotes the set of a-labelled edges from node n. We shall use D_{A}^{∼} to denote the declaration that consists of the equations above, one for each node of A.

Theorem 4.1 Let A, B be timed automata with disjoint sets of clocks. Let n be a node of A and m be a node of B. Assume that u and v are valuations for the clocks of A and B, respectively. Then

(n, u) ∼ (m, v) iff (m, vu) ⊧ Φ^{∼}(n) ,

where (m, vu) ⊧ Φ^{∼}(n) holds with respect to the declaration D_{A}^{∼}.

Proof: We separately prove that:

1. (n, u) ∼ (m, v) only if (m, vu) ⊧ Φ^{∼}(n), and

2. if (m, vu) ⊧ Φ^{∼}(n) then (n, u) ∼ (m, v).

⟨1⟩ To show that the ‘only if’ implication holds, consider the relation ⊢ defined by structural induction on formulae thus: (m ranges over the nodes of B, and n over those of A)

(m, vu) ⊢ tt ⇔ true
(m, vu) ⊢ ff ⇔ false
(m, vu) ⊢ φ ∧ ψ ⇔ (m, vu) ⊢ φ and (m, vu) ⊢ ψ
(m, vu) ⊢ φ ∨ ψ ⇔ (m, vu) ⊢ φ or (m, vu) ⊢ ψ
(m, vu) ⊢ ∃∃φ ⇔ ∃d ∈ ℝ_{≥0}.(m, (v + d)(u + d)) ⊢ φ
(m, vu) ⊢ ∀∀φ ⇔ ∀d ∈ ℝ_{≥0}.(m, (v + d)(u + d)) ⊢ φ
(m, vu) ⊢ ⟨a⟩φ ⇔ ∃(m′, v′).(m, v) →^{a} (m′, v′) and
(m′, v′u) ⊢ φ
(m, vu) ⊢ [a]φ ⇔ ∀(m′, v′).(m, v) →^{a} (m′, v′) implies
(m′, v′u) ⊢ φ
(m, vu) ⊢ x ⋈ p ⇔ u(x) ⋈ p
(m, vu) ⊢ x + p ⋈ y + q ⇔ u(x) + p ⋈ u(y) + q
(m, vu) ⊢ x \underline{in} φ ⇔ (m, vu′) ⊢ φ where u′ = u[\{x\} ↦ 0]
(m, vu) ⊢ Φ^{∼}(n) ⇔ (m, v) ∼ (n, u) .

We prove that ⊢ is a satisfiability relation. The only interesting part of the proof is to show that if (m, vu) ⊢ Φ^{∼}(n), then (m, vu) ⊢ D_{A}^{∼}(Φ^{∼}(n)). This we now present in detail. Assume that (m, vu) ⊢ Φ^{∼}(n) and let ξ be a conjunct of D_{A}^{∼}(Φ^{∼}(n)). We prove that (m, vu) ⊢ ξ holds for each of the three types of conjuncts of the characteristic formula.

⟨1⟩.1 Case ξ ≡ g_{e} ⇒ (⟨a⟩r_{e} \underline{in} Φ^{∼}(n_{e})), where a ∈ Act and e ∈ E(n, a). The claim is trivial if u |̸= g_{e}. Assume now that u ⊧ g_{e}. We wish to argue that

(m, vu) ⊢ ⟨a⟩r_{e} \underline{in} Φ^{∼}(n_{e}) .  (2)

Since u ⊧ g_{e} and e ∈ E(n, a), it follows that (n, u) →^{a} (n_{e}, u[r_{e} ↦ 0]). By the assumption that (m, vu) ⊢ Φ^{∼}(n), we have that (n, u) ∼ (m, v). Thus there is a transition (m, v) →^{a} (m′, v′) with

(m′, v′) ∼ (n_{e}, u[r_{e} ↦ 0]) .

By the definition of ⊢, it follows that

(m′, v′(u[r_{e} ↦ 0])) ⊢ Φ^{∼}(n_{e}) .

Thus, again by the definition of ⊢, it holds that

(m′, v′u) ⊢ r_{e} \underline{in} Φ^{∼}(n_{e}) ,

from which (2) follows because (m, v) →^{a} (m′, v′).

⟨1⟩.2 Case ξ ≡ [a]( ⋁_{e∈E(n,a)} g_{e} ∧ (r_{e} \underline{in} Φ^{∼}(n_{e}))), where a ∈ Act.

Assume that (m, v) →^{a} (m′, v′). We prove that

(m′, v′u) ⊢ ⋁_{e∈E(n,a)} g_{e} ∧ (r_{e} \underline{in} Φ^{∼}(n_{e})) .  (3)

To this end, note that, since (n, u) ∼ (m, v) by the assumption that (m, vu) ⊢ Φ^{∼}(n), there is a transition (n, u) →^{a} (n′, u′) with

(n′, u′) ∼ (m′, v′) .  (4)

Since (n, u) →^{a} (n′, u′) holds, there is an edge e ∈ E(n, a) such that

- u ⊧ g_{e},

- n′ = n_{e}, and

- u′ = u[r_{e} ↦ 0].

Thus (m′, v′u) ⊢ g_{e} and, by (4), (m′, v′(u[r_{e} ↦ 0])) ⊢ Φ^{∼}(n_{e}). By the definition of ⊢, we may now infer that

(m′, v′u) ⊢ r_{e} \underline{in} Φ^{∼}(n_{e})

from which (3) finally follows.

⟨1⟩.3 Case ξ ≡ ∀∀Φ^{∼}(n). Assume that d ∈ ℝ_{≥0}. We prove that

(m, (v + d)(u + d)) ⊢ Φ^{∼}(n) .  (5)

Since (m, v) →^{ϵ(d)} (m, v + d), (n, u) →^{ϵ(d)} (n, u + d), and (m, v) ∼ (n, u)

hold, it follows by time determinism that (m, v + d) ∼ (n, u + d) also holds. The definition of ⊢ now yields (5), which was to be shown.

The proof of statement ⟨1⟩ is now complete.

⟨2⟩ We prove that the relation

R = {((n, u), (m, v)), ((m, v), (n, u)) | (m, vu) ⊧ Φ^{∼}(n)}

is a timed bisimulation. Note, first of all, that R is symmetric by definition. We proceed to prove that the relation R satisfies the clauses in Defn. 3.1. Assume to this end that (n, u)R(m, v) because (m, vu) ⊧ Φ^{∼}(n).

⟨2⟩.1 Case (n, u) →^{a} (n′, u′).

Since (n, u) →^{a} (n′, u′) holds, there is an edge e = (n, n_{e}, a, g_{e}, r_{e}) ∈ E(n, a) such that

(i) u ⊧ g_{e}, (ii) n′ = n_{e}, and (iii) u′ = u[r_{e} ↦ 0]. Since (m, vu) ⊧ Φ^{∼}(n) and (i) holds, it follows that

(m, vu) ⊧ ⟨a⟩r_{e} \underline{in} Φ^{∼}(n_{e}) .

This means that there is a state (m′, v′) such that (m, v) →^{a} (m′, v′) and (m′, v′(u[r_{e} ↦ 0])) ⊧ Φ^{∼}(n_{e}). For such an (m′, v′) we infer that (n′, u′)R(m′, v′) by (ii) and (iii).

⟨2⟩.2 Case (n, u) →^{ϵ(d)} (n, u + d).

Since (m, vu) ⊧ ∀∀Φ^{∼}(n), we have that

(m, (v + d)(u + d)) ⊧ Φ^{∼}(n) .

By the definition of R, it follows that (n, u + d)R(m, v + d), and, as (m, v) →^{ϵ(d)} (m, v + d), we are done.

We now consider the case that (m, v)R(n, u) because (m, vu) ⊧ Φ^{∼}(n).

⟨2⟩.3 Case (m, v) →^{a} (m′, v′).

Since (m, vu) ⊧ [a]( ⋁_{e∈E(n,a)} g_{e} ∧ (r_{e} \underline{in} Φ^{∼}(n_{e}))), we have that

(m′, v′u) ⊧ ⋁_{e∈E(n,a)} g_{e} ∧ (r_{e} \underline{in} Φ^{∼}(n_{e})). It follows that, for some

e ∈ E(n, a),

(i) u ⊧ g_{e}, and (ii) (m′, v′(u[r_{e} ↦ 0])) ⊧ Φ^{∼}(n_{e}).

By (i) we have that (n, u) →^{a} (n_{e}, u[r_{e} ↦ 0]) . By (ii) and the definition of R, it follows that (m′, v′)R(n_{e}, u[r_{e} ↦ 0]) and we are done.

⟨2⟩.4 Case (m, v) →^{ϵ(d)} (m, v + d), where d ∈ ℝ_{≥0}. Since (m, vu) ⊧ ∀∀Φ^{∼}(n), it follows that (m, (v + d)(u + d)) ⊧ Φ^{∼}(n). Thus (m, v + d)R(n, u + d) holds. Moreover (n, u) →^{ϵ(d)} (n, u + d) and we are done.

This completes the proof of the theorem □

Note that the characteristic formula for timed bisimulation has size that is linear in that of the argument automaton. Laroussine, Larsen and Weise [19] have proposed a characteristic formula construction for timed automata up to timed bisimilarity. However, their construction is based on directly mimicking the standard construction from the untimed setting on the region graph, and the size of their characteristic formula is therefore linear in the size of the region graph. Unfortunately, however, as observed by Alur and Dill [2], the region graph has size that is exponential in the length of the clock constraints of the argument automaton.

Remark: Laroussine, Larsen and Weise [19] have shown that the logic L_{ν} characterizes timed bisimilarity over timed automata. This means that two timed automata are timed bisimilar if, and only if, they satisfy the same formulae in the logic L_{ν}. As a consequence of Thm. 4.1, we obtain that the existential delay modality ∃∃ is not necessary to obtain this logical characterization of timed bisimilarity.

As a further corollary of Thm. 4.1, and the EXPTIME upper bound on the complexity of model checking for L_{ν} [1], we have another proof of the following well-known result.

Corollary 4.2 The problem of deciding whether two timed automata are timed bisimilar is decidable in exponential time.

Characteristic Formula for Timed Simulation The characteristic formula for ⊏_{∼}_{S} is a minor variation on that for ∼, and is defined thus:

Φ^{⊏_{∼}S} (n) =^{def} ( ⋀_{a∈Act} ⋀_{e∈E(n,a)}g_{e} ⇒ (⟨a⟩ r_{e} \underline{in} Φ^{⊏_{∼}S} (n_{e}))) ∧ (∀∀Φ^{⊏_{∼}S} (n)) ,

where n is a node of A, e = (n, n_{e}, a, r_{e}, g_{e}) and E(n, a) denotes the set of

a labelled edges from node n. We shall use D_{A}^{⊏_{∼}S} to denote the declaration that consists of the equations above, one for each node of A.

A minor variation on the proof of Thm. 4.1 now establishes that:

Theorem 4.3 Let A, B be timed automata with disjoint sets of clocks. Let n be a node of A and m be a node of B. Assume that u and v are valuations for the clocks of A and B, respectively. Then

(n, u) ⊏_{∼}_{S} (m, v) iff (m, vu) ⊧ Φ^{⊏_{∼}S} (n) ,

where (m, vu) ⊧ Φ^{⊏_{∼}S} (n) holds with respect to the declaration D_{A}^{⊏_{∼}S}.

The full proof of this above theorem may be found in [25].

Corollary 4.4 The problem of deciding whether A ⊏_{∼}_{S} B holds for timed automata A, B is decidable in exponential time.

Timed ready simulation The characteristic formula for timed ready simulation is presented below:

Φ^{⊏_{∼}RS} (n) =^{def} ( ⋀_{a∈Act} ⋀_{e∈E(n,a)}g_{e} ⇒ (⟨a⟩ r_{e} \underline{in} Φ^{⊏_{∼}RS} (n_{e}))) ∧

( ⋀_{a∈Act}(\overline{enabled(n, a)} ⇒ [a]ff) ∧

∀∀Φ^{⊏_{∼}RS} (n)

where n is a node of A, e = (n, n_{e}, a, r_{e}, g_{e}) and we recall that E(n, a) denotes the set of a labelled edges from node n. The notation \overline{enabled(n, a)} stands for the negation of the formula enabled(n, a) given in (1). We shall

use D_{A}^{⊏_{∼}RS} to denote the declaration that consists of the equations above, one for each node of A.

A minor variation on the proof of Thm. 4.1 now establishes that:

Theorem 4.5 Let A, B be timed automata with disjoint sets of clocks. Let n be a node of A and m be a node of B. Assume that u and v are valuations for the clocks of A and B, respectively. Then

(n, u) ⊏_{∼}_{RS} (m, v) iff (m, vu) ⊧ Φ(n)^{⊏_{∼}RS} ,

where (m, vu) ⊧ Φ^{⊏_{∼}RS} (n) holds with respect to the declaration D_{A}^{⊏_{∼}RS}.

The full proof of this result may also be found in [25].

Corollary 4.6 The problem of deciding whether A ⊏_{∼}_{RS} B holds for timed automata A, B is decidable in exponential time.

Faster-than preorder In the characteristic formula constructions that we have presented so far no use was made of the existential modality ∃∃ over delay transitions. The use of the ∃∃ modality will instead play a crucial role in the definition of the characteristic property for the faster-than bisimulation preorder. This we now proceed to present.

For every node n in a timed automaton A, we define:

Φ^{⊏_{∼}F T} (n) =^{def} ( ⋀_{a∈Act} ⋀_{e∈E(n,a)}g_{e} ⇒ (r_{e} \underline{in} ∃∃⟨a⟩Φ^{⊏_{∼}F T} (n_{e}))) ∧

( ⋀_{a∈Act} [a]( ⋁_{e∈E(n,a)} g_{e} ∧ (r_{e} \underline{in} Φ^{⊏_{∼}F T} (n_{e}))) ∧

∀∀Φ^{⊏_{∼}F T} (n) ,

where e = (n, n_{e}, a, r_{e}, g_{e}) and E(n, a) denotes the set of a labelled edges

from node n. We shall use D_{A}^{⊏_{∼}F T} to denote the declaration that consists of the equations above, one for each node of A.

Theorem 4.7 Let A, B be timed automata with disjoint sets of clocks. Let n be a node of A and m be a node of B. Assume that u and v are valuations for the clocks of A and B, respectively. Then

(n, u) ⊏_{∼}_{F T} (m, v) iff (m, vu) ⊧ Φ^{⊏_{∼}F T} (n) ,

where (m, vu) ⊧ Φ^{⊏_{∼}F T} (n) holds with respect to the declaration D_{A}^{⊏_{∼}F T}.

Proof: We separately prove that:

1. (n, u) ⊏_{∼}_{F T} (m, v) only if (m, vu) ⊧ Φ^{⊏_{∼}F T} (n), and

2. if (m, vu) ⊧ Φ^{⊏_{∼}F T} (n) then (n, u) ⊏_{∼}_{F T} (m, v).

⟨1⟩ To show that the ‘only if’ implication holds, consider the relation ⊢ defined by structural induction on formulae thus: (m ranges over the nodes of B, and n over those of A)

(m, vu) ⊢ tt ⇔ true
(m, vu) ⊢ ff ⇔ false
(m, vu) ⊢ φ ∧ ψ ⇔ (m, vu) ⊢ φ and (m, vu) ⊢ ψ
(m, vu) ⊢ φ ∨ ψ ⇔ (m, vu) ⊢ φ or (m, vu) ⊢ ψ
(m, vu) ⊢ ∃∃φ ⇔ ∃d ∈ ℝ_{≥0}.(m, (v + d)(u + d)) ⊢ φ
(m, vu) ⊢ ∀∀φ ⇔ ∀d ∈ ℝ_{≥0}.(m, (v + d)(u + d)) ⊢ φ
(m, vu) ⊢ ⟨a⟩φ ⇔ ∃(m′, v′).(m, v) →^{a} (m′, v′) and
(m′, v′u) ⊢ φ
(m, vu) ⊢ [a]φ ⇔ ∀(m′, v′).(m, v) →^{a} (m′, v′) implies
(m′, v′u) ⊢ φ
(m, vu) ⊢ x ⋈ p ⇔ u(x) ⋈ p
(m, vu) ⊢ x + p ⋈ y + q ⇔ u(x) + p ⋈ u(y) + q
(m, vu) ⊢ x \underline{in} φ ⇔ (m, vu′) ⊢ φ where u′ = u[\{x\} ↦ 0]
(m, vu) ⊢ Φ^{⊏_{∼}F T} (n) ⇔ (n, u) ⊏_{∼}_{F T} (m, v) .

We prove that ⊢ is a satisfiability relation. The only interesting part of the

proof is to show that if (m, vu) ⊢ Φ^{⊏_{∼}F T} (n), then (m, vu) ⊢ D_{A}^{⊏_{∼}F T} (Φ^{⊏_{∼}F T} (n)). This we now proceed to prove.

Assume that (m, vu) ⊢ Φ^{⊏_{∼}F T} (n) and let ξ be a conjunct of D_{A}^{⊏_{∼}F T} (Φ^{⊏_{∼}F T} (n)). We prove that (m, vu) ⊢ ξ holds for the first type of conjunct of the characteristic formula. The proof for the other two types of conjuncts is similar to the corresponding cases of the proof of Thm. 4.1.

– Case ξ ≡ g_{e} ⇒ (r_{e} \underline{in} ∃∃⟨a⟩Φ^{⊏_{∼}F T} (n_{e})), where a ∈ Act and e ∈ E(n, a). The claim is trivial if u |̸= g_{e}. Assume thus that u ⊧ g_{e} for some a-labelled edge e emanating from n. We wish to argue that

(m, vu) ⊢ r_{e} \underline{in} ∃∃⟨a⟩ \underline{in} Φ^{⊏_{∼}F T} (n_{e}) .  (6)

To this end, it is sufficient to prove that

(m, v(u[r_{e} ↦ 0])) ⊢ ∃∃⟨a⟩ \underline{in} Φ^{⊏_{∼}F T} (n_{e}) .  (7)

Since u ⊧ g_{e} and e ∈ E(n, a), it follows that (n, u) →^{a} (n_{e}, u[r_{e} ↦ 0]). As (n, u)⊏_{∼}_{F T} (m, v) holds, there are a d ∈ ℝ_{≥0} and a state (m′, v′) such that

- (m, v) →^{ϵ(d)} (m, v + d),

- (m, v + d) →^{a} (m′, v′), and

- (n_{e}, u[r_{e} ↦ 0]) →^{ϵ(d)} (n_{e}, u[r_{e} ↦ 0] + d), with

(n_{e}, (u[r_{e} ↦ 0]) + d) ⊏_{∼}_{F T} (m′, v′) .  (8)

Hence it is sufficient to prove that

(m, (v + d)(u[r_{e} ↦ 0] + d)) ⊢ ⟨a⟩ \underline{in} Φ^{⊏_{∼}F T} (n_{e}) .  (9)

Since (m, v + d) →^{a} (m′, v′), by the definition of ⊢ and by (8) it follows that (m′, v′(u[r_{e} ↦ 0] + d)) ⊢ Φ^{⊏_{∼}F T} (n_{e}), from which we may derive that (9), (7) and finally (6) hold.

⟨2⟩ We now show that the ‘if’ implication holds. To this end we prove that the relation

R = {((n, u), (m, v))|(m, vu) ⊧ Φ^{⊏_{∼}F T} (n)}

is a faster-than bisimulation. Assume that (n, u)R(m, v). We proceed to check that all of the defining properties of a faster-than bisimulation are met.

⟨2⟩.1 Case (n, u) →^{a} (n′, u′).

Then there is an edge e ∈ E(n, a) such that

(i) u ⊧ g_{e}, (ii) n′ = n_{e}, and (iii) u′ = u[r_{e} ↦ 0].

Since (m, vu) ⊧ Φ^{⊏_{∼}F T} (n) and (i) holds, it follows that

(m, vu) ⊧ r_{e} \underline{in} ∃∃⟨a⟩Φ^{⊏_{∼}F T} (n_{e}) .

Hence (m, vu′) ⊧ ∃∃⟨a⟩Φ^{⊏_{∼}F T} (n_{e}). This means that there are a delay d ∈ ℝ_{≥0} and a state (m′, v′) such that

(m, v) →^{ϵ(d)} (m, v + d) →^{a} (m′, v′)

and (m′, v′u′′) ⊧ Φ^{⊏_{∼}F T} (n_{e}), where u′′ = u′ + d. By the definition of R,

we have (n′, u′′)R(m′, v′). Moreover, (n′, u′) →^{ϵ(d)} (n′, u′′), and we are done.

⟨2⟩.2 Case (n, u) →^{ϵ(d)} (n, u + d).

Since (m, vu) ⊧ ∀∀Φ^{⊏_{∼}F T} (n), we have that

(m, (v + d)(u + d)) ⊧ Φ^{⊏_{∼}F T} (n) .

By the definition of R, it follows that (n, u + d)R(m, v + d) and, as

(m, v) →^{ϵ(d)} (m, v + d), we are done.

⟨2⟩.3 Case (m, v) →^{a} (m′, v′).

Since (m, vu) ⊧ [a]( ⋁_{e∈E(n,a)} g_{e} ∧ (r_{e} \underline{in} Φ^{⊏_{∼}F T} (n_{e}))), we have that

(m′, v′u) ⊧ ⋁_{e∈E(n,a)} g_{e} ∧ (r_{e} \underline{in} Φ^{⊏_{∼}F T} (n_{e})). It follows that, for some

e ∈ E(n, a),

(i) u ⊧ g_{e} , and

(ii) (m′, v′(u[r_{e} ↦ 0])) ⊧ Φ^{⊏_{∼}F T} (n) .

By (i) (n, u) →^{a} (n_{e}, u[r_{e} ↦ 0]). By (ii) and the definition of R, it follows that (n_{e}, u[r_{e} ↦ 0])R(m′, v′) and we are done.

⟨2⟩.4 Case (m, v) →^{ϵ(d)} (m, v + d), where d ∈ ℝ_{≥0}.

Since (m, vu) ⊧ Φ^{⊏_{∼}F T} (n), it follows that

(m, (v + d)(u + d)) ⊧ Φ^{⊏_{∼}F T} (n) .

Thus it holds that (n, u + d)R(m, v + d). Moreover (n, u) →^{ϵ(d)} (n, u + d) and we are done.

This completes the proof of the theorem. □

As for the previous behavioural relations studied in this section, we have that:

Corollary 4.8 The problem of deciding whether A ⊏_{∼}_{F T} B holds for timed automata A, B is decidable in exponential time.

5 Concluding Remarks

In their seminal paper [2], Alur and Dill proved that the problem of checking timed trace inclusion between a timed automaton A and a deterministic timed automaton B is PSPACE-complete. Following the classic automata theoretic approach, they achieved this result by reducing this problem to checking for the emptiness of the language accepted by a timed automaton that can be built in polynomial time from A and B. We shall now argue that the use of characteristic formulae offers an alternative approach to checking timed trace inclusion.

For the sake of clarity, we begin with some preliminary definitions.

Definition 5.1 A sequence of actions \overline{σ} = a_{1}a_{2}a_{3} … is a possibly infinite sequence with a_{i} ∈ Act.

A sequence of time instants \overline{t} = t_{1}t_{2}t_{3} … is a possibly infinite, nondecreasing sequence with t_{i} ∈ ℝ_{≥0}.

A timed trace ρ is a pair (\overline{σ}, \overline{t}), where \overline{σ} is a sequence of actions and \overline{t} is a sequence of time instants. The sequences \overline{σ} and \overline{t} are either both infinite or both finite and of the same length.

In a timed trace ρ, the real number t_{i} denotes the absolute time instant at which action a_{i} occurs. In particular, t_{1} always denotes the time instant at which the first action of the timed trace occurs. Assume, for the sake of simplicity, that every timed automaton is supplied with an extra clock x_{0} which is never reset. Such a clock will measure the time that has elapsed since a timed automaton started its execution.

Definition 5.2 Let A = (Act, N, n_{0}, C, E) be a timed automaton. We say that (\overline{σ}, \overline{t}), with \overline{σ} = a_{1}a_{2} … a_{k} and \overline{t} = t_{1}t_{2} … t_{k} (k ≥ 0), is a timed trace of A iff

(n_{0}, [C ↦ 0]) →^{ϵ(d_{1})}→^{a_{1}} (n_{1}, v_{1}) →^{ϵ(d_{2})}→^{a_{2}} (n_{2}, v_{2}) ⋯ (n_{k−1}, v_{k−1}) →^{ϵ(d_{k})}→^{a_{k}} (n_{k}, v_{k})

for some delays d_{1}, d_{2}, …, d_{k} ∈ ℝ_{≥0}, valuations v_{1}, v_{2}, … v_{k} such that t_{i} = v_{i}(x_{0}) for every i ∈ {1, …, k}, and nodes n_{1}, …, n_{k} of A. The set of timed traces of A will be written traces(A).

Let A and B be timed automata. We write A ⊏_{∼}_{T} B iff traces(A) ⊆ traces(B).

As shown by Alur and Dill [2], the relation ⊏_{∼}_{T} is undecidable for timed automata. It becomes decidable if the specification automaton B is deterministic.

Definition 5.3 A timed automaton is deterministic iff for every node n, action a ∈ Act and distinct edges e, e′ ∈ E(n, a), the guards g_{e} and g_{e′} are disjoint, i.e., g_{e} ∧ g_{e′} is unsatisfiable.

A standard argument, that may be found in [25], now suffices to establish the following result. (See, e.g., [11] for a similar statement in the classic, untimed setting.)

Proposition 5.4 Let A and B be timed automata. Then the following statements hold:

1. A ⊏_{∼}_{S} B implies A ⊏_{∼}_{T} B;

2. A ⊏_{∼}_{T} B implies A ⊏_{∼}_{S} B, if B is deterministic.

The import of the above result is that, if B is a deterministic timed automaton, checking whether the set of timed traces of a timed automaton A is included in that of B can be reduced to checking whether B satisfies the characteristic formula of A with respect to timed simulation.

The feasibility of the approach based on establishing behavioural relations for timed automata via model checking characteristic formulae needs to be established experimentally. The master’s thesis [25] describes a prototype implementation of a tool for checking behavioural relations for timed automata based on the theory presented in this study. This tool is rather inefficient, and cannot handle reasonably sized examples. However, we expect that an efficient tool for verifying behavioural equivalences for timed automata can be obtained by implementing a front-end to the L_{ν}-model checker CMC [18] that generates the different characteristic formula constructions we have presented.

References

[1] L. Aceto and F. Laroussinie, Is your model checker on time? On the complexity of model checking for timed modal logics, in Mathematical foundations of computer science 1999 (Szklarska Poreba), Springer-Verlag, Berlin, 1999, pp. 125–136.

[2] R. Alur and D. L. Dill, A theory of timed automata, Theoretical Comput. Sci., 126 (1994), pp. 183–235. Fundamental Study.

[3] S. Arun-Kumar and M. Hennessy, An efficiency preorder for processes, Acta Informatica, 29 (1992), pp. 737–760.

[4] J. Baeten and J. Klop, eds., Proceedings CONCUR 90, Amsterdam, vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990.

[5] B. Bloom, S. Istrail, and A. R. Meyer, Bisimulation can’t be traced, J. Assoc. Comput. Mach., 42 (1995), pp. 232–268.

[6] M. Browne, E. Clarke, and O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Comput. Sci., 59 (1988), pp. 115–131.

[7] E. Clarke and E. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic, in Proceedings of the Workshop on Logic of Programs, Yorktown Heights, D. Kozen, ed., vol. 131 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 52–71.

[8] E. Clarke, O. Grümberg, and D. Peled, Model Checking, MIT Press, 2000.

[9] R. Cleaveland and B. Steffen, Computing behavioral relations, logically, in ICALP ’91: Automata, Languages and Programming, J. L. Albert, B. Monien, and M. R. Artalejo, eds., vol. 510 of Lecture Notes in Computer Science, Madrid, July 1991, Springer-Verlag, pp. 127–138.

[10] , A linear-time model-checking algorithm for the alternationfree modal μ-calculus, Formal Methods in Systems Design, 2 (1993), pp. 121–147.

[11] J. Engelfriet, Determinacy → (observation equivalence = trace equivalence), Theoretical Comput. Sci., 36 (1985), pp. 21–25.

[12] R. J. van Glabbeek, The linear time – branching time spectrum, in Baeten and Klop [4], pp. 278–297.

[13] S. Graf and J. Sifakis, A modal characterization of observational congruence on finite terms of CCS, Information and Control, 68 (1986), pp. 125–145.

[14] M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach., 32 (1985), pp. 137–161.

[15] A. Ingólfsdóttir, J. C. Godskesen, and M. Zeeberg, Fra Hennessy-Milner logik til CCS-processer, Master’s thesis, Department of Computer Science, Aalborg University, 1987. In Danish.

[16] R. Keller, Formal verification of parallel programs, Comm. ACM, 19 (1976), pp. 371–384.

[17] D. Kozen, Results on the propositional mu-calculus, Theoretical Comput. Sci., 27 (1983), pp. 333–354.

[18] F. Laroussinie and K. G. Larsen, CMC: A tool for compositional model-checking of real-time systems, in Proc. IFIP Joint Int. Conf. Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PS TV’98), Kluwer Academic Publishers, 1998, pp. 439–456.

[19] F. Laroussinie, K. G. Larsen, and C. Weise, From timed automata to logic - and back, in Proceedings of the 20^{th} Symposium on Mathematical Foundations of Computer Science, vol. 969 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 529–540.

[20] K. G. Larsen and A. Skou, Bisimulation through probabilistic testing, Information and Computation, 94 (1991), pp. 1–28.

[21] R. Milner, An algebraic definition of simulation between programs, in Proceedings 2^{nd} Joint Conference on Artificial Intelligence, William Kaufmann, 1971, pp. 481–489. Also available as Report No. CS-205, Computer Science Department, Stanford University.

[22] , Communication and Concurrency, Prentice Hall, Englewood Cliffs, 1989.

[23] F. Moller and C. Tofts, Relating processes with respect to speed, in CONCUR ’91: 2^{nd} International Conference on Concurrency Theory, J. C. M. Baeten and J. F. Groote, eds., vol. 527 of Lecture Notes in Computer Science, Amsterdam, The Netherlands, 26–29 Aug. 1991, Springer-Verlag, pp. 424–438.

[24] D. Park, Concurrency and automata on infinite sequences, in 5^{th} GI Conference, Karlsruhe, Germany, P. Deussen, ed., vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167–183.

[25] M. L. Pedersen and J. Poulsen, Model-checking characteristic formulae — a method for proving timed behavioural relations, Master’s thesis, Department of Computer Science, Aalborg University, June 1999.

[26] B. Steffen and A. Ingólfsdóttir, Characteristic formulae for processes with divergence, Information and Computation, 110 (1994), pp. 149–163.

[27] A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, 5 (1955).

[28] Y. Wang, Real-time behaviour of asynchronous agents, in Baeten and Klop [4], pp. 502–520.

Recent BRICS Report Series Publications

RS-00-23 Luca Aceto, Anna Ingólfsdóttir, Mikkel Lykke Pedersen, and Jan Poulsen. Characteristic Formulae for Timed Automata. September 2000. 23 pp.

RS-00-22 Thomas S. Hune and Anders B. Sandholm. Using Automata in Control Synthesis — A Case Study. September 2000. 20 pp. Appears in Maibaum, editor, Fundamental Approaches to Software Engineering: First International Conference, FASE ’00 Proceedings, LNCS 1783, 2000, pages 349–362.

RS-00-21 M. Oliver Möller and Rajeev Alur. Heuristics for Hierarchical Partitioning with Application to Model Checking. August 2000. 30 pp.

RS-00-20 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. 2-Nested Simulation is not Finitely Equationally Axiomatizable. August 2000. 13 pp.

RS-00-19 Vinodchandran N. Variyam. A Note on NP ∩ coNP/poly. August 2000. 7 pp.

RS-00-18 Federico Crazzolara and Glynn Winskel. Language, Semantics, and Methods for Cryptographic Protocols. August 2000. ii+42 pp.

RS-00-17 Thomas S. Hune. Modeling a Language for Embedded Systems in Timed Automata. August 2000. 26 pp. Earlier version entitled Modelling a Real-Time Language appeared in Gnesi and Latella, editors, Fourth International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS ’99 Proceedings of the FLoC Workshop, 1999, pages 259–282.

RS-00-16 Jiří Srba. Complexity of Weak Bisimilarity and Regularity for BPA and BPP. June 2000. 20 pp. To appear in Aceto and Victor, editors, Expressiveness in Concurrency: Fifth International Workshop EXPRESS ’00 Proceedings, ENTCS, 2000.

RS-00-15 Daniel Damian and Olivier Danvy. Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation. June 2000. Extended version of an article to appear in Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming, 2000.