BRICS RS-94-48 Godskesen & Larsen: Synthesizing Distinguishing Formulae for Real Time Systems

BRICS

Basic Research in Computer Science

Synthesizing Distinguishing Formulae for Real Time Systems

Jens Chr. Godskesen Kim G. Larsen

BRICS Report Series RS-94-48 ISSN 0909-0878 December 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, 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

Synthesizing Distinguishing Formulae for Real Time Systems ^{∗}

Jens Chr. Godskesen TeleDanmark Research, DK Kim G. Larsen BRICS ^{†} Aalborg University, DK

Abstract

This paper describes a technique for generating diagnostic information for the timed bisimulation equivalence and the timed simulation preorder. More precisely, given two (parallel) networks of regular real–time processes, the technique will provide a logical formula that differentiates them in case they are not timed (bi)similar. Our method may be seen as an extension of the algorithm by Čerāns for deciding timed bisimilarity in that information of time–quantities has been added sufficient for generating distinguishing formulae. The technique has been added to the automatic verification tool Epsilon and applied to various examples.

1 Introduction

Research in the area of process algebras has created interest in behavioural relations as a tool for verifying correctness of processes [Mil80, Hoa78, Hen88, BHK86]. In this approach, specifications as well as implementations are formalized as process algebraic expressions, and verification consists in establishing a suitable behavioural relationship between an implementation and its specification. A number of equivalences has been proposed in the literature (for an overview see [vG90, vG92]), and several automated tools support verification for finite–state systems based on such equivalences (e.g. [LMV88, CPS89, GLZ89, RRSV87]).

∗This work has been supported by the Danish Basic Research Foundation project BRICS and the ESPRIT Basic Research Action 7166, CONCUR2.

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

However, for a tool to be of real assistance during a design process it is crucial that diagnostic information is offered in case of erroneous design as undoubtedly this troublesome situation will occur more frequently than not. Moreover, the diagnostic information offered must be useful in the subsequent debugging. For a variety of (bi)simulation equivalences [Par81, Mil80, vGW89] the theoretical basis for generation of such diagnostic information is given in terms of a logical characterization of the equivalence: two systems are equivalent exactly when they satisfy the same formulas in a particular modal logic [HM85, DV91]. Thus when two systems are found not to be equivalent, one may explain why by giving a formula satisfied by one but not the other. Algorithms for generating distinguishing formulae for finite–state systems has been described in [Hil87, Cle90, Kor91, CC92, Pol92] and implemented in at least two tools [GLZ89, CPS89].

During the last few years a number of real–time process algebras has been introduced in order to handle quantitative aspects of processes [DS89, Wan90, NRSV90, BB89, Che91]. In addition a number of time–sensitive and time– abstracting (bi)simulation equivalences and preorders has been introduced and studied [Wan90, LW90, GL92, DS89]. Due to the use of the non–negative reals as time domain, even the simplest processes describe infinite states systems. Thus, decidability of (bi)similarity cannot be achieved using the standard algorithmic techniques for finite–state systems. However, decidability of (bi)simulation equivalence between networks of timed regular processes has recently been established by Čerāns [Č92] in the time–sensitive case and by Larsen and Wang [LW90] in the time–abstracted case. The underlying algorithmic techniques has later been implemented in the automatic verification tool Epsilon [ČGL93].

Our goal in this paper is to describe the method used in Epsilon for generating diagnostic information for the timed (bi)simulation equivalence. The diagnostic information relies on a logical characterization of timed (bi)simulation equivalence using a real–timed version of the well known Hennessy–Milner Logic [HM85]. Thus in case of two non–(bi)similar processes, the diagnostic information will consist of a distinguishing formula. Our method may be seen as an extension of Čerāns’ algorithm for deciding timed bisimilarity to which information of time– quantities has been added sufficient (but no more) for generating distinguishing formulae.

The remainder of this paper is organized as follows. The next section introduced the syntax and operational semantics of a slightly simplified version of Wang’s real–time process algebra TCCS [Wan90]. Also, the section defines timed (bi)similarity and examines the connection between it and a real–time version of Hennessy–Milner Logic. Section 3 contains a much simplified account of Čerāns’ algorithm for the (simplified) class of TCCS processes. Thus, the section introduces the notion of symbolic process providing a finite–state representation of real–time processes, and the notion of symbolic (bi)simulation providing the basis for an algorithm deciding timed (bi)similarity. Section 4 introduces the notions of pointed symbolic process and pointed symbolic (bi)similarity providing a representation of real–time processes with explicit information of certain time–quantities yet sufficiently finitary that it provides the basis for an algorithm generating distinguishing formulae. The final section contains our concluding remarks.

2 Timed Processes

Our language for timed processes is based on the real–time calculus TCCS [Wan90] by Wang. In particular, we apply the two–phase functioning principle outlined in [NSY92], which in short means that the behaviour of a system is regarded as being split in two alternating phases: one where all the components of the system agrees to let time progress and one where (some of) the components of the system computes. In order to explain our algorithmic ideas most clearly we have made certain simplifications in comparison to Wang Yi’s calculus. In particular, we assume that all actions are observable, hence avoiding the issue of maximal progress. For the same reason, the parallel operator is simplified to that of pure interleaving without any synchronization on actions. Finally, we assume recursive definitions of regular processes to be in simple sum normal form — a form into which all regular process expressions of TCCS can easily be transformed. Our algorithmic ideas extends to the full calculus of TCCS and has been implemented in the automatic verification tool Epsilon.

2.1 Syntax and Semantics

(Initial Integral) Regular Processes

Let A be a fixed set of actions range over by a, b, c, . . .. We denote by R_{>0} the set of positive reals ranged over by d, d_{1}, d_{2}, …, d′, d′′, . . .. R_{≥0} denotes the set of non–negative reals ranged over by e, e_{1}, e_{2}, …, e′, e′′, . . .. Nat denotes the set of natural numbers (including 0), and finally, D denotes the set {ϵ(d) | d ∈ R_{>0}}. We use σ, σ′, … to range over elements of the set A ∪ D.

Assume a finite set of process variables V and for each process variable X a defining equation of the following (normal) form:

X =^{def} ∑_{i=1}^{n} ϵ(e_{i}).a_{i}.X_{i}  (1)

where e_{i} ∈ Nat and X_{i} ∈ V. We denote by Δ the set of recursive definitions and the process variables are called initial integral regular processes (IIR) ^{1}.

1In the syntax for IIR processes we restrict ourselves to the use of integer delays. However,

