BRICS RS-98-50 Aceto & Ingólfsdóttir: Testing Hennessy-Milner Logic with Recursion BRICS

Basic Research in Computer Science

Testing Hennessy-Milner Logic with Recursion

Luca Aceto Anna Ingólfsdóttir BRICS Report Series RS-98-50 ISSN 0909-0878 December 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/50/

Testing Hennessy-Milner Logic with Recursion^{⋆}

Luca Aceto^{⋆⋆} and Anna Ingólfsdóttir^{⋆ ⋆ ⋆}

BRICS^{†}, Department of Computer Science, Aalborg University, Fredrik Bajers Vej 7-E, DK-9220 Aalborg Ø, Denmark.

Abstract. This study offers a characterization of the collection of properties expressible in Hennessy-Milner Logic (HML) with recursion that can be tested using finite LTSs. In addition to actions used to probe the behaviour of the tested system, the LTSs that we use as tests will be able to perform a distinguished action nok to signal their dissatisfaction during the interaction with the tested process. A process s passes the test T iff T does not perform the action nok when it interacts with s. A test T tests for a property ϕ in HML with recursion iff it is passed by exactly the states that satisfy ϕ. The paper gives an expressive completeness result offering a characterization of the collection of properties in HML with recursion that are testable in the above sense.

1 Introduction

Observational semantics for concurrent processes are based upon the general idea that two processes should be equated, unless they behave differently, in some precise sense, when they are made to interact with some distinguishing environment. Such an idea is, in arguably its purest form, the foundation of the theory of the testing equivalences of De Nicola and Hennessy [4, 6]. In the theory of testing equivalence, two processes, described abstractly as labelled transition systems (LTSs) [8], are deemed to be equivalent iff they pass exactly the same tests. A test is itself an LTS — i.e., a process — which may perform a distinguished action to signal that it is (un)happy with the outcome of its interaction with the tested process. Intuitively, the purpose of submitting a process to a test is to discover whether it enjoys some distinguished property or not. Testing equivalence then stipulates that two processes that enjoy the same properties for which tests can be devised are to be considered equivalent. The main aim of this study is to present a characterization of the collection of properties of concurrent processes that can be tested using LTSs. Of course, in order to be able to even attempt such a characterization (let alone provide it), we need to precisely define a formalism for the description of properties of LTSs, single out a collection of LTSs as tests, and describe the testing process and when an LTS passes or fails a test.

As our specification formalism for properties of processes, we use Hennessy-Milner Logic (HML) with recursion [10]. This is a very expressive property

⋆ The work reported in this paper was mostly carried out during the authors’ stay at the

Dipartimento di Sistemi ed Informatica, Università di Firenze, Italy. ⋆⋆ Partially supported by a grant from the CNR, Gruppo Nazionale per l’Informatica Matem-

atica (GNIM). Email:luca@cs.auc.dk. ⋆ ⋆ ⋆ Supported by the Danish Research Council. Email: annai@cs.auc.dk.

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

language which results from the addition of least and greatest fixed points to the logic considered by Hennessy and Milner in their seminal study [7]. The resulting property language is indeed just a reformulation of the modal μ-calculus [10]. Following the idea of using test automata to check whether processes enjoy properties described by formulae in such a language [2, 1], we use finite LTSs as property testers. In addition to actions used to probe the behaviour of the tested system, the LTSs that we use as tests will be able to perform a distinguished action nok (read ‘not okay’) to signal their dissatisfaction during the interaction with the tested process. As in the approach underlying the testing equivalences, a test interacts with a process by communicating with it, and, in keeping with the aforementioned references, the interaction between processes and tests will be described using the (derived) operation of restricted parallel composition from CCS [13].

We say that a process s fails the test T iff T can perform the action nok when it interacts with s. Otherwise s passes T. A test T tests for a property ϕ in HML with recursion iff it is passed by exactly the states that satisfy ϕ. The main result of the paper is an expressive completeness result offering a characterization of the collection of properties in HML with recursion that are testable in the above sense. We refer to this language as SHML (for ‘safety HML’). More precisely we show that:

– every property ϕ of SHML is testable, in the sense that there exists a test T_{ϕ} such that s satisfies ϕ if and only if s passes T_{ϕ}, for every process s; and

– every test T is expressible in SHML, in the sense that there exists a formula ϕ_{T} of SHML such that, for every process s, the agent s passes T if and only if s satisfies ϕ_{T}.

This expressive completeness result will be obtained as a corollary of a stronger result pertaining to the compositionality of the property language SHML. A property language is compositional if checking whether a composite system s∥T satisfies a property ϕ can be reduced to deciding whether the component s has a corresponding property ϕ/T. As the property ϕ/T is required to be expressible in the property language under consideration, compositionality clearly puts a demand on its expressive power. Let L_{nok} be the property language that only contains the simple safety property [nok]ff, expressing that the nok action cannot be performed. We prove that SHML is the least expressive, compositional extension of the language L_{nok} (Thm. 3.19). This yields the desired expressive completeness result because any compositional property language that can express the property [nok]ff is expressive complete with respect to tests (Propn. 3.13). Any increase in expressiveness for the language SHML can only be obtained at the loss of testability.

