Decidability and Completeness in Real Time Process Algebra

Liang Chen Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ, Scotland cl@lfcs.dcs.ed.ac.uk

Abstract

Time variables are introduced in real time process algebras to represent a notion of time dependency in real time systems. As values of time variables may be real numbers, even a simple finite process (a process which is not recursively defined) can have infinite derivatives. In this paper, we show that strong equivalence (the largest strong bisimulation) for finite processes in real time process algebras with time variables is still decidable. The decidability is independent of the choice of time domain, aloowing time to be discrete or dense. We also present a simple relativised compositional proof system for real time process algebras. The proof system allows us to derive statements of the form A ⊢ E = F, which means that if the first order formula A holds for any assignment of free time variables, then processes E and F are strong bisimilar under the same assignment. The proof system is again independent of the choice of time domain. We show its soundness for both discrete and dense time domains. We prove that the proof system is complete for finite processes over dense time domains. We also discuss how to restrict occurrences of time variables in time expressions such that the proof system is complete for the sublanguage over discrete time domains. Finally, we consider a possible extension of the proof system for recursively defined processes (infinite processes).

1 Introduction

Process algebras, such as CCS [16, 17], CSP [13] and ACP [3], are structured description languages for concurrent systems and have a variety of well developed semantics theories and verification methods. However, none of them consider temporal aspects of systems. Instead they deal with the quantitative aspects of time of systems in a qualitative way. There are many systems and applications for which purely qualitative specification and analysis are inadequate. The examples are real time systems in which the interactions with their environments must satisfy some hard time constraints.

Recently there are some attempts of incorporating time in the well developed process algebras [1, 6, 9, 12, 18, 22, 23, 19, 24] such that the temporal properties of systems can be explicitly formalised. In [1, 6, 9, 24], time variables or infinite choice operators have been introduced in order to express a notion of time dependency, which means that the time for some actions depends on the happening time of the previous actions. In general, real time process algebras with time variables or infinite choice operators are more expressive than those without them. In these real time process algebras, as time variables may have the real numbers as their values and infinite choice operators may be indexed by the real numbers, even a very simple finite process (a process which is not recursively defined) can have infinite derivatives. As an example, consider a process a(x)_{10}^{100}.E of [6]. The process can perform action a at any time t in the interval [10, 100] and after doing so it proceeds to act like process E{t/x}, where E{t/x} is the result of substituting all free occurrences of x in E by t. The behaviour of this latter process depends on the particular value of t, the happening time of action a, if x has free occurrences in process E.

We consider, in this paper, a general and simple real time process algebra, Timed CCS [6], which is an extension of Milner’s CCS with real time. There is no assumption about the underlying nature of time, allowing time to be discrete or dense. For example, we can have the set of nature numbers or the set of non-negative real numbers as the time domain. There is also no assumption of the Maximal Progress Principle. As the language allows time variables, it is very expressive. In this paper, we show that strong equivalence (the largest strong bisimulation) is still decidable for finite processes. The decidability is independent of the choice of the time domain, allowing time to be discrete or dense. We also present a relativised compositional proof system. The proof system is again independent of the choice of the time domain and is sound for both discrete and dense time domains. It is shown complete for finite processes over dense time domains, but complete only for a sublanguage over discrete time domains.

In Section 2, we present the formal syntax and semantics of Timed CCS. The semantics is given by a labelled transition system in the style of Plotkin’s structural operational semantics. In Section 3, we generalize the notion of bisimulation to timed processes and study the properties of strong equivalence. To show the decidability of strong equivalence over discrete time domains as well as dense time domains, we construct in Section 4 a characteristic formula W C(E, F) for E and F, called the weakest condition for E to be bisimilar to F. In Section 5, we present a sound proof system for strong equivalence. We show completeness of the proof system over dense time domains and discuss how to restrict occurrences of time variables in time expressions such that the proof system is complete for the restricted language over discrete time domains. A comparison with related work and conclusion are made in section 6.

2 Timed CCS: its Syntax and Semantics

Timed CCS is an extension of Milner’s CCS [16, 17] with time. To define it, we presuppose a countable set of names Λ, ranged over by a, b, of atomic actions not containing τ. Let Act = Λ∪{τ}, ranged over by α, β. As in CCS, Λ can be partitioned into Γ, the set of names, and \overline{Γ} = \{ā |a ∈ Γ\}, the set of co-names, with the provision that ¯ ā = a. Actions a and ā are called complementary actions which form the basis of communications in the language, analogous to CCS. We also presuppose an infinite set V_{t} of time variables, ranged over by x, y, z. Let the time domain be (T ∪ {∞}, ≤), where T contains a least element 0 to represent the starting time and ≤ is a linear order over T . There is no assumption about the underlying nature of time, allowing T , for example, to be ℵ (the set of natural numbers), or ℜ^{≥0} (the set of non-negative reals). Symbol ∞ is introduced to represent infinite time, where ∞ ∉ T , and time expressions, ranged over by e, f, g, are defined as follows:

Definition 2.1

1 For any u ∈ T and x ∈ V_{t}, u and x are time expressions.

2 For every u ∈ T and time expression e, u × e is a time expression.

3 If e and f are time expressions, then e + f, e ˙−f, max(e, f) and min(e, f) are all time expressions, where e ˙−f represents the conditional expression if e < f then 0 else (e − f).

By convention, for any time expression e, we have e ≤ ∞, ∞ ∘ e = ∞, max(e, ∞) = ∞ and min(e, ∞) = e, where ∘ is + or ˙−. We will write e′ − e in place of e′ ˙−e whenever e ≤ e′. Remark The decidability result of Section 4 will justify our decisions in the choice of time expressions. □

Process expressions of Timed CCS, ranged over by E, F, are defined by the following BNF expression, where S : Act ⟶ Act is a relabelling function which satisfies \overline{S(a)} = S(ā) and S(τ) = τ.

E ::= nil | α(x)_{e}^{e′}. E | E + F | E | F | E\a | F [S]

where e′ is a time expression or ∞.

All processes defined by the above BNF expression are finite processes. In Section 5.4, we will discuss recursively defined processes (infinite processes).

Process nil cannot do any action, but idles indefinitely. Prefix α(x)_{e}^{e′}. E represents a process which performs action α at any time t between e and e′ (inclusive), where e and e′ are called the lower bound and upper bound of action α, respectively. After doing so, it evolves to process E{t/x}, where E{t/x} represents the result of substituting all free occurrence of x in E by t. Note that only the upper bounds are allowed to be the infinite time ∞ and therefore α(x)_{∞}^{100.05}. nil is not a process. The prefix operator α(x)_{e}^{e′} in α(x)_{e}^{e′}. E binds all free occurrences of time variable x in E. This gives, in the usual sense, the notions of free and bound occurrences of time variables. We use fv_{t}(E) to represent the set of all free time variables occurring in E. We identify those process expressions which are the same up to changes of bound time variables. Agents, ranged over by P, Q, are processes which have no free time variable.

Summation E +F represents choice between processes E and F. The choice is made at the time of the first action of E or F, or at the time when only one process can idle (in this case the process which cannot delay is dropped from the future computation). Clearly the choice is deterministic with respect to time proceeding. Process E | F represents the parallel composition of processes E and F. Each of them may perform actions independently, or they may synchronise on complementary actions which represent communications between them. Parallel composition is synchronous with respect to time proceeding, i.e. the parallel composition E | F can delay time u only when both E and F can.

The operational semantics of Timed CCS is defined by a labelled transition system

(P, {⟶^{(α,t)} : (α, t) ∈ (Act ∪ {ϵ}) × T })

where P is the set of agents and ϵ ∉ Act. For convenience, we will write P ⟶^{α}_{t}P′ in place of (P, P′) ∈ ⟶^{(α,t)}, where α ∈ Act, and P ⟶_{t}P′ in place of (P, P′) ∈ ⟶^{(ϵ,t)}.

Transition P ⟶^{α}_{t}P′ is read as that agent P performs action α at time t and after doing so it evolves to P′. Transition P ⟶_{t}P′ means that agent P idles up to time t without any action and then evolves to P′.

To define the transition rules, we first define Moller and Tofts’ maximal delay time of processes before any action [18].

Definition 2.2

\begin{matrix}(1) |nil|_{T} = ∞ & (4) |P | Q|_{T} = min(|P |_{T} , |Q|_{T}) \\ (2) |α(x)_{e}^{e′}. P |_{T} = e′ & (5) |P \a|_{T} = |P |_{T} \\ (3) |P + Q|_{T} = max(|P |_{T} , |Q|_{T}) & (6) |P [S]|_{T} = |P |_{T} \end{matrix}

All transition rules of the language are presented in Table 1. The rules are given in the natural deduction style which are read as follows: if the transition or transitions above the inference line can be inferred, then we can infer the transition below the line.