Intuitively, the definition of X in (1) describes a (real–time) behaviour which after a delay of d will “offer” to its environment all actions a_{i} for which e_{i} ≤ d (thus e_{i} is the enabling time of the action a_{i}); if the environment “accepts” the offered action, X may evolve to the behaviour determined by X_{i}.

Formally, the behaviour of an (initial integral) regular process described by an equation system Δ is given in terms of a transition system with transitions labelled by actions (A) or delays (D). First, let for d ∈ R_{>0}, X^{d} denote the term:

∑_{i=1}^{n} ϵ(e_{i}− · d).a_{i}.X_{i}

assuming that X is defined as in (1) ^{2}. Also, we let X^{0} = X.

Given a set Δ of (recursive) definitions of the form (1), the following labelled transition system is induced:

⟨X, A ∪ D, ⟶⟩

where

X = {X^{e} | X ∈ V, e ∈ R_{≥0}}

and ⟶⊆ X × (A ∪ D) × X is defined by the following two axioms assuming (1) is the defining equation for X:

\begin{matrix}X^{e} ⟶^{a_{i}} X_{i} when e_{i} ≤ e \\ X^{e} ⟶^{ϵ(d)} X^{e+d} \end{matrix}

We shall use P, Q, … to range over X.

Example 2.1 Consider the following equation system for the four variables Z, Z_{b}, Z_{a} and X ^{3}:

\begin{matrix}Z =^{def} & ϵ(1).a.Z_{b} + ϵ(1).b.Z_{a} + b.X & Z_{b} =^{def} & b \\ Z_{a} =^{def} & a & X =^{def} & ϵ(1).a \end{matrix}

Applying the operational semantics of regular processes yields the following transition sequence of Z:

Z ⟶^{ϵ( \frac{1}{2} )} ϵ(\frac{1}{2}).Z_{a} + ϵ(\frac{1}{2}).Z_{b} + b.X ⟶^{b} X ⟶^{ϵ( \frac{1}{2} )} ϵ(\frac{1}{2}).a

Note that the final state (ϵ(\frac{1}{2}).a) cannot perform an a–transition. □

the semantic time domain is of course that of the positive reals, thus derivatives of IIR processes will not in general be IIR — hence the terminology initial integral.

2− · denotes monus on R_{≥0}. That is for e, f ∈ R_{≥0}, e− · f = max{e − f, 0}.

3nil denotes the variable defined to be the empty sum — thus for all d, nil^{d} is the empty sum and the only transitions are delay transitions. We use the abbreviations a.P for ϵ(0).a.P, and a for a.nil.

The above defined transition system enjoys a number of useful properties stated below — for proofs and more information we refer the reader to [Wan90, Wan91]. Note also the (uncountably) infinite state and dense nature of the transition system determined by an equation system Δ.

Proposition 2.2

1. (Time Determinism) Whenever P ⟶^{ϵ(d)} P′ and P ⟶^{ϵ(d)} P′′ then P′ = P′′.

2. (Strong Persistency) If P ⟶^{a} Q and P ⟶^{ϵ(d)} P′ then P′ ⟶^{a} Q.

3. (Time Continuity) For all d_{1}, d_{2} and P′′, P ⟶^{ϵ(d_{1}+d_{2})} P′′ iff P ⟶^{ϵ(d_{1})} P′ ⟶^{ϵ(d_{2})} P′′

for some P′.

Networks

Assume Δ is a system of equations of the form (1) over the finite set of variables V. Then a (parallel) network (over Δ and V) is a term of the form:

\overline{X} = (X_{1} | … | X_{n})

where X_{i} ∈ V.

The set of n–ary networks induces a labelled transition system:

N_{n} = (Net_{n}, A ∪ D, ⟶)

where

Net_{n} = {(X_{1}^{e_{1}} | … | X_{n}^{e_{n}}) | X_{i} ∈ V, e_{i} ∈ R_{≥0}}

and ⟶⊆ Net_{n} ×(A∪D)×Net_{n} is defined by the following axiom and inference rule:

(X_{1}^{e_{1}} | … | X_{n}^{e_{n}}) ⟶^{ϵ(d)} (X_{1}^{e_{1}+d} | … | X_{n}^{e_{n}+d}) ; \frac{X_{i}^{e_{i}} ⟶^{a} X′_{i}}{(X_{1}^{e_{1}} | … | X_{i}^{e_{i}} | … | X_{n}^{e_{n}}) ⟶^{a} (X_{1}^{e_{1}} | … | X′_{i} | … | X_{n}^{e_{n}})}

Thus, in a network, the regular components synchronizes on delay transitions and interleaves on action transitions. We shall use \overline{P} , \overline{Q}, … to range over Net_{n} for arbitrary n.

Example 2.3 Consider the following equation system for the two variables X and Y:

X =^{def} ϵ(1).a Y =^{def} b

Applying the operational semantics for networks yields the following transition sequence of X | Y:

X | Y ⟶^{ϵ( \frac{1}{2} )} (ϵ(\frac{1}{2}).a | b) ⟶^{b} (ϵ(\frac{1}{2}).a | nil) ⟶^{ϵ( \frac{1}{2} )} (a | nil) ⟶^{a} (nil | nil)

□

The properties of time determinism and time continuity (see proposition 2.2) also hold for networks. However, the persistency property only holds in the following weaker form:

Proposition 2.4 1. (Persistency) If \overline{P} ⟶^{a} \overline{Q} and \overline{P} ⟶^{ϵ(d)} \overline{P}′ then \overline{P}′ ⟶^{a} \overline{Q}′ for some \overline{Q}′.

2.2 (Bi)simulation and Distinguishing Formulae

As networks semantically constitutes labelled transition systems we may compare them with respect to a number of behavioural relations such as bisimularity and similarity [Mil80, Par81]. Below we recall the definition of these classical notions:

Definition 2.5 Let T = ⟨S, A, ⟶⟩ be a labelled transition system. Then a simulation S is a binary relation on S such that whenever pSq and a ∈ A then the following holds:

Whenever p ⟶^{a} p′ then q ⟶^{a} q′ for some q′ with p′Sq′

We say that p is simulated by q (or q simulates p) whenever pSq for some simulation S. We write p ≤ q in this case. A binary relation B is a bisimulation if both B and B^{−1} ^{4} are simulations. We say that p and q are bisimilar if pBq for some bisimulation B in which case we write p ∼ q.

Example 2.6 Consider the union of the equation systems from Examples 2.1 and 2.3 (note the agreement with respect to the definition of X). Then the (unique) execution sequences demonstrated in the two examples clearly proves that X | Y ≁ Z and X | Y ≰ Z. ^{5} On the other hand it may be argued that Z ≤ X | Y by checking that the following collection of pairs constitutes a simulation:

{(Z^{e}, X^{e}|Y^{e}) | e ∈ R_{≥0}} ∪ {(Z_{b}^{e}, nil|Y^{e}) | e ∈ R_{≥0}} ∪
{(Z_{a}^{e}, X^{e}|nil) | e ∈ R_{≥0}} ∪ {(X^{e}, X^{e′}|nil) | e′ < e ∈ R_{≥0}} ∪
{(nil, nil|nil)}
□

4B^{−1} = {(q, p) | (p, q) ∈ B}.

5Strictly speaking we are comparing networks from two different transition systems, namely:

Net_{1} and Net_{2}. However, the notion of (bi)simularity may be applied to states of different transition systems by first forming their (disjoint) union.

The above example illustrates two cases of non–(bi)similar networks. Ideally, an automatic verification tool should not only report this fact but also provide explanations as to why there is a lack of (bi)similarity. The well known Hennessy– Milner Logic [HM85] provides the key to such explanations:

Definition 2.7 The formulas of Hennessy–Milner Logic, M, are given by the following abstract syntax:

F ::= tt | F ∧ G | ¬F | ⟨σ⟩F

where σ ranges over actions and delays, i.e. the set A ∪ D. Also, let L denotes the set of negation free formulae.

We interpret Hennessy–Milner Logic relative to the labelled transition system for networks, N_{n}. I.e. we define a satisfaction relation ⊧ between networks (Net_{n}) and formulae (M). For propositional constructs the definition is straightforward, and for the modality, we define:

\overline{P} ⊧ ⟨a⟩F ⇔ ∃\overline{P}′.\overline{P} ⟶^{a} \overline{P}′ ∧ \overline{P}′ ⊧ F

Now let M(\overline{P}) be the set of properties satisfied by \overline{P}. Also, let L(\overline{P}) be the set of negation free properties satisfied by \overline{P}. Then the following characterization result [HM85] shows that Hennessy–Milner Logic can be applied for explanations:

Theorem 2.8 Let \overline{P} and \overline{Q} be networks. Then \overline{P} ∼ \overline{Q} if and only if M(\overline{P}) = M(\overline{Q}). Also, \overline{P} ≤ \overline{Q} if and only if L(\overline{P}) ⊆ L(\overline{Q}). ^{6} □

Example 2.9 Consider the networks X | Y and Z from Example 2.6. The facts that X | Y ≁ Z and X | Y ≰ Z are both “explained” by the formula ⟨ϵ(\frac{1}{2})⟩⟨b⟩⟨ϵ(\frac{1}{2})⟩⟨a⟩tt, which is satisfied by X | Y but not by Z. □

3 Symbolic Processes

It is obvious that the standard semantics of networks is infinitary (even under quotient with bisimilarity and similarity); thus decidability of bisimularity and similarity between networks is beyond the standard algorithmic techniques for finite state systems. However, in [Č92] Čerāns presented a very clever algorithm for deciding timed bisimilarity for a class of parallel timer processes using the region–graph technique devised by Alur and Dill [AD90]. In the following we shall give a much simplified presentation of Čerāns’ algorithm for the very simple type of networks we are dealing with in this paper. Then in the next section we shall show how to extend the algorithm in order that distinguishing formulae may be generated.

6The theorem assumes that the labelled transition system satisfy a technical condition called image–finiteness; i.e. each state has only finitely many derivatives for each label. However, this condition is met by networks due to the property of Time Determinism.

3.1 Symbolic States

Given two networks:

\overline{X} = (X_{1} | … | X_{n}) and \overline{Y} = (Y_{1} | … | Y_{m})

over some equation system Δ and variables V their bisimilarity (or similarity) will be reduced to deciding a suitable property of an induced joint finite–state symbolic transition system, in which states represents sets of pairs of networks.

A symbolic state (of arity (n, m)) over Δ and V is a finite list:

ϕ = [(M_{1}, N_{1}), …, (M_{k}, N_{k})]

where M_{i} and N_{i} are multisets of {X^{l} | X ∈ V, l ∈ Nat} with | ⊎_{i} M_{i}| = m and | ⊎_{i} N_{i}| = n, and with M_{i} ⊎ N_{i} ≠ ∅ for i > 1. ϕ is said to be interior in case M_{1} ⊎ N_{1} = ∅ and boundary otherwise.

A symbolic state ϕ = [(M_{1}, N_{1}), …, (M_{k}, N_{k})] represents a whole family of pairs of networks. More precisely, all pairs of the form:

((M_{1}^{v_{1}} | … | M_{k}^{v_{k}}) , (N_{1}^{v_{1}} | … | N_{k}^{v_{k}}))  (2)

where 0 = v_{1} < v_{2} < ⋯ < v_{k} < 1, and where for a multiset M = {X_{1}, … X_{j}} and e ∈ R_{≥0}, M^{e} = (X_{1}^{e} | … | X_{j}^{e}).

Now, call \overline{v} = (v_{1}, …, v_{k}) ∈ R_{≥0}^{k} well–ordered and fractional (W) if 0 = v_{1} < v_{2} < ⋯ < v_{k}. Then for ϕ = [(M_{1}, N_{1}), …, (M_{k}, N_{k})] a symbolic state and \overline{v} = (v_{1}, …, v_{k}) a well–ordered and fractional tuppel, ϕ(\overline{v}) = (ϕ_{1}(\overline{v}), ϕ_{2}(\overline{v})) denotes the pair in (2) ^{7}. Thus, the set of pairs represented by ϕ is

∥ϕ∥ = \{ϕ(\overline{v)} | \overline{v} ∈ W \}

As all delay–constants in the definitions of variables are integers it follows that ϕ_{1}(\overline{v}) and ϕ_{1}(\overline{v}′) (ϕ_{2}(\overline{v}) and ϕ_{2}(\overline{v}′)) are able to perform precisely the same actions for \overline{v} and \overline{v}′ being arbitrary well-ordered and fractional tuppels.

7We take advantage of the fact that | is commutative and associative wrt.. bisimilarity and similarity.

Example 3.1 Consider once more the union of the equation systems from Examples 2.1 and 2.3. Then the symbolic state [({X, Y }, {Z})] represents the single pair (X|Y, Z) and the symbolic state [(∅, ∅), ({X, Y }, {Z})] represents all pairs of the form (ϵ(1 − d).a|b, ϵ(1 − d).a.Z_{b} + ϵ(1 − d).b.Z_{a} + b.X), where 0 < d < 1. □

