BRICS RS-95-19 Laroussinie & Larsen: Compositional Model Checking of Real Time Systems

BRICS

Basic Research in Computer Science

Compositional Model Checking of Real Time Systems

Franc�ois Laroussinie Kim G. Larsen

BRICS Report Series RS-95-19 ISSN 0909-0878 March 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

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Compositional Model Checking of Real Time Systems ^{∗}

François Laroussinie

BRICS^{†}, Aalborg Univ., Denmark^{‡}

Kim G. Larsen

BRICS, Aalborg Univ., Denmark

Abstract

A major problem in applying model checking to finite–state systems is the potential combinatorial explosion of the state space arising from parallel composition. Solutions of this problem have been attempted for practical applications using a variety of techniques. Recent work by Andersen [And95] proposes a very promising compositional model checking technique, which has experimentally been shown to improve results obtained using Binary Decision Diagrams.

In this paper we make Andersen’s technique applicable to systems described by networks of timed automata. We present a quotient construction, which allows timed automata components to be gradually moved from the network expression into the specification. The intermediate specifications are kept small using minimization heuristics suggested by Andersen. The potential of the combined technique is demonstrated using a prototype implemented in CAML.

∗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.

‡Dept. of Computer Science, Aalborg University, Fredrik Bajers Vej 7-E, DK-9220 Aalborg, Denmark, (email: {fl,kgl}@iesd.auc.dk) fax: (45) 98.15.81.29

Contents

1 Introduction 3 2 Timed Transition Systems and Automata 4 3 Timed Logic 7 4 Regions 9 5 Quotienting 12 6 Minimizations 15 7 Conclusion 17 A Proof of Theorem 2 20

1 Introduction

Within the last decade model checking has turned out to be a useful technique for verifying temporal properties of finite state systems. Efficient model checking algorithms for finite state systems have been obtained with respect to a number of logics, and in the last few years, model checking techniques have been extended to real–time systems and logics using the region technique of Alur, Courcoubetis and Dill [ACD90]. However, the major problem in applying model checking even to moderate–size systems is the potential combinatorial explosion of the state space arising from parallel composition. For real–time systems an additional explosion is induced in the number of regions. In order to avoid this problem algorithms have been sought that avoid exhaustive state (region) space exploration, either by symbolic representation of the states space such as in [HNSY92] and in the use of Binary Decision Diagrams [BCM^{+}90], by application of partial order methods [GW91, Val90] which suppresses unneccesarry interleavings of transitions, or by application of abstractions and symmetries [CFJ93, CGL92, EJ93].

So far the most successful results for larger systems have been obtained using the heuristics of Binary Decision Diagrams. However, recent work by Andersen [And95] introduces a new very promising heuristic model checking technique for finite state systems, for which experimental results on specific examples ^{1} shows an improvement compared with Binary Decision Diagrams. The technique is based on compositional proof rules for parallel composition.

Our aim of this paper is to make this new successful (compositional) model checking technique by Andersen [And95] applicable to real–time systems. For example, consider the following typical model checking problem

(S_{1} | … | S_{n}) ⊧ φ

where the S_{i}’s are real–time systems (described as timed automata [AD94]). We want to verify that the parallel composition of these timed automata satisfies the formula φ without having to construct the complete state (region) space of the process (S_{1} | … | S_{n}). We will avoid this complete construction by removing the components S_{i} one by one while simultaneously transforming the formula accordingly. Thus, when removing the component S_{n} we will transform the formula φ into the quotient formula φ / S_{n} such that

(S_{1} | … | S_{n}) ⊧ φ if and only if (S_{1} | … | S_{n−1}) ⊧ φ / S_{n}  (1)

Now clearly, if the quotient is not much larger than the original formula we have succeeded in simplifying the problem. Repeated application of quotienting yields

(S_{1} | … | S_{n}) ⊧ φ if and only if 1 ⊧ φ / S_{n} /S_{n−1} / … / S_{1}  (2)

where 1 is the unit with respect to parallel composition.

1using a prototype implementation in Standard ML

For finite state systems the quotient with respect to parallel composition is an immediate application of work on compositional reasoning due to Andersen, Larsen, Stirling, Winskel and Xinxin [Lar86, LX91, AW92, ASW94]. However, based on these ideas alone, (2) provides no solution to the problem as the explosion will now occur in the size of the final quotient formula instead. The crucial and experimentally “verified” observation by Andersen was that each quotienting should be followed by a minimization of the formula based on a collection of few, efficiently implementable strategies.

In this paper we provide the basis for and make an initial experimental investigation of the application of Andersen’s compositional model checking technique for real–time systems (timed automata). In particular,

• We give an effective construction of the quotient formula φ / S satisfying the requirement of (1) for φ a formula of the timed logic L_{ν} introduced in [LLW95] and S a real–time system given in terms of a timed automaton;

• Based on a prototype implemented in CAML we make an experimental investigation of the above quotient construction combined with (some of) the minimization heuristics of Andersen. In the examples we consider the minimized quotient formulas have been subject to dramatic reductions and are comparable in size to the original formulas. Thus, we may expect compositional model checking to be successful also for real–time systems.

The remainder of this paper is organized as follows: in the next section we give a short presentation of the notion of timed automata and composition used in this paper; in section 3, the logic L_{ν} is shortly presented, and in section 4 we review the region technique by Alur, Courcoubetis and Dill [ACD90]. Section 5 presents the quotient construction, whereas section 6 presents and investigates the consequences of minimization.

2 Timed Transition Systems and Automata

Let A be a finite 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.

Definition 1 A timed transition system over A is a tuple S = ⟨S, s_{0}, ⟶⟩, where S is a set of states, s_{0} is the initial state and ⟶⊆ S × L × S is a transition relation. We require that for any s ∈ S and d ∈ R, there exists a (unique) state s^{d} such that s ⟶^{ϵ(d)} s^{d}. Moreover (s^{d})^{e} = s^{d+e} ^{2}.