The paper is organized as follows. After reviewing the model of labelled transition systems and HML with recursion (Sect. 2), we introduce tests and describe how they can be used to test for properties of processes (Sect. 3). We then proceed to argue that not every formula in HML with recursion is testable (Propn. 3.4), but that its sub-language SHML is (Sect. 3.1). Our main results on the compositionality and completeness of SHML are presented in Sect. 3.2.

2 Preliminaries

We begin by briefly reviewing the basic notions from process theory that will be needed in this study. The interested reader is referred to, e.g., [7, 10, 13] for more details.

Labelled Transition Systems Let Act be a set of actions, and let a, b range over it. We assume that Act comes equipped with a mapping \overline{·} : Act → Act such that \overline{\overline{a}} = a, for every a ∈ Act. Action ā is said to be the complement of a. We let Act_{τ} (ranged over by μ) stand for Act ∪ {τ}, where τ is a symbol not occurring in Act. Following Milner [13], the symbol τ will stand for an internal action of a system; such actions will typically arise from the synchronization of complementary actions (cf. the rules for the operation of parallel composition in Defn. 2.2).

Definition 2.1. A labelled transition system (LTS) over the set of actions Act_{τ} is a triple T = ⟨S, Act_{τ} , ⟶⟩ where S is a set of states, and ⟶ ⊆ S × Act_{τ} × S is a transition relation. An LTS is finite iff its set of states and its transition relation are both finite. It is rooted if a distinguished state root(T ) ∈ S is singled out as its start state.

As it is standard practice in process theory, we use the more suggestive notation s →^{μ} s′ in lieu of (s, μ, s′) ∈⟶. We also write s ↛^{μ} if there is no state s′ such that s →^{μ} s′. Following [13], we now proceed to define versions of the transition relations that abstract from the internal evolution of states as follows:

\begin{matrix}s ⇒^{ε} s′ iff & s →^{τ}^{∗} s′ \\ s ⇒^{μ} s′ iff & ∃s_{1}, s_{2}. s ⇒^{ε} s_{1} →^{μ} s_{2} ⇒^{ε} s′ \end{matrix}

where we use →^{τ}^{∗} to stand for the reflexive, transitive closure of →^{τ}.

Definition 2.2 (Operations on LTSs).

– Let T_{i} = ⟨S_{i}, Act_{τ} , ⟶_{i}⟩ (i ∈ {1, 2}) be two LTSs. The parallel composition of T_{1} and T_{2} is the LTS T_{1} ∥ T_{2} = ⟨S_{1} × S_{2}, Act_{τ} , ⟶⟩, where the transition relation ⟶ is defined by the rules (μ ∈ Act_{τ} , a ∈ Act):

\frac{s_{1} →^{μ}_{1} s′_{1}}{s_{1}∥s_{2} →^{μ} s′_{1}∥s_{2}}  \frac{s_{2} →^{μ}_{2} s′_{2}}{s_{1}∥s_{2} →^{μ} s_{1}∥s′_{2}}  \frac{s_{1} →^{a}_{1} s′_{1}  s_{2} →^{\overline{a}}_{2} s′_{2}}{s_{1}∥s_{2} →^{τ} s′_{1}∥s′_{2}}

In the rules above, and in the remainder of the paper, we use the more suggestive notation s ∥ s′ in lieu of (s, s′).

– Let T = ⟨S, Act_{τ} , →⟩ be an LTS and let L ⊆ Act be a set of actions. The restriction of T over L is the LTS T \L = ⟨S\L, Act_{τ} , ⇝⟩, where S\L = {s\L | s ∈ S} and the transition relation ⇝ is defined by the rules:

\frac{s →^{τ} s′}{s\L ⇝^{τ} s′\L}  \frac{s →^{a} s′}{s\L ⇝^{a} s′\L}

where a, \overline{a} ∉ L.

The reader familiar with [13] may have noticed that the above definitions of parallel composition and restriction are precisely those of CCS. We refer the interested reader to op. cit. for more details on these operations.

Hennessy-Milner Logic with Recursion In their seminal study [7], Hennessy and Milner gave a logical characterization of bisimulation equivalence [14] (over states of image-finite LTSs) in terms of a (multi-)modal logic which has since then been referred to as Hennessy-Milner Logic (HML). For the sake of completeness and clarity, we now briefly review a variation of this property language for concurrent processes which contains operations for the recursive definition of formulae — a feature that dramatically increases its expressive power. The interested reader is referred to, e.g., [10] for more details.

Definition 2.3. Let Var be a countably infinite set of formula variables, and let nok denote an action symbol not contained in Act. The collection HML(Var) of formulae over Var and Act ∪ {nok} is given by the following grammar:

ϕ ::= tt | ff | ϕ ∨ ϕ | ϕ ∧ ϕ | ⟨α⟩ϕ | [α]ϕ | X | min(X, ϕ) | max(X, ϕ)

where α ∈ Act ∪ {nok}, X is a formula variable and min(X, ϕ) (respectively, max(X, φ)) stands for the least (respectively, largest) solution of the recursion equation X = φ.

We use SHML(Var) (for ‘safety HML’) to stand for the collection of formulae in HML(Var) that do not contain occurrences of ∨, ⟨α⟩ and min(X, ϕ).

