Uli Fahrenberg

Axel Legay

Louis-Marie Traonouez

Structural Refinement for the Modal nu-Calculus

We introduce a new notion of structural refinement, a sound abstraction of logical implication, for the modal nu-calculus. Using new translations between the modal nu-calculus and disjunctive modal transition systems, we show that these two specification formalisms are structurally equivalent. Using our translations, we also transfer the structural operations of composition and quotient from disjunctive modal transition systems to the modal nu-calculus. This shows that the modal nu-calculus supports composition and decomposition of specifications.

Introduction

There are two conceptually different approaches for the specification and verification of properties of formal models. Logical approaches make use of logical formulae for expressing properties and then rely on efficient model checking algorithms for verifying whether or not a model satisfies a formula. Automata-based approaches, on the other hand, exploit equivalence or refinement checking for verifying properties, given that models and properties are specified using the same (or a closely related) formalism.

The logical approaches have been quite successful, with a plethora of logical formalisms available and a number of successful model checking tools. One particularly interesting such formalism is the modal µ-calculus [START_REF] Kozen | Results on the propositional µ-calculus[END_REF], which is universal in the sense that it generalizes most other temporal logics, yet mathematically simple and amenable to analysis.

One central problem in the verification of formal properties is state space explosion: when a model is composed of many components, the state space of the combined system quickly grows too big to be analyzed. To combat this problem, one approach is to employ compositionality. When a model consists of several components, each component would be model checked by itself, and then the components' properties would be composed to yield a property which automatically is satisfied by the combined model.

Similarly, given a global property of a model and a component of the model that is already known to satisfy a local property, one would be able to decompose automatically, from the global property and the local property, a new property which the rest of the model must satisfy. We refer to [START_REF] Larsen | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF] for a good account of these and other features which one would wish specifications to have.

As an alternative to logical specification formalisms and with an eye to compositionality and decomposition, automata-based behavioral specifications were introduced in [START_REF] Larsen | Modal specifications[END_REF]. Here the specification formalism is a generalization of the modeling formalism, and the satisfaction relation between models and specifications is generalized to a refinement relation between specifications, which resembles simulation and bisimulation and can be checked with similar algorithms.

For an example, we refer to Fig. 1 which shows the property informally specified as "after a req(uest), no idle(ing) is allowed, but only work, until grant is executed" using the logical formalisms of CTL [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF] and the modal µ-calculus [START_REF] Kozen | Results on the propositional µ-calculus[END_REF] and the behavioral formalism of disjunctive modal transition systems [START_REF] Larsen | Equation solving using modal transition systems[END_REF].

The precise relationship between logical and behavioral specification formalisms has been subject to some investigation. In [START_REF] Larsen | Modal specifications[END_REF], Larsen shows that any modal transition system can be translated to a formula in Hennessy-Milner logic which is equivalent in the sense of admitting the same models. Conversely, Boudol and Larsen show in [START_REF] Boudol | Graphical versus logical specifications[END_REF] that any formula in Hennessy-Milner logic is equivalent to a finite disjunction of modal transition systems.

We have picked up this work in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF], where we show that any disjunctive modal transition system (DMTS) is equivalent to a formula in the modal ν-calculus, the safety fragment of the modal µ-calculus which uses only maximal fixed points, and vice versa. (Note that the modal ν-calculus is equivalent to Hennessy-Milner logic with recursion and maximal fixed points.) Moreover, we show in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] that DMTS are as expressive as (non-deterministic) acceptance automata [START_REF] Raclet | Residual for component specifications[END_REF][START_REF] Raclet | Residual for component specifications[END_REF]. Together with the inclusions of [START_REF] Beneš | Parametric modal transition systems[END_REF], this settles the expressivity question for behavioral specifications: they are at most as expressive as the modal ν-calculus.

In this paper, we show that not only are DMTS as expressive as the modal ν-calculus, but the two formalisms are structurally equivalent. Introducing a new notion of structural refinement for the modal ν-calculus (a sound abstraction of logical implication), we show that one can freely translate between the modal ν-calculus and DMTS, while preserving structural refinement.

DMTS form a complete specification theory [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] in that they both admit logical operations of conjunction and disjunction and structural operations of composition and quotient [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]. Hence they support full compositionality and decomposition in the sense of [START_REF] Larsen | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF]. Using our translations, we can transport these notions to the modal ν-calculus, thus also turning the modal ν-calculus into a complete specification theory.

In order to arrive at our translations, we first recall DMTS and (non-deterministic) acceptance automata in Section 2. We also introduce a new hybrid modal logic, which can serve as compact representation for acceptance automata and should be of interest in itself. Afterwards we show, using the translations introduced in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF], that these formalisms are structurally equivalent.

In Section 3 we recall the modal ν-calculus and review the translations between DMTS and the modal ν-calculus which were introduced in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]. These in turn are based on work by Boudol and Larsen in [START_REF] Boudol | Graphical versus logical specifications[END_REF][START_REF] Larsen | Modal specifications[END_REF], hence fairly standard. We show that, though semantically correct, the two translations are structurally mismatched in that they relate DMTS refinement to two different notions of ν-calculus refinement. To fix the mismatch, we introduce a new translation from the modal ν-calculus to DMTS and show that using this translation, the two formalisms are structurally equivalent.

In Section 4, we use our translations to turn the modal ν-calculus into a complete specification theory. We remark that all our translations and constructions are based on a new normal form for ν-calculus expressions, and that turning a ν-calculus expression into normal form may incur an exponential blow-up. However, the translations and constructions preserve the normal form, so that this translation only need be applied once in the beginning.

We also note that composition and quotient operators are used in other logics such as e.g. spatial [START_REF] Caires | A spatial logic for concurrency[END_REF] or separation logics [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF][START_REF] O'hearn | Local reasoning about programs that alter data structures[END_REF]. However, in these logics they are treated as first-class operators, i.e. as part of the formal syntax. In our approach, on the other hand, they are defined as operations on logical expressions which as results again yield logical expressions (without compositions or quotients).

Note that some proofs have been relegated to a separate appendix.

Structural Specification Formalisms

Let Σ be a finite set of labels. A labeled transition system (LTS) is a structure I = (S, S 0 , -→) consisting of a finite set of states S, a subset S 0 ⊆ S of initial states and a transition relation -→ ⊆ S × Σ × S.

Disjunctive modal transition systems. A disjunctive modal transition system (DMTS) is a structure D = (S, S 0 , , -→) consisting of finite sets S ⊇ S 0 of states and initial states, a may-transition relation ⊆ S × Σ × S, and a disjunctive must-transition relation -→ ⊆ S × 2 Σ×S . It is assumed that for all (s, N ) ∈ -→ and all (a, t) ∈ N , (s, a, t) ∈ . As customary, we write s a t instead of (s, a, t) ∈ , s -→ N instead of (s, N ) ∈ -→, s a if there exists t for which s a t, and s a if there does not.

The intuition is that may-transitions s a t specify which transitions are permitted in an implementation, whereas a must-transitions s -→ N stipulates a disjunctive requirement: at least one of the choices (a, t) ∈ N must be imple-mented. A DMTS (S, S 0 , , -→) is an implementation if -→ = {(s, {(a, t)}) | s a t}; DMTS implementations are precisely LTS.

DMTS were introduced in [START_REF] Larsen | Equation solving using modal transition systems[END_REF] in the context of equation solving, or quotient, for specifications and are used e.g. in [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF] for LTL model checking. They are a natural closure of modal transition systems (MTS) [START_REF] Larsen | Modal specifications[END_REF] in which all disjunctive must-transitions s -→ N lead to singletons N = {(a, t)}.

Let

D 1 = (S 1 , S 0 1 , 1 , -→ 1 ), D 2 = (S 2 , S 0 2 , 2 , -→ 2 ) be DMTS. A relation R ⊆ S 1 × S 2 is a modal refinement if it holds for all (s 1 , s 2 ) ∈ R that -for all s 1 a t
(s 0 1 , s 0 2 ) ∈ R. We write D 1 ≡ m D 2 if D 1 ≤ m D 2 and D 2 ≤ m D 1 . For states s 1 ∈ S 1 , s 2 ∈ S 2 , we write s 1 ≤ m s 2 if the DMTS (S 1 , {s 1 }, 1 , -→ 1 ) ≤ m (S 2 , {s 2 }, 2 , -→ 2 ).
Note that modal refinement is reflexive and transitive, i.e. a preorder on DMTS. Also, the relation on states ≤ m ⊆ S 1 × S 2 defined above is itself a modal refinement, indeed the maximal modal refinement under the subset ordering.