2The existence of s^{d} corresponds to transition liveness, its unicity corresponds to timedeterminism and the property (s^{d})^{e} = s^{(}d + e) corresponds to time-continuity (or timeadditivity) in [Yi90].

Obviously, we may apply the standard notion of bisimulation [Par81, Mil89] to timed transition systems. For S = ⟨S, s_{0}, ⟶⟩ a timed transition system, strong (timed) bisimulation ∼ is defined as the largest symmetric relation over S such that whenever s_{1} ∼ s_{2} and ℓ ∈ A ∪ D then

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

We may compare states from different timed transition systems by considering their disjoint union. Two timed transition systems S_{1} and S_{2} are said to be strong (timed) bisimilar, written S_{1} ∼ S_{2}, in case their initial states are strong bisimilar.

In order to study compositionality problems we introduce a parallel composition between timed transition systems. Following [HL89] we suggest a composition parameterized with a synchronization function generalizing a large range of existing notions of parallel compositions. A synchronization function f is a partial function (A∪{0})×(A∪{0}) ↪ A, where 0 denotes a distinguished no– action symbol ^{3}. Now, let S_{i} = ⟨S_{i}, s_{i,0}, ⟶_{i}⟩, i = 1, 2, be two timed transition systems and let f be a synchronization function. Then the parallel composition S_{1} |_{f} S_{2} is the timed transition system ⟨S, s_{0}, ⟶⟩, where s_{1} |_{f} s_{2} ∈ S whenever s_{1} ∈ S_{1} and s_{2} ∈ S_{2}, s_{0} = s_{1,0} |_{f} s_{2,0}, and ⟶ is given by the rule ^{4}:

\frac{s_{1} ⟶^{a}_{1} s′_{1} s_{2} ⟶^{b}_{2} s′_{2}}{s_{1} |_{f} s_{2} ⟶^{c} s′_{1} |_{f} s′_{2}} f(a, b) ≃ c

and the requirement that for any d ∈ R, (s_{1} |_{f} s_{2})^{d} = (s_{1}^{d} |_{f} s_{2}^{d}).

Syntactically, timed transition systems are described by timed automata [AD94], which are finite automata extended with a finite collection of real– valued clocks ^{5}. 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 2 A timed automaton A over A is a tuple ⟨N, η_{0}, C, E⟩ where 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 automata A_{e}, B_{d} and C_{d,e} in Figure 1 (d, e ∈ N). The automaton C_{d,e} has four nodes, μ_{0}, μ_{1}, μ_{2} and μ_{3}, two clocks x and y, and three edges. The edge between μ_{1} and μ_{2} has b as action, {x, y} as reset set and the enabling condition for the edge is y > d. □

3We extend the transition relation of a timed transition system such that s ⟶^{0} s′ iff s = s′.

4f(a, b) ≃ c holds if f is defined for the pair (a, b) and the result is c.

5Timed transition systems may alternatively be described using timed process calculi.

η_{2}^{{x}}^{{y}} ϱ_{2}  η_{1}^{{x}}^{{y}} ϱ_{1}  η_{0} ϱ_{0} a b  bc  μ_{2}^{{x, y}}^{{y}} μ_{1} μ_{0} a bc ^{{x}} μ_{3}^{tt}  ^{tt}^{y > d}  ^{x ≥ e}  ^{tt}^{y > d}^{x ≥ e} B_{d}  A_{e}  C_{d,e}

Figure 1: Three timed automata

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.

Formally 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 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′. Whenever v ∈ R^{C}, u ∈ R^{K} and C and K are disjoint vu denotes the time assignment over C ∪ K such that (vu)(x) = v(x) if x ∈ C and (vu)(x) = u(x) if x ∈ K. 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 ⟨N, η_{0}, C, E⟩ such that |C| = k.

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

The semantics of A is given by the timed transition system S_{A} = ⟨S_{A}, σ_{0}, ⟶_{A}⟩, where S_{A} is the set of states of A, σ_{0} is the initial state (η_{0}, v_{0}), and ⟶_{A} is the transition relation defined as follows:

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

Example 2 Reconsider the automaton C_{d,e} of Figure 1. The coordinate systems in Figure 2 indicates (some of) the states of C_{d,e}. Each point of the coordinate systems represents a unique time assignment, with the coordinate systems representing states involving the nodes μ_{0}, μ_{1}, and μ_{2} respectively. We

y  x^{ϵ(d′)} (μ_{1})  y  x^{ϵ(e′)} (μ_{2})  y  x (μ_{3}) x^{ϵ(f)} y  (μ_{0})  c b a

Figure 2: Partial Behaviour of C_{d,e}.

have indicated the following typical transition sequence (where f ≥ 0, d′ > d and e′ ≥ e):

\begin{matrix}(μ_{0}, (0, 0)) ⟶^{ϵ(f)} (μ_{0}, (f, f)) ⟶^{a} (μ_{1}, (f, 0)) ⟶^{ϵ(d′)} (μ_{1}, (f + d′, d′)) \\ and (μ_{1}, (f + d′, d′)) ⟶^{b} (μ_{2}, (0, 0)) ⟶^{ϵ(e′)} (μ_{2}, (e′, e′)) ⟶^{c} \end{matrix}

□

Parallel composition may now be extended to timed automata in the obvious way: for two timed automata A and B and a synchronization function f, the parallel composition A |_{f} B denotes the timed transition system S_{A} |_{f} S_{b}. For two automata A and B and a synchronization function f one may effectively construct an automaton A⊗_{f} B such that S_{A⊗_{f} B} is strong bisimilar to S_{A} |_{f} S_{B}. The nodes of A ⊗_{f} B is simply the product of A’s and B’s nodes, the set of clocks is the (disjoint) union of A’s and B’s clocks, and the edges are based on synchronizable A and B edges with enabling conditions conjuncted and reset– sets unioned.