A closed recursive formula of HML(Var) is a formula in which every formula variable X is bound, i.e., every occurrence of X appears within the scope of some min(X, ϕ) or max(X, ϕ) construct. A variable X is free in the formula ϕ if some occurrence of it in ϕ is not bound. For example, the formula max(X, X) is closed, but min(X, [a]Y) is not because Y is free in it. The collection of closed formulae contained in HML(Var) (respectively, SHML(Var)) will be written HML (resp. SHML). In the remainder of this paper, every formula will be closed, unless specified otherwise, and we shall identify formulae that only differ in the names of their bound variables. For formulae ϕ and ψ, and a variable X, we write ϕ{ψ/X} for the formula obtained by replacing every free occurrence of X in ϕ with ψ. The details of such an operation in the presence of binders are standard (see, e.g., [15]), and are omitted here.

Given an LTS T = ⟨S, Act_{τ} , ⟶⟩, an environment is a mapping ρ : Var → 2^{S}. For an environment ρ, variable X and subset of states S, we write ρ[X ↦ S] for the environment mapping X to S, and acting like ρ on all the other variables.

Definition 2.4 (Satisfaction Relation). Let T = ⟨S, Act_{τ} , ⟶⟩ be an LTS. For every environment ρ and formula φ contained in HML(Var), the collection [[φ]]ρ of states in S satisfying the formula φ with respect to ρ is defined by structural recursion on φ thus:

[[tt]]ρ =^{def} S
[[ff]]ρ =^{def} ∅
[[φ_{1} ∨ φ_{2}]] =^{def} [[φ_{1}]]ρ ∪ [[φ_{2}]]ρ
[[φ_{1} ∧ φ_{2}]] =^{def} [[φ_{1}]]ρ ∩ [[φ_{2}]]ρ
[[⟨α⟩φ]] =^{def} {s | s ⇒^{α} s′ for some s′ ∈ [[φ]]ρ}
[[[α]φ]] =^{def} {s | for every s′, s ⇒^{α} s′ implies s′ ∈ [[φ]]ρ}
[[X]]ρ =^{def} ρ(X)
[[min(X, φ)]]ρ =^{def} ⋂ {S | [[φ]]ρ[X ↦ S] ⊆ S}
[[max(X, φ)]]ρ =^{def} ⋃ {S | S ⊆ [[φ]]ρ[X ↦ S]} .

The interested reader will find more details on this definition in, e.g., [10]. Here we just confine ourselves to remarking that, as the interpretation of each formula ϕ containing at most X free induces a monotone mapping [[ϕ]] : 2^{S} → 2^{S}, the closed formulae min(X, ϕ) and max(X, ϕ) are indeed interpreted as the least and largest solutions, respectively, of the equation X = ϕ. If φ is a closed formula, then the collection of states satisfying it is independent of the environment ρ, and will be written [[φ]]. In the sequel, for every state s and closed formula φ, we shall write s ⊧ φ (read ‘s satisfies φ’) in lieu of s ∈ [[φ]].

When restricted to SHML, the satisfaction relation ⊧ is the largest relation included in S×SHML satisfying the implications in Table 1. A relation satisfying the defining implications for ⊧ will be called a satisfiability relation. It follows from standard fixed-point theory [16] that, over S × HML, the relation ⊧ is the union of all satisfiability relations and that the above implications are in fact biimplications for ⊧.

Remark. Since nok is not contained in Act, every state of an LTS trivially satisfies formulae of the form [nok]ϕ. The role played by these formulae in the developments of this paper will become clear in Sect. 3.2. Dually, no state of an LTS satisfies formulae of the form ⟨nok⟩φ.

Formulae ϕ and ψ are logically equivalent (with respect to ⊧) iff they are satisfied by the same states. We say that a formula is satisfiable iff it is satisfied by at least one state in some LTS, otherwise we say that it is unsatisfiable.

3 Testing Formulae

As mentioned in Sect. 1, the main aim of this paper is to present a complete characterization of the class of testable properties of states of LTSs that can be expressed in the language HML. In this section we define the collection of tests and the notion of property testing used in this study. Informally, testing involves the parallel composition of the tested state with a test. Following the spirit of the classic approach of De Nicola and Hennessy [4, 6], we say that the

s ⊧ tt ⇒ true
s ⊧ ff ⇒ false
s ⊧ φ_{1} ∧ φ_{2} ⇒ s ⊧ φ_{1} and s ⊧ φ_{2}
s ⊧ [α]φ ⇒ ∀s′. s ⇒^{α} s′ implies s′ ⊧ φ
s ⊧ max(X, φ) ⇒ s ⊧ φ{max(X, φ)/X}

Table 1. Satisfaction implications

tested state fails a test if the distinguished reject action nok can be performed by the test while it interacts with it, and passes otherwise. The formal definition of testing then involves the definition of what a test is, how interaction takes place and when the test has failed or succeeded. We now proceed to make these notions precise.

Definition 3.1 (Tests). A test is a finite, rooted LTS over the set of actions Act_{τ} ∪ {nok}.