We let SS_{m,n} denote the set of symbolic states (of arity (m, n)) over Δ and V. Assuming that X is defined using (1) it is clear that the set {X^{l} | l ∈ Nat} is finite as X^{l} = X^{l′} for l, l′ ≥ max{e_{i} |i = 1 … n} (intuitively X^{l} will at some point become invariant under delay–transitions). Hence, it may be concluded that the set of symbolic states SS_{m,n} is indeed finite.

Moreover, it will follow from the following sections, that the pairs represented by a symbolic state ϕ are either all bisimilar or all non–bisimilar; i.e.:

∀\overline{v} ∈ W. ϕ_{1}(\overline{v}) ∼ ϕ_{2}(\overline{v}) or ∀\overline{v} ∈ W. ϕ_{1}(\overline{v}) ≁ ϕ_{2}(\overline{v})

What remains is to determine which symbolic states represents bisimilar pairs. In particular, in order to determine bisimilarity between two networks

\overline{X} = (X_{1} | … | X_{n}) and \overline{Y} = (Y_{1} | … | Y_{m})

we will apply the method to be presented to the following (initial) symbolic state:

ϕ_{\overline{X},\overline{Y}} = [(\{X_{1}, …, X_{n}\} , \{Y_{1}, …, Y_{m}\})]

3.2 Symbolic Semantics

In order to determine which symbolic states represent bisimilar pairs we provide in the following a symbolic semantics for SS_{m,n}. Thus, let ϕ = [(M_{1}, N_{1}), …, (M_{k}, N_{k})] be a symbolic state (of arity (n, m)), then ⟼_{1}, ⟼_{2} and ⟼^{w} are defined by the rules below:

\frac{X ⟶^{a} X′}{ϕ ⟼^{a}_{1} ⟨⟨(\{X′\} ⊎ M_{1}, N_{1}), …, (M_{i}′, N_{i}), …⟩⟩} M_{i} = M_{i}′ ⊎ \{X\}

\frac{Y ⟶^{a} Y′}{ϕ ⟼^{a}_{2} ⟨⟨(M_{1}, \{Y′\} ⊎ N_{1}), …, (M_{i}, N′_{i}), …⟩⟩} N_{i} = N_{i}′ ⊎ \{Y \}

ϕ ⟼^{w} [(∅, ∅), (M_{1}, N_{1}), …, (M_{k}, N_{k})] ϕ is boundary

ϕ ⟼^{w} [(M_{k}^{−1}, N_{k}^{−1}), (M_{2}, N_{2}), …, (M_{k−1}, N_{k−1})] ϕ is interior

where ⟨⟨…⟩⟩ denotes the list resulting from removing all airs (∅, ∅) from the original list (in order to ensure that the result of the transition is a symbolic state); we denote by ↪^{a}_{1} and ↪^{a}_{2} the two transition relations which are defined using the rules for ⟼^{a}_{1} and ⟼^{a}_{2} except that pairs of empty sets are not removed in the resulting “symbolic” state; finally, for M a multiset and d ∈ R_{>0}, M^{−d} = {X^{n+d} | X^{n} ∈ M}.

Example 3.2 Recall the definitions of Examples 2.1 and 2.3. Figure 1 illustrates (part of) the symbolic transition system for the initial symbolic state induced by the network pair X | Y and Z. Symbolic states are indicated by boxes with symbolic state tuples occurring just below their associated box. For additional information we have indicated inside the boxes the families of network pairs represented by the symbolic state. □

The close relationship between the (symbolic) semantics of a symbolic state and the (standard) semantics of the (pairs of) networks it represents are as follows:

Lemma 3.3 (Correspondence)

1. Whenever ϕ ⟼^{a}_{1} ϕ′ and (\overline{P} , \overline{Q}) ∈ ∥ϕ∥, then for some \overline{P}′, \overline{P} ⟶^{a} \overline{P}′ such that (\overline{P}′, \overline{Q}) ∈ ∥ϕ′∥;

2. Whenever (\overline{P} , \overline{Q}) ∈ ∥ϕ∥ and \overline{P} ⟶^{a} \overline{P}′ then for some ϕ′, ϕ ⟼^{a}_{1} ϕ′ with (\overline{P}′, \overline{Q}) ∈ ∥ϕ′∥;

3. Whenever ϕ ⟼^{w} ϕ′ and (\overline{P} , \overline{Q}) ∈ ∥ϕ∥ then for some d ∈ R_{>0}, (\overline{P}^{d}, \overline{Q}^{d}) ∈ ∥ϕ′∥ ^{8};

4. Whenever (\overline{P} , \overline{Q}) ∈ ∥ϕ∥ then for all d ∈ R_{>0} there exists ϕ′ such that

ϕ(⟼^{w})^{∗}ϕ′ with (\overline{P}^{d}, \overline{Q}^{d}) ∈ ∥ϕ′∥;

Obviously, Lemma 3.3 1 and 2 may be dualised with ⟼_{2} replacing ⟼_{1}.

3.3 Symbolic Bisimulation

We may now define the notion of symbolic simulation and bisimulation:

Definition 3.4 B ⊆ SS_{m,n} is a symbolic simulation if whenever ϕ ∈ B and a ∈ A the following holds:

8Here \overline{P}^{d} denotes the unique network such that \overline{P} ⟶^{ϵ(d)} \overline{P}^{d}

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; 2; 1; 1; 2; X | Y; Z; w; [({X, Y }, {Z})]; 0 < d < 1; ϵ(1 − d).a.Z_{b} + ϵ(1 − d).b.Z_{a} + b.X; [(∅, ∅), ({X, Y }, {Z})]; b; b; 0 < d < 1; ϵ(1 − d).a; X; w; [({nil}, {X}), ({X}, {∅})]; 0 < e < d < 1; ϵ(1 − d).a; ϵ(1 − e).a; w; [(∅, ∅), ({nil}, {X}), ({X}, {∅})]; a; a; a; 0 < e < 1; [({a}, {∅}), ({nil}, {X})]; ϵ(1 − d).a | b; ϵ(1 − e).a]

Figure 1: Part of the symbolic transition system induced by X | Y and Z.

1. Whenever ϕ ⟼^{a}_{1} ϕ′ then ϕ′ ⟼^{a}_{2} ϕ′′ for some ϕ′′ with ϕ′′ ∈ B,

2. Whenever ϕ ⟼^{w} ϕ′ then ϕ′ ∈ B

If in addition B satisfies the following condition:

3. Whenever ϕ ⟼^{a}_{2} ϕ′ then ϕ′ ⟼^{a}_{1} ϕ′′ for some ϕ′′ with ϕ′′ ∈ B

B is a symbolic bisimulation. We write ϕ ∈≤_{s} whenever ϕ is contained in some symbolic simulation. Similarly we write ϕ ∈∼_{s} whenever ϕ is contained in some symbolic bisimulation.

As SS_{m,n} is finite–state and both ≤_{s} and ∼_{s} are maximal fixedpoints of simple monotonic functions on sets of symbolic states (which constitutes a complete finite lattice with respect to set inclusion) it follows from standard techniques (iterative, local, on–the–fly, etc.) that questions of the form ϕ ∈≤_{s} and ϕ ∈∼_{s} are decidable. Moreover, using the previous Correspondence Theorem 3.3 the following close relationships between (ordinary) (bi)simulation and the symbolic counterparts may be easily established:

Theorem 3.5 Let ≪ be either ≤ or ∼. Then whenever \overline{P} ≪ \overline{Q} and (\overline{P} , \overline{Q}) ∈ ∥ϕ∥ then ϕ ∈≪_{s}. Also, whenever ϕ ∈≪_{s} and (\overline{P} , \overline{Q}) ∈ ∥ϕ∥ then \overline{P} ≪ \overline{Q}.

It follows that in order to decide whether two networks \overline{X} and \overline{Y} are (bi)similar we may alternatively decide whether the initial symbolic state ϕ_{\overline{X},\overline{Y}} is a member of the symbolic (bi)simulation.

Example 3.6 Using the definition of symbolic (bi)similarity it follows clearly from Figure 1 and Theorem 3.5 that X | Y ≁ Z and X | Y ≰ Z. □

4 Pointed Symbolic Processes

The previous section provides a finite symbolic semantics based on which (bi)similarity between networks can be decided. However, the semantics has completely abstracted away from all time–quantities, and it is not possible to synthesize distinguishing formulae (and in particular not the time–quantities of modalities) based on this semantics. Therefore, we provide in this section a more informative yet still (sufficiently) finitary pointed symbolic semantics with explicit information of time–quantities. We show that this semantics provides the basis for an algorithm constructing distinguishing formulae (an algorithm which in fact has been implemented in the Epsilon tool [ČGL93]).

4.1 Pointed Symbolic States and Semantics

A pointed symbolic state (of arity (m, n) and over Δ and V) is a pair ⟨ϕ, \overline{v}⟩, where ϕ is a symbolic state and \overline{v} is a (corresponding) well–ordered fractional. We denote by PSS_{m,n} the set of all pointed symbolic states (of arity (m, n) and over Δ and V). Observe that PSS_{m,n} in contrast to SS_{m,n} is infinite (in fact uncountable).

A pointed symbolic state ⟨ϕ, \overline{v}⟩ represents both the family of network pairs represented by ϕ, i.e. ∥ϕ∥, as well as the particular network pair pointed out by \overline{v}, i.e. ϕ(\overline{v}).

The symbolic semantics of PSS_{m,n} refines that of SS_{m,n} in that symbolic wait (w) transitions are parameterized explicitly with time–quantities in order to capture precisely the corresponding delay transition between the represented networks.

Before giving the symbolic semantics of PSS_{m,n} we need some notation for well– ordered and fractional tuples: for \overline{v} = (v_{1}, …, v_{k}) ∈ W we define \overline{v}^{∗} = (1 − v_{k}), next_{B}(\overline{v}) = (0, v_{1} + (\frac{\overline{v}^{∗}}{2} ) , …, v_{k} + (\frac{\overline{v}^{∗}}{2} )) and next_{I}(\overline{v}) = (0, v_{1} + \overline{v}^{∗}, …, v_{k−1} + \overline{v}^{∗}). Note that the tuples next_{B}(\overline{v}) and next_{I}(\overline{v}) are well–ordered and fractional.

Now let ⟨ϕ, \overline{v}⟩ ∈ PSS_{m,n}. Then the ⟹_{1}, ⟹_{2} and ⟹^{w(d)} transition relations are defined by the rules below:

\frac{ϕ ↪^{a}_{1} ϕ′}{⟨ϕ, \overline{v}⟩ ⟹^{a}_{1} ⟨⟨ϕ′, \overline{v}⟩⟩}

\frac{ϕ ↪^{a}_{2} ϕ′}{⟨ϕ, \overline{v}⟩ ⟹^{a}_{2} ⟨⟨ϕ′, \overline{v}⟩⟩}

\frac{ϕ ⟼^{w} ϕ′}{⟨ϕ, \overline{v}⟩ ⟹^{w(\overline{v}^{∗}/2)} ⟨ϕ′, next_{B}(\overline{v})⟩} ϕ is boundary

\frac{ϕ ⟼^{w} ϕ′}{⟨ϕ, \overline{v}⟩ ⟹^{w(\overline{v}^{∗})} ⟨ϕ′, next_{I}(\overline{v})⟩} ϕ is interior

where ⟨⟨ϕ, \overline{v}⟩⟩ denotes the pointed symbolic state resulting from removing all pairs (∅, ∅) from ϕ and at the same time removing the corresponding component v_{i} from \overline{v}.

Example 4.1 Figure 2 illustrates (part) of the pointed symbolic transition system for the initial pointed symbolic state induced by the network pair X | Y and Z. Pointed symbolic states are indicated by boxes with pointed symbolic state pairs occurring just below their associated box. For additional information we indicate inside a box the network pair represented by the pointed symbolic state. □

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}2 1 1 2 X | Y Z  w(\frac{1}{2}) ϵ(1 − d).a.Z_{b} + ϵ(1 − d).b.Z_{a} + b.X bb ϵ(1 − d).a w(\frac{1}{4}) ϵ(1 − d).a ϵ(1 − e).a X a  a w(\frac{1}{4}) a  d = \frac{1}{2} d = \frac{1}{2} e = \frac{1}{4}, d = \frac{3}{4} e = \frac{1}{4} [(\{X, Y \}, \{Z\})] (0) [(∅, ∅), (\{X, Y \}, \{Z\})] (0, \frac{1}{2}) [(\{nil\}, \{X\}), (\{X\}, \{∅\})] (0, \frac{1}{2}) [(∅, ∅), (\{nil\}, \{X\}), (\{X\}, \{∅\})] (0, \frac{1}{4}, \frac{3}{4}) [(\{a\}, \{∅\}), (\{nil\}, \{X\})] (0, \frac{1}{2}) ϵ(1 − d).a | b ϵ(1 − e).a