Example 3 Let f be the synchronization function completely specified by f(a, 0) = a, f(b, b) = b and f(0, c) = c. Then the automaton C_{d,e} in Figure 1 is isomorphic to the part of B_{d} ⊗_{f} A_{e} which is reachable from (ρ_{0}, η_{0}). □

3 Timed Logic

We consider a dense–time logic L_{ν} with clocks and recursion. This logic may be seen as a certain fragment ^{6} of the μ–calculus T_{μ} presented in [HNSY92]. In [LLW95] it has been shown that this logic is sufficiently expressive that for any timed automaton one may construct a single characteristic formula uniquely characterizing the automaton up to timed bisimilarity. Also, decidability of a satisfiability ^{7} problem is demonstrated.

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

7Bounded in the number of clocks and maximal constant allowed in the satisfying automata.

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

Table 1: Definition of satisfiability.

Definition 3 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 transition system S we interpret the L_{ν} formulas over an extended state ⟨s, u⟩, where s is a state of S and u is a time assignment for K. 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 φ) initializes the formula clock x 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 ⊧_{D} between extended states and formulas is defined as the largest relation satisfying the implications of Table 1. We have left out the cases for ∨, [a] and ∀∀ as they are immediate duals.

Any relation satisfying the implications in Table 1 is called a satisfiability relation. It follows from standard fixpoint theory [Tar55] that ⊧_{D} is the union of all satisfiability relations and that the implications in Table 1 in fact are bi– implications for ⊧_{D}. We say that S satisfies a closed L_{ν} formula φ and write S ⊧ φ when ⟨s_{0}, u⟩ ⊧_{D} φ for any u. Note that if φ is closed, then ⟨s, u⟩ ⊧_{D} φ iff ⟨s, u′⟩ ⊧_{D} φ for any u, u′ ∈ R^{K}. Similarly, we say that a timed automaton A satisfies a closed L_{ν} formula φ in case S_{A} ⊧_{D} φ. We write A ⊧_{D} φ in this case.

Example 4 Consider the following declaration F of the identifiers X_{g} and Z_{g} where g ∈ N.

F = { X_{g} =^{def} [a](y in Z_{g}) , Z_{g} =^{def} (y > g) ∨ ([c]ff ∧ [a]Z_{g} ∧ [b]Z_{g} ∧ ∀∀Z_{g}) }

That is X_{g} expresses the property that the accumulated time between an initial a– and a following c–transition must exceed g. Thus for any transition sequence of the form (where α_{i} ∈ {a, b}):

s_{0} ⟶^{a} t_{0} ⟶^{ϵ(d_{1})} s_{1} ⟶^{α_{1}} t_{2} ⟶^{ϵ(d_{2})} s_{2} ⟶^{α_{2}} ⋯ t_{n} ⟶^{ϵ(d_{n})} s_{n} ⟶^{c}

∑ d_{i} > g. Now, reconsider the automata A_{e}, B_{d} and C_{d,e} of Figure 1 and Examples 1 and 2. Then it may be argued that C_{d,e} ⊧_{F} X_{d+e} and (consequently), that B_{d} |_{f} A_{e} ⊧_{F} X_{d+e}. □

Combining the parameterized parallel composition with L_{ν} we are able to express timed bisimilarity between timed transition systems as a single formula. This provides a timed extension of a similar characterization of strong bisimilarity for finite state systems [And94]: First we close the action set A under tagging; i.e. A^{t} = A ∪ A × {l} ∪ A × {r}. Now consider the ‘interleaving’ synchronization function h over A^{t} completely defined by h(a, 0) = a_{l} and h(0, a) = a_{r} where a ∈ A (i.e. h is undefined for all other pairs). Consider the following declaration E of the identifier Z:

Z =^{def} ⋀_{a∈A}([a_{l}]⟨a_{r}⟩Z ∧ [a_{r}]⟨a_{l}⟩Z) ∧ ∀∀Z

Then timed bisimilarity between timed transition systems is characterized as follows ^{8}:

Theorem 1 Let S be a timed transition system over A, and let s_{1}, s_{2} be states of S. Then s_{1} ∼ s_{2} if and only if s_{1} |_{h} s_{2} ⊧_{E} Z.

4 Regions

The model-checking problem for L_{ν} consists in deciding if a given timed automata A satisfies a given specification φ in L_{ν}. In [LLW95] this problem has been shown decidable using the region technique of Alur and Dill [AD94, ACD90]. The region technique provides an abstract interpretation of timed automata sufficiently complete that all information necessary for model–checking with respect to L_{ν} is maintained, yet finitary and thus enabling standard algorithmic model–checking techniques to be applied.

8It may be shown that the speed relation of [FT91] is characterized in a similar manner by Y defined recursively by Y =^{def} ⋀_{a∈A}([a_{1}]∃∃⟨a_{2}⟩Y ∧ [a_{2}]⟨a_{1}⟩Y) ∧ ∀∀Y.

The basic idea is that, given a timed automaton A, two states (η, v_{1}) and (η, v_{2}) 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}⟩ and ⟨(η, v_{2}), u_{2}⟩ where v_{1} u_{1} and v_{2} u_{2} are in the same region, satisfy the same L_{ν} formulas ^{9}. The notion of region is defined as an equivalence class of a relation over time assignments [ACD90] 10 . 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 ∈ γ ^{11}. Thus, given a region γ′, β(γ)(γ′) is mapped to the value tt precisely when γ = γ′. Finally, note that β(γ) itself can be viewed as an 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 successor 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}

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