In the remainder of this study, tests will often be concisely described using the regular fragment of Milner’s CCS [13] given by the following grammar:

T ::= 0 | α.T | T + T | X | fix(X = T)

where α ∈ Act_{τ} ∪ {nok}, and X ranges over Var. As usual, we shall only be concerned with the closed expressions generated by the above grammar, with fix(X = T) as the binding construct, and we shall identify expressions that only differ in the names of their bound variables. In the sequel, the symbol ≡ will be used to denote syntactic equality up to renaming of bound variables. The operation of substitution over the set of expressions given above is defined exactly as for formulae in HML(Var). The operational semantics of the expressions generated by the above grammar is given by the classic rules for CCS. These are reported below for the sake of clarity:

\overline{α.T →^{α} T}  \frac{T_{1} →^{α} T′_{1}}{T_{1} + T_{2} →^{α} T′_{1}}  \frac{T_{2} →^{α} T′_{2}}{T_{1} + T_{2} →^{α} T′_{2}}  \frac{T \{fix(X = T)/X\} →^{α} T′}{fix(X = T) →^{α} T′}

where α is either nok or an action in Act_{τ}. The intention is that the term T stands for the test whose start state is T itself, whose transitions are precisely those that are provable using the above inference rules, and whose set of states is the collection of expressions reachable from T by performing zero or more transitions. We refer the reader to [13] for more information on the operational semantics of CCS.

Definition 3.2 (Testing Properties). Let φ be a formula in HML, and let T be a test.

– A state s of an LTS passes the test T iff (s∥root(T))\Act ⇏^{nok}. Otherwise we say that s fails the test T.

– We say that the test T tests for the formula φ (and that φ is testable) iff for every LTS T and every state s of T , s ⊧ φ iff s passes the test T.

– Let L be a collection of formulae in HML. We say that L is testable iff each of the formulae in L is.

Example 3.3. The formula [a]ff states that a process does not afford a ⇒^{a}- transition. We therefore expect that a suitable test for such a property is T ≡ ā.nok.0. Indeed, the reader will easily realize that (s∥T)\Act ⇏^{nok} iff s ⇏^{a}, for every state s. The formula [a]ff is thus testable, in the sense of this paper.

The formula max(X, [a]ff∧[b]X) is satisfied by those states which cannot perform a ⇒^{a}-transition, no matter how they engage in a sequence of ⇒^{b}-transitions. A suitable test for such a property is fix(X = ā.nok.0 + b̄.X), and the formula max(X, [a]ff ∧ [b]X) is thus testable.

As already stated, our main aim in this paper is to present a characterization of the collection of HML-properties that are testable in the sense of Defn. 3.2. To this end, we begin by providing evidence to the effect that not every property expressible in HML is testable.

Proposition 3.4 (Two Negative Results).

1. Let ϕ be a formula in HML. Suppose that ϕ is satisfiable. Then, for every action a in Act, the formula ⟨a⟩ϕ is not testable.

2. Let a and b be two distinct actions in Act. Then the formula [a]ff ∨ [b]ff is not testable.

Remark. If φ is unsatisfiable, then the formula ⟨a⟩φ is logically equivalent to ff. Since ff is testable using the test nok.0, the requirement on φ is necessary for Propn. 3.4(1) to hold. Note moreover that, as previously remarked, both the formulae [a]ff and [b]ff are testable, but their disjunction is not (Propn. 3.4(2)).

Our aim in the remainder of this paper is to show that the collection of testable properties is precisely SHML. This is formalized by the following result.

Theorem 3.5. The collection of formulae SHML is testable. Moreover, every testable property in HML can be expressed in SHML.

The remainder of this paper will be devoted to a proof of the above theorem. In the process of developing such a proof, we shall also establish some results pertaining to the expressive power of SHML which may be of independent interest.

3.1 Testability of SHML

We begin our proof of Thm. 3.5 by showing that the language SHML is testable. To this end, we define, for every open formula ϕ in the language SHML(Var), a regular CCS expression T_{ϕ} by structural recursion thus:

Ttt =^{def} 0  T_{[a]ϕ} =^{def} ā.T_{ϕ}
Tff =^{def} nok.0  T_{X} =^{def} X
T_{ϕ_{1}∧ϕ_{2}} =^{def} τ.T_{ϕ_{1}} + τ.T_{ϕ_{2}} T_{max(X,ϕ)} =^{def} fix(X = T_{ϕ}) .

For example, if ϕ ≡ max(X, [a]ff∧ [b]X) then T_{ϕ} is the test fix(X = τ.ā.nok.0 + τ.b̄.X). We recall that we identify CCS descriptions of tests that only differ in the name of their bound variables since they give rise to isomorphic LTSs. Our order of business in this section will be to show the following result:

Theorem 3.6. Let ϕ be a closed formula contained in SHML. Then the test T_{ϕ} tests for it.

In the proof of this theorem, it will be convenient to have an alternative, novel characterization of the satisfaction relation for formulae in the language SHML. This we now proceed to present.

Definition 3.7. Let T = ⟨S, Act_{τ} , ⟶⟩ be an LTS. The satisfaction relation ⊧_{ε} is the largest relation included in S ×SHML satisfying the following implications:

s ⊧_{ε} tt ⇒ true
s ⊧_{ε} ff ⇒ false
s ⊧_{ε} φ_{1} ∧ φ_{2} ⇒ s′ ⊧_{ε} φ_{1} and s′ ⊧_{ε} φ_{2}, for every s′ such that s ⇒^{ε} s′
s ⊧_{ε} [a]φ ⇒ s ⇒^{a} s′ implies s′ ⊧_{ε} φ, for every s′
s ⊧_{ε} max(X, φ) ⇒ s′ ⊧_{ε} φ{max(X, φ)/X}, for every s′ such that s ⇒^{ε} s′

A relation satisfying the above implications will be called a weak satisfiability relation.

The satisfaction relation ⊧_{ε} is closed with respect to the relation ⇒^{ε}, in the sense of the following proposition.

Proposition 3.8. Let T = ⟨S, Act_{τ} , ⟶⟩ be an LTS. Then, for every s ∈ S and φ ∈ SHML, s ⊧_{ε} φ iff s′ ⊧_{ε} φ, for every s′ such that s ⇒^{ε} s′.

Proof. The only interesting thing to check is that if s ⊧_{ε} φ and s ⇒^{ε} s′, then s′ ⊧_{ε} φ. To this end, it is sufficient to prove that the relation R defined thus:

R =^{def} {(s, φ) | ∃t. t ⊧_{ε} φ and t ⇒^{ε} s}

is a weak satisfiability relation. The straightforward verification is left to the reader. □

We now proceed to establish that the relations ⊧_{ε} and ⊧ coincide for formulae in SHML.

Proposition 3.9. Let ϕ be a formula contained in SHML. Then, for every state s of an LTS, s ⊧ ϕ iff s ⊧_{ε} ϕ.

In the proof of Thm. 3.6, it will be convenient to have at our disposal some further auxiliary results. For ease of reference, these are collected in the following lemma.

Lemma 3.10.

1. Let ϕ be a formula in SHML. Assume that T_{ϕ} →^{nok}. Then ϕ is logically equivalent to ff.

2. Let ϕ be a formula in SHML. Assume that T_{ϕ} →^{τ} T. Then there are formulae ϕ_{1} and ϕ_{2} in SHML such that T ≡ T_{ϕ_{1}}, and ϕ is logically equivalent to ϕ_{1}∧ϕ_{2}.

3. Let ϕ be a formula in SHML. Assume that T_{ϕ} →^{ā} T. Then there is a formula ψ in SHML such that T ≡ T_{ψ}, and ϕ is logically equivalent to [a]ψ.

Using these results, we are now in a position to prove Thm. 3.6.

Proof of Thm. 3.6: In light of Propn. 3.9, it is sufficient to show that, for every state s of an LTS and closed formula ϕ ∈ SHML,

s ⊧_{ε} ϕ iff (s∥T_{ϕ})\Act ⇏^{nok} .

We prove the two implications separately.

– ‘If Implication’. It is sufficient to show that the relation

R =^{def} {(s, ϕ) | (s∥T_{ϕ})\Act ⇏^{nok} and ϕ ∈ SHML}

is a weak satisfiability relation. The details of the proof are left to the reader.

– ‘Only If Implication’. We prove the contrapositive statement. To this end, assume that

(s∥T_{ϕ})\Act ⇒^{ε} (s′∥T′)\Act →^{nok}

for some state s′ and test T′. We show that s |̸=_{ε} ϕ holds by induction on the length of the computation (s∥T_{ϕ})\Act ⇒^{ε} (s′∥T′)\Act.

• Base Case: (s∥T_{ϕ})\Act ≡ (s′∥T′)\Act →^{nok}. In this case, we may infer that T_{ϕ} →^{nok}. By Lemma 3.10(1), it follows that ϕ is unsatisfiable. Propn. 3.9 now yields that s |̸=_{ε} ϕ, which was to be shown.

• Inductive Step: (s∥T_{ϕ})\Act →^{τ} (s′′∥T′′)\Act ⇒^{ε} (s′∥T′)\Act →^{nok}, for some state s′′ and test T′′. We proceed by a case analysis on the form the transition

(s∥T_{ϕ})\Act →^{τ} (s′′∥T′′)\Act

may take.

∗ Case: s →^{τ} s′′ and T′′ ≡ T_{ϕ}.

In this case, we may apply the inductive hypothesis to infer that s′′ |̸=_{ε} ϕ. By Propn. 3.8, it follows that s |̸=_{ε} ϕ, which was to be shown.

∗ Case: T_{ϕ} →^{τ} T′′ and s = s′′.

By Lemma 3.10(2), it follows that ϕ is logically equivalent to ϕ_{1} ∧ ϕ_{2} for some formulae ϕ_{1} and ϕ_{2} in SHML, and that T′′ ≡ T_{ϕ_{1}}. By induction, we may now infer that s |̸=_{ε} ϕ_{1}. Since ϕ is logically equivalent to ϕ_{1} ∧ ϕ_{2}, this implies that s |̸=_{ε} ϕ (Propn. 3.9), which was to be shown.