The set of implementations of an DMTS D is D = {I ≤ m D | I implement-ation}. This is, thus, the set of all LTS which satisfy the specification given by the DMTS D. We say that D 1 thoroughly refines D 2 , and write

D 1 ≤ th D 2 , if D 1 ⊆ D 2 . We write D 1 ≡ th D 2 if D 1 ≤ th D 2 and D 2 ≤ th D 1 . For states s 1 ∈ S 1 , s 2 ∈ S 2 , we write s 1 = (S 1 , {s 1 }, 1 , -→ 1 ) and s 1 ≤ th s 2 if s 1 ⊆ s 2 .
The below proposition, which follows directly from transitivity of modal refinement, shows that modal refinement is sound with respect to thorough refinement; in the context of specification theories, this is what one would expect, and we only include it for completeness of presentation. It can be shown that modal refinement is also complete for deterministic DMTS [START_REF] Beneš | On determinism in modal transition systems[END_REF], but we will not need this here.

Proposition 1. For all DMTS D 1 , D 2 , D 1 ≤ m D 2 implies D 1 ≤ th D 2 . ⊓ ⊔
We introduce a new construction on DMTS which will be of interest for us; intuitively, it adds all possible may-transitions without changing the implementation semantics. The may-completion of a DMTS D = (S, S 0 , ,

-→) is mc(D) = (S, S 0 , mc , -→) with mc = {(s, a, t ′ ) ⊆ S × Σ × S | ∃(s, a, t) ∈ : t ′ ≤ th t}.
Note that to compute the may-completion of a DMTS, one has to decide thorough refinements, hence this computation (or, more precisely, deciding whether a given DMTS is may-complete) is EXPTIME-complete [START_REF] Beneš | EXPTIME-completeness of thorough refinement on modal transition systems[END_REF]. We show an example of a may-completion in Fig. 2. Proof. It is always the case that D ≤ m D, and adding may transitions on the right side preserves modal refinement. Therefore it is immediate that D ≤ m mc(D), hence also D ≤ th mc(D).

s ′ t ′ 1 t ′ 3 u ′ 1 u ′ 2 u ′ 3 v ′ 1 v ′
To prove that mc(D) ≤ th D, we consider an implementation I ≤ m mc(D); we must prove that I ≤ m D. Write D = (S, S 0 , , -→), I = (I, I 0 , I , -→ I ) and mc(D) = (S, S 0 , mc , -→). Let R ⊆ I × S be the largest modal refinement between I and mc(D). We now prove that R is also a modal refinement between I and D. For all (i, d) ∈ R:

-For all i a I i ′ , there exists d ′ ∈ S such that d a mc d ′ and (i ′ , d ′ ) ∈ R.
Then by definition of mc , there exists d ′′ ∈ S such that d a d ′′ and

d ′ ⊆ d ′′ . (i ′ , d ′ ) ∈ R implies i ′ ∈ d ′ , which implies i ′ ∈ d ′′ . This means that i ′ ≤ m d ′′ ,
I 0 , -→) ∈ t 3 with modal refinement R ⊆ I × {t 3 , u 3 , v 3 }, define R ′ ⊆ I × {t 1 , u 1 , u 2 , v 1 } by R ′ = {(i, t 1 ) | (i, t 3 ) ∈ R} ∪ {(i, v 1 ) | (i, v 3 ) ∈ R} ∪ {(i, u 1 ) | (i, u 3 ) ∈ R, i a -→} ∪ {(i, u 2 ) | (i, u 3 ) ∈ R, i a -→}, then R ′ is a modal refinement I ≤ m t 1 . Similarly, t ′ 3 ≤ th t ′ 1 in mc(D). On the other hand, t 3 ≤ m t 1 (and similarly, t ′ 3 ≤ m t ′ 1 ), because neither u 3 ≤ m u 1 nor u 3 ≤ m u 2
. Now in the modal refinement game between mc(D) and D, the may-transition s ′ a t ′ 3 has to be matched by

s a t 1 , but then t ′ 3 ≤ m t 1 , hence mc(D) ≤ m D.
Also, the may-completion does not necessarily preserve modal refinement: Consider the DMTS D from Fig. 2 and D 1 from Fig. 3, and note first that double-prime cousins in D 1 ), but mc(D) ≤ m mc(D 1 ) = D 1 : the may-transition s ′ a t ′ 3 has to be matched by s ′′ a t ′′ 1 and t ′ 3 ≤ m t ′′ 1 . Lastly, the may-completion can also create modal refinement: Considering the DMTS D 2 from Fig. 3, we see that

mc(D 1 ) = D 1 . It is easy to see that D ≤ m D 1 (just match states in D with their D1 s ′′ t ′′ 1 u ′′ 1 u ′′ 2 v ′′ 1 a a a a b, c d D2 s ′′ t ′′ u ′′ v ′′ a a a b
D 2 ≤ m D, but mc(D 2 ) = D 2 ≤ m mc(D).
Acceptance automata. A (non-deterministic) acceptance automaton (AA) is a structure A = (S, S 0 , Tran), with S ⊇ S 0 finite sets of states and initial states and Tran : S → 2 2 Σ×S an assignment of transition constraints. We assume that for all s 0 ∈ S 0 , Tran(s 0 ) = ∅.

An AA is an implementation if it holds for all s ∈ S that Tran(s) = {M } is a singleton; hence also AA implementations are precisely LTS. Acceptance automata were first introduced in [START_REF] Raclet | Residual for component specifications[END_REF] (see also [START_REF] Raclet | Residual for component specifications[END_REF], where a slightly different language-based approach is taken), based on the notion of acceptance trees in [START_REF] Hennessy | Acceptance trees[END_REF]; however, there they are restricted to be deterministic. We employ no such restriction here. The following notion of modal refinement for AA was also introduced in [START_REF] Raclet | Residual for component specifications[END_REF].

Let

A 1 = (S 1 , S 0 1 , Tran 1 ) and A 2 = (S 2 , S 0 2 , Tran 2 ) be AA. A relation R ⊆ S 1 ×S 2 is a modal refinement if it holds for all (s 1 , s 2 ) ∈ R and all M 1 ∈ Tran 1 (s 1 ) that there exists M 2 ∈ Tran 2 (s 2 ) such that -∀(a, t 1 ) ∈ M 1 : ∃(a, t 2 ) ∈ M 2 : (t 1 , t 2 ) ∈ R, -∀(a, t 2 ) ∈ M 2 : ∃(a, t 1 ) ∈ M 1 : (t 1 , t 2 ) ∈ R.
As for DMTS, we write A 1 ≤ m A 2 whenever there exists a modal refinement R such that for all s 0 1 ∈ S 0 1 , there exists s 0 2 ∈ S 0 2 for which (s 0 1 , s 0 2 ) ∈ R. Sets of implementations and thorough refinement are defined as for DMTS. Note that as both AA and DMTS implementations are LTS, it makes sense to use thorough refinement and equivalence across formalisms, writing e.g. A ≡ th D for an AA A and a DMTS D.

Hybrid modal logic. We introduce a hybrid modal logic which can serve as compact representation of AA. This logic is closely related to the Boolean modal transition systems of [START_REF] Beneš | Parametric modal transition systems[END_REF] and hybrid in the sense of [START_REF] Prior | Papers on Time and Tense[END_REF][START_REF] Blackburn | Representation, reasoning, and relational structures: a hybrid logic manifesto[END_REF]: it contains nominals, and the semantics of a nominal is given as all sets which contain the nominal.

For a finite set X of nominals, let L(X) be the set of formulae generated by the abstract syntax L(X) ∋ φ := tt | ff | a x | ¬φ | φ ∧ φ, for a ∈ Σ and x ∈ X. The semantics of a formula is a set of subsets of Σ × X, given as follows:

tt = 2 Σ×X , ff = ∅, ¬φ = 2 Σ×X \ φ , a x = {M ⊆ Σ × X | (a, x) ∈ M }, and φ ∧ ψ = φ ∩ ψ . We also define disjunction φ 1 ∨ φ 2 = ¬(φ 1 ∧ φ 2 ).
An L-expression is a structure E = (X, X 0 , Φ) consisting of finite sets X 0 ⊆ X of variables and a mapping Φ : X → L(X). Such an expression is an implementation if Φ(x) = {M } is a singleton for each x ∈ X. It can easily be shown that L-implementations precisely correspond to LTS.

Let

E 1 = (X 1 , X 0 1 , Φ 1 ) and E 2 = (X 2 , X 0 2 , Φ 2 ) be L-expressions. A relation R ⊆ X 1 × X 2 is a modal refinement if it holds for all (x 1 , x 2 ) ∈ R and all M 1 ∈ Φ 1 (x 1 ) that there exists M 2 ∈ Φ 2 (x 2 ) such that -∀(a, t 1 ) ∈ M 1 : ∃(a, t 2 ) ∈ M 2 : (t 1 , t 2 ) ∈ R, -∀(a, t 2 ) ∈ M 2 : ∃(a, t 1 ) ∈ M 1 : (t 1 , t 2 ) ∈ R. Again, we write E 1 ≤ m E 2
whenever there exists such a modal refinement R such that for all x 0 1 ∈ X 0 1 , there exists x 0 2 ∈ X 0 2 for which (x 0 1 , x 0 2 ) ∈ R. Sets of implementations and thorough refinement are defined as for DMTS.

Structural equivalence. We proceed to show that the three formalisms introduced in this section are structurally equivalent. Using the translations between AA and DMTS discovered in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] and new translations between AA and hybrid logic, we show that these respect modal refinement.