9Without loss of generality, we will in all the following assume that that the formula clock set K and the automaton clock set C are disjoint.

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

11An 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.

12if this set is empty, then f = 0

0  (1) (1)  4 5 y  x 1  2 3 7 8 9 10 6 14  …  0 < x < 1∧ 0 < y < 1∧ y = x β(γ_{0}) = (x = 0 ∧ y = 0)  0 < x < 1∧ 0 < y < 1∧ succ(γ_{0}) = γ_{1} succ(γ_{5}) = γ_{6} β(γ_{6}) = (0 < y < 1 ∧ x = 1)  β(γ_{1}) = β(γ_{5}) = y < x 192021 24 28 18
Figure 3: R_{k}^{C} with C = {x, y} and k = 1

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

Example 5 Figure 3 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 32 different regions, of which only 17 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 = ⟨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} (η′, u′) 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 = ⟨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∪K} with 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. Observe that γ_{|C} ∈ R^{C} and γ_{|K} ∈ R^{K}.

Using the finitary symbolic semantics of timed automata a symbolic interpretation of L_{ν} is defined in [LLW95] faithfully reflecting the standard interpretation in Table 1. This symbolic interpretation provides the basis for decidability of model–checking for L_{ν}, and consequently (due to Theorem 1) for decidability of timed bisimilarity between timed automata.

tt/_{f} [η, γ] = tt
ff/_{f} [η, γ] = ff
(φ_{1} ∧ φ_{2})/_{f} [η, γ] = (φ_{1}/_{f} [η, γ]) ∧ (φ_{2}/_{f} [η, γ])
⟨a⟩φ/_{f} [η, γ] = ⋁_{b,[η′,γ′]∈E(η,γ,a)}⟨b⟩(r_{γ′} in φ/_{f} [η′γ′])

∃∃φ/_{f} [η, γ] = ∃∃( ⋁_{l=0...l_{γ}} β(γ^{l}) ∧ φ/_{f} [η, γ^{l}])

(x + c ∼ y + d)/_{f} [η, γ] = (x + c ∼ y + d)(γ)
(x in φ)/_{f} [η, γ] = x in (φ/_{f} [η, γ′]) where γ′ = [{x} → 0]γ
Z/_{f} [η, γ] = Z^{[η,γ]}

Table 2: Structural definition of quotient, φ/_{f} [η, γ].

5 Quotienting

Given an L_{ν} formula φ, and two timed transition systems S_{1} and S_{2} we aim at constructing a formula (called the quotient) φ/_{f} S_{2} such that

S_{1} |_{f} S_{2} ⊧ φ if and only if S_{1} ⊧ φ/_{f} S_{2}  (3)

The bi–implication indicates that we are moving parts of the parallel system into the formula. Clearly, if the quotient is not much larger than the original formula, we have simplified the task of model checking, as the (symbolic) semantics of S_{1} is significantly smaller than that of S_{1} |_{f} S_{2}.

In general it will not be possible to express within L_{ν} such a quotienting formula. However, whenever S_{2} is described using a timed automata we are able to express the quotient using the (extended) symbolic semantics of automata. More precisely, whenever φ is a formula over K and A is a timed automaton over C, we define quotient formulas φ/_{f} [η, γ] over C ∪ K, where [η, γ] is an extended symbolic state. For η_{0} the initial node of A and γ_{0} the initial region, φ/_{f} [η_{0}, γ_{0}] will express the sufficient and necessary requirement to a timed transition system S in order that S |_{f} S_{A} satisfies φ — see also Corollary 3 below. The quotient construction is defined structurally in Table 2. We have left out the cases for [a], ∨, and ∀∀ as they are immediate duals. The Table uses the

following notation: b, [η′γ′] ∈ E(η, γ, a) iff [η, γ_{|C}] ⟶^{c} [η′, γ′_{|C}], γ′_{|K} = γ_{|K} and

f(b, c) ≃ a for some c. We denote by r_{γ} the set of C clocks which has the value 0 in γ. Moreover (r in φ) is an abbreviation for (x_{1} in (x_{2} in … (x_{n} in φ))) whenever r is {x_{1}, …, x_{n}}. Finally, ⟨0⟩φ = [0]φ = φ.

Note that the quotient construction for identifiers introduces new identifiers of the form Z^{[η,γ]}, where Z ∈ Id. The definition of these are collected in the (quotient) declaration D_{A} given by:

Z^{[η,γ]} =^{def} D(Z)/_{f} [η, γ]

The following Theorem and Corollary shows that the quotient construction of Table 2 satisfies the requirements of (3). A proof of Theorem 2 is sketched in Appendix A.

Theorem 2 Let S = ⟨S, s_{0}, ⟶⟩ be a timed transition system, let A = ⟨N, η_{0}, C, E⟩ be a timed automaton, and let φ be an L_{ν} formula over clock set K, all over an action set A. Then for any s ∈ S, η ∈ N, v ∈ R^{C}, and u ∈ R^{K}:

⟨ s |_{f} (η, v) , u ⟩ ⊧_{D} φ if and only if ⟨ s, v u ⟩ ⊧_{D_{A}} φ/_{f} [η, [v u]]

Corollary 3 Let S be a timed transition system, let A be a timed automaton with clock set C, and let φ be a closed L_{ν} formula over clock set K, all over an action set A. Then:

S |_{f} S_{A} ⊧_{D} φ if and only if S ⊧_{D_{A}} φ/_{f} A

where φ/_{f} A abbreviates φ/_{f} [η_{0}, γ_{0}] with η_{0} being the initial node of A and γ_{0} the initial region over C ∪ K.