For convenience, we introduce a notation δ to represent a dead process (a(x)_{0}^{0}. nil)\a. Intuitively, the dead process δ neither performs any action nor idles. We also define some derived operators which will be used in the sequel. The first derived operator is the time prefix (e)E of [18].

Definition 2.3

- (e)nil = nil

- (e)(a(x)_{f}^{f′}. E) = a(x)_{f+e}^{f′+e}. (E{x − e/x}) where x ∉ fv(e)

- (e)(E + F) = (e)E + (e)F

- (e)(E | F) = (e)E | (e)F

\overline{α(x)_{v}^{v′}. P ⟶^{α}_{t}P \{t/x\}} (v ≤ t ≤ v′)

\overline{α(x)_{v}^{v′}. P ⟶_{t}α(x)_{v ˙−t}^{v′−t}. (P \{t + x/x\})} (t ≤ v′)

\overline{nil⟶_{t}nil}  \frac{P ⟶_{t}P′  Q⟶_{t}Q′}{P + Q⟶_{t}P′ + Q′}
\frac{P ⟶_{t}P′}{P + Q⟶_{t}P′}  (|Q|_{T} < t)  \frac{Q⟶_{t}Q′}{P + Q⟶_{t}Q′}  (|P |_{T} < t)
\frac{P ⟶^{α}_{t}P′}{P + Q⟶^{α}_{t}P′}  \frac{Q⟶^{α}_{t}Q′}{P + Q⟶^{α}_{t}Q′}
\frac{P ⟶_{t}P′  Q⟶_{t}Q′}{P | Q⟶_{t}P′ | Q′}  \frac{P ⟶^{a}_{t}P′  Q⟶^{ā}_{t}Q′}{P | Q⟶^{τ}_{t}P′ | Q′}
\frac{P ⟶^{α}_{t}P′  Q⟶_{t}Q′}{P | Q⟶^{α}_{t}P′ | Q′}  \frac{P ⟶_{t}P′  Q⟶^{α}_{t}Q′}{P | Q⟶^{α}_{t}P′ | Q′}
\frac{P ⟶_{t}P′}{P \a⟶_{t}P′\a}  \frac{P ⟶^{α}_{t}P′}{P \a⟶^{α}_{t}P′\a}  (α ≠ a ∧ α ≠ ā)
\frac{P ⟶_{t}P′}{P [S]⟶_{t}P′[S]}  \frac{P ⟶^{α}_{t}P′}{P [S]⟶^{S(α)}_{t}P′[S]}

Table 1: Operational Rules for Timed CCS - (e)(E\a) = ((e)E)\a

- (e)(E[S]) = ((e)E)[S]

Intuitively, (e)E represents a process which, after a delay of time e, has the same behaviour as process E.

Note that ∞ is not a time expression and therefore (∞)δ is not a process. However, for convenience, we will allow ourselves to write (∞)δ as syntactically identical to the process nil in the rest of the paper.

The second derived operator is time shift which is the relative version of that of [1].

Definition 2.4 - e >> nil = nil

- e >> (α(x)_{f}^{f′}. E) = α(x)_{(f.–e)+(max(e,f′)−f′)}^{f′.–e}. (E{e + x/x}) where x ∉

fv(e)

- e >> (E + F) = e >> E + e >> F

- e >> (E | F) = e >> E | e >> F

- e >> (E\a) = (e >> E)\a

- e >> (E[S]) = (e >> E)[S]