The translations al, la between AA and our hybrid logic are straightforward: For an AA A = (S, S 0 , Tran) and all s ∈ S, let

Φ(s) = M∈Tran(s) (a,t)∈M a t ∧ (b,u) / ∈M ¬ b u
and define the L-expression al(A) = (S, S 0 , Φ).

For an L-expression E = (X, X 0 , Φ) and all x ∈ X, let Tran(x) = Φ(x) and define the AA la(E) = (X, X 0 , Tran).

The translations da, ad between DMTS and AA were discovered in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]. For a DMTS D = (S, S 0 , , -→) and all s ∈ S, let

Tran(s) = {M ⊆ Σ × S | ∀(a, t) ∈ M : s a t, ∀s -→ N : N ∩ M = ∅}
and define the AA da(D) = (S, S 0 , Tran). 1For an AA A = (S, S 0 , Tran), define the DMTS ad(A) = (D, D 0 , , -→) as follows:

D = {M ∈ Tran(s) | s ∈ S} D 0 = {M 0 ∈ Tran(s 0 ) | s 0 ∈ S 0 } -→ = M, {(a, M ′ ) | M ′ ∈ Tran(t)} (a, t) ∈ M = {(M, a, M ′ ) | ∃M -→ N : (a, M ′ ) ∈ N }
Note that the state spaces of A and ad(A) are not the same; the one of ad(A) may be exponentially larger. The following lemma shows that this explosion is unavoidable: Lemma 4. There exists a one-state AA A for which any DMTS D ≡ th A has at least 2 n-1 states, where n is the size of the alphabet Σ.

We notice that LTS are preserved by all translations: for any LTS I, al(I) = la(I) = da(I) = ad(I) = I. In [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] it is shown that the translations between AA and DMTS respect sets of implementations, i.e. that da(D) ≡ th D and ad(A) ≡ th A for all DMTS D and all AA A. The next theorem shows that these and the other presented translations respect modal refinement, hence these formalisms are not only semantically equivalent, but structurally equivalent.

Theorem 5. For all AA A 1 , A 2 , DMTS D 1 , D 2 and L-expressions E 1 , E 2 : 1. A 1 ≤ m A 2 iff al(A 1 ) ≤ m al(A 2 ), 2. E 1 ≤ m E 2 iff la(E 1 ) ≤ m la(E 2 ), 3. D 1 ≤ m D 2 iff da(D 1 ) ≤ m da(D 2 ), and 4. A 1 ≤ m A 2 iff ad(A 1 ) ≤ m ad(A 2 ).
Proof (sketch). We give a few hints about the proofs of the equivalences; the details can be found in appendix. The first two equivalences follow easily from the definitions, once one notices that for both translations, Φ(x) = Tran(x) for all x ∈ X. For the third equivalence, we can show that a DMTS modal refinement D 1 ≤ m D 2 is also an AA modal refinement da(D 1 ) ≤ m da(D 2 ) and vice versa.

The fourth equivalence is slightly more tricky, as the state space changes.

If R ⊆ S 1 × S 2 is an AA modal refinement relation witnessing A 1 ≤ m A 2 , then we can construct a DMTS modal refinement R ′ ⊆ D 1 × D 2 , which witnesses ad(A 1 ) ≤ m ad(A 2 ), by R ′ = {(M 1 , M 2 ) | ∃(s 1 , s 2 ) ∈ R : M 1 ∈ Tran 1 (s 1 ), M 2 ∈ Tran(s 2 ), ∀(a, t 1 ) ∈ M 1 : ∃(a, t 2 ) ∈ M 2 : (t 1 , t 2 ) ∈ R, ∀(a, t 2 ) ∈ M 2 : ∃(a, t 1 ) ∈ M 1 : (t 1 , t 2 ) ∈ R}. Conversely, if R ⊆ D 1 × D 2 is a DMTS modal refinement witnessing ad(A 1 ) ≤ m ad(A 2 ), then R ′ ⊆ S 1 × S 2 given by R ′ = {(s 1 , s 2 ) | ∀M 1 ∈ Tran 1 (s 1 ) : ∃M 2 ∈ Tran 2 (s 2 ) : (M 1 , M 2 ) ∈ R} is an AA modal refinement. ⊓ ⊔
The result on thorough equivalence from [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] now easily follows:

Corollary 6. For all AA A, DMTS D and L-expressions E, al(A) ≡ th A, la(E) ≡ th E, da(D) ≡ th D, and ad(A) ≡ th A. ⊓ ⊔ Also soundness of modal refinement for AA and hybrid logic follows directly from Theorem 5:

Corollary 7. For all AA A 1 and A 2 , A 1 ≤ m A 2 implies A 1 ≤ th A 2 . For all L-expressions E 1 and E 2 , E 1 ≤ m E 2 implies E 1 ≤ th E 2 .
⊓ ⊔

The Modal ν-Calculus

We wish to extend the structural equivalences of the previous section to the modal ν-calculus. Using translations between AA, DMTS and ν-calculus based on work in [START_REF] Larsen | Modal specifications[END_REF][START_REF] Boudol | Graphical versus logical specifications[END_REF], it has been shown in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] that ν-calculus and DMTS/AA are semantically equivalent. We will see below that there is a mismatch between the translations from [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] (and hence between the translations in [START_REF] Larsen | Modal specifications[END_REF][START_REF] Boudol | Graphical versus logical specifications[END_REF]) which precludes structural equivalence and then proceed to propose a new translation which fixes the mismatch.

Syntax and semantics. We first recall the syntax and semantics of the modal ν-calculus, the fragment of the modal µ-calculus [START_REF] Scott | A theory of programs[END_REF][START_REF] Kozen | Results on the propositional µ-calculus[END_REF] with only maximal fixed points. Instead of an explicit maximal fixed point operator, we use the representation by equation systems in Hennessy-Milner logic developed in [START_REF] Larsen | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF]. For a finite set X of variables, let H(X) be the set of Hennessy-Milner formulae, generated by the abstract syntax H(X) ∋ φ ::

= tt | ff | x | a φ | [a]φ | φ ∧ φ | φ ∨ φ, for a ∈ Σ and x ∈ X.
A declaration is a mapping ∆ : X → H(X); we recall the maximal fixed point semantics of declarations from [START_REF] Larsen | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF]. Let (S, S 0 , -→) be an LTS, then an assignment is a mapping σ : X → 2 S . The set of assignments forms a complete lattice with order σ 1 ⊑ σ 2 iff σ 1 (x) ⊆ σ 2 (x) for all x ∈ X and lowest upper bound i∈I σ i (x) = i∈I σ i (x). The semantics of a formula is a subset of S, given relative to an assignment σ, defined as follows:

tt σ = S, ff σ = ∅, x σ = σ(x), φ ∧ ψ σ = φ σ ∩ ψ σ, φ ∨ ψ σ = φ σ ∪ ψ σ, and
a φ σ = {s ∈ S | ∃s a -→ s ′ : s ′ ∈ φ σ}, [a]φ σ = {s ∈ S | ∀s a -→ s ′ : s ′ ∈ φ σ}.
The semantics of a declaration ∆ is then the assignment defined by

∆ = {σ : X → 2 S | ∀x ∈ X : σ(x) ⊆ ∆(x) σ};
the maximal (pre)fixed point of ∆.

A ν-calculus expression is a structure N = (X, X 0 , ∆), with X 0 ⊆ X sets of variables and ∆ : X → H(X) a declaration. We say that an LTS I = (S, S 0 , -→) implements (or models) the expression, and write I |= N , if it holds that for all s 0 ∈ S 0 , there is x 0 ∈ X 0 such that s 0 ∈ ∆ (x 0 ). We write N for the set of implementations (models) of a ν-calculus expression N . As for DMTS, we write x = (X, {x}, ∆) for x ∈ X, and thorough refinement of expressions and states is defined accordingly.

The following lemma introduces a normal form for ν-calculus expressions:

Lemma 8. For any ν-calculus expression N 1 = (X 1 , X 0 1 , ∆ 1 ), there exists another expression N 2 = (X 2 , X 0 2 , ∆ 2 ) with N 1 = N 2 and such that for any x ∈ X, ∆ 2 (x) is of the form

∆ 2 (x) = i∈I j∈Ji a ij x ij ∧ a∈Σ [a] j∈Ja y a,j (1)
for finite (possibly empty) index sets I, J i , J a , for i ∈ I and a ∈ Σ, and all x ij , y a,j ∈ X 2 . Additionally, for all i ∈ I and j ∈ J i , there exists j ′ ∈ J aij for which x ij ≤ th y aij,j ′ .

As this is a type of conjunctive normal form, it is clear that translating a ν-calculus expression into normal form may incur an exponential blow-up.

We introduce some notation for ν-calculus expressions in normal form which will make our life easier later. Let N = (X, X 0 , ∆) be such an expression and x ∈ X, with ∆(x) = i∈I j∈Ji a ij x ij ∧ a∈Σ [a] j∈Ja y a,j as in the lemma.

Define ♦(x) = {{(a ij , x ij ) | j ∈ J i } | i ∈ I} and, for each a ∈ Σ, a (x) = {y a,j | j ∈ J a }. Note that now ∆(x) = N ∈♦(x) (a,y)∈N a y ∧ a∈Σ [a] y∈ a (x) y .
Refinement. In order to expose our structural equivalence, we need to introduce a notion of modal refinement for the modal ν-calculus. For reasons which will become apparent later, we define two different such notions:

Let

N 1 = (X 1 , X 0 1 , ∆ 1 ), N 2 = (X 2 , X 0 2 , ∆ 2 ) be ν-calculus expressions in normal form and R ⊆ X 1 × X 2 . The relation R is a modal refinement if it holds for all (x 1 , x 2 ) ∈ R that 1.
for all a ∈ Σ and every y 1 ∈ a 1 (x 1 ), there is y 2 ∈ a 2 (x 2 ) for which (y 1 , y 2 ) ∈ R, and 2. for all

N 2 ∈ ♦ 2 (x 2 ) there is N 1 ∈ ♦ 1 (x 1 ) such that for each (a, y 1 ) ∈ N 1 , there exists (a, y 2 ) ∈ N 2 with (y 1 , y 2 ) ∈ R.
R is a modal-thorough refinement if, instead of 1., it holds that 1 ′ . for all a ∈ Σ, all y 1 ∈ a 1 (x 1 ) and every y ′ 1 ∈ X 1 with y ′ 1 ≤ th y 1 , there is y 2 ∈ a 2 (x 2 ) and y ′ 2 ∈ X 2 such that y ′ 2 ≤ th y 2 and (y ′ 1 , y ′ 2 ) ∈ R.

We say that N 1 refines N 2 whenever there exists such a refinement R such that for every x 0 1 ∈ X 0 1 there exists x 0 2 ∈ X 0 2 for which (x 0 1 , x 0 2 ) ∈ R. We write N 1 ≤ m N 2 in case of modal and N 1 ≤ mt N 2 in case of modal-thorough refinement.

We remark that whereas modal refinement for ν-calculus expressions is a simple and entirely syntactic notion, modal-thorough refinement involves semantic inclusions of states. Using results in [START_REF] Beneš | EXPTIME-completeness of thorough refinement on modal transition systems[END_REF], this implies that modal refinement can be decided in time polynomial in the size of the (normal-form) expressions, whereas deciding modal-thorough refinement is EXPTIME-complete.

Translation from DMTS to ν-calculus. Our translation from DMTS to νcalculus is new, but similar to the translation from AA to ν-calculus given in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]. This in turn is based on the characteristic formulae of [START_REF] Larsen | Modal specifications[END_REF] (see also [START_REF] Aceto | Reactive Systems[END_REF]).

For a DMTS D = (S, S 0 , , -→) and all s ∈ S, we define ♦(s) = {N | s -→ N } and, for each a ∈ Σ, a (s) = {t | s a t}. Then, let Note how the formula precisely expresses that we demand at least one of every choice of disjunctive must-transitions (first part) and permit all may-transitions (second part); this is also the intuition of the characteristic formulae of [START_REF] Larsen | Modal specifications[END_REF]. Using results of [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] (which introduces a very similar translation from AA to ν-calculus expressions), we see that dh(D) ≡ th D for all DMTS D. Proof. For the forward direction, let R ⊆ S 1 ×S 2 be a modal refinement between

∆(s) = N ∈♦(s) (a,t)∈N a t ∧ a∈Σ [a]
D 1 = (S 1 , S 0 1 , 1 , -→ 1 ) and D 2 = (S 2 , S 0 2 , 2 , -→ 2 ); we show that R is also a modal refinement between dh(D 1 ) = (S 1 , S 0 1 , ∆ 1 ) and dh(D 2 ) = (S 2 , S 0 2 , ∆ 2 ). Let (s 1 , s 2 ) ∈ R.
-Let a ∈ Σ and t 1 ∈ a 1 (s 1 ), then s 1 a 1 t 1 , which implies that there is

t 2 ∈ S 2 for which s 2 a 2 t 2 and (t 1 , t 2 ) ∈ R. By definition of a 2 , t 2 ∈ a 2 (s 2 ). -Let N 2 ∈ ♦ 2 (s 2 ), then s 2 -→ 2 N 2 , which implies that there exists s 1 -→ 1 N 1 such that ∀(a, t 1 ) ∈ N 1 : ∃(a, t 2 ) ∈ N 2 : (t 1 , t 2 ) ∈ R. By definition of a 1 , N 1 ∈ a 1 (s 1
). For the other direction, let R ⊆ S 1 × S 2 be a modal refinement between dh(D 1 ) and dh(D 2 ), we show that R is also a modal refinement between D 1 and

D 2 . Let (s 1 , s 2 ) ∈ R. -For all s 1 a 1 t 1 , t 1 ∈ a 1 (s 1 ), which implies that there is t 2 ∈ a 2 (s 2 ) with (t 1 , t 2 ) ∈ R, and by definition of a 2 , s 2 a 2 t 2 . -For all s 2 -→ 2 N 2 , N 2 ∈ ♦ 2 (s 2 ), which implies that there is N 1 ∈ ♦ 1 (s 1 )
such that ∀(a, t 1 ) ∈ N 1 : ∃(a, t 2 ) ∈ N 2 : (t 1 , t 2 ) ∈ R, and by definition of a 1 ,

s 1 -→ 1 N 1 . ⊓ ⊔
Old translation from ν-calculus to DMTS. We recall the translation from ν-calculus to DMTS given in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF], which is based on a translation from Hennessy-Milner formulae (without recursion and fixed points) to sets of acyclic MTS in [START_REF] Boudol | Graphical versus logical specifications[END_REF]. For a ν-calculus expression N = (X, X 0 , ∆) in normal form, let

