BRICS RS-95-2 Laroussinie et al.: From Timed Automata to Logic - and Back

BRICS

Basic Research in Computer Science

From Timed Automata to Logic

- and Back

Franc�ois Laroussinie Kim G. Larsen Carsten Weise

BRICS Report Series RS-95-2 ISSN 0909-0878 January 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, 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 publications in the BRICS Report Series. 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@daimi.aau.dk

From Timed Automata to Logic — and Back ^{∗}

François Laroussinie

BRICS^{†}, Aalborg Univ., Denmark

Kim G. Larsen

BRICS, Aalborg Univ., Denmark

Carsten Weise

Aachen Univ., Germany

Abstract

One of the most successful techniques for automatic verification is that of model checking. For finite automata there exist since long extremely efficient model–checking algorithms, and in the last few years these algorithms have been made applicable to the verification of real–time automata using the region–techniques of Alur and Dill.

In this paper, we continue this transfer of existing techniques from the setting of finite (untimed) automata to that of timed automata. In particular, a timed logic L_{ν} is put forward, which is sufficiently expressive that we for any timed automaton may construct a single characteristic L_{ν} formula uniquely characterizing the automaton up to timed bisimilarity. Also, we prove decidability of the satisfiability problem for L_{ν} with respect to given bounds on the number of clocks and constants of the timed automata to be constructed. None of these results have as yet been succesfully accounted for in the presence of time ^{1}.

∗This work has been supported by the European Communities under CONCUR2, BRA 7166

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

1An exception occurs in Alur’s thesis [Alu91] in which a decidability result is presented for a linear timed logic called MITL.

Contents

1 Introduction 3 2 Timed Automata 4 3 Timed Modal Logic L_{ν} 6 4 Model Checking 8 5 Characteristic Properties 10 6 Model Construction 13 A Proof of Theorem 2 20 B Proof of Proposition 1 21

1 Introduction

One of the most successful techniques for automatic verification is that of model–checking; i.e. a property is given as a formula of a propositional temporal logic and automatically compared with an automata ^{2} representing the actual behaviour of the system. Extremely efficient model–checking algorithms have been obtained for finite automata with respect to the branching–time temporal logics CTL [CE81, QS82, CES86] and (various fragments of) the modal μ–calculus [Koz82, AC88, EL86, CS91, And92, Xin92].

In the last few years, model–checking has been extended to real–time systems, with time considered to be a dense linear order. A timed extension of finite automata through addition of a finite set of real–valued clocks has been put forward [AD94], and the corresponding model–checking problem has been proven decidable for a number of timed logics including timed extensions of CTL (TCTL) [ACD90] and a timed μ–calculus (T_{μ}) [HNSY92].

However, in the untimed setting automata and logics enjoy a number of other important relationships which at present are either absent or at best unaccounted for in the setting of real–time automata and the corresponding real–time logics:

— Given a finite automaton, both CTL and the modal μ–calculus are sufficiently expressive that corresponding characteristic formulas may be expressed with respect to a number of behavioural preorders and equivalences (e.g. bisimilarity) [BCG88, GS86, IS94]: i.e. an automaton is related to another in the preorder if and only if the first automaton satisfies the characteristic formula of the second. As characteristic formulas can be automatically constructed in time linear in the size of the argument automaton, this yields a preorder checking method that outperforms other known algorithms [CS91]. No such relationship has so far been established between timed automata and any of the proposed real–timed logics;

— The satisfiability problems for CTL and the modal μ–calculus have been proven decidable [EC82, EH85, Wol85, KP83]; thus given a logical property it is possible to automatically synthesize a satisfying finite automata (provided any such exists). In contrast, the satisfiability problems for both TCTL and T_{μ} are undecidable [ACD90, HNSY92]

In this paper we present results establishing both of the two above desired relationships in the presence of real–time (timed automaton). In particular we put forward a timed logic L_{ν} for which we establish the following:

— First, we present an effective characteristic formula construction for timed bisimilarity, transforming any timed automaton into a formula of L_{ν} characterizing precisely the equivalence class of the automaton. Thus, timed bisimilarity between automata reduces to a model–checking problem, which — when combined with the model–checking algorithm for L_{ν} — yields an alternative algorithm for timed bisimulation compared with [Cer92]. In addition, characteristic formula constructions may be given for time–abstracted equivalence [LW93] and the “faster–than” relation in [FT91], immediately yielding decision procedures for these relationships as well;

2or a kripke structure

— Second, we prove decidability of bounded satisfiable for L_{ν}. That is, we present a model–construction algorithm, which given a formula of L_{ν} and bounds k and M will synthesize a timed automata with no more than k clocks and no clock being compared with constants greater than M (provided any such exits).

Combining the characteristic formula construction with the bounded model– construction algorithm enables us to decide whether an automaton can be simplified in terms of number of clocks and constants used for comparison.

The remainder of this paper is organized as follows: In the next section we give a short presentation of the notion of timed automata used in this paper; in section 3, the logic L_{ν} is presented, and in section 4 we review the region technique by Alur and Dill [AD94] and present a decidability result for the model–checking problem of L_{ν}. Section 5 presents the characteristic formula construction, whereas section 6 presents the bounded model–construction algorithm.

2 Timed Automata

Let A be a fixed set of actions ranged over by a, b, c, . . .. We denote by N the set of natural numbers and by R the set of non–negative real numbers. D denotes the set of delay actions {ϵ(d) | d ∈ R}, and L denotes the union A ∪ D. If C is a set of clocks, B(C) denotes the set of formulas built using boolean connectives over atomic formulas of the form x ≤ m, m ≤ x, x ≤ y + m and y + m ≤ x with x, y ∈ C and m ∈ N. Moreover B_{M}(C) denotes the subset of B(C) with no constant greater than M.

Definition 1 A timed automaton A is a tuple ⟨A, N, η_{0}, C, E⟩ where A is a finite set of actions, N is a finite set of nodes, η_{0} is the initial node, C is a finite set of clocks, and E ⊆ N × N × A × 2^{C} × B(C) corresponds to the set of edges. e = ⟨η, η′, a, r, b⟩ ∈ E represents an edge from the node η to the node η′ with action a, r denoting the set of clocks to be reset and b is the enabling condition over the clocks of A.

Example 1 Consider the 2-clock automaton A described in the left part of figure 1. The automaton has four nodes, η_{0}, η_{1}, η_{2} and η_{3}, two clocks, x and y, and three edges. The edge between η_{0} and η_{1} has a as action, {x} as reset set and the enabling condition for the edge is 0 < x < 1. □

Informally, the system starts at node η_{0} with all its clocks initialized to 0. The values of the clocks increase synchronously with time. At any time, the automaton whose current node is η can change node by following an edge ⟨η, η′, a, r, b⟩ ∈ E provided the current values of the clocks satisfy b. With this transition the clocks in r get reset to 0.

A time assignment v for C is a function from C to R. We denote by R^{C} the set of time assignments for C. For v ∈ R^{C}, x ∈ C and d ∈ R, v + d denotes the time assignment which maps each clock x in C to the value v(x) + d. For

{x}^{0 < x < 1} a A η_{0} η_{2}  ^{1}^{1}  ^{x}^{y}  ^{1}^{1}  ^{x}^{(η_{1})}^{y}  (η_{2}) ^{(η_{0})}^{ϵ(e)}^{ϵ(d)}^{y ≤ 1}b  c η_{3} η_{1} ^{x = 0}  a  b c^{(η_{3})}

Figure 1: An automaton and its behaviour

C′ ⊆ C, [C′ ↦ 0]v denotes the assignment for C which maps each clock in C′ to the value 0 and agrees with v over C\C′. Given a condition b ∈ B(C) and a time assignment v ∈ R^{C}, b(v) is a boolean value describing whether b is satisfied by v or not. Finally a k–clock automata is a timed automata ⟨A, S, η_{0}, C, E⟩ such that |C| = k.