∗ Case: s →^{a} s′′ and T_{ϕ} →^{ā} T′′, for some action a ∈ Act. By Lemma 3.10(3), it follows that ϕ is logically equivalent to [a]ψ for some formula ψ in SHML, and that T′′ ≡ T_{ψ}. By induction, we may now infer that s′′ |̸=_{ε} ψ. Since ϕ is logically equivalent to [a]ψ and s →^{a} s′′ |̸=_{ε} ψ, this implies that s |̸=_{ε} ϕ (Propn. 3.9), which was to be shown.

This completes the inductive argument, and the proof of the ‘only if’ implication.

The proof of the theorem is now complete. □

3.2 Expressive Completeness of SHML

We have just shown that every property φ which can be expressed in the language SHML is testable, in the sense of Defn. 3.2. We now address the problem of the expressive completeness of this property language with respect to tests. More precisely, we study whether all properties that are testable can be expressed in the property language SHML — in the sense that, for every test T, there exists a formula ψ_{T} in SHML such that every state of an LTS passes the test T if, and only if, it satisfies ψ_{T}. Our aim in this section is to complete the proof of Thm. 3.5 by arguing that the language SHML is expressive complete, in the sense that every test T may be expressed as a property in the language SHML in the precise technical sense outlined above. This amounts to establishing an expressive completeness result for SHML akin to classic ones presented in, e.g., [9, 5, 17]. In the proof of this expressive completeness result, we shall follow an indirect approach by focusing on the compositionality of a property language L with respect to tests and the parallel composition operator ∥. As we shall see (cf. Propn. 3.13), if a property language L, that contains the property [nok]ff, is compositional with respect to tests and ∥ (cf. Defn. 3.12) then it is expressive complete (cf. Defn. 3.11). We shall show that SHML is compositional with respect to tests and ∥, and obtain the expressive completeness of such a language as a corollary of this stronger result.

We begin with some preliminary definitions, introducing the key concepts of compositionality and (expressive) completeness.

Definition 3.11 (Expressive completeness). Let L be a collection of formulae in HML. We say that L is (expressive) complete (with respect to tests) if for every test T there exists a formula φ_{T} ∈ L such that, for every state s of an LTS, s ⊧ φ_{T} iff s passes the test T.

Compositionality, on the other hand, is formally defined as follows:

Definition 3.12 (Compositionality). Let L be a collection of formulae in HML. We say that L is compositional (with respect to tests and ∥) if, for every φ ∈ L and every test T, there exists a formula φ/T ∈ L such that, for every state s of an LTS, s ∥ root(T) ⊧ φ iff s ⊧ φ/T.

Intuitively, the formula φ/T states a necessary and sufficient condition for state s to satisfy φ when it is made to interact with the test T.

Our interest in compositionality stems from the following result that links it to the notion of completeness. In the sequel, we use L_{nok} to denote the property language that only consists of the formula [nok]ff. (Recall that nok is a fresh action not contained in Act.)

Proposition 3.13. Let L be a collection of formulae in HML that includes L_{nok}. Suppose that L is compositional. Then L is complete with respect to tests.

Proof. Consider an arbitrary test T. We aim at exhibiting a formula ϕ_{T} ∈ L meeting the requirements in Defn. 3.11. Since L is compositional and contains the formula [nok]ff, we may define φ_{T} to be the formula ([nok]ff)/T. Let s be an arbitrary state of an LTS. We can now argue that s passes T iff it satisfies ϕ_{T} thus:

s passes the test T iff (s∥root(T))\Act ⇏^{nok}
iff (s∥root(T))\Act ⊧ [nok]ff
iff (s∥root(T)) ⊧ [nok]ff

(As nok ∉ Act)

iff s ⊧ ([nok]ff)/T

(As L is compositional)

iff s ⊧ φ_{T} .

This completes the proof. □

As we shall now show, SHML is compositional with respect to tests and ∥, and thus expressive complete with respect to tests. We begin by defining a quotient construction for formulae of SHML, in the spirit of those given for different property languages and over different models in, e.g., [12, 3, 11].

Definition 3.14 (Quotient Construction). Let T be a test, and let t be one of its states. For every formula φ SHML, we define the formula φ/t (read ‘φ quotiented by t’) as shown in Table 2.

ff/t =^{def} ff
tt/t =^{def} tt
(ϕ_{1} ∧ ϕ_{2})/t =^{def} ϕ_{1}/t ∧ ϕ_{2}/t
([α]ϕ)/t =^{def} [α](ϕ/t) ∧ \begin{matrix}⋀ \\ \{ & t′ | t ⇒^{α} t′ & \} \end{matrix}(ϕ/t′) ∧ \begin{matrix}⋀ \\ \{ & (b, t′) | t ⇒^{b} t′ & \} \end{matrix}[\overline{b}](([α]ϕ)/t′)

max(X, ϕ)/t =^{def} (ϕ{max(X, ϕ)/X})/t

Table 2. Quotient construct for SHML Some remarks about the definition presented in Table 2 are now in order. The definition of the quotient formula φ/t presented ibidem should be read as yielding a finite list of recursion equations, over variables of the form ψ/t′, for every formula φ and state t of a test. The quotient formula φ/t itself is the component associated with φ/t in the largest solution of the system of equations having φ/t as leading variable. For instance, if φ is the formula [a]ff and t is a node of a