= {(x, a, y ′ ) ∈ X × Σ × X | ∃y ∈ a (x) : y ′ ≤ th y}, -→ = {(x, N ) | x ∈ X, N ∈ ♦(x)}.
and define the DMTS hd t (N ) = (X, X 0 , , -→). Note how this translates diamonds to disjunctive must-transitions directly, but for boxes takes semantic inclusions into account: for a subformula [a]y, maytransitions are created to all variables which are semantically below y. This is consistent with the interpretation of formulae-as-properties: [a]y means "for any a-transition, ∆(y) must hold"; but ∆(y) holds for all variables which are semantically below y.

It follows from results in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] (which uses a slightly different normal form for ν-calculus expressions) that hd t (N ) ≡ th N for all ν-calculus expressions N .

Theorem 10. For all ν-calculus expressions, N 1 ≤ mt N 2 iff hd t (N 1 ) ≤ m hd t (N 2 ).

Proof. For the forward direction, let R ⊆ X 1 × X 2 be a modal-thorough refinement between N 1 = (X 1 , X 0 1 , ∆ 1 ) and N 2 = (X 2 , X 0 2 , ∆ 2 ). We show that R is also a modal refinement between hd t (N

1 ) = (X 1 , X 0 1 , 1 , -→ 2 ) and hd t (N 2 ) = (X 2 , X 0 2 , 2 , -→ 2 ). Let (x 1 , x 2 ) ∈ R. -Let x 1 a 1 y ′ 1 .
By definition of 1 , there is y 1 ∈ a 1 (x 1 ) for which y ′ 1 ≤ th y 1 . Then by modal-thorough refinement, this implies that there exists

y 2 ∈ a 2 (x 2 ) and y ′ 2 ∈ X 2 such that y ′ 2 ≤ th y 2 and (y ′ 1 , y ′ 2 ) ∈ R. By definition of 2 we have x 2 a 2 y ′ 2 . -Let x 2 -→ 2 N 2 , then we have N 2 ∈ ♦ 2 (x 2 )
. By modal-thorough refinement, this implies that there is

N 1 ∈ ♦ 1 (x 1 ) such that ∀(a, y 1 ) ∈ N 1 : ∃(a, y 2 ) ∈ N 2 : (y 1 , y 2 ) ∈ R. By definition of -→ 1 , x 1 -→ 1 N 1 . Now to the proof that hd t (N 1 ) ≤ m hd t (N 2 ) implies N 1 ≤ mt N 2 . We have a modal refinement (in the DMTS sense) R ⊆ X 1 × X 2 . We must show that R is also a modal-thorough refinement. Let (x 1 , x 2 ) ∈ R. -Let a ∈ Σ, y 1 ∈ a 1 (x 1 ) and y ′ 1 ∈ X 1 such that y ′ 1 ≤ th y 1 . Then by definition of 1 , x 1 a 1 y ′ 1
. By modal refinement, this implies that there exists

x 2 a 2 y ′ 2 with (y ′ 1 , y ′ 2 ) ∈ R.
Finally, by definition of 2 , there exists

y 2 ∈ a 2 (x 2 ) such that y ′ 2 ≤ th y 2 . -Let N 2 ∈ ♦ 2 (x 2 ), then by definition of -→ 2 , x 2 -→ 2 N 2 .
Then, by modal refinement, this implies that there exists

x 1 -→ 1 N 1 such that ∀(a, y 1 ) ∈ N 1 : ∃(a, y 2 ) ∈ N 2 : (y 1 , y 2 ) ∈ R. By definition of -→ 1 , N 1 ∈ a 1 (x 1 ). ⊓ ⊔
Discussion. Notice how Theorems 9 and 10 expose a mismatch between the translations: dh relates DMTS refinement to ν-calculus modal refinement, whereas hd t relates it to modal-thorough refinement. Both translations are well-grounded in the literature and well-understood, cf. [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF][START_REF] Boudol | Graphical versus logical specifications[END_REF][START_REF] Larsen | Modal specifications[END_REF], but this mismatch has not been discovered up to now. Given that the above theorems can be understood as universal properties of the translations, it means that there is no notion of refinement for ν-calculus which is consistent with them both.

The following lemma, easily shown by inspection, shows that this discrepancy is related to the may-completion for DMTS: Lemma 11. For any DMTS D, mc(D) = hd t (dh(D)).

⊓ ⊔

As a corollary, we see that modal refinement and modal-thorough refinement for ν-calculus are incomparable: Referring back to Example 3, we have D ≤ m D 1 , hence by Theorem 9, dh(D) ≤ m dh(D 1 ). On the other hand, we know that mc(D) ≤ m mc(D 1 ), i.e. by Lemma 11, hd t (dh(D)) ≤ m hd t (dh(D 1 )), and then by Theorem 10, dh(D) ≤ mt dh(D 1 ).

To expose an example where modal-thorough refinement holds, but modal refinement does not, we note that mc(D 2 ) ≤ m mc(D) implies, again using Lemma 11 and Theorem 10, that dh(D 2 ) ≤ mt dh(D). On the other hand, we know that D 2 ≤ m D, so by Theorem 9, dh(D 2 ) ≤ m dh(D).

New translation from ν-calculus to DMTS. We now show that the mismatch between DMTS and ν-calculus expressions can be fixed by introducing a new, simpler translation from ν-calculus to DMTS.

For a ν-calculus expression N = (X, X 0 , ∆) in normal form, let

= {(x, a, y) ∈ X × Σ × X | y ∈ a (x)}, -→ = {(x, N ) | x ∈ X, N ∈ ♦(x)}.
and define the DMTS hd(N ) = (X, X 0 , , -→). This is a simple syntactic translation: boxes are translated to disjunctive must-transitions and diamonds to may-transitions.

Theorem 12. For all ν-calculus expressions, N 1 ≤ m N 2 iff hd(N 1 ) ≤ m hd(N 2 ). Proof. Let R ⊆ X 1 × X 2 be a modal refinement between N 1 = (X 1 , X 0 1 , ∆ 1 ) and N 2 = (X 2 , X 0 2 , ∆ 2 ); we show that R is also a modal refinement between hd(N 1 ) = (S 1 , S 0 1 , 1 , -→ 1 ) and hd(N 2 ) = (S 2 , S 0 2 , 2 , -→ 2 ). Let (x 1 , x 2 ) ∈ R.
-Let x 1 a 1 y 1 , then y 1 ∈ a 1 (x 1 ), which implies that there exists y 2 ∈ a 2 (x 2 ) for which (y 1 , y 2 ) ∈ R, and by definition of

2 , x 2 a 2 y 2 . -Let x 2 -→ 2 N 2 , then N 2 ∈ ♦ 2 (x 2 ), hence there is N 1 ∈ ♦ 1 (x 1 ) such that ∀(a, y 1 ) ∈ N 1 : ∃(a, y 2 ) ∈ N 2 : (y 1 , y 2 ) ∈ R, and by definition of -→ 1 , x 1 -→ 1 N 1 . Now let R ⊆ X 1 × X 2
be a modal refinement between hd(N 1 ) and hd(N 2 ), we show that R is also a modal refinement between N 1 and N 2 . Let (x 1 , x 2 ) ∈ R, -Let a ∈ Σ and y 1 ∈ a 1 (x 1 ). Then x 1 a 1 y 1 , which implies that there is y 2 ∈ X 2 for which x 2 a 2 y 2 and (y 1 , y 2 ) ∈ R, and by definition of

2 , t 2 ∈ a 2 (s 2 ). -Let N 2 ∈ ♦ 2 (x 2 ), then x 2 -→ 2 N 2 , so there is x 1 -→ 1 N 1 such that ∀(a, y 1 ) ∈ N 1 : ∃(a, y 2 ) ∈ N 2 : (y 1 , y 2 ) ∈ R. By definition of -→ 1 , N 1 ∈ a 1 (x 1 ). ⊓ ⊔
We finish the section by proving that also for the syntactic translation hd(N ) ≡ th N for all ν-calculus expressions; this shows that our translation can serve as a replacement for the partly-semantic hd t translation from [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF][START_REF] Boudol | Graphical versus logical specifications[END_REF]. First we remark that dh and hd are inverses to each other: Now that we have exposed a close structural correspondence between the modal ν-calculus and DMTS, we can transfer the operations which make DMTS a complete specification theory to the ν-calculus.