Figure 2: Part of the pointed symbolic transition system induced by X | Y and Z.

Though PSS_{m,n} is an infinite set the above symbolic semantics is finitary in the following important sense: the total set of immediate ⟹–derivatives of any pointed symbolic state ⟨ϕ, \overline{v}⟩ is finite! In particular, for each pair ⟨ϕ, \overline{v}⟩ there is a unique d, ϕ′ and \overline{v}′ for which ⟨ϕ, \overline{v}⟩ ⟹^{w(d)} ⟨ϕ′, \overline{v}′⟩ (in contrast to the standard semantics) ^{9}. As we shall see this will enable the pointed symbolic semantics to be used for algorithmically generating distinguishing formulae.

The following Correspondence Lemma shows that the pointed symbolic semantics indeed is an extension of the symbolic semantics from the previous section:

Lemma 4.2 (Correspondence)

1. Whenever (\overline{P} , \overline{Q}) = ϕ(\overline{v}) and \overline{P} ⟶^{a} \overline{P}′ then for some ϕ′ and \overline{v}′, ⟨ϕ, \overline{v}⟩ ⟹^{a}_{1} ⟨ϕ′, \overline{v}′⟩ with (\overline{P}′, \overline{Q}) = ϕ′(\overline{v}′).

2. Whenever ⟨ϕ, \overline{v}⟩ ⟹^{a}_{1} ⟨ϕ′, \overline{v}′⟩ then ϕ_{1}(\overline{v}) ⟶^{a} ϕ′(\overline{v}′) and ϕ_{2}(\overline{v}) = ϕ_{2}(\overline{v}′).

3. Whenever ϕ ⟼^{w} ϕ′ then for all \overline{v}, ⟨ϕ, \overline{v}⟩ ⟹^{w(d)} ⟨ϕ′, \overline{v}′⟩ for some \overline{v}′ and d.

4. Whenever ⟨ϕ, \overline{v}⟩ ⟹^{w(d)} ⟨ϕ′, \overline{v}′⟩ then ϕ_{1}(\overline{v}) ⟶^{ϵ(d)} ϕ′_{1}(\overline{v}′), ϕ_{2}(\overline{v}) ⟶^{ϵ(d)} ϕ′_{2}(\overline{v}′) and

ϕ ⟼^{w} ϕ′.

Obviously, clause 1 and 2 have analogous counterparts for ⟹_{2}.

4.2 Pointed Symbolic Bisimulation

Definition 4.3 B ⊆ PSS_{m,n} is a pointed symbolic simulation if whenever ⟨ϕ, \overline{v}⟩ ∈ B, a ∈ A and d ∈ R_{>0} the following holds:

1. Whenever ⟨ϕ, \overline{v}⟩ ⟹^{a}_{1} ⟨ϕ′, \overline{v}′⟩ then ⟨ϕ′, \overline{v}′⟩ ⟹^{a}_{2} ⟨ϕ′′, \overline{v}′′⟩ for some ϕ′′ and \overline{v}′′

with ⟨ϕ′′, \overline{v}′′⟩ ∈ B,

2. Whenever ⟨ϕ, \overline{v}⟩ ⟹^{w(d)} ⟨ϕ′, \overline{v}′⟩ then ⟨ϕ′, \overline{v}′⟩ ∈ B

If in addition B satisfies the following condition:

3. Whenever ⟨ϕ, \overline{v}⟩ ⟹^{a}_{2} ⟨ϕ′, \overline{v}′⟩ then ⟨ϕ′, \overline{v}′⟩ ⟹^{a}_{1} ⟨ϕ′′, \overline{v}′′⟩ for some ϕ′′ and \overline{v}′′

with ⟨ϕ′′, \overline{v}′′⟩ ∈ B

and \{⟨ϕ′, \overline{v}′⟩ | ∃d ∈ R_{>0}.⟨ϕ, \overline{v}⟩ ⟹^{w(d)} ⟨ϕ′, \overline{v}′⟩\}.

9The set of derivatives of ⟨ϕ, \overline{v}⟩ is the union of the sets \{⟨ϕ′, \overline{v}′⟩ | ∃a.∃i.⟨ϕ, \overline{v}⟩ ⟹^{a}_{i} ⟨ϕ′, \overline{v}′⟩\}

B is a pointed symbolic bisimulation. We write ⟨ϕ, \overline{v}⟩ ∈≤_{ps} whenever ⟨ϕ, \overline{v}⟩ is contained in some pointed symbolic simulation. Similarly we write ⟨ϕ, \overline{v}⟩ ∈∼_{ps} whenever ⟨ϕ, \overline{v}⟩ is contained in some pointed symbolic bisimulation.

For B ⊆ SS_{m,n}, let B^{↑} = \{⟨ϕ, \overline{v}⟩ | ϕ ∈ B\}. Dually, for B ⊆ PSS_{m,n} let B^{↓} = \{ϕ | ⟨ϕ, \overline{v}⟩ ∈ B\}.

Lemma 4.4 Whenever B is a symbolic (bi)simulation then B^{↑} is a pointed symbolic (bi)simulation. Dually, whenever B is a pointed symbolic (bi)simulation then B^{↓} is a symbolic (bi)simulation. □

This leads directly to the following using the existing result of Theorem 3.5:

Theorem 4.5 ⟨ϕ, \overline{v}⟩ ∈≤_{ps} if and only if ϕ_{1}(\overline{v}) ≤ ϕ_{2}(\overline{v}). Also, ⟨ϕ, \overline{v}⟩ ∈∼_{ps} if and only if ϕ_{1}(\overline{v}) ∼ ϕ_{2}(\overline{v}). □

Thus, two networks \overline{X} and \overline{Y} are (bi)similar just in case the initial pointed symbolic state ⟨ϕ_{\overline{X},\overline{Y}} , (0)⟩ is a member of the pointed symbolic (bi)simulation. However, due to the infinite nature of PSS_{m,n} this does not directly lead to an alternative algorithm for (bi)similarity, a problem we will deal with in the following subsection.

4.3 Computing Distinguishing Formulae

In standard fashion we may define for n a natural number the n’th approximations of the various (pointed) symbolic relations (≤_{s}, ∼_{s}, ≤_{ps} and ∼_{ps}). The 0’th approximate is simply the entire set of (pointed) symbolic states, and the (n + 1)’th approximate is defined using the definition schemas of Definitions 3.4 and 4.3 with the n’th approximate substituting B in the (relevant) defining clauses. For ≡ one of the above four relations the corresponding n’th approximate will be denoted ≡^{n}. It is easy to see that in all four cases ≡^{n} will be decreasing in n. Also, in all four cases ≡^{n} approximates ≡ in the sense that ≡ equals the intersection of all its approximations (i.e. ≡= ∩_{n∈ω} ≡^{n}).