Example 6 Recall the timed automata and declaration from Examples 1 and 4. The quotient X_{1}/_{f} A_{1} describes the sufficient and necessary requirement to a timed transition system S in order that S |_{f} S_{A_{1}} satisfies X_{1}. Clearly, we expect the timed automata B_{0} to satisfy this property. Now using a CAML prototype implementation of the quotient construction X_{1}/_{f} A_{1} is computed. The definition of X_{1}/_{f} A_{1} is found in the quotient declaration F_{A_{1}} part of which is given below:

X_{1}/_{f} A_{1} =^{def} [a] y in Z_{1}^{[η_{0},γ_{0}]}
Z_{1}^{[η_{0},γ_{0}]} =^{def} ff ∨ [tt ∧ ([b]x in Z_{1}^{[η_{1},γ_{0}]}) ∧ ([a]Z_{1}^{[η_{0},γ_{0}]}) ∧ ∀∀(β(γ_{0}) ⇒ Z_{1}^{[η_{0},γ_{0}]} ∧
β(γ_{1}) ⇒ Z_{1}^{[η_{0},γ_{1}]} ∧ β(γ_{2}) ⇒ Z_{1}^{[η_{0},γ_{2}]} ∧ β(γ_{3}) ⇒ Z_{1}^{[η_{0},γ_{3}]})]
Z_{1}^{[η_{1},γ_{0}]} =^{def} ff ∨ [tt ∧ tt ∧ ([a]Z_{1}^{[η_{1},γ_{0}]}) ∧ ∀∀(β(γ_{0}) ⇒ Z_{1}^{[η_{1},γ_{0}]} ∧ β(γ_{1}) ⇒ Z_{1}^{[η_{1},γ_{1}]} ∧
β(γ_{2}) ⇒ Z_{1}^{[η_{1},γ_{2}]} ∧ β(γ_{3}) ⇒ Z_{1}^{[η_{1},γ_{3}]})]
Z_{1}^{[η_{0},γ_{1}]} =^{def} ff ∨ [tt ∧ ([b]x in Z_{1}^{[η_{1},γ_{18}]}) ∧ ([a]Z_{1}^{[η_{0},γ_{1}]}) ∧ ∀∀(β(γ_{0}) ⇒ Z_{1}^{[η_{0},γ_{0}]} ∧
β(γ_{1}) ⇒ Z_{1}^{[η_{0},γ_{1}]} ∧ β(γ_{2}) ⇒ Z_{1}^{[η_{0},γ_{2}]} ∧ β(γ_{3}) ⇒ Z_{1}^{[η_{0},γ_{3}]})]
Z_{1}^{[η_{0},γ_{2}]} =^{def} ff ∨ [tt ∧ ([b]x in Z_{1}^{[η_{1},γ_{24}]}) ∧ ([a]Z_{1}^{[η_{0},γ_{2}]}) ∧ ∀∀(β(γ_{0}) ⇒ Z_{1}^{[η_{0},γ_{0}]} ∧
β(γ_{1}) ⇒ Z_{1}^{[η_{0},γ_{1}]} ∧ β(γ_{2}) ⇒ Z_{1}^{[η_{0},γ_{2}]} ∧ β(γ_{3}) ⇒ Z_{1}^{[η_{0},γ_{3}]})]
Z_{1}^{[η_{0},γ_{3}]} =^{def} tt ∨ [tt ∧ ([b]x in Z_{1}^{[η_{1},γ_{28}]}) ∧ ([a]Z_{1}^{[η_{0},γ_{3}]}) ∧ ∀∀(β(γ_{0}) ⇒ Z_{1}^{[η_{0},γ_{0}]} ∧
β(γ_{1}) ⇒ Z_{1}^{[η_{0},γ_{1}]} ∧ β(γ_{2}) ⇒ Z_{1}^{[η_{0},γ_{2}]} ∧ β(γ_{3}) ⇒ Z_{1}^{[η_{0},γ_{3}]})]

The quotient declaration F_{A_{1}} contains in total definitions of 96 identifiers. We expect X_{1}/_{f} A_{1} to express that the accumulated time between an initial a–action and a following b–action must be strictly greater than 0 as described by the following property U_{0}:

U_{0} =^{def} [a](y in V_{0}) V_{0} =^{def} (y > 0) ∨ ([b]ff ∧ [a]V_{0} ∧ ∀∀V_{0})

In the next section we will present effective minimization strategies, which essentially transforms the large quotient declaration F_{A_{1}} into the small yet equivalent declaration above. □

Now, let π be the synchronization function completely specified by π(0, a) = a for all a ∈ A (i.e. the left argument to π is completely ignored). Then it is easy to see that for any timed transition system S, S_{A} and S |_{π} S_{A} satisfies the same formulas. In particular S_{A} and S_{1} |_{π} S_{A} satisfies the same formula, where 1 is the 0–clock timed automaton with just one (initial) node and no edges. Using this observation, the quotient construction can be used to obtain alternative model–checking algorithms for L_{ν} as follows:

Corollary 4 Let A be a timed automaton with clock set C, and let φ be a closed L_{ν} formula over clock set K, all over an action set A. Then:

A ⊧_{D} φ if and only if 1 ⊧_{D_{A}} φ/_{π} A if and only if φ/_{π} A ⇔ tt

Due to the projective nature of π it is clear that φ/_{π} A contains no action modalities, and it is easy to build a special purpose model checker for the simple automata 1.

Example 7 Recall once more the timed automata and declaration from Examples 1 and 4. From these Examples we expect that C_{0,1} satisfies the property X_{1}. Now, using the Corollary 4 we may verify this by showing that the quotient formula X_{1}/_{f} C_{0,1} is either valid or satisfied by 1. X_{1}/_{f} C_{0,1} is defined in the following quotient declaration F_{C_{0,1}} ^{13}:

X_{1}^{[μ_{0},γ_{0}]} =^{def} x in y in Z_{1}^{[μ_{1},γ_{0}]}
Z_{1}^{[μ_{1},γ_{0}]} =^{def} ∀∀(β(γ_{0}) ⇒ Z_{1}^{[μ_{1},γ_{0}]} ∧ β(γ_{1}) ⇒ Z_{1}^{[μ_{1},γ_{1}]} ∧ β(γ_{2}) ⇒ Z_{1}^{[μ_{1},γ_{2}]})
Z_{1}^{[μ_{1},γ_{1}]} =^{def} (x in Z_{1}^{[μ_{2},γ_{18}]}) ∧ ∀∀(β(γ_{0}) ⇒ Z_{1}^{[μ_{1},γ_{0}]} ∧ β(γ_{1}) ⇒ Z_{1}^{[μ_{1},γ_{1}]} ∧
β(γ_{2}) ⇒ Z_{1}^{[μ_{1},γ_{2}]})
Z_{1}^{[μ_{2},γ_{18}]} =^{def} ∀∀(β(γ_{18}) ⇒ Z_{1}^{[μ_{2},γ_{18}]} ∧ β(γ_{19}) ⇒ Z_{1}^{[μ_{2},γ_{19}]} ∧ β(γ_{20}) ⇒ Z_{1}^{[μ_{2},γ_{20}]})
Z_{1}^{[μ_{2},γ_{19}]} =^{def} ∀∀(β(γ_{18}) ⇒ Z_{1}^{[μ_{2},γ_{18}]} ∧ β(γ_{19}) ⇒ Z_{1}^{[μ_{2},γ_{19}]} ∧ β(γ_{20}) ⇒ Z_{1}^{[μ_{2},γ_{20}]})
Z_{1}^{[μ_{2},γ_{20}]} =^{def} ∀∀(β(γ_{18}) ⇒ Z_{1}^{[μ_{2},γ_{18}]} ∧ β(γ_{19}) ⇒ Z_{1}^{[μ_{2},γ_{19}]} ∧ β(γ_{20}) ⇒ Z_{1}^{[μ_{2},γ_{20}]})

13Found using the CAML prototype with subsequent application of boolean simplifications.

Z_{1}^{[μ_{1},γ_{2}]} =^{def} (x in Z_{1}^{[μ_{2},γ_{24}]}) ∧ ∀∀(β(γ_{0}) ⇒ Z_{1}^{[μ_{1},γ_{0}]} ∧ β(γ_{1}) ⇒ Z_{1}^{[μ_{1},γ_{1}]} ∧
β(γ_{2}) ⇒ Z_{1}^{[μ_{1},γ_{2}]})
Z_{1}^{[μ_{2},γ_{24}]} =^{def} ∀∀β(γ_{24}) ⇒ Z_{1}^{[μ_{2},γ_{24}]}

□

Finally, combining the characterization of timed bisimulation in Theorem 1 with the quotient construct of Table 2, we can for any timed automaton A construct a characteristic L_{ν} formula uniquely characterizing the automaton up to timed bisimilarity in the following manner: Let E, Z and h be as in Theorem 1. Then for any timed transition system S the following holds:

S ∼ S_{A} if and only if S ⊧_{E} Z/_{h} [η_{0}, γ_{0}]

where η_{0} is the initial node of A and γ_{0} is the initial region over the clocks of A (note that Z is an L_{ν} formula over the empty set of clocks). This provides an alternative characteristic formula construction compared with [LLW95].

6 Minimizations

It is evident from the examples in the previous section that repeated quotienting leads to an explosion in the formula. A similar phenomena was observed by Andersen for the quotient construction of modal μ–calculus formulas with respect to finite–state systems. The crucial observation by Andersen is that simple and cost effective transformations of the formulas in practice often lead to significant reductions.

We have implemented in CAML the quotient construction of the previous section as well as (simplified versions of some of) Andersen’s minimization strategies. In the investigated examples the minimization strategies lead to dramatic reductions. Below we describe the transformations considered in terms of transformations on formulas and declarations (defining equations).

Reachability: When considering an initial quotient formula φ/_{f} [η_{0}, γ_{0}] not all identifiers of D_{A} may be relevant or reachable. In our CAML implementation an “on–the–fly” technique insures that only the reachable part of D_{A} is generated.

Boolean Simplification: Formulas may be simplified using the following simple boolean equations and their duals: ff ∧ φ ≡ ff, tt ∧ φ ≡ φ, ⟨a⟩ff ≡ ff, ∃∃ff ≡ ff, x in ff ≡ ff, ⟨a⟩φ ∧ [a]ff ≡ ff.

Constant Propagation: Identifiers which are declared to either tt or ff may be removed while substituting their definitions in the declaration of all other identifiers.

Trivial Equation Elimination: Equations of the form X =^{def} [a]X are easily seen to have X = tt as solution. More generally, whenever X =^{def} φ where φ[tt/X] ^{14} can be simplified to tt, we can perform a removal of the identifier X provided the value tt is propagated to all uses of X (as under Constant Propagation).

Equivalence Reduction: If two identifiers X and Y are equivalent (i.e. are satisfied by the same timed transition systems) we may collapse them into a single identifier. To obtain a cost effective strategy we approximate equivalence of identifiers with the following check: whenever X =^{def} φ and Y =^{def} ϑ such that φ[Y/X] is syntactically identical to ϑ[Y/X] we conclude that X and Y are equivalent and may be identified.

We apply the above transformation strategies repeatedly on quotient formulas and declarations. As can be seen in Table 2, quotienting transforms atomic propositions of the form x + c ∼ y + d into either tt or ff, thus yielding high applicability of Boolean Simplification and Constant Propagation. Also, quotient versions of the same original formula tend to have same structure thus making applicability of Equivalence Reduction high.