A state of an automaton A is a pair ⟨η, v⟩_{A} where η is a node of A and v a time assignment for C. The initial state of A is ⟨η_{0}, v_{0}⟩_{A} where v_{0} is the time assignment mapping all clocks in C to 0.

The semantics of A is given by a labelled transition system M_{A} = ⟨Σ_{A}, L, σ_{0}, ⟶_{A}⟩, where Σ_{A} is the set of states of A, σ_{0} is the initial state ⟨η_{0}, v_{0}⟩_{A}, and ⟶_{A} is the transition relation defined as follows:

\begin{matrix}⟨η, v⟩⟶^{a}_{A}⟨η′, v′⟩ & iff & ∃r, b. ⟨η, η′, a, r, b⟩ ∈ E ∧ b(v) ∧ v′ = [r → 0]v \\ ⟨η, v⟩⟶^{ϵ(d)}_{A}⟨η′, v′⟩ & iff & η = η′ and v′ = v + d \end{matrix}

We may now apply the standard notion of bisimulation [Mil89, Par81] to the labelled transition systems determined by two automata A and B. Letting s_{A} and s_{B} range over states of respectively A and B, stong timed bisimulation ∼ is defined as the largest symmetric relation over Σ_{A} ×Σ_{B} such that whenever s_{A} ∼ s_{B} and ℓ ∈ A ∪ D then

• Whenever s_{A}⟶^{ℓ}_{A}s′_{A} then there exists s′_{B} such that s_{B}⟶^{ℓ}_{B}s′_{B} and s′_{A} ∼ s′_{B}.

We say that A and B are strong timed bisimular if their initial states are strong bisimilar.

Example 2 Reconsider the automaton A of Figure 1. The two coordinate systems in the right part of the Figure indicates (some of) the states of A. Each point of the coordinate systems represents a unique time assignment, with the top (resp. bottom) coordinate system representing states involving the node η_{0} (resp. η_{1}). In the Figure we have indicated the following transition sequence (where d < 1 and e + d ≤ 1):

⟨η_{0}, (0, 0)⟩ ⟶^{ϵ(d)} ⟨η_{0}, (d, d)⟩ ⟶^{a} ⟨η_{1}, (0, d)⟩ ⟶^{ϵ(e)} ⟨η_{1}, (e, d + e)⟩ ⟶^{b}

In addition, it is indicated that A can perform a c–transition in the state ⟨η_{1}, (0, d)⟩. □

3 Timed Modal Logic L_{ν}

We consider a dense–time logic L_{ν} with clocks and recursion. This logic may be seen as a certain fragment ^{3} of the μ–calculus T_{μ} presented in [HNSY92].

Definition 2 Let K a finite set of clocks, Id a set of identifiers and k an integer. The set L_{ν} of formulae over K, Id and k is generated by the abstract syntax with φ and ψ ranging over L_{ν}:

\begin{aligned}φ & ::= & tt | ff | φ ∧ ψ | φ ∨ ψ | ∃∃ φ | ∀∀ φ | ⟨a⟩ φ | [a] φ \\ & & | x in φ | x + n ∼ y + m | Z \end{aligned}

where a ∈ A; x, y ∈ K; n, m ∈ {0, 1, …, k}; ∼ ∈ {=, <, ≤, >, ≥} and Z ∈ Id.

The meaning of the identifiers is specified by a declaration D assigning a formula of L_{ν} to each identifier. When D is understood we write Z =^{def} φ for D(Z) = φ. The K clocks are called formula clocks and a formula φ is said to be closed if every formula clock x occurring in φ is in the scope of an “x in …” operator.

Given a timed automata A = ⟨A, N, η_{0}, C, E⟩, we interpret the L_{ν} formulas over an extended state ⟨η, vu⟩_{A^{+}} where ⟨η, v⟩_{A} is a state of A and u a time assignment for K. Transitions between extended states are defined by:

⟨η, vu⟩_{A^{+}} ⟶^{ϵ(d)} ⟨η′, v + d u + d⟩_{A^{+}} and ⟨η, vu⟩_{A^{+}} ⟶^{a} ⟨η′, v′u′⟩_{A^{+}} iff ⟨η, v⟩_{A} ⟶^{a}

⟨η′, v′⟩_{A} and u = u′.

Informally, ∃ ∃φ holds in an extended state if there is a delay transition leading to an extended state satisfying φ. Thus ∃∃ denotes existential quantification over (arbitrary) delay transitions. Similarly, ∀∀ denotes universal quantification over delay transitions, and ⟨a⟩ (resp. [a]) denotes existential (resp. universal) quantification over a–transitions. The formula (x in φ) introduces a formula clock x and initializes it to 0; i.e. an extended state satisfies the formula in case the modified state with x being reset to 0 satisfies φ. Introduced formula clocks are used by formulas of the type (x + n ∼ y + m), which is satisfied by an extended state provided the values of the named formula clocks satisfies the required relationship. Finally, an extended state satisfies an identifier Z if it satisfies the corresponding declaration (or definition) D(Z). Formally, the satisfaction relation between extended states and formulas is defined as follows:

3allowing only maximal recursion and using a slightly different notion of model

Definition 3 Let A be a timed automaton and D a declaration. The satisfaction relation ⊧_{D} is the largest relation satisfying the following implications:

⟨η, v u⟩_{A^{+}} ⊧_{D} tt ⇒ true
⟨η, v u⟩_{A^{+}} ⊧_{D} ff ⇒ false
⟨η, v u⟩_{A^{+}} ⊧_{D} φ ∧ ψ ⇒ ⟨η, v u⟩_{A^{+}} ⊧_{D} φ and ⟨η, v u⟩_{A^{+}} ⊧_{D} ψ
⟨η, v u⟩_{A^{+}} ⊧_{D} φ ∨ ψ ⇒ ⟨η, v u⟩_{A^{+}} ⊧_{D} φ or ⟨η, v u⟩_{A^{+}} ⊧_{D} ψ
⟨η, v u⟩_{A^{+}} ⊧_{D} ∃∃ φ ⇒ ∃d ∈ R. ⟨η, v+d u+d⟩_{A^{+}} ⊧_{D} φ
⟨η, v u⟩_{A^{+}} ⊧_{D} ∀∀ φ ⇒ ∀d ∈ R. ⟨η, v+d u+d⟩_{A^{+}} ⊧_{D} φ
⟨η, v u⟩_{A^{+}} ⊧_{D} ⟨a⟩ φ ⇒ ∃ ⟨η′, v′⟩_{A}. ⟨η, v⟩_{A} ⟶^{a} ⟨η′, v′⟩_{A} and
⟨η′, v′ u⟩_{A^{+}} ⊧_{D} φ
⟨η, v u⟩_{A^{+}} ⊧_{D} [a] φ ⇒ ∀ ⟨η′, v′⟩_{A}. ⟨η, v⟩_{A} ⟶^{a} ⟨η′, v′⟩_{A} implies
⟨η′, v′ u⟩_{A^{+}} ⊧_{D} φ
⟨η, v u⟩_{A^{+}} ⊧_{D} x+m∼y+n ⇒ u(x) + m ∼ u(y) + n
⟨η, v u⟩_{A^{+}} ⊧_{D} x in φ ⇒ ⟨η, v u′⟩_{A^{+}} ⊧_{D} φ where u′ = [{x} → 0]u
⟨η, v u⟩_{A^{+}} ⊧_{D} Z ⇒ ⟨η, v u⟩_{A^{+}} ⊧_{D} D(Z)

Any relation satisfying the above implications is called a satisfiability relation. It follows from standard fixpoint theory [Tar55] that ⊧_{D} is the union of all satisfiability relations and that the above implications in fact are biimplications for ⊧_{D}. We say that A satisfies a closed L_{ν} formula φ and write A ⊧ φ when ⟨η_{0}, v_{0} u⟩_{A^{+}} ⊧_{D} φ for any u. Note that if φ is closed, then ⟨η, vu⟩_{A^{+}} ⊧_{D} φ iff ⟨η, vu′⟩_{A^{+}} ⊧_{D} φ for any u, u′ ∈ R^{K}.