test whose only transition is t →^{b̄} t, then, as the reader can easily verify, φ/t is the largest solution of the recursion equation:

φ/t =^{def} [a]ff ∧ [b](φ/t)

which corresponds to the formula max(X, [a]ff∧ [b]X) in the property language SHML. This formula states the, intuitively clear, fact that a state of the form s ∥ t cannot perform a ⇒^{a}-transition iff s cannot execute such a step no matter how it engages in a sequence of synchronizations on b with t. Note that the quotient of a recursion-free formula may be a formula involving recursion. It can be shown that this is inevitable, because the recursion-free fragment of SHML is not compositional. Finally, we remark that, because of our finiteness restrictions on tests, the right-hand side of the defining equation for ([α]ϕ)/t is a finite conjunction of formulae.

The following key result states the correctness of the quotient construction.

Theorem 3.15. Let φ be a closed formula in SHML. Suppose that s is a state of an LTS, and t is a state of a test. Then s ∥ t ⊧ φ iff s ⊧ φ/t.

Proof. We prove the two implications separately.

– ‘Only If Implication’. Consider the environment ρ mapping each variable φ/t in the list of equations in Table 2 to the set of states {s | s∥t ⊧ φ}. We prove that ρ is a post-fixed point of the monotonic functional on environments associated with the equations in Table 2, i.e., that if s ∈ ρ(ϕ/t) then s ∈ [[ψ]]ρ, where ψ is the right-hand side of the defining equation for ϕ/t. This we now proceed to do by a case analysis on the form the formula φ may take. We only present the details for the most interesting case in the proof.

• Case: φ ≡ [α]ψ. Assume that s∥t ⊧ [α]ψ. We show that state s is contained in [[ξ]]ρ for every conjunct ξ in the right-hand side of the defining equation for ([α]ψ)/t.

∗ Case: ξ ≡ [α](ψ/t). To show that s ∈ [[ξ]]ρ, it is sufficient to prove that s′ ∈ [[ψ/t]]ρ, for every s′ such that s ⇒^{α} s′. To this end, we reason as follows:

s ⇒^{α} s′ implies s∥t ⇒^{α} s′∥t
implies s′∥t ⊧ ψ

(As s∥t ⊧ [α]ψ)

iff s′ ∈ ρ(ψ/t)

(By the definition of ρ)

iff s′ ∈ [[ψ/t]]ρ .

∗ Case: ξ ≡ ψ/t′ with t ⇒^{α} t′. To show that s ∈ [[ξ]]ρ, it is sufficient to prove that s ∈ [[ψ/t′]]ρ, for every t′ such that t ⇒^{α} t′. To this end, we reason as follows:

t ⇒^{α} t′ implies s∥t ⇒^{α} s∥t′
implies s∥t′ ⊧ ψ

(As s∥t ⊧ [α]ψ)

iff s ∈ ρ(ψ/t′)

(By the definition of ρ)

iff s ∈ [ ; [ψ/t′] ; ]ρ .

∗ Case: ξ ≡ [b̄](([α]ψ)/t′) with t ⇒^{b} t′. To show that s ∈ [[ξ]]ρ, it is

sufficient to prove that s′ ∈ [[([α]ψ)/t′]]ρ, for every s′ such that s ⇒^{b̄} s′. To this end, we reason as follows:

s ⇒^{b̄} s′ and t ⇒^{b} t′ imply s∥t ⇒^{τ} s′∥t′
implies s′∥t′ ⊧ [α]ψ

(By Propns. 3.8 and 3.9, as s∥t ⊧ [α]ψ)

iff s′ ∈ ρ(([α]ψ)/t′)

(By the definition of ρ)

iff s′ ∈ [ ; [([α]ψ)/t′] ; ]ρ .

The proof for the case ϕ ≡ [α]ψ is now complete.

– ‘If Implication’. Consider the relation R defined thus:

R =^{def} {(s∥t, φ) | s ⊧ φ/t} .

It is not hard to show that R is a satisfiability relation.

The proof of the theorem is now complete. □

Corollary 3.16. The property language SHML is compositional with respect to tests and the parallel composition operator ∥.

Proof. Given a property φ ∈ SHML and a test T, define φ/T to be the formula φ/root(T) given by the quotient construction. The claim is now an immediate consequence of Thm. 3.15. □

Theorem 3.17. The property language SHML is expressive complete.

Example 3.18. Applying the construction in the proof of Propn. 3.13, and the definition of the quotient formula to the tests

T_{1} ≡ fix(X = ā.nok.0 + b̄.X) and
T_{2} ≡ fix(X = τ.ā.nok.0 + τ.b̄.X)

yields that the formula tested by both T_{1} and T_{2} is max(X, [a]ff ∧ [b]X).

Collecting the results in Thms. 3.6 and 3.17, we have now finally completed the proof of Thm. 3.5. Thus, as claimed, the collection of testable properties coincides with that of the properties expressible in SHML. The following result gives another characterization of the expressive power of SHML which has some independent interest.

Theorem 3.19. The property language SHML is the least expressive extension of L_{nok} that is compositional with respect to tests and ∥.