In our CAML prototype implementation we have implemented the above reported very simple strategies for Trivial Equation Elimination and Equivalence Reduction. Generalized and more sophisticated (yet still efficient) strategies can or course easily be given. However, even with the implemented simple versions we obtain a very high degree of reduction as observed in the following examples.

Example 8 Recall Example 6. Applying the minimization strategies of the CAML prototype we find that X_{1}/_{f} A_{1} is equivalent to Y_{0} with the following definition:

Y_{0} =^{def} [a]y in Y_{1}
Y_{1} =^{def} [b]ff ∧ [a]Y_{1} ∧ ∀∀(β(γ_{0}) ⇒ Y_{1} ∧ (β(γ_{1}) ∨ β(γ_{2})) ⇒ Y_{2})
Y_{2} =^{def} [a]Y_{2} ∧ ∀∀(β(γ_{0}) ⇒ Y_{1} ∧ (β(γ_{1}) ∨ β(γ_{2})) ⇒ Y_{2})

During minimization only 23 identifiers of F_{A_{1}} were found to be reachable from X_{1}/_{f} A_{1}, 14 respectively 3 of which were found to be equivalent to tt respectively ff. The remaining 6 identifiers were finally partitioned into 3 classes. Though dramatically reduced, the declaration leaves room for one additional simplification as it may be observed that (β(γ_{1}) ∨ β(γ_{2})) ⇒ Y_{2} is equivalent to tt. With this observation we finally obtain:

Y′_{0} =^{def} [a]y in Y′_{1} Y′_{1} =^{def} [b]ff ∧ [a]Y′_{1} ∧ ∀∀(β(γ_{0}) ⇒ Y′_{1})

which clearly meets the expectations of 6. Minimization of the quotient formula X_{7}/_{f} A_{10} leads directly to the formula tt indicating that for any timed transition system S the composition S |_{f} S_{A_{10}} satisfies X_{7}. Intuitively this is clear as the component A_{10} by itself ensures the delay required by X_{7}. The corresponding quotient declaration contains 3498 identifiers 617 of which were found to be reachable. Subsequently all these were simplified to tt. □

14φ[tt/X] is the formula obtained by substituting all occurrences of X in φ with the formula tt.

Example 9 Recall Example 7. Using the minimization strategies of the CAML prototype we find directly that X_{1}/_{f} C_{0,1} simplifies to tt thus implying that C_{0,1} satisfies the property X_{1}. Similarly, minimization of the quotient formula X_{2}/_{f} C_{0,1} yields ff confirming that C_{0,1} does not satisfy X_{2}! □

Example 10 Now we want to confirm that B_{0} does indeed satisfy the requirement X_{1}/_{f} A_{1} and hence that B_{0} |_{f} A_{1} satisfies X_{1}. Using the equivalent, minimized formula Y_{0} from Example 8 it suffices according to Corollary 4 to verify validity of the quotient formula Y_{0}/_{π} B_{0}. The CAML prototype confirms this through immediate minimization to tt. □

7 Conclusion

This paper has presented the basis for a compositional model checking technique for real–time systems. Based on initial experiments with the CAML prototype we conjecture that compositional model checking will prove not only a feasible but also an efficient technique for real–time systems. However, it is clear that many more experiments must be performed before the conjecture can be finally settled, and in this process we will need to extend our prototype with more sophisticated minimization strategies as the success of compositional model checking is completely determined by these.

Our work on quotient formulas extends that of [AKLN95], where a quotient construction for 1-clock automata has been given. Moreover it can be generalized trivially to logics with minimal fixpoint constructs (such as T_{μ} in [HNSY92]) as quotienting is easily seen to distribute over negation.

Acknowledgement

The authors would like to thank Henrik Reif Andersen for interesting and enlightening discussions on the topic of compositional (partial) model–checking.

References

[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.

[AKLN95] J. H. Andersen, K. J. Kristoffersen, K. G. Larsen, and J. Niedermann. Automatic Synthesis of Real Time Systems. Lecture Notes in Computer Science, 1995. To appear in Proceedings of ICALP’95.

[And94] H. R. Andersen. A Polyadic Modal μ–calculus. Id–tr: 1994–145, Department of Computer Science, Technical University of Denmark, 1994.

[And95] H. R. Andersen. Partial Model Checking. To appear in Proceedings of LICS’95, 1995.

[ASW94] H. R. Andersen, C. Stirling, and G. Winskel. A Compositional Proof System for the Modal Mu–Calculus. Logic in Computer Science, 1994.

[AW92] H.R. Andersen and G. Winskel. Compositional checking of satisfaction. Formal Methods in Systems Design, 1992. To appear.

[BCM^{+}90] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 1)^{2}0 states and beyond. Logic in Computer Science, 1990.

[CFJ93] E. M. Clarke, T. Filkorn, and S. Jha. Exploiting Symmetry in Temporal Logic Model Checking. Lecture Notes in Computer Science, 697, 1993.

[CGL92] E. M. Clarke, O. Grümberg, and D. E. Long. Model Checking and Abstraction. Principles of Programming Languages, 1992.

[EJ93] E. A. Emerson and C. S. Jutla. Symmetry and Model Checking. Lecture Notes in Computer Science, 697, 1993.