Informally, for any process E, if e ≤ |E|_{T}, then e >> E represents a state of E after a delay of time e without any action. If e > |E|_{T}, then e >> E represents the dead process δ. Note the subtlety in the definition of e >> (α(x)_{f}^{f′}. E. It ensures the lower bound (f .– e) + (max(e, f′) − f′) > 0 whenever f′ ≤ e.

3 Strong Bisimulation and its Properties

We do not wish to distinguish agents which, in some sense, have the same behaviours. The notion of bisimulation between agents captures the idea of having the same behaviours. We say two agents are not equivalent if a distinction can be detected by an experimenter who interacts with each of them.

Definition 3.1 A binary relation R over agents is a strong T -bisimulation if (P, Q) ∈ R implies that for all α ∈ Act and u ∈ T

(1) if P ⟶^{α}_{u}P′, then there is a Q′ such that Q⟶^{α}_{u}Q′ and (P′, Q′) ∈ R.

(2) if Q⟶^{α}_{u}Q′, then there is a P′ such that P ⟶^{α}_{u}P′ and (P′, Q′) ∈ R.

(3) |P |_{T} = |Q|_{T}.

Two agents P and Q are strongly bisimilar, written as P ∼ Q, if there is a strong T -bisimulation R such that (P, Q) ∈ R.

It is easy to see that ∼ itself is a strong T -bisimulation, the largest T - bisimulation. Moreover, ∼ is an equivalence relation, which is called strong equivalence.

Strong equivalence can be extended to any processes as follows: Definition 3.2 Given any processes E and F which contain at most free time variables x⃗ = (x_{1}, …, x_{n}), we say E ∼ F if for any t⃗ ∈ T^{n}, E{t⃗/x⃗} ∼ F {t⃗/x⃗}.

All following laws can be proved in a standard way by demonstrating appropriate strong T -bisimulations. We omit their proofs, which are mostly straightforward and tedious. Proposition 3.3 (Laws for Prefix) 1 a(x)_{e}^{e′}. E ∼ a(y)_{e}^{e′}. (E{y/x}) y is free for x in E 2 a(x)_{e}^{e′}. E ∼ (e′)δ e > e′ 3 a(x)_{e}^{e′}. E ∼ a(x)_{e}^{e′}. E + (e′)δ 4 a(x)_{e}^{f}. E + a(x)_{f}^{e′}. X ∼ a(x)_{e}^{e′}. E e ≤ f ≤ e′

Property (1) shows that α-conversion preserves strong equivalence. By (2), we know that timing may also block actions. For example, the agent a(t)_{10}^{5}. nil cannot perform action a, but idles time 5 before dies. Proposition 3.4 (Laws for Summation) 1 E + δ ∼ E 2 E + E ∼ E 3 E + F ∼ F + E 4 E + (F + G) ∼ (E + F) + G

The above laws together just say that (E, +, δ) is a monoid, where E is the set of all processes. Proposition 3.5 (Laws for Restriction) 1 nil\a ∼ nil 2 (α(x)_{e}^{e′}. E)\a ∼ α(x)_{e}^{e′}. (E\a) α ≠ a ⋀ α ≠ ā 3 (α(x)_{e}^{e′}. E)\a ∼ (max(0, e′))δ α = a ⋁ α = ā 4 (E + F)\a ∼ E\a + F \a Proposition 3.6 (Laws for Relabelling)

1 ((e)δ)[S] ∼ (e)δ 2 (α(x)_{e}^{e′}. E)[S] ∼ (S(α))(x)_{e}^{e′}. (E[S]) 3 (E + F)[S] ∼ E[S] + F [S]

To simplify a presentation of expansion law, we introduce a notion of normal forms. Definition 3.7 A process E ≡ ∑_{i∈I} a_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ is in normal form if for any i ∈ I, e′_{i} ≤ e and E_{i} is also in normal form. Proposition 3.8 (Expansion Law) Given

E ≡ ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ and F ≡ ∑_{j∈J} β_{j}(y_{j})_{f_{j}}^{f′_{j}}. F_{j} + (f)δ

which are both in normal form, we have E | F ∼

∑_{i∈I} α_{i}(z_{i})_{e_{i}}^{min(e_{i},f)}. (E_{i}{z_{i}/x_{i}} | z_{i} >> F)

+

∑_{j∈J} β_{j}(z_{j})_{f_{j}}^{min(f′_{j},e)}. (z_{j} >> E | F_{j}{z_{j}/y_{j}})

+

∑_{j∈J^{i∈I}^{a_{i}=b̄_{j}}} τ(z_{ij})_{max(e_{i},f_{j})}^{min(e′_{i},f′_{j})}. (E_{i}{z_{ij}/x_{i}} | F_{j}{z_{ij}/y_{j}})

+ (min(e, f))δ

where for any i ∈ I, j ∈ J, z_{i}, z_{j} and z_{ij} are some fresh time variables.

Strong equivalence is a congruence relation, i.e. it is substitutive under all operators. Proposition 3.9 For any processes E and F, E ∼ F implies

(1) α(x)_{e}^{e′}. E ∼ α(x)_{e}^{e′}. F  (4) E\a ∼ F \a
(2) E + G ∼ F + G  (5) E[S] ∼ F [S]
(3) E | G ∼ F | G

It is easy to see that for any process E, there is a process E′ which is in normal form such that E ∼ E′.

4 Decidability

A variety of equivalences have been proposed in the field of process theory in order to capture the behavioural aspects of processes. Various criteria exist for comparing the merits and deficiencies of these equivalences. One of the most important criteria is decidability.

For CCS, every finite process has only finite derivatives and therefore the decidability of strong equivalence for finite processes is straightforward. However for real time process algebras, as time may be dense, the situation is completely different. Even a very simple finite process can have infinite derivatives. In this section, we show that strong equivalence for finite processes in Timed CCS is still decidable and the decidability is independent of the choice of time domain.

4.1 Characteristic Formulas

For any processes E and F, we construct a formula W C(E, F), the characteristic formula of E and F, of the first-order theory over some structure such that E ∼ F if and only if W C(E, F).

Definition 4.1 For any processes E and F, which contain at most free time variables x⃗ = (x_{1}, …, x_{n}), and a formula A of the first order language, where A has at most free variables x_{1}, …, x_{n}, we say A is a condition for E to be bisimilar to F, written as A ⊧ E ∼ F, if for any t⃗ ∈ T^{n}, A{t⃗/x⃗} implies E{t⃗/x⃗} ∼ F {t⃗/x⃗}.

Definition 4.2 A formula A is said to be a weakest condition for E to be bisimilar to F if A ⊧ E ∼ F and for any formula B, B ⊧ E ∼ F implies B → A holds.

Proposition 4.3 If A is a weakest condition for E to be bisimilar to F, then

B ⊧ E ∼ F if and only if B → A

Proof: Straightforward. □

Corollary 4.4 If A and B are weakest conditions for E to be bisimilar to F, then A ↔ B holds.

We will identify formulas which are logically equivalent. With the above corollary, we have that if weakest conditions for E to be bisimilar to F exist, then they are unique up to this equality.

Now we show that for any processes E and F, the weakest condition for E to be bisimilar to F exists. We first consider the weakest condition W C(E, F) for E to be bisimilar to F, where E and F are both in normal form.

Definition 4.5 For any normal forms E and F, where

E ≡ ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ and F ≡ ∑_{j∈J} β_{j}(y_{j})_{f_{j}}^{f′_{j}}. F_{j} + (f)δ

let

W C(E, F) = ∧ e = f

∧ ⋀_{i∈I}(∀x.(e_{i} ≤ x ≤ e′_{i} → ⋁_{j∈J^{α_{i}=β_{j}}}(f_{j} ≤ x ≤ f′_{j} ∧ W C(E_{i}{x/x_{i}}, F_{j}{x/y_{j}}))))

∧ ⋀_{j∈J}(∀y.(f_{j} ≤ y ≤ f′_{j} → ⋁_{i∈I^{α_{i}=β_{j}}}(e_{i} ≤ y ≤ e′_{i} ∧ W C(E_{i}{y/x_{i}}, F_{j}{y/y_{j}}))))

We will show next that W C(E, F), where both E and F are in normal form, is the weakest condition for E to be bisimilar to F. We first show that W C(E, F) is a condition for E to be bisimilar to F.

Proposition 4.6 For any processes E and F, where both E and F are in normal form, W C(E, F) ⊧ E ∼ F.

Proof: Let E be ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ and F be ∑_{j∈J} β_{j}(y_{j})_{f_{j}}^{f′_{j}}. F_{j} + (f)δ. Suppose E and F contain at most free time variables z⃗ = (z_{1}, …, z_{n}). We proceed by induction on the maximum depth of E and F, where the depth d(E) of E is inductively defined as follows:

\begin{matrix}d((e)δ) = 0 & d(α(x)_{e}^{e′}. E) = 1 + d(E) \\ d(E + F) = max(d(E), d(F)) \end{matrix}

For any u⃗ = (u_{1}, …, u_{n}) ∈ T^{n}, we suppose W C(E, F){u⃗/z⃗} holds.

Firstly, E{u⃗/z⃗}⟶^{α}_{v}P, then there is i ∈ I such that α = α_{i}, e_{i}{u⃗/z⃗} ≤ v ≤ e′_{i}{u⃗/z⃗} and P ≡ E_{i}{u⃗/z⃗}{v/x_{i}}. By definition of W C(E, F), there is j ∈ J, such that β_{j} = α_{i}, f_{j}{u⃗/z⃗} ≤ v ≤ f′_{j}{u⃗/z⃗} and W C(E_{i}{u⃗/z⃗}{v/x_{i}}, F_{j}{u⃗/z⃗}{v/y_{j}}) holds. By induction, we have E_{i}{u⃗/z⃗}{v/x_{i}} ∼ F_{j}{u⃗/z⃗}{v/y_{j}} hold. Clearly

F {u⃗/z⃗}⟶^{β_{j}}_{v}F_{j}{u⃗/z⃗}{v/y_{j}}.

Similarly, F {u⃗/z⃗}⟶^{α}_{v}Q implies E{u⃗/z⃗}⟶^{α}_{v}P with P ∼ Q for some P.

Finally, e{u⃗/z⃗} = f{u⃗/z⃗}. Therefore E{u⃗/z⃗} ∼ F {u⃗/z⃗}. □

Now we show that W C(E, F), where E and F are both in normal form, is the weakest condition for E to be bisimilar to F. To do so we first prove the following lemma.

Lemma 4.7 For any processes E and F, where both E and F are in normal form, E ∼ F implies W C(E, F).

Proof: We only need to consider the case where both E and F are agents. Let E be ∑_{i∈I} α_{i}(x_{i})_{v_{i}}^{v′_{i}}. E_{i} + (v)δ and F be ∑_{j∈J} β_{j}(y_{j})_{w_{j}}^{w′_{j}}. F_{j} + (w)δ. Suppose E ∼ F. We proceed by induction on the maximum depth m of E and F. It is easy to see that E ∼ F implies d(E) = d(F).

Case m = 0. Then E must have form (v)δ and F must have form (w)δ. Clearly E ∼ F implies v = w.

Case m = m′ + 1.

(1) For any i ∈ I and u ∈ T , if v_{i} ≤ u ≤ v′_{i}, then E⟶^{α_{i}}_{u}E_{i}{u/x_{i}}. So

there is a j ∈ J such that F ⟶^{β_{j}}_{u}F_{j}{u/y_{j}} and F_{j}{u/y_{j}} ∼ E_{i}{u/x_{i}},

where α_{i} = β_{j} and w_{j} ≤ u ≤ w′_{j}. By induction, W C(E_{i}{u/x_{i}}, F_{j}{u/y_{j}}) holds.

(2) Similarly, for any j ∈ J and u ∈ T , w_{j} ≤ u ≤ w′_{j} implies that there is a i ∈ I such that v_{i} ≤ u ≤ v′_{i} and W C(E_{i}{u/x_{i}}, F_{j}{u/y_{j}}) holds.

(3) v = w.

Therefore W C(E, F) holds □

Proposition 4.8 For any formula A and processes E, F, where E and F are both in normal form, A ⊧ E ∼ F implies A → W C(E, F) holds.

Proof: Let E be ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ and F be ∑_{j∈J} β_{j}(y_{j})_{f_{j}}^{f′_{j}}. F_{j} + (f)δ. Suppose E and F contain at most time variables z⃗ = (z_{1}, …, z_{n}) and A ⊧ E ∼ F. For any u⃗ = (u_{1}, …, u_{n}) ∈ T^{n}, if A{u⃗/z⃗} holds, then E{u⃗/z⃗} ∼ F {u⃗/z⃗}. By Lemma 4.7, W C(E{u⃗/z⃗}, F {u⃗/z⃗}) holds. Hence A → W C(E, F) holds. □

Corollary 4.9 For any processes E, E′ and F, where E, E′ and F are all in normal form, if E ∼ E′ then W C(E, F) is logically equivalent to W C(E′, F).

Now we can consider characteristic formulas W C(E, F) for any processes E and F. Recall that for any process E, there is a process E′ such that E ∼ E′, where E′ is in normal form.

Definition 4.10 For any processes E and F, let W C(E, F) be W C(E′, F′), where both E′ and F′ are in normal form and satisfy E ∼ E′, F ∼ F′.

Clearly W C(E, F) is well defined. We will show next that W C(E, F) is the weakest condition for E to be bisimilar to F.

Proposition 4.11 For any processes E and F, W C(E, F) is the weakest condition for E to be bisimilar to F.

Proof: We first show that W C(E, F) is a condition for E to be bisimilar to F, i.e. W C(E, F) ⊧ E ∼ F holds. Suppose E and F contain at most free time variables x⃗ = (x_{1}, ⋯, x_{n}). Let E′ and F′ be normal forms such that E ∼ E′ and F ∼ F′. For any u⃗ ∈ T^{n}, suppose W C(E, F){u⃗/x⃗} holds. Then E′{u⃗/x⃗} ∼ F′{u⃗/x⃗}. So E{u⃗/x⃗} ∼ F {u⃗/x⃗} holds.

Now we suppose A ⊧ E ∼ F holds. We further assume A{u⃗/x⃗} holds, where u⃗ ∈ T^{n}. Then E{u⃗/x⃗} ∼ F {u⃗/x⃗}. So E′{u⃗/x⃗} ∼ F′{u⃗/x⃗} and therefore W C(E, F){u⃗/x⃗}. □

4.2 Decidability over Discrete Time Domains

In this section, we consider discrete time. Let T be ℵ, the set of natural numbers. We can define the following relations in the structure (ℵ, +):

(1) Zero ({m : m = 0}): ∀x(x + m = x)

(2) Ordering ({(m, n) : m ≤ n}): ∃x(m + x = n)

(3) Successor ({(m, n) : n = S(m)}):

∃x∀y¬(x = 0) ∧ (y = 0 ∨ x ≤ y) ∧ m + x = n

(4) Subtraction ({(l, m, n) : n = l ˙−m}): (l < m ∧ n = 0) ∨ (l ≥ m ∧ l = m + n)

(5) Max ({(l, m, n) : n = max(l, m)}): (l ≥ m ∧ n = l) ∨ (l < m ∧ n = m)

(6) Min ({(l, m, n) : n = min(l, m)}): (l ≥ m ∧ n = m) ∨ (l < m ∧ n = l)

For any time expression e over time domain (ℵ ∪ {∞}, ≤), we have e < ∞. We can read the terms of the form e ≤ ∞ as 0 = 0 throughout W C(P, Q), for any agents P and Q. As a result, W C(P, Q) is a formula of the first-order theory over structure (ℵ, +).

Theorem 4.12 ∼ is decidable for agents.

Proof: The proof follows from the decidability of the first-order theory of the natural numbers with + [11]. □

Lemma 4.13 For any processes E and F which contain at most free time variables x⃗ = (x_{1}, …, x_{n}), we have

E ∼ F if and only if ∀x_{1} … ∀x_{n}.W C(E, F)

Proof: The proof follows from the definition of strong equivalence of processes. □

Lemma 4.14 For any processes E and F, where E and F contain at most free time variables x_{1}, …, x_{n}, the formula ∀x_{1} … ∀x_{n}.W C(E, F) is a sentence of the first-order theory over structure (ℵ, +).

Proof: Straightforward. □

Theorem 4.15 ∼ is decidable.

Proof: Analogous to Theorem 4.12. □

Since the first-order theory of the natural numbers with + and ×, i.e. Th(ℵ, +, ×), is undecidable, this justifies our decisions in the choice of time expressions.

4.3 Decidability over Dense Time Domains

In this section, we consider dense time. As an example, let T be ℜ^{≥0}, the set of non-negative real numbers.

As for the structure (ℵ, +), we can also define relations: Zero, Ordering, Subtraction, Max and Min in the structure (ℜ, +, ×).

Lemma 4.16 For any processes E and F, where E and F contain at most free time variables x_{1}, …, x_{n}, the formula ∀x_{1} … ∀x_{n}.W C(E, F) is a sentence of the first-order theory over structure (ℜ, +, ×).

Proof: Straightforward. □

Theorem 4.17 ∼ is decidable.

Proof: The result follows from the decidability of the first-order theory of the reals with + and × [10].

5 A Proof System

In the last section we have shown that for any processes E and F, we have a characteristic formula W C(E, F) such that E ∼ F if and only if W C(E, F) holds. We use the notation A ⊧ E ∼ F to indicate that the formula A is a condition for process E to be bisimilar to process F. In this section, we describe a proof system in which we derive statements of the form A ⊢ E = F. The proof system is sound for both discrete and dense time. It will be shown complete for finite processes over dense time domains, but only complete for a restricted language over discrete time domains.

5.1 The Proof System

It is easy to see that every normal form E (process which is in normal form) can be defined by the following BNF expressions:

E ::= δ | (e′)E | α(x)_{e}^{e′}. E | E + F

where e is a time expression and e′ is a time expression or ∞. For convenience, we write (∞)E, for any process E, as syntactical equal to the process nil. As for any process E there is a normal form E′ such that E ∼ E′, henceforth we will focus on the sublanguage defined by the above syntax.

Table 2 contains all axioms and Table 3 contains all proof rules. The proof rules are in the form

\frac{S_{1} … S_{n}}{S}

where S_{1}, …, S_{n}, S are statements. The rule can be read as: if all premises S_{1}, …, S_{n} can be derived, then the conclusion S can be deduced.

We say A ⊢ X = Y is derivable if it can be derived from the axioms in Table 2 by using the proof rules in Table 3. For convenience, we write A ⊢ X = Y to assert that A ⊢ X = Y is derivable.

false ⊢ X = Y  true ⊢ X = X
true ⊢ X = X + δ  true ⊢ X = X + X
true ⊢ X + Y = Y + X  true ⊢ X + (Y + Z) = (X + Y) + Z
true ⊢ X = (0)X  true ⊢ (e)(e′)δ = (e + e′)δ
true ⊢ (e)(X + Y) = (e)X + (e)Y true ⊢ α(x)_{e}^{e′}. X = α(x)_{e}^{e′}. X + (e′)δ

e′ < e ⊢ α(x)_{e}^{e′}. X = (e′)δ

e ≤ y ≤ e′ ⊢ α(x)_{e}^{e′}. X = α(x)_{e}^{y}. X + α(x)_{y}^{e′}. X

true ⊢ α(x){e′ \atop e}. X = α(y){e′ \atop e}. X\{y/x\} (y is free for x in X) true ⊢ (e)(α(x)_{f}^{f′}. X) = α(x)_{f+e}^{f′+e}. X{x − e/x} (x ∉ fv(e))

Table 2: Axioms

1  \frac{A ⊢ X = Y  A ⊢ Y = Z}{A ⊢ X = Z}
2  \frac{A ⊢ X = Y  B ⊢ X = Y}{A ∨ B ⊢ X = Y}
3  \frac{B ⊢ X = Y}{A ⊢ X = Y}  (A → B)

4 \frac{A ⊢ X = Y}{A ∧ e = f ⊢ (e)X = (f)Y}

5  \frac{A ∧ e ≤ x ≤ e′ ⊢ X = Y}{A ∧ e = f ∧ e′ = f′ ⊢ α(x)_{e}^{e′}. X = α(x)_{f}^{f′}. Y}  (x ∉ fv(A))
6  \frac{A ⊢ X = Y  A ⊢ X′ = Y′}{A ⊢ X + X′ = Y + Y′}
7  \frac{A ⊢ X = Y  B ⊢ X = Z}{A ∨ B ⊢ X + Y + Z = Y + Z}

Table 3: Proof Rules Lemma 5.1 The following are derivable:

(1) e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(x)_{f}^{f′}. E + α(x)_{e}^{e′}. E = α(x)_{e}^{e′}. E

(2) e ≤ f ∧ f ≤ e′ ∧ e′ ≤ f′ ⊢ α(x)_{f}^{f′}. E + α(x)_{e}^{e′}. E = α(x)_{e}^{f′}. E

Proof: We only consider (1), as (2) is similar. For (1), we have

e ≤ f ≤ e′ ⊢ α(x)_{e}^{e′}. E = α(x)_{e}^{f}. E + α(x)_{f}^{e′}. E
f ≤ f′ ≤ e′ ⊢ α(x)_{f}^{e′}. E = α(x)_{f}^{f′}. E + α(x)_{f′}^{e′}. E

Clearly

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ → e ≤ f ≤ e′

and

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ → f ≤ f′ ≤ e′

So

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(x)_{e}^{e′}. E = α(x)_{e}^{f}. E + α(x)_{f}^{e′}. E

and

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(x)_{f}^{e′}. E = α(x)_{f}^{f′}. E + α(x)_{f′}^{e′}. E

Thus

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(x)_{f}^{e′}. E = α(x)_{f}^{e′}. E + α(x)_{f}^{f′}. E

and

e ≤ f ∧ f ≤ f′ ∧ f′ ≤ e′ ⊢ α(x)_{e}^{e′}. E = α(x)_{e}^{e′}. E + α(x)_{f}^{f′}. E □

Lemma 5.2

(1) If A ⊢ X = Y and x ∉ fv(A), then A ∧ (e ≤ x ≤ e′) ⊢ α(x)_{e}^{e′}. X = α(x)_{e}^{e′}. Y.

(2) If A ⊢ X = Y and x ∉ fv(A), then A ∧ e = f ∧ e′ = f′ ⊢ α(x)_{e}^{e′}. X = α(x)_{f}^{f′}. Y.

Proof: We only consider (2), as (1) is similar.

Suppose A ⊢ X = Y and x ∉ fv(A). Since A ∧ e ≤ x ≤ e′ → A, we have A ∧ e ≤ x ≤ e′ ⊢ X = Y. Thus A ∧ e = f ∧ e′ = f′ ⊢ α(x)_{e}^{e′}. X = α(x)_{f}^{f′}. Y. □

Remark Rules (1) and (2) of Lemma 5.2 are equipotent with the proof rule 5. In fact they were the version which was first proposed. Thanks to Faron Moller for suggesting the present rule. □

For convenience, we will write ⊢ E = F in place of true ⊢ E = F. Now we consider a simple example and show how the proof system works.

Example Let E ≡ b(y)_{0}^{x−(2 ˙−x)}. δ, F ≡ b(y)_{0}^{2x−2}. δ and G ≡ b(y)_{0}^{x} . δ. We will show that

⊢ a(x)_{1}^{10}. (E + F + G) = a(x)_{1}^{10}. (F + G)

is derivable.

\frac{⊢ δ = δ}{\frac{x − (2 ˙−x) = 2x − 2 ⊢ b(y)_{0}^{x−(2 ˙−x)}. δ = b(y)_{0}^{2x−2}. δ}{x ≤ 2 ⊢ b(y)_{0}^{x−(2 ˙−x)}. δ = b(y)_{0}^{2x−2}. δ} x ≤ 2 → (x − (2 ˙−x) = 2x − 2)}

and

\frac{⊢ δ = δ}{\frac{x − (2 ˙−x) = x ⊢ b(y)_{0}^{x−(2 ˙−x)}. δ = b(y)_{0}^{x} . δ}{x > 2 ⊢ b(y)_{0}^{x−(2 ˙−x)}. δ = b(y)_{0}^{x} . δ} x > 2 → (x − (2 ˙−x) = x)}

By rule 7

x ≤ 2 ∨ x > 2 ⊢ E + F + G = F + G

and

\frac{\frac{x ≤ 2 ∨ x > 2 ⊢ E + F + G = F + G}{1 ≤ x ≤ 10 ⊢ E + F + G = F + G} 1 ≤ x ≤ 10 → (x ≤ 2 ∨ x > 2)}{⊢ a(x)_{1}^{10}. (E + F + G) = a(x)_{1}^{10}. (F + G)}

5.2 Soundness

The soundness of the proof system is shown by the following proposition.

Proposition 5.3 (Soundness) If A ⊢ E = F, then A ⊧ E ∼ F.

Proof: We only need to show that every instance of the axioms of Table 2 is valid, i.e. if A ⊢ E = F is an instance of an axiom, then A ⊧ E ∼ F, and every proof rule of Table 3 preserves the validity. The validity of every instance of the axioms follows from the properties of strong equivalence.

The proofs of rules (1), (2), (3) and (4) are straightforward.

For (5), we suppose A ∧ e ≤ x ≤ e′ ⊧ X ∼ Y, where the formula A and the processes α(x)_{e}^{e′}. X, α(x)_{f}^{f′}. Y contain at most free time variables y⃗ = (y_{1}, ⋯, y_{n}). For any v⃗ ∈ T^{n}, we also suppose A{v⃗/y⃗} holds, e{v⃗/y⃗} = f{v⃗/y⃗}

and e′{v⃗/y⃗} = f′{v⃗/y⃗}. If (α(x)_{e}^{e′}. X){v⃗/y⃗}⟶^{β}_{u}P, then β = α, and P ≡

X{v⃗/y⃗}{u/x} where e{v⃗/y⃗} ≤ u ≤ e′{v⃗/y⃗}. Clearly (α(x)_{f}^{f′}. Y){v⃗/y⃗}⟶^{α}_{u}Y {v⃗/y⃗}{u/x}

and X{v⃗/y⃗}{u/x} ∼ Y {v⃗/y⃗}{u/x} (note that x ∉ fv(A)). By symmetry, we finish the proof of rule (5).

For (6), we suppose A ⊧ X ∼ Y and A ⊧ X′ ∼ Y′. We further assume the formula A, the processes X, X′, Y and Y′ contain at most free time variables y⃗ = (y_{1}, ⋯, y_{n}). For any v⃗ ∈ T^{n}, we suppose A{v⃗/y⃗} holds. So we have X{v⃗/y⃗} ∼ Y {v⃗/y⃗} and X′{v⃗/y⃗} ∼ Y′{v⃗/y⃗}. Therefore (X + X′){v⃗/y⃗} ∼ (Y + Y′){v⃗/y⃗}.

The proof of rule (7) is similar to that of rule (6). □

Note that the side condition of rule 5 is important, as otherwise the rule is invalid. For example, let the formula A be 1 ≤ x ≤ 5, the processes X and Y be b(y)_{0}^{10−x}. nil and b(y)_{0}^{x}. nil, respectively. Clearly we have A ∧ 5 ≤ x ≤ 10 ⊧ X ∼ Y, but A |̸= a(x)_{5}^{10}. X ∼ a(x)_{5}^{10}. Y.

5.3 Completeness

The completeness result of the proof system depends heavily on the existence of normal forms.

Lemma 5.4 For any process E, there is a normal form E′ such that ⊢ E = E′.

Proof: We proceed by induction on the structure of E.

Case 1 E ≡ δ. Clearly ⊢ δ = (0)δ.

Case 2 E ≡ (f)F. By induction, there is a normal form ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. F_{i}+(e)δ

such that

⊢ F = ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. F_{i} + (e)δ

So

⊢ (f)F = (f)(∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. F_{i} + (e)δ)

Therefore

⊢ (f)F = ∑_{i∈I} α_{i}(x_{i})_{e_{i}+f}^{e′_{i}+f}. F_{i}{x_{i} − f/x_{i}} + (e + f)δ

and ∑_{i∈I} α_{i}(x_{i})_{e_{i}+f}^{e′_{i}+f}. F_{i}{x_{i} − f/x_{i}} + (e + f)δ is in normal form.

Case 3 E ≡ α(x)_{e}^{e′}. F. By induction, there is a normal form F′ such that ⊢ F = F′. So ⊢ α(x)_{e}^{e′}. F = α(x)_{e}^{e′}. F′ and therefore ⊢ α(x)_{e}^{e′}. F = a(x)_{e}^{e′}. F′ +(e′)δ

where a(x)_{e}^{e′}. F′ + (e′)δ is in normal form.

Case 4 E ≡ E_{1} + E_{2}. By induction, there is a normal form ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E′_{i} +

(e)δ such that

⊢ E_{1} = ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E′_{i} + (e)δ

and normal form ∑_{j∈J} β_{j}(y_{j})_{f_{j}}^{f′_{j}}. E′′_{j} + (f)δ such that

⊢ E_{2} = ∑_{j∈J} β_{j}(y_{j})_{f_{j}}^{f′_{j}}. E′′_{j} + (f)δ

So

⊢ E_{1} + E_{2} = ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E′_{i} + ∑_{j∈J} β_{j}(y_{j})_{f_{j}}^{f′_{j}}. E′′_{j} + (max(e, f))δ

where ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E′_{i} + ∑_{j∈J} β_{j}(y_{j})_{f_{j}}^{f′_{j}}. E′′_{j} + (max(e, f))δ is in normal form. □

5.3.1 Completeness in Dense Time Domains

In this section, we consider dense time. As an example, we assume the time domain (ℜ^{≥0} ∪ {∞}, ≤). By Lemma 5.4, we can further assume that every process is in normal form.

We first show that for any processes E and F, the characteristic formula W C(E, F) can be written in disjunctive normal form.

Lemma 5.5 For any processes E and F which contain at most free time variables (x_{1}, …, x_{n}), W C(E, F) can be written in disjunctive normal form

⋁_{i∈I} e_{1}^{i} ≤ x_{1} ≤ f_{1}^{i} ∧ ⋯ ∧ e_{n}^{i}(x_{1}, …, x_{n−1}) ≤ x_{n} ≤ f_{n}^{i}(x_{1}, …, x_{n−1})

for some finite set I, time expressions e_{k}^{i}(x_{1}, ⋯, x_{k−1}) and f_{k}^{i}(x_{1}, ⋯, x_{k−1}), where i ∈ I, k = 1, ⋯, n, e_{k}^{i}(x_{1}, ⋯, x_{k−1}) and f_{k}^{i}(x_{1}, ⋯, x_{k−1}) contain at most variables x_{1}, ⋯, x_{k−1}.

Proof: We proceed by induction on the maximal depth of E and F.

For the base case, we have W C(E, F) ≡ (e = f). If e = e′ + u × x, where u ∈ T is a non-zero constant, x ∉ fv(e′) and x ∉ fv(f), then e = f can be replaced by (f ˙−e′) × u^{−1} ≤ x ≤ (f − e′) × u^{−1} which can be written in the above form. If e = e′ ˙−u × x, where u ∈ T and u ≠ 0, x ∉ fv(e′) and x ∉ fv(f), then e = f can be replaced by ((u^{−1} × e′ ≤ x ≤ ∞) ∧ 0 = f) ∨ (0 ≤ x ≤ u^{−1} × e′ ∧ u^{−1} × (e′ ˙−f) ≤ x ≤ u^{−1} × (e′ − f)) which can also be written in the above form. All other cases are similar.

For the inductive case, we have W C(E, F) ≡ (e = f) ∧

⋀_{i∈I}(∀x.(e_{i} ≤ x ≤ e′_{i} → ⋁_{a_{i}=b_{j}^{j∈J}}(f_{j} ≤ x ≤ f′_{j} ∧ W C(E_{i}{x/x_{i}}, F_{j}{x/y_{j}}))))

⋀_{j∈J}(∀y.(f_{j} ≤ y ≤ f′_{j} → ⋁_{a_{i}=b_{j}^{i∈I}}(e_{i} ≤ y ≤ e′_{i} ∧ W C(E_{i}{y/x_{i}}, F_{j}{y/y_{j}}))))

For any i ∈ I and j ∈ J, by induction

W C(E_{i}{x/x_{i}}, F_{j}{x/y_{j}}) = ⋁_{l∈L}(g_{l} ≤ x ≤ g′_{l}) ∧ D_{ij}^{l}

where for every l ∈ L, x ∉ fv(D_{ij}^{l}) and L is finite, and

W C(E_{i}{y/x_{i}}, F_{j}{y/y_{j}}) = ⋁_{k∈K}(h_{k} ≤ y ≤ h′_{k}) ∧ C_{ij}^{k}

where for every k ∈ K, y ∉ fv(C_{ij}^{k}) and K is finite.

So W C(E, F) = (e = f)∧

⋀_{i∈I} ∀x.(e_{i} ≤ x ≤ e′_{i} → ⋁_{a_{i}=b_{j}^{l∈L}^{j∈J}}(max(f_{i}, g_{l}) ≤ x ≤ min(f′_{j}, g′_{l}) ∧ D_{ij}^{l}))

⋀_{j∈J} ∀y.(max(0, f_{j}) ≤ y ≤ f′_{j} → ⋁_{a_{i}=b_{j}^{k∈K}^{i∈I}}(max(e_{i}, h_{k}) ≤ y ≤ min(e′_{i}, h′_{k}) ∧ C_{ij}^{k}))

For any i ∈ I, we may replace

∀x.(e_{i} ≤ x ≤ e′_{i} → ⋁_{a_{i}=b_{j}^{l∈L}^{j∈J}}(max(f_{i}, g_{l}) ≤ x ≤ min(f′_{j}, g′_{l}) ∧ D_{ij}^{l}))

by

∀x.( ⋁_{⋮ ; (u_{n}, v_{n}) ∈ Inv^{(u_{1},v_{1})∈Inv}}(e_{i} ≥ u_{1} ∧ u_{1} ≤ v_{1} ∧ u_{2} ≤ v_{1} ≤ v_{2} ∧ ⋯ ∧

u_{n} ≤ v_{n−1} ≤ v_{n} ∧ v_{n} ≥ e′_{i} ∧ ⋀_{l∈L′} D_{ij}^{l}))

where

Inv = {(max(f_{j}, g_{l}), min(f′_{j}, g′_{l})) : j ∈ J, l ∈ L}
L′ = {l : max(f_{j}, g_{l}) ∈ {u_{1}, …, u_{n}}}

in W C(E, F).

Since x ∉ fv({e_{i}, e′_{i}, f_{j}, f′_{j}, g_{l}, g′_{l}, D_{ij}^{l′} : j ∈ J, l ∈ L, l′ ∈ L′}), the result can further be replaced by

⋁_{⋮^{(u_{1},v_{1})∈Inv} ; (u_{n}, v_{n}) ∈ Inv}(e_{i} ≥ u_{1} ∧ u_{1} ≤ v_{1} ∧ u_{2} ≤ v_{1} ≤ v_{2} ∧ ⋯ ∧

u_{n} ≤ v_{n−1} ≤ v_{n} ∧ v_{n} ≥ e′_{i} ⋀_{l∈L′} D_{ij}^{l})

For the other parts, we can do the same replacements. It is easy to show that the final result can be written in the required disjunctive normal form. □

Remark For discrete time domains, the lemma in general does not hold. For example, the formula 3t = 5s cannot be written in the required form. In the next section, we will show how to restrict the occurrences of time variables in time expressions such that we can still retain the lemma for discrete time domains. □

Proposition 5.6 For any processes E and F, W C(E, F) ⊢ E = F.

Proof: We proceed by induction on the maximal depth of E and F.

For the base case, we have E ≡ (e)δ and F ≡ (f)δ. Then W C(E, F) ≡ (e = f) and e = f ⊢ E = F.

For the inductive case, let

E ≡ ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} + (e)δ and F ≡ ∑_{j∈J} β_{j}(y_{j})_{f_{j}}^{f′_{j}}. F_{j} + (f)δ