Refinement and implementations. As for DMTS and AA, we can define an embedding of LTS into the modal ν-calculus so that implementation |= and refinement ≤ m coincide. We say that a ν-calculus expression (X, X 0 , ∆) in normal form is an implementation if ♦(x) = {{(a, y)} | y ∈ a (x), a ∈ Σ} for all x ∈ X. The ν-calculus translation of a LTS (S, S 0 , -→) is the expression (S, S 0 , ∆) in normal form with ♦(s) = {{(a, t)} | s Using transitivity, this implies that modal refinement for ν-calculus is sound:

Corollary 16. For all ν-calculus expressions, N 1 ≤ m N 2 implies N 1 ≤ th N 2 .
Disjunction and conjunction. As for DMTS, disjunction of ν-calculus expressions is straight-forward. Given ν-calculus expressions

N 1 = (X 1 , X 0 1 , ∆ 1 ), N 2 = (X 2 , X 0 2 , ∆ 2 ) in normal form, their disjunction is N 1 ∨N 2 = (X 1 ∪X 2 , X 0 1 ∪X 0 2 , ∆) with ∆(x 1 ) = ∆ 1 (x 1 ) for x 1 ∈ X 1 and ∆(x 2 ) = ∆ 2 (x 2 ) for x 2 ∈ X 2 .
The conjunction of ν-calculus expressions like above is

N 1 ∧ N 2 = (X, X 0 , ∆) defined by X = X 1 × X 2 , X 0 = X 0 1 × X 0 2 , a (x 1 , x 2 ) = a 1 (x 1 ) × a 2 (
x 2 ) for each (x 1 , x 2 ) ∈ X, a ∈ Σ, and for each (x 1 , x 2 ) ∈ X,

♦(x 1 , x 2 ) = {(a, (y 1 , y 2 )) | (a, y 1 ) ∈ N 1 , (y 1 , y 2 ) ∈ a (x 1 , x 2 )} N 1 ∈ ♦ 1 (x 1 ) ∪ {(a, (y 1 , y 2 )) | (a, y 2 ) ∈ N 2 , (y 1 , y 2 ) ∈ a (x 1 , x 2 )} N 2 ∈ ♦ 2 (x 2 ) .
Note that both N 1 ∨ N 2 and N 1 ∧ N 2 are again ν-calculus expressions in normal form.

Theorem 17. For all ν-calculus expressions N 1 , N 2 , N 3 in normal form, -N 1 ∨ N 2 ≤ m N 3 iff N 1 ≤ m N 3 and N 2 ≤ m N 3 , -N 1 ≤ m N 2 ∧ N 3 iff N 1 ≤ m N 2 and N 1 ≤ m N 3 , -N 1 ∨ N 2 = N 1 ∪ N 2 , and N 1 ∧ N 2 = N 1 ∩ N 2 .
Theorem 18. With operations ∨ and ∧, the class of ν-calculus expressions forms a bounded distributive lattice up to ≡ m .

The bottom element (up to ≡ m ) in the lattice is the empty ν-calculus expression ⊥ = (∅, ∅, ∅), and the top element (up to ≡ m ) is ⊤ = ({s}, {s}, ∆) with ∆(s) = tt.

Structural composition. The structural composition operator for a specification theory is to mimic, at specification level, the structural composition of implementations. That is to say, if is a composition operator for implementations (LTS), then the goal is to extend to specifications such that for all specifications S 1 , S 2 ,

S 1 S 2 = I 1 I 2 | I 1 ∈ S 1 , I 2 ∈ S 2 .
(

) 2
For simplicity, we use CSP-style synchronization for structural composition of LTS, however, our results readily carry over to other types of composition. Analogously to the situation for MTS [START_REF] Beneš | On determinism in modal transition systems[END_REF], we have the following negative result: Theorem 19. There is no operator for the ν-calculus which satisfies (2).

Proof. We first note that due to Theorem 17, it is the case that implementation sets of ν-calculus expressions are closed under disjunction: for any ν-calculus expression N and I 1 , I 2 ∈ N , also I 1 ∨ I 2 ∈ N . Now assume there were an operator as in the theorem, then because of the translations, (2) would also hold for DMTS. Hence for all DMTS D 1 , D 2 , {I 1 I 2 | I 1 ∈ D 1 , I 2 ∈ D 2 } would be closed under disjunction. But Example 7.8 in [START_REF] Beneš | On determinism in modal transition systems[END_REF] exhibits two DMTS (actually, MTS) for which this is not the case, a contradiction.

⊓ ⊔

Given that we cannot have (2), the revised goal is to have a sound composition operator for which the right-to-left inclusion holds in [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF]. We can obtain one such from the structural composition of AA introduced in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]. We hence define, for ν-calculus expressions N 1 = (X 1 , X 0 1 , ∆ 1 ), N 2 = (X 2 , X 0 2 , ∆ 2 ) in normal form, N 1 N 2 = ah(ha(N 1 ) A ha(N 2 )), where A is AA composition and we write ah = dh • ad and ha = da • hd for the composed translations.

Notice that the involved translation from AA to DMTS may lead to an exponential blow-up. Unraveling the definition gives us the following explicit expression for N 1 N 2 = (X, X 0 , ∆):

-