The following real–time interval modalities present in the Extended Timed Modal Logic introduced in [HLY92] are obtainable as derived operators of L_{ν}, e.g.:

∃]0; ∞[ φ =^{def} x in (∃∃ (x > 0 ∧ φ))
∃]m; n[ φ =^{def} x in (∃∃ (x > m ∧ x < n ∧ φ))

Thus, ∃]m; n[φ is satisfied by and extended state if an extended state satisfying φ can be reached with a delay between m and n. A formula is called a q-clocks formula if it contains no more than q formula clocks. Thus formulas using only the derived ∃]m; n[ or ∃]0; ∞[ modalities are clearly 1-clock formulas (as each use of an interval modality can be defined using the same formula clock x).

Example 3 Consider the timed automaton described in Figure 1. It may be argued that the initial state ⟨η_{0}, v_{0} u_{0}⟩ satisfies the following L_{ν} formula φ:

φ = ∃]0; 1[ ⟨a⟩ [(⟨c⟩ tt) ∧ (∀]0; 1[ [c] ff) ∧ (∃]0; 1[ ⟨b⟩ tt) ∧ (∃]0; 1[ [b] ff)] (1)

Intuitively this formula means that “the action a can be performed after a delay (strictly) between 0 and 1, after which (1) the action c can be performed immediately but not after any positive delay, (2) the action b can be performed after some delay in the interval ]0; 1[, and (3) the action b cannot be performed after some delay in ]0; 1[”. □

4 Model Checking

The model-checking problem for L_{ν} consists in deciding if a given timed automata A satisfies a given specification φ in L_{ν}. This problem is decidable using the region technique of Alur and Dill [AD94, ACD90] which provides an abstract semantics of timed automata in the form of finite labelled transition systems with the truth value of L_{ν} formulas being maintained.

The basic idea is that, given a timed automaton A, two states ⟨η, v_{1}⟩_{A} and ⟨η, v_{2}⟩_{A} which are close enough with respect to their clocks values (we will say that v_{1} and v_{2} are in the same region) can perform the same actions, and two extended states ⟨η, v_{1} u_{1}⟩_{A^{+}} and ⟨η, v_{2} u_{2}⟩_{A^{+}} where v_{1} u_{1} and v_{2} u_{2} are in the same region, satisfy the same L_{ν} formulas. The notion of region is defined as an equivalence class of a relation over time assignments [HNSY92] 4 . First, for t ∈ R, let ⌊t⌋ =^{def} max{n ∈ N | n ≤ t} denote the integral part of t, and let {t} =^{def} t − ⌊t⌋ denote its fractional part. Moreover we have:

⌈t⌉ =^{def} min{n ∈ N | t ≤ n}.

Definition 4 Let k ∈ N and let C be a set of clocks. Then u, u′ ∈ R^{C} are equivalent with respect to k, denoted by u =^{.} u′ iff:

i) ∀x ∈ C. u(x) > k iff u′(x) > k
ii) ∀x ∈ C s.t. u(x) ≤ k. ⌊u(x)⌋ = ⌊u′(x)⌋ and {u(x)} = 0 ⇔ {u′(x)} = 0
iii) ∀x, y ∈ C. u(x) − u(y) > k iff u′(x) − u′(y) > k
iv) ∀x, y ∈ C s.t. 0 ≤ u(x) − u(y) ≤ k. ⌊u(x) − u(y)⌋ = ⌊u′(x) − u′(y)⌋
and {u(x) − u(y)} = 0 ⇔ {u′(x) − u′(y)} = 0

The equivalence classes under =^{.} are called regions, and [u] denotes the region which contains the time assignment u. R_{k}^{C} denotes the set of all regions for a set C of clocks and the maximal constant k. From a decision point of view it is important to note that R_{k}^{C} is finite.

Note that for any condition b in B(C) with no constant greater than k, we have b(u) ⇔ b(u′), whenever u and u′ belong to the same region in R_{k}^{C}. Thus for a region γ ∈ R_{k}^{C}, we can define b(γ) as the truth value of b(u) for any u in γ. Conversely given a region γ, we can easily build a formula of B(C), called β(γ), such that β(γ)(u) = tt iff u ∈ γ ^{5}. Thus, given a region γ′, β(γ)(γ′) is mapped to the value tt precisely when γ = γ′. Finally, note that β(γ) itself can be viewed as a L_{ν} formula.

Given a region [u] in R_{k}^{C} and C′ ⊆ C we define the following reset operator: [C′ → 0][u] = [[C′ → 0]u]. Moreover, for a region [u], we define the succssor region (denoted by succ([u])) as the region [u′], where:

u′(x) = \{ \begin{matrix}u(x) + f ∀x ∈ C. u(x) > k ∨ \{u(x)\} ≠ 0 \\ u(x) + f/2 ∃x ∈ C. u(x) ≤ k ∧ \{u(x)\} = 0 \end{matrix}

4The notion of region used in the present paper is slightly more refined.

5An obvious way of building β(γ) is to consider the conjunction of all B(C, k) formulas satisfied by γ, where B(C, k) denotes the finite set (modulo boolean reductions) of B(C)

formulas with no constant greater than k.

succ(γ_{0}) = γ_{6}
…

succ(γ_{5}) = γ_{13}

0 < x < 1∧

0 < y < 1∧ β(γ_{6}) =

y = x

β(γ_{0}) = (x = 0 ∧ y = 0)
β(γ_{8}) = (0 < x < 1 ∧ y = 1)

β(γ_{7}) =

0 < x < 1∧ 0 < y < 1∧

y > x 0

6 (1)

(1)

14

1

4 12 3

5 7 8

13 9 10 11 24 y

x

2

Figure 2: R_{k}^{C} with C = {x, y} and k = 1

where f = min{1 − {u(x)} | u(x) ≤ k} ^{6}. Informally the change from γ to succ(γ) correspond to the minimal elapse of time which can modify the enabled actions of the current state.

We denote by γ^{l} the l^{th} successor region of γ (i.e. γ^{l} = succ^{l}(γ)). From each region γ, it is possible to reach a region γ′ s.t. succ(γ′) = γ′, and we denote by l_{γ} the required number of step s.t. γ^{l_{γ}} = succ(γ^{l_{γ}}).

Example 4 The Figure 2 gives an overview of the set of regions defined by two clocks x and y, and the maximal constant 1. In this case there are 31 different regions, of which only 14 are numbered in the figure. Corresponding B(C)–formulas as well as successor regions are indicated for some of the regions. In general successor regions are determined by following 45^{o} lines upwards to the right. □

Given a timed automata A = ⟨A, N, η_{0}, C, E⟩, let k_{A} be the maximal constant occurring in the enabling condition of the edges E. Then for any k ≥ k_{A} we can define a symbolic semantics of A over symbolic states [η, γ]_{A} where η ∈ S and γ ∈ R_{k}^{C} as follows:

[η, γ]_{A} ⟶^{a} [η′, γ′]_{A}  iff ∃ u ∈ γ, ⟨η, u⟩_{A} ⟶^{a} ⟨η′, u′⟩_{A} and u′ ∈ γ′
[η, γ]_{A} ⟶^{χ} [η, succ(γ)]_{A} iff true

Consider now L_{ν} with respect to formula clock set K and maximal constant k_{L}. Also consider a given timed automata A = ⟨A, N, η_{0}, C, E⟩ (s.t. K and C are disjoint). Then an extended symbolic state is a pair [η, γ]_{A^{+}} where η ∈ N and γ ∈ R_{k}^{C^{+}} with C^{+} = C ∪ K and k = max(k_{A}, k_{L}). Whenever γ is a region over C ∪ K we denote by γ_{|C} the set of time assignments in γ restricted to the (automata) clock set C. Similarly, γ_{|K} denotes the projection of all time assignments in γ to the (formula) clock set K. Now we define a symbolic semantics for L_{ν} as follows:

6if this set is empty, then f = 0

Definition 5 ⊢_{D} is the largest relation satisfying the following implications:

i) [η, γ]_{A^{+}} ⊢_{D} tt ⇒ true
ii) [η, γ]_{A^{+}} ⊢_{D} ff ⇒ false
iii) [η, γ]_{A^{+}} ⊢_{D} φ ∧ ψ ⇒ [η, γ]_{A^{+}} ⊢_{D} φ and [η, γ]_{A^{+}} ⊢_{D} ψ
iv) [η, γ]_{A^{+}} ⊢_{D} φ ∨ ψ ⇒ [η, γ]_{A^{+}} ⊢_{D} φ or [η, γ]_{A^{+}} ⊢_{D} ψ
v) [η, γ]_{A^{+}} ⊢_{D} ∃∃ φ ⇒ ∃l ∈ N. [η, succ^{l}(γ)]_{A^{+}} ⊢_{D} φ
vi) [η, γ]_{A^{+}} ⊢_{D} ∀∀ φ ⇒ ∀l ∈ N. [η, succ^{l}(γ)]_{A^{+}} ⊢_{D} φ
vii) [η, γ]_{A^{+}} ⊢_{D} ⟨a⟩ φ ⇒ ∃ [η′, γ′]_{A^{+}}. [η, γ_{|C}]_{A} ⟶^{a} [η′, γ′_{|C}]_{A} and