Suppose I ≠ ∅. If J = ∅, then F ≡ (f)δ and

W C(E, F) ↔ (e = f) ∧ ⋀_{i∈I}(e_{i} > e′_{i})

Clearly

(e = f) ∧ ⋀_{i∈I}(e_{i} > e′_{i}) ⊢ E = F

Hence W C(E, F) ⊢ E = F.

Now suppose J ≠ ∅, for any i ∈ I, j ∈ J, by induction

W C(E_{i}{x/x_{i}}, F_{j}{x/y_{j}}) ⊢ E_{i}{x/x_{i}} = F_{j}{x/y_{j}}

By the lemma, W C(E_{i}{x/x_{i}}, F_{j}{x/y_{j}}) can be written as

⋁_{l∈L}(g_{l} ≤ x ≤ g′_{l} ∧ D_{ij}^{l})

where for any l ∈ L, x ∉ fv(D_{ij}^{l}). So, for any l ∈ L

g_{l} ≤ x ≤ g′_{l} ∧ D_{ij}^{l} ⊢ E_{i}{x/x_{i}} = F_{i}{x/y_{j}}

Thus

(max(e_{i}, f_{j}, g_{l}) ≤ x ≤ min(e′_{i}, f′_{j}, g′_{l})) ∧ D_{ij}^{l} ⊢ E_{i}{x/x_{i}} = F_{i}{x/y_{j}}