X = {(a, (y 1 , y 2 )) | ∀i ∈ {1, 2} : (a, y i ) ∈ M i } ∀i ∈ {1, 2} : M i ⊆ Σ × X i , ∃x i ∈ X i : ∀(a, y ′ i ) ∈ M i : y ′ i ∈ a i (x i ), ∀N i ∈ ♦ i (x i ) : N i ∩ M i = ∅ , -X 0 = {(a, (y 1 , y 2 )) | ∀i ∈ {1, 2} : (a, y i ) ∈ M i } ∀i ∈ {1, 2} : M i ⊆ Σ × X i , ∃x i ∈ X 0 i : ∀(a, y ′ i ) ∈ M i : y ′ i ∈ a i (x i ), ∀N i ∈ ♦ i (x i ) : N i ∩ M i = ∅ , -♦(x) = {(a, {(b, (z 1 , z 2 )) | ∀i ∈ {1, 2} : (b, z i ) ∈ M i } | ∀i ∈ {1, 2} : M i ⊆ Σ × X i , ∀(a, z ′ i ) ∈ M i : z ′ i ∈ b i (y i ), ∀N i ∈ ♦ i (y i ) : N i ∩ M i = ∅} (a, (y 1 , y 2 )) ∈ x for each x ∈ X, and -a (x) = {y | ∃N ∈ ♦(x) : (a, y) ∈ N }. Theorem 20. For all ν-calculus expressions N 1 , N 2 , N 3 , N 4 in normal form, N 1 ≤ m N 3 and N 2 ≤ m N 4 imply N 1 N 2 ≤ m N 3 N 4 .
Proof. This follows directly from the analogous property for AA [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] Here, s ′ = {(a, (t1, t2)), (a, (t1, u2))}, t ′ = {(a, (t1, t2))} and u ′ = ∅. Note that D1 D2 has two initial states.

Theorem 21. For all ν-calculus expressions

N , N 1 , N 2 in normal form, N 2 ≤ m N / N 1 iff N 1 N 2 ≤ m N .
Proof. From the analogous property for AA [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF] and Theorems 5, 9 and 12. ⊓ ⊔

As a corollary, we get (3):

If I 2 ∈ N /N 1 , i.e. I 2 ≤ m N /N 1 , then N 1 I 2 ≤ m N , which using I 1 ≤ m N 1 and Theorem 20 implies I 1 I 2 ≤ m N 1 I 2 ≤ m N .
The reverse implication in Theorem 21 implies that N / N 1 is as permissive as possible.

Theorem 22. With operations ∧, ∨, and /, the class of ν-calculus expressions forms a commutative residuated lattice up to ≡ m .

The unit of (up to ≡ m ) is the ν-calculus expression corresponding to the LTS U = ({u}, {u}, {(u, a, u) | a ∈ Σ}). We refer to [START_REF] Hart | The structure of commutative residuated lattices[END_REF] for a good reference on commutative residuated lattices.

Conclusion and Further Work

Using new translations between the modal ν-calculus and DMTS, we have exposed a structural equivalence between these two specification formalisms. This means that both types of specifications can be freely mixed; there is no more any need to decide, whether due to personal preference or for technical reasons, between one and the other. Of course, the modal ν-calculus can only express safety properties; for more expressivity, one has to turn to more expressive logics, and no behavioral analogue to these stronger logics is known (neither is it likely to exist, we believe).

Our constructions of composition and quotient for the modal ν-calculus expect (and return) ν-calculus expressions in normal form, and it is an interesting question whether they can be defined for general ν-calculus expressions. (For disjunction and conjunction this is of course trivial.) Larsen's [START_REF] Larsen | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF] has composition and quotient operators for Hennessy-Milner logic (restricted to "deterministic context systems"), but we know of no extension (other than ours) to more general logics.

We also note that our hybrid modal logic appears related to the Boolean equation systems [START_REF] Mader | Verification of Modal Properties Using Boolean Equation Systems[END_REF][START_REF] Larsen | Efficient local correctness checking[END_REF] which are used in some µ-calculus model checking algorithms. The precise relation between the modal ν-calculus, our L-expressions and Boolean equation systems should be worked out. Similarly, acceptance automata bear some similarity to the modal automata of [START_REF] Bradfield | Modal mu-calculi[END_REF].

Lastly, we should note that we have in [START_REF] Bauer | General quantitative specification theories with modalities[END_REF][START_REF] Bauer | Quantitative refinement for weighted modal transition systems[END_REF] introduced quantitative specification theories for weighted modal transition systems. These are well-suited for specification and analysis of systems with quantitative information, in that they replace the standard Boolean notion of refinement with a robust distancebased notion. We are working on an extension of these quantitative formalisms to DMTS, and hence to the modal ν-calculus, which should relate our work to other approaches at quantitative model checking such as e.g. [START_REF] De Alfaro | Discounting the future in systems theory[END_REF][START_REF] Alfaro | Quantitative verification and control via the mu-calculus[END_REF][START_REF] Gebler | Compositionality of probabilistic Hennessy-Milner logic through structural operational semantics[END_REF].

Let D 1 = (S 1 , S 0 1 , 1 , -→ 1 ), D 2 = (S 2 , S 0 2 , 2 , -→ 2 ) be DMTS and assume D 1 ≤ m D 2 . Then we have a modal refinement relation (in the DMTS sense) R ⊆ S 1 × S 2 . Now let (s 1 , s 2 ) ∈ R and M 1 ∈ Tran 1 (s 1 ), and define By DMTS refinement, we have s 1 -→ N 1 such that ∀(a, t 1 ) ∈ N 1 : ∃(a, t 2 ) ∈ N 2 : (t 1 , t 2 ) ∈ R. We know that N 1 ∩ M 1 = ∅, so let (a, t 1 ) ∈ N 1 ∩ M 1 . Then there also is (a, t 2 ) ∈ N 2 with (t 1 , t 2 ) ∈ R. But (a, t 2 ) ∈ N 2 implies s 2 Let s 1 a 1 t 1 , then we cannot have s 1 -→ ∅. Let M 1 = {(a, t 1 )} ∪ {N 1 | s 1 -→ N 1 }, then M 1 ∈ Tran 1 (s 1 ) by construction. This implies that there is M 2 ∈ Tran 2 (s 2 ) and (a, t 2 ) ∈ M 2 with (t 1 , t 2 ) ∈ R, but then also s 2 a t 2 as was to be shown. Let s 2 -→ N 2 and assume, for the sake of contradiction, that there is no s 1 -→ N 1 for which ∀(a, t 1 ) ∈ N 1 : ∃(a, t 2 ) ∈ N 2 : (t 1 , t 2 ) ∈ R holds. Then for each s 1 -→ N 1 , there is an element (a N1 , t N1 ) ∈ N 1 for which there is no (a N1 , t 2 ) ∈ N 2 with (t N1 , t 2 ) ∈ R.

M 2 = {(
Let M 1 = {(a N1 , t N1 ) | s 1 -→ N 1 }, then M 1 ∈ Tran 1 (s 1 ) by construction. Hence we have M 2 ∈ Tran 2 (s 2 ) satisfying the conditions in the definition of AA refinement. By construction of Tran 2 (s 2 ), N 2 ∩ M 2 = ∅, so let (a, t 2 ) ∈ N 2 ∩ M 2 . Then there exists (a, t 1 ) ∈ M 1 for which (t 1 , t 2 ) ∈ R, in contradiction to the definition of M 1 .

Fig. 1 .

 1 Fig.1. An example property specified in CTL (top left), in the modal µ-calculus (below left), as a modal equation system (third left), and as a DMTS (right).

Proposition 2 .

 2 For any DMTS D, D ≤ m mc(D) and D ≡ th mc(D).

Fig. 2 .

 2 Fig. 2. A MTS D (left) and its may-completion mc(D) (right). In mc(D), the semantic inclusions which lead to extra may-transitions are depicted with dotted arrows.

Example 3 .

 3 and since R is the largest refinement relation in I × S it must be the case that (i ′ , d ′′ ) ∈ R.-The case of must transitions follows immediately, since must transitions are exactly the same in D and mc(D). ⊓ ⊔ The example in Fig.2shows that generally, mc(D) ≤ m D. First, t 3 ≤ th t 1 : For an implementation I = (I,

Fig. 3 .

 3 Fig. 3. DMTS D1, D2 from Example 3.

  t∈ a (s) t and define the (normal-form) ν-calculus expression dh(D) = (S, S 0 , ∆).

Theorem 9 .

 9 For all DMTS D 1 and D 2 , D 1 ≤ m D 2 iff dh(D 1 ) ≤ m dh(D 2 ).

Proposition 13 .Corollary 14 .

 1314 For any ν-calculus expression N , dh(hd(N )) = N ; for any DMTS D, hd(dh(D)) = D. ⊓ ⊔ For all ν-calculus expressions N , hd(N ) ≡ th N . ⊓ ⊔ 4 The Modal ν-Calculus as a Specification Theory

a-→

  t} and a (s) = {t | s a -→ t}. This defines a bijection between LTS and ν-calculus implementations. Theorem 15. For any LTS I and any ν-calculus expression N , I |= N iff I ≤ m N . Proof. I |= N is the same as I ∈ N , which by Corollary 14 is equivalent to I ∈ hd(N ) . By definition, this is the same as I ≤ m hd(N ), which using Theorem 12 is equivalent to I ≤ m N .⊓ ⊔

Fig. 4 .

 4 Fig. 4. DMTS D1, D2 and the reachable parts of their structural composition D1 D2.Here, s ′ = {(a, (t1, t2)), (a, (t1, u2))}, t ′ = {(a, (t1, t2))} and u ′ = ∅. Note that D1 D2 has two initial states.

a 2 t 2 2 , 2 ,

 222 , hence (a, t 2 ) ∈ M 2 . da(D 1 ) ≤ m da(D 2 ) implies D 1 ≤ m D 2 : Let D 1 = (S 1 , S 0 1 , 1 , -→ 1 ), D 2 = (S 2 , S 0 -→ 2 )be DMTS and assume da(D 1 ) ≤ m da(D 2 ). Then we have a modal refinement relation (in the AA sense) R ⊆ S 1 × S 2 . Let (s 1 , s 2 ) ∈ R.

A 1 ≤ 1 , 2 ,

 112 m A 2 implies ad(A 1 ) ≤ m ad(A 2 ):Let A 1 = (S 1 , S 0 Tran 1 ), A 2 = (S 2 , S 0 Tran 2 ) be AA, with DMTS translations (D 1 , D 0 1 , -→ 1 , 1 ), (D 2 , D 0 2 , -→ 2 ,2 ), and assume A 1 ≤ m A 2 . Then we have a modal refinement relation (in the AA sense) R ⊆ S 1 × S 2 . Define

  1 there is t 2 ∈ S 2 with s 2 a t 2 and (t 1 , t 2 ) ∈ R, andfor all s 2 -→ N 2 there is s 1 -→ N 1 such that for each (a, t 1 ) ∈ N 1 there is (a, t 2 ) ∈ N 2 with (t 1 , t 2 ) ∈ R. We say that D 1 modally refines D 2 , denoted D 1 ≤ m D 2 ,whenever there exists a modal refinement R such that for all s 0

	1 ∈ S 0 1 , there exists s 0 2 ∈ S 0 2 for which

  a, t 2 ) | s 2 a 2 t 2 , ∃(a, t 1 ) ∈ M 1 : (t 1 , t 2 ) ∈ R}. condition ∀(a, t 2 ) ∈ M 2 : ∃(a, t 1 ) ∈ M 1 : (t 1 , t 2 ) ∈ R in thedefinition of AA refinement is satisfied by construction. For the inverse condition, let (a, t 1 ) ∈ M 1 , then s 1 a 1 t 1 , so by DMTS refinement, there is t 2 ∈ S 2 with s 2 a 2 t 2 and (t 1 , t 2 ) ∈ R, whence (a, t 2 ) ∈ M 2 by construction. We are left with showing that M 2 ∈ Tran 2 (s 2 ). First we notice that by construction, indeed s 2 a 2 t 2 for all (a, t 2 ) ∈ M 2 . Now let s 2 -→ N 2 ; we need to show that N 2 ∩ M 2 = ∅.

	The

Note that there is an error in the corresponding formula in[START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF].

This implies the right-to-left inclusion in [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF], i.e.

⊆ N 1 N 2 . It also entails independent implementability, in that the structural composition of the two refined specifications N 1 , N 2 is a refinement of the composition of the original specifications N 3 , N 4 . Fig. 4 shows an example of the DMTS analogue of this structural composition.

Quotient. The quotient operator / for a specification theory is used to synthesize specifications for components of a structural composition. Hence it is to have the property, for all specifications S, S 1 and all implementations I 1 , I 2 , that I 1 ∈ S 1 and I 2 ∈ S / S 1 imply

Furthermore, S / S 1 is to be as permissive as possible. We can again obtain such a quotient operator for ν-calculus from the one for AA introduced in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]. Hence we define, for ν-calculus expressions N 1 , N 2 in normal form, N 1 / N 2 = ah(ha(N 1 ) / A ha(N 2 )), where / A is AA quotient. We recall the construction of / A from [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]:

Let A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ) be AA and define

, and Tran given as follows:

Let Tran(∅) = 2 Σ×{∅} . For s = {(s 1 1 , s 1 2 ), . . . , (s n 1 , s n 2 )} ∈ S, say that a ∈ Σ is permissible from s if it holds for all i = 1, . . . , n that there is M 1 ∈ Tran 1 (s i 1 ) and t 1 ∈ S 1 for which (a, t 1 ) ∈ M 1 , or else there is no M 2 ∈ Tran 2 (s i 2 ) and no

For a permissible from s and i ∈ {1, . . . , n}, let {t i,1 2 , . . . , t i,mi

2 ) : (a, t 2 ) ∈ M 2 } be an enumeration of the possible states in S 2 after an a-transition and define pt a (s) = {(t i,j 1 , t i,j 2 ) | i = 1, . . . , n, j = 1, . . . , m i } ∀i : ∀j : ∃M 1 ∈ Tran 1 (s i 1 ) : (a, t i,j 1 ) ∈ M 1 , the set of all sets of possible assignments of next-a states from s i 1 to next-a states from s i 2 . Now let pt(s) = {(a, t) | t ∈ pt a (s), a admissible from s} and define Tran(s

Here ⊲ is the composition-projection operator defined by

1 (note that by construction, there is precisely one pair in t whose second component is t i

2 ).

Appendix: Extra Lemmas and Proofs

Lemma 23. Let D = (S, S 0 , , -→) be a DMTS and s ∈ S. For all M 1 , M 2 ∈ Tran(s) and all M ⊆ Σ × S with M 1 ⊆ M ⊆ M 1 ∪ M 2 , also M ∈ Tran(s).

Proof. For i = 1, 2, since M i ∈ Tran(s), we know that for all (a, t) ∈ M i , (s, a, t) ∈ , and

the transition constraint containing all disjunctive choices of even cardinality. Let D = (T, T 0 , , -→) be a DMTS with cD ≡ th A; we claim that D must have at least 2 n-1 initial states.

Assume, for the purpose of contradiction, that

has greater cardinality than M 1 , so that there will be an M ∈ Tran T (t 0 j ) with odd cardinality. ⊓ ⊔ Proof (of Theorem 5). The first two equivalences in the theorem follow directly from the definitions. Indeed, for the translation from L-expressions to AA, we have Φ(x) = Tran(x) by definition, hence M ∈ Φ(x) iff M ∈ Tran(x). For the other translation, we compute

We show that R ′ is a modal refinement in the DMTS sense.

implies that there must be (a, t 1 ) ∈ M 1 for which (t 1 , t 2 ) ∈ R, and we can define

We show that ∀(a,

. This in turn implies that there must be (a,

On the other hand, the argument in the previous paragraph shows that there is (a,

). As R is initialized, this entails that there is s 0 2 ∈ S 0 2 with (s 0 1 , s 0 2 ) ∈ R, which gives us M 0 2 ∈ Tran 2 (s 0 2 ) which satisfies the AA refinement conditions, whence

2 ), and assume ad(A 1 ) ≤ m ad(A 2 ).

Then we have a modal refinement relation (in the DMTS

2 ) ∈ N 2 , and we have (a, t 2 ) ∈ M 2 for which

2 ) for some s 0 2 ∈ S 0 2 , and then Lemma 8). It is shown in [START_REF] Boudol | Graphical versus logical specifications[END_REF] that any Hennessy-Milner formula is equivalent to one in so-called strong normal form, i.e. of the form i∈I ( j∈Ji a ij φ ij ∧ a∈Σ [a]ψ i,a ) for HML formulas φ ij , ψ i,a which are also in strong normal form. Now we can replace the φ ij , ψ i,a by (new) variables x ij , y i,a and add declarations ∆ 2 (x ij ) = φ ij , ∆ 2 (y i,a ) = ψ i,a to arrive at an expression in which all formulae are of the form

Now for each such formula, replace (recursively) x by new variables [START_REF] De Alfaro | Discounting the future in systems theory[END_REF]. This follows directly from the fact, easy to prove because of the purely syntactic translation, that hd(N 1 ∨ N 2 ) = hd(N 1 ) ∨ hd(N 2 ) and similarly for conjunction, where the operations on the right-hand side are the ones defined for DMTS in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]. Given this, the theorem follows from similar properties for the DMTS operations [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points[END_REF]. ⊓ ⊔ Proof (of Theorem 18). Only distributivity remains to be verified. Let N i = (X i , X 0 i , ∆ i ), for i = 1, 2, 3, be ν-calculus expressions in normal form. The set of variables of both

and one easily sees that the identity relation is a two-sided modal refinement. Things are similar for the other distributive law.

⊓ ⊔ Proof (of Theorem 22). We have already seen that the class of ν-calculus expressions forms a lattice, up to ≡ m , under ∧ and ∨, and by Theorem 21, / is the residual, up to ≡ m , of . We only miss to show that U is indeed the unit of ; all other properties (such as distributivity of over ∨ or N ⊥ ≡ m ⊥) follow. We show that A A U ≡ m A for all AA A; the analogous property for νcalculus expressions follows from the translations. Let A = (S, S 0 , Tran) be an AA and define R = {((s, u), s) | s ∈ S}; we show that R is a two-sided modal refinement. Let ((s, u), s) ∈ R and M ∈ Tran(s, u), then there must be M 1 ∈ Tran(s) for which M = M 1 (Σ×{u}). Thus M 1 = {(a, t) | (a, (t, u)) ∈ M }. Then any element of M has a corresponding one in M 1 , and vice versa, and their states are related by R. For the other direction, let M 1 ∈ Tran(s), then M = M 1 (Σ × {u}) = {(a, (t, u)) | (a, t) ∈ M 1 } ∈ Tran(s, u), and the same argument applies.

⊓ ⊔