As the set of symbolic states is finite, there exists a K (being simply the number of symbolic states of the given arity) such that ≤_{s}^{n} and ∼_{s}^{n} will be constant when n exceeds K. This fact leads directly to an iterative algorithm for deciding ≤_{s} and ∼_{s} and hence — due to Theorem 3.5 — for deciding ≤ and ∼. In contrast, the set of pointed symbolic states is infinite and there is therefore no apriori guarantee that the decreasing sequences ⟨≤_{ps}^{n}⟩_{n} and ⟨∼_{ps}^{n}⟩_{n} will converge at any finite stage. However, finite convergence is ensured by the following Lemma relating symbolic and pointed symbolic approximates:

Lemma 4.6 For all n, (≤_{ps}^{n})^{↓} =≤_{s}^{n} and (≤_{s}^{n})^{↑} =≤_{ps}^{n}. Also, for all n, (∼_{ps}^{n})^{↓} =∼_{s}^{n} and (∼_{s}^{n})^{↑} =∼_{ps}^{n}.

Thus the pointed symbolic approximates converges at the same iteration as the symbolic counterparts. Furthermore, as any pointed symbolic state has only a finite (and computable) set of immediate derivatives, it follows that ≤_{ps}^{n} and ∼_{ps}^{n} are decidable for any n. Hence (bi)similarity between networks may alternatively be computed by deciding ≤_{ps}^{K}– (∼_{ps}^{K}–) membership problems for a sufficiently large K.

In addition, the use of pointed symbolic (bi)simulation enables the generation of distinguishing formulae in cases of non–(bi)similarity as stated by the following theorem. The proof given is constructive and constitutes the generation algorithm.

Theorem 4.7

1. Whenever ⟨ϕ, \overline{v}⟩ ∉≤_{ps} then ϕ_{1}(\overline{v}) ⊧ F and ϕ_{2}(\overline{v}) |̸= F for some F ∈ L.

2. Whenever ⟨ϕ, \overline{v}⟩ ∉∼_{ps} then ϕ_{1}(\overline{v}) ⊧ F and ϕ_{2}(\overline{v}) |̸= F for some F ∈ M.

Proof: We only give the proof of 2 (being slightly more involved). We proceed by induction in n, where ⟨ϕ, \overline{v}⟩ ∉∼_{ps}^{n}.

Basis: As ⟨ϕ, \overline{v}⟩ ∈∼_{ps}^{0} no distinguishing formula is required.

Induction Step: Assume ⟨ϕ, \overline{v}⟩ ∉∼_{ps}^{n+1}. There are three cases to consider depending on which of the conditions for membership of ∼_{ps}^{n+1} that fails:

Case 1: Assume ⟨ϕ, \overline{v}⟩ ⟹^{a}_{1} ⟨ϕ′, \overline{v}′⟩ but whenever ⟨ϕ′, \overline{v}′⟩ ⟹^{a}_{2} ⟨ϕ^{j}, \overline{v}^{j}⟩ (j =

1 … m) then ⟨ϕ^{j}, \overline{v}^{j}⟩ ∉∼_{ps}^{n}. Now, using the Induction Hypothesis we may conclude that there exists some formula F_{j} such that ϕ^{j}_{1}(\overline{v}^{j}) ⊧ F_{j} but ϕ^{j}_{2}(\overline{v}^{j}) |̸= F_{j}. Now, let F = ⟨a⟩(F_{1} ∧ … ∧ F_{m}) then it follows easily using the Correspondence Lemma 4.2 that ϕ_{1}(\overline{v}) ⊧ F whereas ϕ_{2}(\overline{v}) |̸= F. Case 2: Assume ⟨ϕ, \overline{v}⟩ ⟹^{w(d)} ⟨ϕ′, \overline{v}′⟩ but ⟨ϕ′, \overline{v}′⟩ ∉∼_{ps}^{n}. Now, using the Induction Hypothesis we may conclude that there exists a formula F′ such that ϕ′_{1}(\overline{v}′) ⊧ F′ but ϕ′_{2}(\overline{v}′) |̸= F′. Now let F = ⟨ϵ(d)⟩F′, then it follows from the Correspondence Lemma 4.2 that ϕ_{1}(\overline{v}) ⊧ F whereas ϕ_{2}(\overline{v}) |̸= F.

Case 3: Assume ⟨ϕ, \overline{v}⟩ ⟹^{a}_{2} ⟨ϕ′, \overline{v}′⟩ but whenever ⟨ϕ′, \overline{v}′⟩ ⟹^{a}_{1} ⟨ϕ^{i}, \overline{v}^{i}⟩ (i = 1 … l)

then ⟨ϕ^{i}, \overline{v}^{i}⟩ ∉∼_{ps}^{n}. Now, using the Induction Hypothesis we may conclude that there exists some formula F_{i} such that ϕ^{i}_{1}(\overline{v}^{i}) ⊧ F_{i} but ϕ^{i}_{2}(\overline{v}^{i}) |̸= F_{i}. Now, let F = ¬⟨a⟩(¬F_{1}∧…∧¬F_{l}) then it follows easily using the Correspondence Lemma 4.2 that ϕ_{1}(\overline{v}) ⊧ F whereas ϕ_{2}(\overline{v}) |̸= F. □

Example 4.8 Applying the construction of the above Theorem 4.7 to the pointed symbolic transition system induced by X | Y and Z (partially shown in Figure 2) we may generate the formula ⟨ϵ(\frac{1}{2})⟩⟨b⟩⟨ϵ(\frac{1}{4})⟩⟨ϵ(\frac{1}{4})⟩⟨a⟩tt distinguishing X | Y and Z. □

The construction of Theorem 4.7 has been implemented in the verification tool Epsilon which provides automatic computation of distinguishing formulae for a variety of equivalences and refinements (in particular time–abstracting and observational ones). The implementation uses the (efficient) local correctness checking described in [Lar92]. To give the reader some idea of the resulting implementation we offer below a very informal outline.