and

D_{ij}^{l} ⊢ α_{i}(x_{i})_{max(e_{i},f_{j},g_{l})}^{min(e′_{i},f′_{j},g′_{l})}. E_{i} = α_{i}(y_{j})_{max(e_{i},f_{j},g_{l})}^{min(e′_{i},f′_{j},g′_{l})}. F_{j}

Let Inv = {(max(f_{j}, g_{l}), min(f′_{l}, g′_{j})) : j ∈ J&l ∈ L}. For any (u_{1}, v_{1}), …, (u_{n}, v_{n}) ∈ Inv, let

C = e_{i} ≥ u_{1} ∧ u_{1} ≤ u_{2} ≤ v_{1} ∧ ⋯ ∧ u_{n−1} ≤ u_{n} ∧ u_{n} ≤ v_{n−1} ≤ v_{n} ∧ v_{n} ≥ e′_{i}

Then

C ⊢ α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} = ∑_{k=1}^{n} α_{i}(x_{i})_{max(e_{i},u_{k})}^{min(e′_{i},v_{k})}. E_{i}

and

( ⋀_{l∈L′} D_{ij}^{l}) ∧ C ⊢ α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} = ∑_{α_{i}=β_{π(k)}^{k=1}}^{n} β_{π(k)}(y_{π(k)})_{max(e_{i},u_{k})}^{min(e′_{i},v_{k})}. F_{π(k)}