γ′_{|K} = γ_{|K} and [η′, γ′]_{A^{+}} ⊢_{D} φ

viii) [η, γ]_{A^{+}} ⊢_{D} [a] φ ⇒ ∀ [η′, γ′]_{A^{+}}. [η, γ_{|C}]_{A} ⟶^{a} [η′, γ′_{|C}]_{A} and

γ′_{|K} = γ_{|K} implies [η′, γ′]_{A^{+}} ⊢_{D} φ

ix) [η, γ]_{A^{+}} ⊢_{D} x+c∼y+d ⇒ (x + c ∼ y + d)(γ)
x) [η, γ]_{A^{+}} ⊢_{D} x in φ ⇒ [η, [{x} → 0]γ]_{A^{+}} ⊢_{D} φ
xi) [η, γ]_{A^{+}} ⊢_{D} Z ⇒ [η, γ]_{A^{+}} ⊢_{D} D(Z)

Any relation satisfying the above implications is called a symbolic satisfiability relation. In the following we write [η, γ] instead of [η, γ]_{A^{+}} when no confusion is possible. The above symbolic interpretation of L_{ν} is closely related to the standard interpretation from Definition 3 as stated in the following theorem:

Theorem 1 Let φ be a formula of L_{ν}, and let ⟨η, v u⟩_{A^{+}} be an extended state over some timed automaton A . Then we have ^{7}:

⟨η, v u⟩_{A^{+}} ⊧_{D} φ if and only if [η, [v · u]]_{A^{+}} ⊢_{D} φ

It follows that the model checking problem for L_{ν} is decidable since, given φ ∈ L_{ν}, it suffices to to check the truth value of any given L_{ν} formula φ with respect to the finite transition system ⟨N ×R_{k}^{C^{+}}, A∪{χ}, σ_{0}, →⟩ corresponding to the extended symbolic semantics of A.

5 Characteristic Properties

First let us recall the characteristic formula construction for finite automata ^{8} [IS94, GS86, BCG88] (see Figure 3). The construction defines the characteristic formula Φ(A) of a node A in terms of similar characteristic formulas of the derivates A_{1} … A_{n} of A: whenever A has an a_{i}–transition to A_{i} this is reflected in Φ(A) by addition of a conjunct ⟨a_{i}⟩Φ(A_{i}). To characterize A up to strong bisimilarity Φ(A) contains in addition a conjunct [a]Ψ_{a} for each action a, where Ψ_{a} is a disjunction over all a–transitions out of A. In general the definitions of characteristic formulas Φ(A) constitutes a simultaneous recursive definition (as the automaton may have cycles), and to obtain the desired characterization the solution sought is the maximum one.

For timed automata the characteristic formula construction must necessarily take account of the time assignment in addition to the actual node. Thus, for a

7where v · u is the time assignment over C ∪ K such that (v · u)(x) = v(x) if x ∈ C and (v · u)(x) = u(x) if x ∈ K.

8Alternatively you may think of finite automata as zero–clock timed automata.

A_{1} A_{n}

A

a_{1} a_{n} Φ(A) = ⋀_{i=1}^{n}⟨a_{i}⟩ Φ(A_{i}) ∧ ⋀_{a}[a] ( ⋁_{i.a_{i}=a} Φ(A_{i}))

Figure 3: Characteristic formula for finite automata.

timed automaton A = ⟨A, N, η_{0}, C, E⟩, we shall define characteristic formulas of the form Φ(η, γ), where η is a node of A and γ is a region over the clocks of A. The construction of Φ(η, γ) follows closely the pattern from the finite automa case. However, we first need to be able to determine the (a–) edges out of η which are enabled in the region γ. Given an edge e = ⟨η, η′, a, r, b⟩ in E, η_{e} (resp. η′_{e}, a_{e}, r_{e}, b_{e}) denotes η (resp. η′, a, r, b). Given η ∈ N and γ ∈ R_{k_{A}}^{C}, we define E(η, γ) = {e | η_{e} = η and b_{e}(γ) = tt} and E(η, γ, a) = {e ∈ E(η, γ) | a_{e} = a}. Thus, E(η, γ) (resp. E(η, γ, a)) is the set of all enabled transitions (resp. atransitions) from [η, γ]_{A}.

We may now present the characteristic formula construction for timed automata:

Definition 6 Let A be a timed automata ⟨A, N, η_{0}, C, E⟩. For any region γ in R_{k_{A}}^{C}, and node η in N, we introduce an identifier Φ(η, γ) (the characteristic formula) associated with the symbolic state [η, γ]_{A}. The definition (declaration) for Φ(η, γ) is:

Φ(η, γ) =^{def} ( \begin{matrix}⋀_{e∈E(η,γ)} ⟨a_{e}⟩ (r_{e} in Φ(η′_{e}, r_{e}(γ))) ∧ ⋀_{a}[a] ( ⋁_{e∈E(η,γ,a)} (r_{e} in Φ(η′_{e}, r_{e}(γ)))) \\ ∧ ∀∀( ⋀_{l=0..l_{γ}}β(γ^{l}) ⇒ Φ(η, γ^{l})) \end{matrix} )

We denote by Id_{A} the set of identifiers Φ(η, γ) and by D_{A} the corresponding declaration.

Note that the declaration for Φ(η, γ) is not quite a L_{ν} formula due to the presence of implication. However, it is easy to transform it into an equivalent L_{ν} formula because the negation of β(γ) can be expressed in L_{ν}. Moreover (r in φ) is an abbreviation for (c_{1}in(c_{2}in … (c_{n}inφ))) whenever r is {c_{1}, …, c_{n}}. Finally r(γ) denotes [r → 0]γ. Note that D_{A} uses no more than |C| formula clocks.

The declaration for Φ(η, γ) contains three groups of conjunctions the two first of which are closely related to the characteristic formula construction for finite automata. The first group contains a ⟨a_{e}⟩–formula for any edge e, which is enabled at η in the region γ. Following this edge clearly takes the automaton to the extended state [η′_{e}, r_{e}(γ)]. The second group of conjuncts contains for each action a a formula of the type [a]Ψ_{a}, where Ψ is a disjunction over all a– labelled edges being enabled at η in the region γ. Whereas the two first groups exhaustively characterizes the action behaviour of the extended state [η, γ], the third conjunct is a ∀∀–formula dealing with all delay transitions by requiring that any delay leading to a particular successor region γ^{l} should satisfy the corresponding characteristic formula.