In checking the pointed symbolic (ps–) (bi)similarity of a pointed symbolic state ⟨ϕ, \overline{v}⟩ the implementation makes use of two datastructures: (1) a set B of symbolic states (assumed to be symbolic (bi)similar); and (2) a set N containing pointed symbolic states ⟨ϕ′, \overline{v}′⟩ paired with a formula F distinguishing the networks ϕ′_{1}(\overline{v}′) and ϕ′_{2}(\overline{v}′). Both B and N are initialized to the empty set ∅. Now, if either ϕ belongs to B or ⟨ϕ, \overline{v}⟩ occurs in N the algorithm terminates immediately (with success in the first case and failure in the latter). Otherwise, the assumption set B is augmented with ϕ and the (three) two conditions for ps–(bi)similarity (Definition 4.3) are checked one by one. For each condition all the relevant transitions for ⟨ϕ, \overline{v}⟩ are treated in turn. If all conditions turn out to be successful ⟨ϕ, \overline{v}⟩ is indeed ps–(bi)similar relative to B and N; otherwise ⟨ϕ, \overline{v}⟩ represents a non–(bi)similar pair of networks and is hence added to N together with a distinguishing formula obtained from the construction of the above proof — also the assumption set B is reset to its initial value (i.e. ϕ and all subsequently added symbolic states are (logically) removed from B).

In this paper we have described a constructive technique for generating diagnostic information for the timed bisimulation equivalence and the timed simulation preorder for a subclass of TCCS defined in [Wan90]. More precisely, given two networks of initially integral regular processes the technique will provide a logical formula in Hennessy–Milner Logic [HM85] that distinguishes them in case they are not timed (bi)similar. Our method may be seen as an extension of the algorithm by Čerāns for deciding timed bisimilarity in that information of time–quantities has been added sufficient for generating distinguishing formulae.

The technique devised in this paper generalizes straightforward to all of TCCS and moreover it generalizes easily to the modal extension of TCCS TMS defined in [ČGL93] in which a variety of equivalences and preorders is considered. The technique has been added to the automatic verification tool for TMS, Epsilon, and it has been applied in the analysis and verification of a simple protocol using timing considerations in its retransmission strategy [GLS93].

References

[AD90] R. Alur and D. Dill. Automata for modelling real–time systems. In Automata, Languages and Programming: Proceedings of the 17th ICALP, LNCS 443. Springer-Verlag, 1990.

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

[BHK86] J. A. Bergstra, J. Heering, and P. Klint. Algebra of communicating processes. In CWI symposium on Mathematics and Computer Science, pages 89–138. North–Holland, 1986.

[CC92] Ufuk Celikkan and Rance Cleaveland. Diagnostic information for behavioral preorders. In Proceedings of CAV’92, volume 663 of Lecture Notes In Computer Science, Springer Verlag. Springer-Verlag, 1992.

[ČGL93] Kārlis Čerāns, Jens Chr. Godskesen, and Kim G. Larsen. Timed modal specifications — theory and tools. In Proceedings of CAV’93, 1993. To appear.

[Che91] Liang Chen. An interleaving model for real–time systems. Technical report, LFCS, University of Edinburgh, Scotland, 1991. Preliminary version.

[Cle90] R. Cleaveland. On automatically distinguishing inequivalent processes. In Proceedings of CAV’90, Lecture Notes In Computer Science, Springer Verlag. Springer-Verlag, 1990.

[CPS89] R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. Technical report, LFCS, University of Edinburgh, Scotland, 1989.

[DS89] Jim Davis and Steve Schneider. An introduction to timed CSP. Technical Report PRG–75, Oxford University Computing Laboratory, 1989.

[DV91] R. DeNicola and F.W. Vaandrager. Three logics for branching bisimulation (extended abstract). In Proceedings of Fifth Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 1991.

[GL92] J.C. Godskesen and K.G. Larsen. Real time calculi and expansion theorems. Lecture Notes In Computer Science, Springer Verlag, 1992. In Proceedings of FST-TCS’92. To appear.

[GLS93] Jens Chr. Godskesen, Kim G. Larsen, and Arne Skou. Automatic verification of real–timed systems using epsilon. Unpublished, December 1993.

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

[Hen88] M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.

[Hil87] M. Hillerström. Verification of CCS–processes. PhD thesis, Aalborg University Center, Denmark, 1987. R 87–27.

[HM85] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, pages 137–161, 1985.

[Hoa78] C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978.

[Kor91] Henri Korver. Computing distinguishing formulas for branching bisimulation. In Proceedings of CAV’91, volume 575 of Lecture Notes In Computer Science, Springer Verlag. Springer-Verlag, 1991.

[Lar92] K.G. Larsen. Efficient local correctness checking. lncs, 663, 1992.

[LMV88] V. Lecompte, E. Madelaine, and D. Vergamini. Auto: A verification system for parallel and communicating processes. INRIA, Sophia–Antipolis, 1988.

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

[Mil80] R. Milner. Calculus of Communicating Systems, volume 92 of Lecture Notes In Computer Science, Springer Verlag. Springer Verlag, 1980.

[NRSV90] X. Nicollin, J.-L. Richier, J. Sifakis, and J. Voiron. ATP: an algebra for timed processes. In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel, April 1990.

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

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

[Pol92] E.E. Polak. An efficient implementation of branching bisimulation and distinguishing formulae. Technical Report P9216, University of Amsterdam, 1992.

[RRSV87] J.L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Xesar: a tool for protocol validation. users’ guide. Technical report, LGI–IMAG, 1987.

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

[vG90] R.J. van Glabbeek. The linear time — branching time spectrum. In Proceedings of CONCUR’90, volume 458 of Lecture Notes In Computer Science, Springer Verlag. Springer-Verlag, 1990.

[vG92] R.J. van Glabbeek. The linear time — branching time spectrum II (the semantics of sequential systems with silent moves). In Proceedings of CON-CUR’92, volume 715 of Lecture Notes In Computer Science, Springer Verlag. Springer-Verlag, 1992.

[vGW89] R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). Information Processing 89, 1989.

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

[Wan91] Y. Wang. A Calculus of Real Time Systems. PhD thesis, Chalmers University of Technology, Göteborg, Sweden, 1991.

Recent Publications in the BRICS Report Series

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

RS-94-40 Luca Aceto and Anna Ing� olfsd� ottir. CPO Models for GSOS Languages � Part I: Compact GSOS Languages. December 1994. 70 pp. An extended abstract of the paper will appear in: Proceedings of CAAP ’95, LNCS, 1995.

RS-94-39 Ivan Damg� ard, Oded Goldreich, and Avi Wigderson. Hashing Functions can Simplify Zero-Knowledge Protocol Design (too). November 1994. 18 pp.

RS-94-38 Ivan B. Damg� ard and Lars Ramkilde Knudsen. Enhancing the Strength of Conventional Cryptosystems. November 1994. 12 pp.