where L′ = {l : max(f_{j}, g_{l}) ∈ {u_{1}, …, u_{n}}} and π(k) = j where u_{k} = max(f_{j}, g_{l}). So

C ∧ ⋀_{l∈L′} D_{ij}^{l} ⊢ α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} + F = F

and

⋁_{⋮^{(u_{1},v_{1})∈Inv} ; (u_{n}, v_{n}) ∈ Inv}( ⋀_{l∈L′} D_{ij}^{l} ∧ C) ⊢ α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i} + F = F

where

C ≡ e_{i} ≥ u_{1} ∧ u_{1} ≤ u_{2} ≤ v_{1} ∧ ⋯ ∧ u_{n−1} ≤ u_{n} ∧ u_{n} ≤ v_{n−1} ≤ v_{n} ∧ v_{n} ≥ e′_{i}

Hence

⋀_{i∈I}( ⋁_{⋮^{(u_{1},v_{1})∈Inv} ; (u_{n}, v_{n}) ∈ Inv}( ⋀_{l∈L′} D_{ij}^{l} ∧ C)) ∧ (e = f) ⊢ E + F = F

and

W C(E, F) ⊢ E + F = F

Similarly

W C(E, F) ⊢ E + F = E

So

W C(E, F) ⊢ E = F □

Corollary 5.7 A ⊧ E ∼ F implies A ⊢ E = F.

Corollary 5.8 (Completeness) For any processes E and F, E ∼ F implies ⊢ E = F.

5.3.2 Completeness in Discrete Time Domains