Example 5 Reconsider the timed automata A described in Example 1 and the corresponding regions from Example 4. Below we give the declaration of some of the characteristic formulas. We define φ_{nil} =^{def} ⋀_{a}[a] ff ^{9} and we denote β(γ_{i}) by β_{i}. We have:

Φ(η_{0}, γ_{0}) =^{def} φ_{nil} ∧ ∀∀[(β_{0} ⇒ Φ(η_{0}, γ_{0})) ∧ (β_{6} ⇒ Φ(η_{0}, γ_{6})) ∧ (β_{14} ⇒ Φ(η_{0}, γ_{14}))
∧(β_{24} ⇒ Φ(η_{0}, γ_{24}))]
Φ(η_{0}, γ_{6}) =^{def} ⟨a⟩ Φ(η_{1}, γ_{4}) ∧ [a] Φ(η_{1}, γ_{4}) ∧ [b] ff ∧ [c] ff

∧∀∀[(β_{6} ⇒ Φ(η_{0}, γ_{6})) ∧ (β_{14} ⇒ Φ(η_{0}, γ_{14})) ∧ (β_{24} ⇒ Φ(η_{0}, γ_{24}))]

Φ(η_{1}, γ_{4}) =^{def} ⟨b⟩ Φ(η_{2}, γ_{4}) ∧ ⟨c⟩ Φ(η_{3}, γ_{4}) ∧ [b] Φ(η_{2}, γ_{4}) ∧ [c] Φ(η_{3}, γ_{4}) ∧ [a] ff
∧∀∀[(β_{4} ⇒ Φ(η_{1}, γ_{4})) ∧ (β_{5} ⇒ Φ(η_{1}, γ_{5})) ∧ (β_{13} ⇒ Φ(η_{1}, γ_{13}))
∧(β_{21} ∨ β_{22} ∨ β_{23}) ⇒ φ_{nil}]
Φ(η_{1}, γ_{5}) =^{def} ⟨b⟩ Φ(η_{2}, γ_{4}) ∧ [b] Φ(η_{2}, γ_{4}) ∧ [c] ff ∧ [a] ff
∧∀∀[(β_{5} ⇒ Φ(η_{1}, γ_{5})) ∧ (β_{13} ⇒ Φ(η_{1}, γ_{13}))
∧(β_{21} ∨ β_{22} ∨ β_{23}) ⇒ φ_{nil}]
Φ(η_{2}, γ) =^{def} ∀∀φ_{nil}
Φ(η_{3}, γ) =^{def} ∀∀φ_{nil}
□

We have the following Main Theorem the proof of which is given in Appendix A.

Theorem 2 Let A = ⟨A, N, η_{0}, C, E⟩ and B = ⟨A, M, ρ_{0}, K, F ⟩ be two timed automata. Then for any ρ ∈ M, η ∈ N, v ∈ R^{K} and u ∈ R^{C}:

⟨ρ, v⟩_{B} ∼ ⟨η, u⟩_{A} iff ⟨ρ, v u⟩_{B^{+}} ⊧_{D_{A}} Φ(η, [u])

where D_{A} corresponds to the previous definition of Φ(η, γ) for each η ∈ N and γ ∈ R_{k_{A}}^{C}.

As model–checking of L_{ν} is decidable we may use the above characteristic formula construction to decide timed bisimilarity between timed automata: to decide if two timed automata are timed bisimilar simply compare the one automaton to the characteristic formula of the other.

Corollary 1 Timed bisimilarity between timed automata is decidable.

9a state satisfies φ_{nil} whenever no action can be performed.

6 Model Construction

In this section we address the satisfiability problem for L_{ν}. That is we want to decide whether there exists a timed automaton A satisfying a given L_{ν}–formula φ. The hardness of this problem is illustrated by the following Proposition:

Proposition 1 Let Ψ_{l} be the 1-clock formula defined as follows:

Ψ_{l} =^{def} (\underbrace{∃]0; ∞[ ⟨a⟩ ⋯ ∃]0; ∞[ ⟨a⟩}_{l})[ ⋀_{i=1..l} ∃]0; 1[ (⟨a_{i}⟩ tt ∧ ⋀_{j≠i}[a_{j}] ff)]

where l ∈ N. Then Ψ_{l} is satisfiable by some p-clock automata if and only if l ≤ 2p + 1.

As a consequence of this Proposition ^{10} we cannot deduce the number of clocks in the automata from the number of clocks in φ. In fact, similar to the results for TCTL and T_{μ}, we conjecture that the satisfiability problem for L_{ν} is undecidable ^{11}.

Instead, we address the following more restricted bounded satisfiability problem in which bounds have been placed on both the number of automaton clocks as well as the size of the constants these clocks are compared to: given a formula φ (over a declaration D), a set of clocks C and an integer M, we want to decide (and synthesize) whether there exists a (C, M)–automata ^{12} s.t. A ⊧_{D} φ. We have the following main result:

Theorem 3 The bounded satisfiability problem for L_{ν} is decidable.

The remainder of this section is devoted to the proof of this theorem and to an example of bounded satisfiability checking. The decision procedure is closely related to the canonical model construction for modal logic [HC68].

Let φ be a given L_{ν} formula with k_{φ} as maximal constant. Let K be the set of formula clocks occurring in φ. Given C a set of clocks (with C ∩ K = ∅) and M an integer, we want to decide if there exists a (C, M)–automaton satisfying φ.

Let C^{+} = C ∪ K. Let L_{ν}^{φ} be the set of all subformulae of φ ^{13}. Obviously L_{ν}^{φ} is finite.

A problem Π is a subset of R_{k}^{C^{+}}×L_{ν}^{φ} where k = max(M, k_{φ}). A problem Π is said to be satisfiable^{14} if there exists a (C, M)-automaton A and a node η of A such that for any (γ, ψ) ∈ Π we have [η, γ]_{A^{+}} ⊧_{D} ψ. We call A a solution to Π.

10the proof is given in appendix B

11due to the lack of a minimal fixed–point construct in L_{ν} and hence the lack of ability to express liveness properties we are unable to adopt the undecidability proofs for TCTL and T_{μ}.

12i.e. a |C|-clock automata A with maximum constant M.

13including φ and with D(Z) being a subformula of Z.

14or more precisely (C, M)–satisfiable.

A problem Π is said to be maximal if it satisfies the following closure conditions:

(γ, ψ) ∈ Π  ⇒ (γ, tt) ∈ Π
(γ, ψ_{1} ∧ ψ_{2}) ∈ Π ⇒ (γ, ψ_{1}) ∈ Π and (γ, ψ_{2}) ∈ Π
(γ, ψ_{1} ∨ ψ_{2}) ∈ Π ⇒ (γ, ψ_{1}) ∈ Π or (γ, ψ_{2}) ∈ Π
(γ, ∃∃ψ) ∈ Π  ⇒ ∃l. (γ^{l}, ψ) ∈ Π
(γ, ∀∀ψ) ∈ Π  ⇒ ∀l. (γ^{l}, ψ) ∈ Π
(γ, x in ψ) ∈ Π  ⇒ ([{x} → 0]γ, ψ) ∈ Π
(γ, Z) ∈ Π  ⇒ (γ, D(Z)) ∈ Π

We have the two following lemmas, the proofs of which are trivial:

Lemma 1 If Π ⊆ Π′ and Π′ is satisfiable then also Π is satisfiable.

Lemma 2 If Π is satisfiable then there exists a maximal problem Π′ containing Π and being satisfiable.

Thus it suffices to consider satisfiability of maximal problems. Given a problem Π, a region γ and an action a we define the problem Π_{a}^{γ,r} as the set {(r(γ), ψ) | (γ, [a] ψ) ∈ Π}. Now we introduce a new notion about problems. Let C be a set of maximal problems. Then C is a consistency relation if whenever Π ∈ C then:

1− If (γ, x + m ∼ y + n) ∈ Π then γ(x) + m ∼ γ(y) + n
2− For all γ, (γ, ff) ∉ Π
3− Whenever (γ, ⟨a⟩ ψ) ∈ Π , there exists some r ⊆ C, b ∈ B_{M}(C) with
b(γ) = tt and Π′ ∈ C s.t. :
i) (r(γ), ψ) ∪ Π_{a}^{γ,r} ⊆ Π′
ii) ∀γ′, b(γ′) = tt ⇒ Π_{a}^{γ′,r} ⊆ Π′

We say that a maximal problem is consistent if it belongs to some consistency relation. We have the following key lemma:

Lemma 3 Let Π be a maximal problem. Then Π is consistent if and only if Π is satisfiable.

Proof ⇐ It’s easy to show that C = {Π | Π maximal and satisfiable} is a consistency relation. ⇒ Let C be a consistency relation (containing Π). Now construct the canonical automaton A_{C} = ⟨A, N, η_{0}, C, E⟩ s.t. :

• N = {η_{Π} | Π ∈ C}

• η_{0} is some η_{Π} ∈ N.

• ⟨η_{Π}, η_{Π′}, a, r, b⟩ ∈ E iff whenever (γ, [a]ψ) ∈ Π and b(γ) = tt then (r(γ), ψ) ∈ Π′.

Now it can be shown that A_{C} solves all problems of C. In particular whenever (γ, ψ) ∈ Π for some Π ∈ C, then [η_{Π}, γ]_{A_{C}^{+}} ⊧_{D} ψ. To prove this we show that the relation ⊩ defined by: [η_{Π}, γ] ⊩ ψ iff (γ, ψ) ∈ Π with Π ∈ C is a symbolic satisfiability relation. That is, we must show that ⊩ satisfies the eleven implications of definition 5:

• The implications i), iii) − vi), x) and xi) follow from maximality of any Π in C.

• The implications ii) and ix) follow directly from consistency of C.

• The implications vii) and viii) follow from the construction of E which

is always possible thanks to the consistency of C.

□

Finally we have:

Lemma 4 It is decidable whether a maximal problem is consistent.

Proof Let S_{Π_{m}} be the set of maximal problems over R_{k}^{C^{+}}×L_{ν}^{φ}. Clearly S_{Π_{m}} is finite (since L_{ν}^{φ} and R_{k}^{C^{+}} are too). Thus the set of relations C over maximal problems is finite. Now given a relation C it is easy to check whether C is consistent since the choices for possible reset set r over C and the set B_{M}(C)^{15} are both finite. □

Thus given a formula φ and bounds C and M, we can consider the (finitely many) maximal problems Π over C and M containing (γ_{0}, φ). It follows that φ is (C, M)–satisfiable precisely if one of these maximal problems is consistent, which is decidable due to Lemma 4. Note that the proof of Theorem 2 is constructive: given a consistency relation it gives a (C, M)-timed automata satisfying φ.

Example 6 Consider the formula φ in Example 3:

φ = ∃]0; 1[ ⟨a⟩ [(⟨c⟩ tt) ∧ (∀]0; 1[ [c] ff) ∧ (∃]0; 1[ ⟨b⟩ tt) ∧ (∃]0; 1[ [b] ff)]

We can use the model construction algorithm presented above to show that no (1, 1)-automata satisfies φ. Since φ is a one-formula clock and |C| = 1, we have C^{+} = {x, y} where x denotes the automata clock and y the formula clock. Let ψ be the formula s.t. φ = ∃]0; 1[ ⟨a⟩ ψ.

Consider the problem Π = {(γ_{0}, ∃]0; 1[⟨a⟩ψ)}, where γ_{0} refers to the regions of Example 4. The maximal problem including Π is Π_{0} = {(γ_{0}, ∃]0,; 1[⟨a⟩ψ), (γ_{6}, ⟨a⟩ ψ), (γ_{0}, tt), (γ_{6}, tt)}. If Π_{0} is consistent, there exists a relation C containing a maximal problem Π_{1} s.t. for some r_{1} ∈ {{x}, ∅} and b_{1} ∈ B_{1}({x}) with b_{1}(γ_{6}) = tt we have: (r_{1}(γ_{6}), ψ) ∈ Π_{1}. We distinguish two cases depending on r_{1}:

• r_{1} = ∅ : Π_{1} contains (γ_{6}, ψ). Since it’s maximal, it also contains (γ_{6}, ⟨c⟩tt) and (γ_{6}, ∀]0; 1[[c]ff. Then {(γ_{6}, [c]ff), (γ_{14}, [c]ff), (γ_{24}, [c]ff)} ⊂ Π_{1}. Thus Π_{1} is not consistent since (γ_{6}, ⟨c⟩ tt) and (γ_{6}, [c] ff) require the existence of a maximal problem containing (γ_{6}, ff) or (γ_{1}, ff). Thus C is not a consistency relation.

15modulo boolean reduction

• r_{1} = {x} : Π_{1} contains (γ_{1}, ψ), (γ_{1}, ⟨c⟩tt), (γ_{1}, ∀]0; 1[[c]ff), (γ_{1}, ∃]0; 1[⟨b⟩tt) and (γ_{1}, ∃]0; 1[ [b] ff). In fact there are several possibilities for Π_{1} depending on which term among (γ_{7}, ⟨b⟩ tt), (γ_{8}, ⟨b⟩ tt), γ_{9}, ⟨b⟩ tt) and which term among (γ_{7}, [b] ff), (γ_{8}, [b] ff), γ_{9}, [b] ff) are contained in Π_{1} due to its maximality. In any case there are some (γ, ⟨b⟩ tt) and (γ′, [b] ff) in Π_{1} with γ, γ′ ∈ {γ_{7}, γ_{8}, γ_{9}}. Then there exists a maximal problem Π_{2} s.t. for some r_{2} ∈ {{x}, ∅} and b_{2} ∈ B_{1}({x}) with b_{2}(γ) = tt and (r_{2}(γ), tt) ∈ Π_{2}. But for any condition b ∈ B_{1}({x}) we have: b(γ_{7}) = b(γ_{8}) = b(γ_{9}), and thus (γ′, [b]ff) ∈ Π_{1} requires that (r_{2}(γ′), ff) is in Π_{2}. Thus C is not a consistency relation.

Thus no (1, 1)-automata satisfies φ. □

Thus the formula in the above example is satisfiable by a 2–clock automaton but by no (1, 1)–automata. Using the easily established fact that timed bisimilar automata satisfy the same L_{ν}–formulas it follows that the automaton of Example 3 is inequivalent to all (1, 1)–automata with respect to timed bisimilarity. Now combining the above bounded model–construction algorithm with the characteristic property construction of the previous section we obtain an algorithm for deciding whether a timed automaton can be simplified in either its number clocks or the size of the constants these clocks are compared to. Using this combined method it can (constructively) be seen that the 2–clock automaton obtained by changing the c–edge enabling condition in Example 1 from x = 0 to x > 0 may endeed be simplified to an equivalent (1, 1)–automaton.

Corollary 2 Given a timed automaton A, a clock set C and a natural number M, it is decidable whether there exists a (C, M)–automaton being timed bisimilar to A.

Conclusion

This paper has presented two main contributions: (1) a characteristic formula construction which for any given timed automaton give a logical formula uniquely characterizing it; and (2) a model construction algorithm, which given a logical formula will (if possible) synthesize a satisfying timed automaton within given bounds on the number of clocks and constants used.

The results presented may be pursued and improved in a number of directions: The notion of a characteristic formula construction may be applied to other behavioural preorders in order to obtain corresponding preorder checking algorithms. We have already shown that characteristic formula constructs also exists for the “faster–than”–relation in [FT91] and the time–abstracted equivalence in [LW93].

The results of this paper only solve (positively) the decidability of a bounded satisfiability problem for L_{ν}. However, it follows from this result that the unconstrainted satisfiability problem is at least r.e. though we conjecture that this problem is in fact undecidable. Decidability of the satisfiability problem with only bounds on the number of clocks is also left as an open (and interesting) problem.