[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.

[GW91] P. Godefroid and P. Wolper. A Partial Approach to Model Checking. Logic in Computer Science, 1991.

[HL89] H. Hüttel and K. G. Larsen. The use of static constructs in a modal process logic. Lecture Notes in Computer Science, Springer Verlag, 363, 1989.

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

[Lar86] K.G. Larsen. Context–Dependent Bisimulation Between Processes. PhD thesis, University of Edinburgh, Mayfield Road, Edinburgh, Scotland, 1986.

[LLW95] F. Laroussinie, K. G. Larsen, and C. Weise. From Timed Automata to Logic — and Back. Technical Report RS–95–2, BRICS, 1995.

[LX90] K.G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts. Lecture Notes in Computer Science, Springer Verlag, 443, 1990. In Proceedings of 17th International Colloquium on Automata, Languages and Programming 1990.

[LX91] K.G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts. Journal of Logic and Computation, 1(6):761–795, 1991.

[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.

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

[Val90] A. Valmari. A Stubborn Attack on State Explosion. Theoretical Computer Science, 3, 1990.

[Yi90] W. Yi. A Calculus of Real Time Systems. Lecture Notes in Computer Science, 458, 1990. In Proceedings of CONCUR.

A Proof of Theorem 2

Proof We only sketch the proof for the identifier free formulas of L_{ν} using structural induction on φ. Consequently we drop declaration subscripts on ⊧. The full proof follows the structure used in [LX90].

We consider only the cases ⟨a⟩φ, ∃∃φ and x in φ leaving the remaining more trivial cases to the reader.

• Assume ⟨ s |_{f} (η, v) , u ⟩ ⊧ ⟨a⟩φ. Then we have:

⟨ s |_{f} (η, v) , u ⟩ ⊧ ⟨a⟩φ

⇔ ⟨ s′ |_{f} (η′, v′) , u ⟩ ⊧ φ For some s ⟶^{a_{1}} s′ and ∃⟨η, η′, a_{2}, r, b⟩ ∈ E

s.t. v′ = [r → 0]v and b(v) = tt and

f(a_{1}, a_{2}) ≃ a
⇔ ⟨ s′, v′ u ⟩ ⊧ φ/_{f} [η′, [v′ u]]  by IH
⇔ ⟨ s′, v u ⟩ ⊧ r in φ/_{f} [η′, [v′ u]]
⇔ ⟨ s, v u ⟩ ⊧ ⟨a_{1}⟩(r in φ/_{f} [η′, [v′ u]])
⇔ ⟨ s, v u ⟩ ⊧ ⋁_{a_{1},[η′,[v′ u]]∈E(η,[vu],a)} ⟨a_{1}⟩(r_{v′} in φ/_{f} [η′, [v′ u]])
⇔ ⟨ s, v u ⟩ ⊧ (⟨a⟩φ)/_{f} [η, [v u]]

• Assume ⟨ s |_{f} (η, v) , u ⟩ ⊧ ∃∃φ. Then we have:

⟨ s |_{f} (η, v) , u ⟩ ⊧ ∃∃φ
⇔ ⟨ s^{d} |_{f} (η, v+d) , u+d ⟩ ⊧ φ  For some d ∈ R
⇔ ⟨ s^{d}, v+d u+d ⟩ ⊧ φ/_{f} [η, [v+d u+d]] by IH
⇔ ⟨ s^{d}, v+d u+d ⟩ ⊧ φ/_{f} [η, [v u]^{i}]  Where (v+d u+d) ∈ [vu]^{i}
⇔ ⟨ s^{d}, v+d u+d ⟩ ⊧ β([v u]^{i}) ∧ φ/_{f} [η, [v u]^{i}]
⇔ ⟨ s, v u ⟩ ⊧ (∃∃φ)/_{f} [η, [v u]]

• Assume ⟨ s |_{f} (η, v) , u ⟩ ⊧ x in φ. Then we have:

⟨ s |_{f} (η, v) , u ⟩ ⊧ x in φ
⇔ ⟨ s |_{f} (η, v) , u′⟩ ⊧ φ  with u′ = [x → 0]u
⇔ ⟨ s, v u′, ⟩ ⊧ φ/_{f} [η, [v u′]]  by IH
⇔ ⟨ s, v u ⟩ ⊧ x in φ/_{f} [η, [v u′]]
⇔ ⟨ s, v u ⟩ ⊧ (x in φ)/_{f} [η, [v u]]
□

Recent Publications in the BRICS Report Series

RS-95-19 Franc�ois Laroussinie and Kim G. Larsen. Compositional Model Checking of Real Time Systems. March 1995. 20 pp.

RS-95-18 Allan Cheng. Complexity Results for Model Checking. February 1995. 18pp.

RS-95-17 Jari Koistinen, Nils Klarlund, and Michael I. Schwartzbach. Design Architectures through Category Constraints. February 1995. 19 pp.

RS-95-16 Dany Breslauer and Ramesh Hariharan. Optimal Parallel Construction of Minimal Suf�x and Factor Automata. February 1995. 9 pp.

RS-95-15 Devdatt P. Dubhashi, Grammati E. Pantziou, Paul G. Spirakis, and Christos D. Zaroliagis. The Fourth Moment in Luby’s Distribution. February 1995. 10 pp.

RS-95-14 Devdatt P. Dubhashi. Inclusion�Exclusion(3) Implies Inclusion�Exclusion(n). February 1995. 6 pp.

RS-95-13 Torben Bra� uner. The Girard Translation Extended with Recursion. 1995. Full version of paper to appear in Proceedings of CSL ’94, LNCS.

RS-95-12 Gerth St�lting Brodal. Fast Meldable Priority Queues. February 1995. 12 pp.

RS-95-11 Alberto Apostolico and Dany Breslauer. An Optimal O(log log n) Time Parallel Algorithm for Detecting all Squares in a String. February 1995. 18 pp. To appear in SIAM Journal on Computing.

RS-95-10 Dany Breslauer and Devdatt P. Dubhashi. Transforming Comparison Model Lower Bounds to the Parallel-Random-Access-Machine. February 1995. 11 pp.

RS-95-9 Lars R. Knudsen. Partial and Higher Order Differentials and Applications to the DES. February 1995. 24 pp.

RS-95-8 Ole I. Hougaard, Michael I. Schwartzbach, and Hosein Askari. Type Inference of Turbo Pascal. February 1995. 19 pp.