In this section, we assume time to be discrete. For example, the time domain is (ℵ ∪ {∞}, ≤) where ℵ is the set of natural numbers.

As shown in the last section, Lemma 5.5 in general does not hold for discrete time domains. As a result, the proof system is not complete for processes over discrete time domain (ℵ ∪ {∞}, ≤). For example, consider processes P ≡ a(t)_{6}^{6}. b(s)_{10}^{10}. (3s)δ and Q ≡ a(t)_{6}^{6}. b(s)_{10}^{10}. (5t)δ. Clearly we have ⊧ P ∼ Q, but ⊢ P = Q is not derivable from the proof system. However, if we restrict the occurrences of time variables in time expressions, we can still retain the lemma.

We first formalise a notion of time expressions of a process. Notation Let e be a time expression and S be a set of time expressions. We write e + S in place of the set {e + f : f ∈ S} of time expressions. □

Definition 5.9 For any process P, the set of time expressions Exp_{1}(P) of P is inductively defined as follows:

\begin{matrix}Exp_{1}(δ) = \{0\} & Exp_{1}((e′)E) = e′ + Exp_{1}(E) \\ Exp_{1}(α(x)_{e}^{e′}. E) = \{e, e′\} & Exp_{1}(E + F) = Exp_{1}(E) ∪ Exp_{1}(F) \end{matrix}

Definition 5.10 For any process E, the sets Exp_{2}(E) and Exp_{3}(E) of time expressions are defined as follows:

\begin{matrix}Exp_{2}(δ) = ∅ & Exp_{3}((e′)E) = Exp_{1}((e′)E) ∪ Exp_{2}(E) \\ Exp_{3}(δ) = ∅ & Exp_{3}(α(x)_{e}^{e′}. E) = Exp_{1}(α(x)_{e}^{e′}. E) ∪ Exp_{3}(E) \\ Exp_{2}(al(x)_{e}^{e′}. E) = Exp_{3}(E) & Exp_{2}(E + F) = Exp_{2}(E) ∪ Exp_{2}(F) \\ Exp_{2}((e′)E) = Exp_{2}(E) & Exp_{3}(E + F) = Exp_{3}(E) ∪ Exp_{3}(F) \end{matrix}

Proposition 5.11 For any normal form E, where E ≡ ∑_{i∈I} α_{i}(x_{i})_{e_{i}}^{e′_{i}}. E_{i}+(e)δ, we have

Exp_{3}(E) = ⋃_{i∈I} Exp_{3}(E_{i}) ∪ {e + 0, e_{i}, e′_{i} : i ∈ I}

Proof: Straightforward. □

For any set S of time expressions, let Basic(S) be the set of time expressions resulted by eliminating max and min in S by the following procedure:

1 Let Basic(S) be S.

2 If max(e, f) ∈ Basic(S) or min(e, f) ∈ Basic(S), then replace max(e, f) or min(e, f) by e and f in Basic(S).

3 If e ∘ max(f, f′) ∈ Basic(S), or max(f, f′) ∘ e ∈ Basic(S), replace them by e ∘ f and e ∘ f′, where ∘ is + or ˙−.

4 If e ∘ min(f, f′) ∈ Basic(S), or min(f, f′) ∘ e ∈ Basic(S), replace them by e ∘ f and e ∘ f′, where ∘ is + or ˙−.

5 Repeat steps 2 to 4 until there is no occurrence of min and max in Basic(S).

For any set of time expressions S, we say S contains only time expressions which have at most a single occurrence of the same time variables if for any time expression e of Basic(S) and any time variable x, x occurs in e implies that e satisfies one of the following conditions:

(1) e = f ∘ x or e = x ∘ f for some time expression f, where x ∉ fv(f), and ∘ is + or ˙−.

(2) e = e_{1} ∘ e_{2} for some time expressions e_{1} and e_{2} such that x ∉ fv(e_{2}) and e_{1} satisfies one of the two conditions, or x ∉ fv(e_{1}) and e_{2} satisfies one of the two conditions, where ∘ is + or ˙−.

Let E′ be the set of all processes such that for any E ∈ E′, Basic(Exp_{3}(E)) contains only time expressions which have at most a single occurrence of the same time variables. The sublanguage of E′ is still very rich. In fact, we have the following property:

Proposition 5.12 For any processes E and F, if E, F ∈ E′ , then E + F is still in E′. Also if e, e′ are time expressions which have at most a single occurrence of the same time variables and E ∈ E′, then α(x)_{e}^{e′}. E ∈ E′.

Proof: Note that Basic(Exp_{3}(E + F)) = Basic(Exp_{3}(E)) ∪ Basic(Exp_{3}(F)) and Basic(Exp_{3}(α(x)_{e}^{e′}. E)) = Basic({e, e′}) ∪ Basic(Exp_{3}(E)). The result is straightforward. □

Remark If we consider the language defined by the syntax of Section 2, we only need to restrict the definition of time expressions such that the new definition of time expressions only allows those time expressions which have a single occurrence of the same time variables, i.e. we only allow time expressions defined by the following:

1. for any u ∈ T and x ∈ V_{t}, u and x are time expressions;

2. for any time expression e and time variable x ∈ V_{t}, if x does not occur in e, then e + t, t + e, e ˙−t, t ˙−e, max(e, t), max(t, e), min(e, t) and min(t, e) are all time expressions. □

Now we can show that for the processes in E′, Lemma 5.5 of the last section still holds.

Lemma 5.13 For any processes E and F, where E ∈ E′, F ∈ E′ and E and F contain at most free time variable x_{1}, …, x_{n}, W C(E, F) can be written in a disjunctive normal form

⋁_{i∈I} e_{1}^{i} ≤ x_{1} ≤ f_{1}^{i} ∧ ⋯ ∧ e_{n}^{i}(x_{1}, …, x_{n−1}) ≤ x_{n} ≤ f_{n}^{i}(x_{1}, …, x_{n−1})

for some finite set I, time expressions e_{k}^{i}(x_{1}, …, x_{k−1}) and f_{k}^{i}(x_{1}, …, x_{k−1}), where i ∈ I, k = 1, …, n, e_{k}^{i}(x_{1}, …, x_{k−1}) and f_{k}^{i}(x_{1}, …, x_{k−1}) contain at most variables x_{1}, …, x_{k−1}.

Proof: The proof is similar to that of Lemma 5.5 (Note the restriction over occurrences of time variables in time expressions). □

Proposition 5.14 For any processes E and F, where E ∈ E′ and F ∈ E′, W C(E, F) ⊢ E = F.

Proof: Analogous to Proposition 5.6. □

Corollary 5.15 For any processes E ∈ E′ and F ∈ E′, A ⊧ E ∼ F implies A ⊢ E = F.

Corollary 5.16 (Completeness) For any processes E and F, where E ∈ E′ and F ∈ E′, E ∼ F implies ⊢ E = E.

5.4 Proofs of Recursively Defined Processes

In [6], we also allow recursively defined processes. As an example, μX.E represents an infinite process which is recursively defined by the equation X = E, where E may contain process variable X. The operational rules of the recursively defined process μX.E are:

\frac{P \{μX.E/X\}⟶_{t}P}{μX.E⟶_{t}P}  and  \frac{E\{μX.E/X\}⟶^{α}_{t}P}{μX.E⟶^{α}_{t}P}

We say a process E is weakly guarded if every process variable X in E is weakly guarded, where X is weakly guarded in E if every occurrence of X is in some subterm of form α(x)_{e}^{e′}. F of E. For example, the process a(x)_{0}^{∞}. X + b(y)_{1}^{10}. nil is weakly guarded. However the process a(x)_{0}^{∞}. X + X is not weakly guarded as the second occurrence of X is not weakly guarded in it.

In this section, we consider the proofs of recursively defined processes. We show by an example how the proof system works for recursively defined processes. To do so, the proof system needs to be augmented with an axiom

true ⊢ μX.E = E{μX.E/X}

and some form of induction. We choose a very simple form of induction, namely Unique Fixpoint Induction:

\frac{true ⊢ F = E\{F/X\}}{true ⊢ F = μX.E}

The soundness of the axiom can be proved by demonstrating an appropriate strong T -bisimulation. For a waekly guarded process E, the soundness of the above inductive rule follows from the property of unique solution of weakly guarded equations up to strong bisimulation [7]. However, the inductive rule in general is not valid for processes which are not weakly guarded. For example, if E ≡ X, then for any process F we have F ∼ X{F/X} and clearly a(x)_{0}^{10}. nil ≁ μX.X. Also, for any agent P, we have P + a(t)_{0}^{10}. δ ∼ (a(t)_{0}^{10}. δ + X){(P + a(t)_{0}^{10}. δ)/X}, but P + a(t)_{0}^{10}. δ ≁ μX.a(t)_{0}^{10}. δ + X if we let P be b(s)_{0}^{10}. δ.

Now we consider processes