Finally, future work includes study of the decidability of the satisfiability problems for L_{ν} extended with a minimal fixedpoint construction.

References

[AC88] A. Arnold and P. Crubille. A linear algorithm to solve fixed–point equations on transition systems. Information Processing Letters, 29, 1988.

[ACD90] R. Alur, C. Courcoubetis, and D. Dill. Model–checking for Real–Time Systems. In Proceedings of Logic in Computer Science, pages 414–425. IEEE Computer Society Press, 1990.

[AD94] R. Alur and D. Dill. Automata for Modelling Real–Time Systems. Theoretical Computer Science, 126(2):183–236, April 1994.

[Alu91] R. Alur. Techniques for Automatic Verification of Real-time Systems. PhD thesis, Stanford University, 1991.

[And92] H.R. Andersen. Model checking and boolean graphs. In Proceedings of ESOP’92, volume 582 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1992. Springer.

[BCG88] M. C. Browne, E. M. Clarke, and O. Grümberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115–131, 1988.

[CE81] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using Branching Time Temporal Logic. In Proc. Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71, Berlin, 1981. Springer Verlag.

[Cer92] Karlis Cerans. Decidability of bisimulation equivalences for parallel timer processes. In Proc. of CAV’92, volume 663 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1992. Springer Verlag.

[CES86] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent system using temporal logic. ACM Trans. on Programming Languages and Systems, 8(2):244–263, 1986.

[CS91] R. Cleaveland and B. Steffen. Computing behavioural relations, logically. In Proceedings of 18th International Colloquium on Automata, Languages and Programming, volume 510 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1991. Springer.

[EC82] E. A. Emerson and E. M. Clarke. Using Branching Time Temporal Logic to synthesize synchronization skeletons. Sci. Comput. Programming, 2:241– 266, 1982.

[EH85] E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the Temporal Logic of Branching Time. J. Comput. System Sci., 30(1):1–24, 1985.

[EL86] E.A. Emerson and C.L Lei. Efficient model checking in fragments of the propositional mu–calculus. In Proceedings of Logic in Computer Science, pages 267–278. IEEE Computer Society Press, 1986.

[FT91] F.Moller and C. Tofts. Relating Processes with Respect to Speed. Technical Report ECS–LFCS–91–143, Department of Computer Science, University of Edinburgh, 1991.

[GS86] S. Graf and J. Sifakis. A Modal Characterization of Observational Congruence on Finite Terms of CCS. Information and Control, 68:125–145, 1986.

[HC68] G.E. Hughes and M.J. Cresswell. An Introduction to Modal Logic. Methuen and Co., 1968.

[HLY92] U. Holmer, K.G. Larsen, and W. Yi. Decidability of bisimulation equivalence between regular timed processes. In Proceedings of CAV’91, volume 575 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1992.

[HNSY92] T. A. Henzinger, Z. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Logic in Computer Science, 1992.

[IS94] A. Ingolfsdottir and B. Steffen. Characteristic formulae. Information and Computation, 110(1), 1994. To appear.

[Koz82] D. Kozen. Results on the propositional mu–calculus. In Proc. of International Colloquium on Algorithms, Languages and Programming 1982, volume 140 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1982.

[KP83] D. Kozen and R. Parikh. A decision procedure for the propositional mu– calculus. Lecture Notes in Computer Science, 1983.

[LW93] K.G. Larsen and Y. Wang. Time Abstracted Bisimulation: Implicit Specifications and Decidability. In Proceedings of MFPS’93, 1993.

[Mil89] R. Milner. Communication and Concurrency. prentice, Englewood Cliffs, 1989.

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

[QS82] J. P. Queille and J. Sifakis. Specification and verification of concurrent programs in CESAR. In Proc. 5th Internat. Symp. on Programming, volume 137 of Lecture Notes in Computer Science, pages 195–220, Berlin, 1982. Springer Verlag.

[Tar55] A. Tarski. A lattice–theoretical fixpoint theorem and its applications. Pacific Journal of Math., 5, 1955.

[Wol85] P. Wolper. The tableau method for Temporal Logic: an overview. Logique et Anal., 28:119–136, 1985.

[Xin92] Liu Xinxin. Specification and Decomposition in Concurrency. PhD thesis, Aalborg University, 1992. R 92–2005.

A Proof of Theorem 2

Proof ⇐ We are going to show that B = {(⟨ρ, v⟩_{B}, ⟨η, u⟩_{A}) | ⟨ρ, v u⟩ ⊧_{B,D} Φ(η, [u])} is a timed strong bisimulation.

• Assume ⟨η, u⟩_{A} ⟶^{a} ⟨η′, r(u)⟩_{A}. But as ⟨ρ, v u⟩_{B^{+}} ⊧ Φ(η, [u]) we have

⟨ρ, v u⟩_{B^{+}} ⊧ ⟨a⟩ (r in Φ(η′, r([u]))). Thus ⟨ρ, v u⟩_{B^{+}} ⟶^{a} ⟨ρ′, v′ u⟩_{B^{+}} s.t.

⟨ρ′, v′ r(u)⟩_{B^{+}} ⊧ Φ(η′, r([u])). Then ⟨ρ, v⟩_{B} ⟶^{a} ⟨ρ′, v′⟩_{B} and by i.h.

(⟨ρ′, v′⟩_{B}, ⟨η′, r(u)⟩_{A}) ∈ B.

• Assume ⟨ρ, v⟩_{B} ⟶^{a} ⟨ρ′, v′⟩_{B}. Then ⟨ρ, v u⟩_{B^{+}} ⟶^{a} ⟨ρ′, v′ u⟩_{B^{+}}. And as

⟨ρ, v u⟩_{B^{+}} ⊧ Φ(η, [u]) we have ⟨ρ′, v′ u⟩_{B^{+}} ⊧ r_{e} in Φ(η′_{e}, r_{e}(r[u])) for some e ∈ E(η, [u], a). Then ⟨ρ′, v′ r_{e}(u)⟩_{B^{+}} ⊧ Φ(η′_{e}, [r_{e}(u)]). Thus we have (⟨ρ′, v′⟩_{B}, ⟨η′_{e}, r_{e}(u)⟩_{A}) ∈ B.

• Finally to complete the proof we must show that for all d ∈ R, we have: (⟨ρ, v + d⟩_{B}, ⟨η, u + d⟩_{A}) ∈ B. There exists k s.t. [u + d] = [u]^{k}. As ⟨ρ, v u⟩_{B^{+}} ⊧ Φ(η, [u]) it follows that ⟨ρ, v + d u + d⟩_{B^{+}} ⊧ β([u]^{k}) ⇒ Φ(η, [u]^{k}). Clearly it implies ⟨ρ, v +du+d⟩_{B^{+}} ⊧ Φ(η, [u]^{k}) or ⟨ρ, v +du+ d⟩_{B^{+}} ⊧ Φ(η, [u + d]). Thus (⟨ρ, v + d⟩_{B}, ⟨η, u + d⟩_{A}) ∈ B.

⇒ Let D the declaration associating each [η, γ] with Φ(η, γ). We define ⊳_{D} by structural induction as follows:

⟨ρ, v u⟩_{B^{+}} ⊳_{D} tt  ⇔ true
⟨ρ, v u⟩_{B^{+}} ⊳_{D} ff  ⇔ false
⟨ρ, v u⟩_{B^{+}} ⊳_{D} φ ∧ ψ  ⇔ ⟨ρ, v u⟩_{B^{+}} ⊳_{D} φ and ⟨ρ, v u⟩_{B^{+}} ⊳_{D} ψ
⟨ρ, v u⟩_{B^{+}} ⊳_{D} φ ∨ ψ  ⇔ ⟨ρ, v u⟩_{B^{+}} ⊳_{D} φ or ⟨ρ, v u⟩_{B^{+}} ⊳_{D} ψ
⟨ρ, v u⟩_{B^{+}} ⊳_{D} ∃∃ φ  ⇔ ∃d ∈ R. ⟨ρ, v+d u+d⟩_{B^{+}} ⊳_{D} φ
⟨ρ, v u⟩_{B^{+}} ⊳_{D} ∀∀ φ  ⇔ ∀d ∈ R. ⟨ρ, v+d u+d⟩_{B^{+}} ⊳_{D} φ
⟨ρ, v u⟩_{B^{+}} ⊳_{D} ⟨a⟩ φ  ⇔ ∃ ⟨ρ′, v′⟩_{B}. ⟨ρ, v⟩_{B} ⟶^{a} ⟨ρ′, v′⟩_{B} and
⟨ρ′, v′ u⟩_{B^{+}} ⊳_{D} φ
⟨ρ, v u⟩_{B^{+}} ⊳_{D} [a] φ  ⇔ ∀ ⟨ρ′, v′⟩_{B}. ⟨ρ, v⟩_{B} ⟶^{a} ⟨ρ′, v′⟩_{B} implies
⟨ρ′, v′ u⟩_{B^{+}} ⊳_{D} φ
⟨ρ, v u⟩_{B^{+}} ⊳_{D} x+m∼y+n ⇔ u(x) + m ∼ u(y) + n
⟨ρ, v u⟩_{B^{+}} ⊳_{D} x in φ  ⇔ ⟨ρ, v u′⟩_{B^{+}} ⊳_{D} φ and u′ = [{x} → 0]u
⟨ρ, v u⟩_{B^{+}} ⊳_{D} Φ(η, [u])  ⇔ ⟨ρ, v⟩_{B} ∼ ⟨η, u⟩_{A}

We are going to prove that ⊳_{D} is a satisfiabilty relation. To show this it is sufficient to demonstrate that ⟨ρ, v u⟩_{B^{+}} ⊳_{D} Φ(η, [u]) implies ⟨ρ, v u⟩_{B^{+}} ⊳_{D} D(Φ(η, [u])):

• Consider ⟨η, u⟩_{A} ⟶^{a_{e}} ⟨η′_{e}, r_{e}(u)⟩_{A}. Since ⟨ρ, v u⟩_{B^{+}} ⊳_{D} Φ(η, [u]), we have

⟨η, u⟩_{A} ∼ ⟨ρ, v⟩_{B}. Then there exists ⟨ρ, v⟩_{B} ⟶^{a_{e}} ⟨ρ′, v′⟩_{B} s.t. ⟨η′_{e}, r_{e}(u)⟩_{A} ∼

⟨ρ′, v′⟩_{B}. Thus by def. of ⊳_{D} we have ⟨ρ′, v′ r_{e}(u)⟩_{B^{+}} ⊳_{D} Φ(η′_{e}, [r_{e}(u)]). Finally we have ⟨ρ, vu⟩_{B^{+}} ⊳_{D} ⟨a_{e}⟩(r_{e}inΦ(η′_{e}, r([u]))) for any e ∈ E(η, [u]).

• Consider ⟨ρ, v⟩_{B} ⟶^{a} ⟨ρ′, v′⟩_{B}. Since ⟨η, u⟩_{A} ∼ ⟨ρ, v⟩_{B}, there exists ⟨η, u⟩_{A}

⟶^{a} ⟨η′_{e}, r_{e}(u)⟩_{A} s.t. ⟨η′_{e}, r_{e}(u)⟩_{A} ∼ ⟨ρ′, v′⟩_{B}. Thus ⟨ρ′, v′ r_{e}(u)⟩_{B^{+}} ⊳_{D}

Φ(η′_{e}, [r_{e}(u)]), and we have ⟨ρ′, v′ u⟩_{B^{+}} ⊳_{D} r_{e} in Φ(η′_{e}, r([u])) for some e ∈ E(η, [u], a).

• Consider ⟨ρ, v⟩_{B} ⟶^{ϵ(d)} ⟨ρ, v + d⟩_{B}. Then we know ⟨η, u + d⟩_{A} ∼ ⟨ρ, v + d⟩_{B}

and thus ⟨ρ, v + d u + d⟩_{B^{+}} ⊳_{D} Φ(η, [u + d]). Let l ∈ N s.t. [u]^{l} = [u + d], We have ⟨ρ, v + d u + d⟩_{B^{+}} ⊳_{D} β([u]^{l}) ⇒ Φ(η, [u]^{l}).

Then we have ⟨ρ, vu⟩_{B^{+}} ⊳_{D} Φ(η, [u]) ⇒ ⟨ρ, vu⟩_{B^{+}} ⊳_{D} D(Φ(η, [u])). Thus ⊳_{D} is a satisfiability relation and is included in ⊧_{D}. Thus, we can conclude that ⟨ρ, v u⟩_{B^{+}} ⊧_{D} Φ(η, [u]) whenever ⟨ρ, v⟩_{B} ∼ ⟨η, u⟩_{A}. □

B Proof of Proposition 1

Proof ⇒ Given A = ⟨A, N, η_{0}, C, E⟩ a timed automata s.t. A ⊧ Ψ_{l} (i.e. ⟨η_{0}, v_{0}⟩_{A} ⊧ Ψ_{l}). Let Φ_{l} be the subformula [ ⋀_{i=1..l} ∃]0; 1[ (⟨a_{i}⟩ tt ∧ ⋀_{j≠i}[a_{j}] ff)].

Since A ⊧ Ψ_{l}, there exists a state ⟨η, v⟩_{A} satisfying Φ_{l}. But it requires that there exists at least l different reachable regions with a ]0; 1[ delay from ⟨η, v⟩_{A} and then 2|C| + 1 ≥ l.

⇐ It is easy to build a p-clock automata (with l ≤ 2p + 1) satisfying Ψ_{l}: Consider the p-clock automata s.t. the first l a-transitions ^{16} allow to reach a state ⟨η, v⟩_{A} s.t. 0 < v(x_{p}) < … < v(x_{1}) < 1. Moreover we build l transitions ⟨η, η′_{i}, a_{i}, {}, b_{i}⟩ with b_{1} = (x_{1} < 1), b_{2} = (x_{1} = 1), b_{3} = (x_{2} < 1 ∧ x_{1} > 1), … □

16In fact p transitions suffices to reach such a state.

Recent Publications in the BRICS Report Series

RS-95-2 Franc�ois Laroussinie, Kim G. Larsen, and Carsten Weise. From Timed Automata to Logic - and Back. January 1995. 21 pp.

RS-95-1 Gudmund Skovbjerg Frandsen, Thore Husfeldt, Peter Bro Miltersen, Theis Rauhe, and S�ren Skyum. Dynamic Algorithms for the Dyck Languages. January 1995. 21 pp.

RS-94-48 Jens Chr. Godskesen and Kim G. Larsen. Synthesizing Distinguishing Formulae for Real Time Systems. December 1994. 21 pp.

RS-94-47 Kim G. Larsen, Bernhard Steffen, and Carsten Weise. A Constraint Oriented Proof Methodology based on Modal Transition Systems. December 1994. 13 pp.

RS-94-46 Amos Beimel, Anna G� al, and Mike Paterson. Lower Bounds for Monotone Span Programs. December 1994. 14 pp.

RS-94-45 J�rgen H. Andersen, K� are J. Kristoffersen, Kim G. Larsen, and Jesper Niedermann. Automatic Synthesis of Real Time Systems. December 1994. 17 pp.

RS-94-44 Sten Agerholm. A HOL Basis for Reasoning about Functional Programs. December 1994. PhD thesis. viii+224 pp.

RS-94-43 Luca Aceto and Alan Jeffrey. A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours (Revised Version). December 1994. 18 pp. To appear in Theoretical Computer Science.

RS-94-42 Dany Breslauer and Leszek Ga�sieniec. Ef�cient String Matching on Coded Texts. December 1994. 20 pp.

RS-94-41 Peter Bro Miltersen, Noam Nisan, Shmuel Safra, and Avi Wigderson. On Data Structures and Asymmetric Communication Complexity. December 1994. 17 pp.