Proof. Assume that L is a property language that extends L_{nok} and is compositional. We show that every property in SHML is logically equivalent to one in L, i.e., that L is at least as expressive as SHML. To this end, let φ be a property in SHML. By Thm. 3.6, there is a test T_{φ} such that s ⊧ φ iff s passes the test T_{φ}, for every state s. Since L is an extension of L_{nok} that is compositional, Propn. 3.13 yields that L is complete. Thus there is a formula ψ ∈ L such that s ⊧ ψ iff s passes the test T_{φ}, for every state s. It follows that ψ and φ are satisfied by precisely the same states, and are therefore logically equivalent. □

Acknowledgements: We thank Kim Guldstrand Larsen for previous joint work and discussions that gave us the inspiration for this study. The anonymous referees provided useful comments.

References

1. L. Aceto, P. Bouyer, A. Burgueño, and K. G. Larsen, The power of reachability testing for timed automata, in Proceedings of the Eighteenth Conference on the Foundations of Software Technology and Theoretical Computer Science, V. Arvind and R. Ramanujam, eds., Lecture Notes in Computer Science, Springer-Verlag, December 1998.

2. L. Aceto, A. Burgueño, and K. G. Larsen, Model checking via reachability testing for timed automata, in Proceedings of TACAS ’98, Lisbon, B. Steffen, ed., vol. 1384 of Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 263–280.

3. H. R. Andersen, Partial model checking (extended abstract), in Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science, San Diego, California, 26–29 June 1995, IEEE Computer Society Press, pp. 398–407.

4. R. De Nicola and M. Hennessy, Testing equivalences for processes, Theoretical Comput. Sci., 34 (1984), pp. 83–133.

5. D. M. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, On the temporal basis of fairness, in Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, Jan. 1980, pp. 163–173.

6. M. Hennessy, Algebraic Theory of Processes, MIT Press, Cambridge, Massachusetts, 1988.

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

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

9. S. Kleene, Representation of events in nerve nets and finite automata, in Automata Studies, C. Shannon and J. McCarthy, eds., Princeton University Press, 1956, pp. 3–41.

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

11. F. Laroussinie, K. G. Larsen, and C. Weise, From timed automata to logic - and back, in Mathematical Foundations of Computer Science 1995, 20th International Symposium, J. Wiedermann and P. Hájek, eds., vol. 969 of Lecture Notes in Computer Science, Prague, Czech Republic, 28 Aug.–1 Sept. 1995, Springer-Verlag, pp. 529–539.

12. K. G. Larsen and L. Xinxin, Compositionality through an operational semantics of contexts, Journal of Logic and Computation, 1 (1991), pp. 761–795.

13. R. Milner, Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.

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

15. A. Stoughton, Substitution revisited, Theoretical Comput. Sci., 59 (1988), pp. 317–325.

16. A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, 5 (1955), pp. 285–309.

17. M. Y. Vardi and P. Wolper, Reasoning about infinite computations, Information and Computation, 115 (1994), pp. 1–37.

Recent BRICS Report Series Publications

RS-98-50 Luca Aceto and Anna Ingólfsdóttir. Testing Hennessy-Milner Logic with Recursion. December 1998. 15 pp. To appear in Thomas, editor, Foundations of Software Science and Computation Structures: Second International Conference, FoSSaCS ’99 Proceedings, LNCS, 1998.

RS-98-49 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. A Cook’s Tour of Equational Axiomatizations for Prefix Iteration. December 1998. 14 pp. Appears in Nivat, editor, Foundations of Software Science and Computation Structures: First International Conference, FoSSaCS ’98 Proceedings, LNCS 1378, 1998, pages 20–34.

RS-98-48 Luca Aceto, Patricia Bouyer, Augusto Burgueño, and Kim G. Larsen. The Power of Reachability Testing for Timed Automata. December 1998. 12 pp. Appears in Arvind and Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science: 18th Conference, FST&TCS ’98 Proceedings, LNCS 1530, 1998, pages 245–256.

RS-98-47 Gerd Behrmann, Kim G. Larsen, Justin Pearson, Carsten Weise, and Yi Wang. Efficient Timed Reachability Analysis using Clock Difference Diagrams. December 1998. 13 pp.

RS-98-46 Kim G. Larsen, Carsten Weise, Yi Wang, and Justin Pearson. Clock Difference Diagrams. December 1998. 18 pp.

RS-98-45 Morten Vadskær Jensen and Brian Nielsen. Real-Time Layered Video Compression using SIMD Computation. December 1998. 37 pp. Appears in Zinterhof, Vajtersic and Uhl, editors, Parallel Computing: Fourth International ACPC Conference, ACPC ’99 Proceedings, LNCS 1557, 1999.

RS-98-44 Brian Nielsen and Gul Agha. Towards Re-usable Real-Time Objects. December 1998. 36 pp. To appear in The Annals of Software Engineering, IEEE, 7, 1999.

RS-98-43 Peter D. Mosses. CASL: A Guided Tour of its Design. December 1998. 31 pp. To appear in Fiadeiro, editor, Recent Trends in Algebraic Development Techniques: 13th Workshop, WADT ’98 Selected Papers, LNCS, 1999.