E ≡ μX.a(x)_{1}^{10}. (b(y)_{0}^{x−(2 ˙−x)}. X + b(y)_{0}^{2x−2}. X + b(y)_{0}^{x}. X)

and

F ≡ μX.a(x)_{1}^{10}. (b(y)_{0}^{2x−2}. X + b(y)_{0}^{x}. X)

and show how to derive

⊢ E = F

in the extended proof system.

Since F is recursively defined and weakly guarded, by the above induction rule we only need to show that

⊢ E = a(x)_{1}^{10}. (b(y)_{0}^{2x−2}. E + b(x)_{0}^{x}. E)

However we have

⊢ E = a(x)_{1}^{10}. (b(y)_{0}^{x−(2 ˙−x)}. E + b(y)_{0}^{2x−2}. P + b(y)_{0}^{x}. E)

By rule 1 we only need to show

⊢ a(x)_{1}^{10}. (b(y)_{0}^{x−(2 ˙−x)}. E+b(y)_{0}^{2x−2}. E+b(y)_{0}^{x}. E) = a(x)_{1}^{10}. (b(y)_{0}^{2x−2}. E+b(y)_{0}^{x}. E)

Clearly

⊢ E = E
⊢ b(y)_{0}^{2x−2}. E = b(y)_{0}^{2x−2}. E

and

⊢ b(y)_{0}^{x}. E = b(y)_{0}^{x}. E

By rule 5, we have

x ≥ 2 ⊢ b(y)_{0}^{x−(2 ˙−x)}. E = b(y)_{0}^{x}. E

and

x ≤ 2 ⊢ b(y)_{0}^{x−(2 ˙−x)}. E = b(y)_{0}^{2x−2}. E

By rule 7, we have

x ≤ 2 ∨ x ≥ 2 ⊢ b(y)_{0}^{x−(2 ˙−x)}. E + b(y)_{0}^{2x−2}. E + b(y)_{0}^{x}. E = b(y)_{0}^{2x−2}. E + b(y)_{0}^{x}. E

Since 1 ≤ x ≤ 10 → x ≤ 2 ⋁ x ≥ 2, by rule 3 we have

1 ≤ x ≤ 10 ⊢ b(y)_{0}^{x−(2 ˙−x)}. E + b(y)_{0}^{2x−2}. E + b(y)_{0}^{x}. E = b(y)_{0}^{2x−2}. E + b(y)_{0}^{x}. E

By rule 5, we have the result

⊢ a(x)_{1}^{10}. (b(y)_{0}^{x−(2 ˙−x)}. E+b(y)_{0}^{2x−2}. E+b(y)_{0}^{x}. E) = a(x)_{1}^{10}. (b(y)_{0}^{2x−2}. E+b(y)_{0}^{x}. E)

Remark Even untimed CCS is Turing-powerful [17] and therefore no effective complete proof system can exist. By adding sufficiently powerful inductive methods for handing recursively defined processes, we would have a complete (and therefore ineffective) proof system for reasoning about real-timed processes.

6 Conclusion and Related Work

In this paper, we have shown that strong equivalence for finite processes in real time process algebras with time variables is still decidable. The decidability is independent of the choice of time domain, allowing time to be discrete or dense. We have also presented a relativised compositional proof system for real time process algebras with time variables. It is again independent of choice of the time domain. The proof system is sound for both discrete and dense time. It has been shown complete for finite processes over dense time domains, but only complete for a sublanguage over discrete time domains. We have discussed how to restrict occurrences of time variables in time expressions to get the sublanguage. There is no infinite rule in the proof system and therefore it is realistic and (we hope) useful.

Although our discussions are based on Timed CCS, the approach and results can also be applied to other real time process algebras. For example, the approach and results can be applied to a restricted language of Baeten and Bergstra’s ACP ρI (only allow those prefixed integrations) [15]. As shown in [7], the restricted language of ACP ρI is closely related to Timed CCS. For real time process algebras with an assumption of the Maximal Progress Principle, such as [24], we need two extra axioms:

⊢ τ(x)_{e}^{e+f}. X = τ(x)_{e}^{e}. X

and

⊢ α(x)_{e}^{e′}. X + τ(y)_{f}^{f}. Y = α(x)_{e}^{min(e′,f)}. X + τ(y)_{f}^{f}. Y

There is a simple proof system pointed out by Kim Larsen which consists of a single rule

\frac{W C(E, F)}{⊢ E = F}

It is easy to see that the proof system is sound and complete for finite processes. The soundness and completeness is independent of choice of the time domain.

There is some other work on decidability for real time process algebras. In [14], it has shown that strong equivalence over regular processes without time variables is decidable. The work of [4] has generalised that of [14] by also including parallel composition, but still not allowing time variables.

In [15], Klusener has presented a proof system for the restricted language of ACP ρI and the work is for absolute time. As there are some powerful infinite rules, the proof system, although sound and complete, is only of theoretical interest. Acknowledgements: I would like to thank Stuart Anderson, Faron Moller and John Power for many helpful discussions and constructive suggestions, Kim Larsen for pointing out the simple proof system and providing helpful comments, Mark Jerrum for many interesting discussions on decidability.

References

[1] J.C.M. Baeten and J.A. Bergstra, Real Time Process Algebra, Formal Aspects of Computing 3(2), pages 142 - 188, 1991.

[2] M. Ben-Or, D. Kozen and J. Reif, The Complexity of Elementary Algebra and Geometry, Journal of Computer and System Sciences 32, pages 251 - 264, 1986.

[3] J. A. Bergstra & J. W. Klop, Algebra of Communicating Processes with Abstraction, Theoretical Computer Science 37, pages 77 - 121, 1985.

[4] K. Cerans, Decidability of Bisimulation Equivalences for Parallel Timer Processes, in Proc. of CAV’92, Lecture Notes in Computer Science 663, 1992.

[5] L. Chen, Decidability and Completeness in Real-Time Processes, Technical Report ECS-LFCS-91-185, University of Edinburgh, 1991.

[6] L. Chen, An Interleaving Model for Real-Time Systems, in Proc. of Symp. of Logical Foundations of Computer Science, Lecture Notes in Computer Science 620, pages 81 - 92, 1992.

[7] L. Chen, Timed Processes: Models, Axioms and Decidability, Ph.D Thesis, CST-101-93 (also published as ECS-LFCS-93-271), University of Edinburgh, 1993.

[8] L. Chen, Axiomatising Real-Time Processes, in Proc. of 9th Conf. on Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science 802, pages 215 - 229, 1993.

[9] L. Chen, S. Anderson and F. Moller, A Timed Calculus of Communicating System, Technical Report ECS-LFCS-90-127, University of Edinburgh, 1990.

[10] G. E. Collins, Quantifer Elimination for Real Closed Fields by Cylindric Algebraic Decomposition, in Proc. 2nd GI Conference on Automata Theory and Formal Language, pages 134 - 183, 1975.

[11] H. B. Enderton, A Mathematical Introduction to Logic, Academic Press, Inc., 1972.

[12] M. Hennessy and T. Regan, A Temporal Process Algebra, Technical Report 2/90 University of Sussex, 1990.

[13] C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall International, 1985.

[14] U. Holmer, K. Larsen & Y. Wang, Deciding Properties of Regular Real Time Processes, in Proc. of CAV’91, Lecture Notes in Computer Science, 1991.

[15] A. S. Klusener, Completeness in Real Time Process Algebra, Proceedings of CONCUR’91, Lecture Notes in Computer Science 527, pages 96 - 110, 1991.

[16] R. Milner, A Calculus of Communicating systems, Lecture Notes in Computer Science 92, Springer-verlag, 1980.

[17] R. Milner, Communication and Concurrency, Prentice-Hall international, 1989.

[18] F. Moller and C. Tofts, A Temporal Calculus of Communicating System, Lecture Notes in Computer Science 458, pages 401 - 415, 1990.

[19] X. Nicollin, J. Richier, J. Sifakis and J. Voiron, ATP : an Algebra for Timed Processes, Laboratoire de Genie Informatique, IMAG-Campus, 38041 Grenoble Cedex, France, 1990.

[20] D.M.R. Park, Concurrency and Automata on Infinite Sequences, Lecture Notes in Computer Science 104, Springer-Verlag, 1981.

[21] G. D. Plotkin, A Structured Approach to Operational Semantics, DAIMI FN-19, Computer Science Department, Arhus University, Denmark, 1981.

[22] R. Reed and A. W. Roscoe, A Timed Model for Communicating Sequential Processes, Theoretical Computer Science 58, pages 249-261, 1988.

[23] S. Schneider, An Operational Semantics for Timed CSP, in Procc. of Chalmers Workshop on Concurrency, to appear in Information and Computation, 1991.

[24] Y. Wang, Real-time Behaviour of Asynchronous Agents, Lecture Notes in Computer Science 458, pages 502 - 520, 1990.