Nikola Beneš

Benoît Delahaye

Uli Fahrenberg

Jan Křetínský

Axel Legay

Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory

There are two fundamentally different approaches to specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations.

In this paper we provide translations between the logical formalism of Hennessy-Milner logic with greatest fixed points and the behavioural formalism of disjunctive modal transition systems. We also introduce a new operation of quotient for the above equivalent formalisms, which is adjoint to structural composition and allows synthesis of missing specifications from partial implementations. This is a substantial generalisation of the quotient for deterministic modal transition systems defined in earlier papers.

Introduction

There are two fundamentally different approaches to specifying and verifying properties of systems. Firstly, the logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms. Secondly, the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations.

In this paper, we discuss different formalisms and their relationship. As an example, let us consider labelled transition systems and the property that "at all time points after executing request, no idle nor further requests but only work is allowed until grant is executed". The property can be written in e.g. CTL [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF] as AG(request ⇒ AX(work AW grant)) or as a recursive system of equations in Hennessy-Milner logic [START_REF] Larsen | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF] as

X = [grant, idle, work]X ∧ [request]Y Y = ( work Y ∨ grant X) ∧ [idle, request]ff
where the solution is given by the greatest fixed point. As formulae of modal logics can be difficult to read, some people prefer automata-based behavioural specifications to logical ones. One such behavioural specification formalism is the one of disjunctive modal transition systems (DMTS) [START_REF] Larsen | Equation solving using modal transition systems[END_REF]. Fig. 1 (left) displays a specification of our example property as a DMTS.

Here the dashed arrows indicate that the transitions may or may not be present, while branching of the solid arrow indicates that at least one of the branches must be present. An example of a labelled transition system that satisfies our logical specifications and implements the behavioural one is also given in Fig. 1.

The alternative between logical and behavioural specifications is not only a question of preference. Logical specification formalisms put a powerful logical language at the disposal of the user, and the logical approach to model checking [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF] has seen a lot of success and tool implementations. Automata-based specifications [START_REF] Bruns | Model checking partial state spaces with 3-valued temporal logics[END_REF][START_REF] Larsen | Modal specifications[END_REF], on the other hand, have a focus on compositional and incremental design in which logical specifications are somewhat lacking, with the trade-off of generally being less expressive than logics.

To be more precise, automata-based specifications are, by design, compositional in the sense that they support structural composition of specifications and, in most cases, its adjoint, quotient. This is useful, even necessary, in practical verification, as it means that (1) it is possible to infer properties of a system from the specifications of its components, and (2) the problem of correctness for a system can be decomposed into verification problems for its components. We refer to [START_REF] Larsen | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF] for a detailed account on composition and decomposition.

It is thus desirable to be able to translate specifications from the logical realm into behavioural formalisms, and vice versa from behavioural formalisms to logic-based specifications. This is, then, the first contribution of this paper: we show that Hennessy-Milner logic with greatest fixed points (νHML) and DMTS (with several initial states) are equally expressive, and we provide translations forth and back. For doing this, we introduce an auxiliary intermediate formalism NAA (a nondeterministic extension of acceptance automata [START_REF] Hennessy | Acceptance trees[END_REF][START_REF] Raclet | Residual for component specifications[END_REF]) which is equivalent in expressiveness to both νHML and DMTS.

We also discuss other desirable features of specification formalisms, namely structural composition and quotient. As an example, consider a specification S of the final system to be constructed and T either an already implemented component or a specification of a service to be used. The task is to construct the most general specification of the rest of the system to be implemented, in such a way that when composed with any implementation of T , it conforms with the specification S. This specification is exactly the quotient S/T . Contribution Firstly, we show that the formalisms of νHML, NAA and DMTS have the same expressive power, and provide the respective translations. As a result, the established connection allows for a graphical representation of νHML as DMTS. This extends the graphical representability of HML without fixed points as modal transition systems [START_REF] Boudol | Graphical versus logical specifications[END_REF][START_REF] Larsen | Modal specifications[END_REF]. In some sense this is optimal, as due to the alternation of least and greatest fixed points, there seems to be no hope that the whole µ-calculus could be drawn in a similarly simple way.

Secondly, we show that there are natural operations of conjunction and disjunction for NAA which mimic the ones of νHML. As we work with multiple initial states, disjunction is readily defined, and conjunction extends the one for DMTS [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF]. Thirdly, we introduce structural composition on NAA. For simplicity we assume CSP-style synchronisation of labels, but the construction can easily be generalised to other types of label synchronisation.

Finally, we provide a solution to the open problem of the general quotient. We extend the quotient constructions for deterministic modal transition systems (MTS) and acceptance automata [START_REF] Raclet | Residual for component specifications[END_REF] to define the quotient for the full class of (possibly nondeterministic) NAA. We also provide a more efficient procedure for (possibly nondeterministic) MTS. These constructions are the technically most demanding parts of the paper.

With the operations of structural composition and quotient, NAA, and hence also DMTS and νHML, are fully compositional behavioural specification theories and form a commutative residuated lattice [START_REF] Hart | The structure of commutative residuated lattices[END_REF][START_REF] Ward | Residuated lattices[END_REF] up to equivalence. This makes a rich algebraic theory available for compositional reasoning about specifications. Most of the constructions we introduce are implemented in a prototype tool [8]. Due to space constraints, some of the proofs had to be omitted from the paper and can be found in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory[END_REF]. [START_REF] Larsen | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF] is a popular logical specification formalism which has the same expressive power as µ-calculus [START_REF] Kozen | Results on the propositional mu-calculus[END_REF]. It is obtained from Hennessy-Milner logic (HML) [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF] by introducing variables and greatest and least fixed points. Hennessy-Milner logic with greatest fixed points (νHML) is equivalent to ν-calculus, i.e. µ-calculus with greatest fixed points only.

Related work Hennessy-Milner logic with recursion

DMTS have been proposed as solutions to algebraic process equations in [START_REF] Larsen | Equation solving using modal transition systems[END_REF] and further investigated also as a specification formalism [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF][START_REF] Larsen | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF]. The DMTS formalism is a member of the modal transition systems (MTS) family and as such has also received attention recently. The MTS formalisms have proven to be useful in practice. Industrial applications started as early as [START_REF] Bruns | An industrial application of modal process logic[END_REF] where MTS have been used for an air-traffic system at Heathrow airport. Besides, MTS classes are advocated as an appropriate base for interface theories in [START_REF] Raclet | Why are modalities good for interface theories?[END_REF] and for product line theories in [START_REF] Nyman | Modal Transition Systems as the Basis for Interface Theories and Product Lines[END_REF]. Further, an MTS based software engineering methodology for design via merging partial descriptions of behaviour has been established in [START_REF] Uchitel | Merging partial behavioural models[END_REF] and methods for supervisory control of MTS shown in [START_REF] Darondeau | Supervisory control for modal specifications of services[END_REF]. Tool support is quite extensive, e.g. [START_REF] Bauer | MIO workbench: A tool for compositional design with modal input/output interfaces[END_REF][START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF][START_REF] Børjesson | Generality in design and compositional verification using TAV[END_REF][START_REF] Ippolito | MTSA: Eclipse support for modal transition systems construction, analysis and elaboration[END_REF].

Over the years, many extensions of MTS have been proposed. While MTS can only specify whether or not a particular transition is required, some extensions equip MTS with more general abilities to describe what combinations of transitions are possible. These include DMTS [START_REF] Larsen | Equation solving using modal transition systems[END_REF], 1-MTS [START_REF] Fecher | Comparing disjunctive modal transition systems with an one-selecting variant[END_REF] allowing to express exclusive disjunction, OTS [START_REF] Beneš | Process algebra for modal transition systemses[END_REF] capable of expressing positive Boolean combinations, and Boolean MTS [START_REF] Beneš | Parametric modal transition systems[END_REF] covering all Boolean combinations. The last one is closely related to our NAA, the acceptance automata of [START_REF] Hennessy | Acceptance trees[END_REF][START_REF] Raclet | Residual for component specifications[END_REF], as well as hybrid modal logic [START_REF] Blackburn | Representation, reasoning, and relational structures: a hybrid logic manifesto[END_REF][START_REF] Prior | Papers on Time and Tense[END_REF].

Larsen has shown in [START_REF] Larsen | Modal specifications[END_REF] that any finite MTS is equivalent to a HML formula (without recursion or fixed points), the characteristic formula of the given MTS. Conversely, Boudol and Larsen show in [START_REF] Boudol | Graphical versus logical specifications[END_REF] that any consistent and prime HML formula is equivalent to a MTS. Here we extend these results to νHML formulae, and show that any such formula is equivalent to a DMTS, solving a problem left open in [START_REF] Larsen | Equation solving using modal transition systems[END_REF]. Hence νHML supports full compositionality and decomposition in the sense of [START_REF] Larsen | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF]. This finishes some of the work started in [START_REF] Boudol | Graphical versus logical specifications[END_REF][START_REF] Larsen | Modal specifications[END_REF][START_REF] Larsen | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF].

Quotients are related to decomposition of processes and properties, an issue which has received considerable attention through the years. In [START_REF] Larsen | Equation solving using modal transition systems[END_REF], a solution to bisimulation C(X) ∼ P for a given process P and context C is provided (as a DMTS). This solves the quotienting problem P/C for the special case where both P and C are processes. This is extended in [START_REF] Larsen | Compositionality through an operational semantics of contexts[END_REF] to the setting where the context C can have several holes and C(X 1 , . . . , X n ) must satisfy a property Q of νHML. However, C remains to be a process context, not a specification context. Our specification context allows for arbitrary specifications, representing infinite sets of processes and process equations. Another extension uses infinite conjunctions [START_REF] Fokkink | Compositionality of Hennessy-Milner logic by structural operational semantics[END_REF], but similarly to the other approaches, generates partial specifications from an overall specification and a given set of processes. This is subsumed by a general quotient.

Quotient operators, or guarantee or multiplicative implication as they are called there, are also well-known from various logical formalisms. Indeed, the algebraic properties of our parallel composition and quotient / resemble closely those of multiplicative conjunction & and implication in linear logic [START_REF] Girard | Linear logic[END_REF], and of spatial conjunction and implication in spatial logic [START_REF] Caires | A spatial logic for concurrency (part I)[END_REF] and separation logic [START_REF] O'hearn | Local reasoning about programs that alter data structures[END_REF][START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. For these and other logics, proof systems have been developed which allow one to reason about expressions containing these operators.

In spatial and separation logic, & and (or the operators corresponding to these linear-logic symbols) are first-class operators on par with the other logical operators, and their semantics are defined as certain sets of processes. In contrast, for NAA and hence, via the translations, also for νHML, and / are derived operators, and we provide constructions to reduce any expression which contains them, to one which does not. This is important from the perspective of reuse of components and useful in industrial applications.

Specification Formalisms

In this section, we define the specification formalisms νHML, DMTS and NAA and show that they are equivalent.

For the rest of the paper, we fix a finite alphabet Σ. In each of the formalisms, the semantics of a specification is a set of implementations, in our case always a set of labelled transition systems (LTS) over Σ, i.e. structures (S, s 0 , -→) consisting of a set S of states, an initial state s 0 ∈ S, and a transition relation -→ ⊆ S × Σ × S. We assume that the transition relation of LTS is always image-finite, i.e. that for every a ∈ Σ and s ∈ S the set {s ∈ S | s a -→ s } is finite.

Hennessy-Milner Logic with Greatest Fixed Points

We recap the syntax and semantics of HML with variables developed in [START_REF] Larsen | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF]. A HML formula φ over a set X of variables is given by the abstract syntax

φ ::= tt | ff | x | φ ∧ φ | φ ∨ φ | a φ | [a]
φ, where x ranges over X and a over Σ. The set of such formulae is denoted H(X). Notice that instead of including fixed point operators in the logic, we choose to use declarations with a greatest fixed point semantics, as explained below.

A declaration is a mapping ∆ : X → H(X). We shall give a greatest fixed point semantics to declarations. 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 σ 1 σ 2 iff σ 1 (x) ⊆ σ 2 (x) for all x ∈ X and 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), φ ∧ ψ σ = φ σ ∩ ψ σ, φ ∨ ψ σ = φ σ ∪ ψ σ, a φ σ = {s ∈ S | ∃s a -→ s : s ∈ φ σ}, and [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 greatest (pre)fixed point of ∆.

An initialised HML declaration, or νHML formula, is a structure (X, X 0 , ∆), with X 0 ⊆ X finite sets of variables and ∆ : X → H(X) a declaration. We say that an LTS (S, s 0 , -→) implements (or models) the formula, and write S |= ∆, if it holds that there is x 0 ∈ X 0 such that s 0 ∈ ∆ (x 0 ). We write ∆ for the set of implementations (models) of a νHML formula ∆.

Disjunctive Modal Transition Systems

A DMTS is essentially a labelled transition system (LTS) with two types of transitions, may transitions which indicate that implementations are permitted to implement the specified behaviour, and must transitions which proclaim that any implementation is required to implement the specified behaviour. Additionally, must transitions may be disjunctive, in the sense that they can require that at least one out of a number of specified behaviours must be implemented. We now recall the syntax and semantics of DMTS as introduced in [START_REF] Larsen | Equation solving using modal transition systems[END_REF]. We modify the syntax slightly to permit multiple initial states and, in the spirit of later work [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF][START_REF] Fecher | Characteristic mu-calculus formulas for underspecified transition systems[END_REF], ensure that all required behaviour is also allowed:

A disjunctive modal transition system (DMTS) over the alphabet Σ is a structure (S, S 0 , , -→) consisting of a set of states S, a finite subset S 0 ⊆ S of initial states, a may-transition relation ⊆ S × Σ × S, and a disjunctive musttransition relation -→ ⊆ S × 2 Σ×S . It is assumed that for all (s, N ) ∈ -→ and all (a, t) ∈ N , (s, a, t) ∈

. We usually write s a t instead of (s, a, t) ∈ and s -→ N instead of (s, N ) ∈ -→. We also assume that the may transition relation is image-finite. Note that the two assumptions imply that -→ ⊆ S × 2 Σ×S Fin where 2 X

Fin denotes the set of all finite subsets of X.

A DMTS (S, S 0 , , -→) is an implementation if S 0 = {s 0 } is a singleton and -→ = {(s, {(a, t)} | s a t}, hence if N is a singleton for each s -→ N
and there are no superfluous may-transitions. Thus DMTS implementations are precisely LTS. We proceed to define the semantics of DMTS. First, a relation

R ⊆ S 1 × S 2 is a modal refinement between DMTS (S 1 , S 0 1 , 1 , -→ 1 ) and (S 2 , S 0 2 , 2 , -→ 2 ) if it holds for all (s 1 , s 2 ) ∈ R that -for all s 1 a t 1 there is s 2 a t 2 for some t 2 ∈ S 2 with (t 1 , t 2 ) ∈ R, and
-for 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.
Such a modal refinement is initialised if it is the case that, for each s 0 1 ∈ S 0 1 , there is s 0 2 ∈ S 0 2 for which (s 0 1 , s 0 2 ) ∈ R. In that case, we say that S 1 refines S 2 and write S 1 ≤ m S 2 . We write

S 1 ≡ m S 2 if S 1 ≤ m S 2 and S 2 ≤ m S 1 .
We say that an LTS I implements a DMTS S if I ≤ m S and write S for the set of implementations of S. Notice that the notions of implementation and modal refinement agree, capturing the essence of DMTS as a specification theory: A DMTS may be gradually refined, until an LTS, in which all behaviour is fully specified, is obtained.

For DMTS S 1 , S 2 we say that S 1 thoroughly refines S 2 , and write

S 1 ≤ t S 2 , if S 1 ⊆ S 2 . We write S 1 ≡ t S 2 if S 1 ≤ t S 2 and S 2 ≤ t S 1 . By transitivity, S 1 ≤ m S 2 implies S 1 ≤ t S 2 .
Example 1. Figs. 2 and3 show examples of important basic properties expressed both as νHML formulae, NAA (see below) and DMTS. For DMTS, may transitions are drawn as dashed arrows and disjunctive must transitions as branching arrows. States with a short incoming arrow are initial (the DMTS in Fig. 3 has two initial states).

X = a tt ∧ [a]X ∧ [b]X ({s0}, {s0}, Tran) Tran(s0) = {(a, s0)}, {(a, s0), (b, s0)} a b
Fig. 2. νHML formula, NAA and DMTS for the invariance property "there is always an 'a' transition available", with Σ = {a, b} Modal Transition Systems An interesting subclass of DMTS are modal transition systems (MTS) [START_REF] Larsen | Modal specifications[END_REF]. A DMTS (S, S 0 , , -→) is said to be a MTS if (1) S 0 = {s 0 } is a singleton, (2) for every s -→ N , the set N is a singleton. Hence, for each transition, we specify whether it must, may, or must not be present; no disjunctions can be expressed. It is easy to see that MTS are less expressive than DMTS, i.e. there are DMTS S for which no MTS S exists so that S = S . One example is provided on the right. Here any implementation must have an a or a b transition from the initial state, but then any MTS which permits all such implementations will also allow implementations without any transition from the initial state.

X = b tt ∨ a tt ∧ [a]X ∧ [b]X ∧ [c]X ({s0,

NAA

We now define NAA, the nondeterministic extension to the formalism of acceptance automata [START_REF] Raclet | Residual for component specifications[END_REF]. We shall use this formalism to bridge the gap between νHML and DMTS. A nondeterministic acceptance automaton over the alphabet Σ is a structure (S, S 0 , Tran) where S and S 0 are the states and initial states as previously, and Tran : S → 2 2 Σ×S Fin assigns admissible transition sets. A NAA (S, S 0 , Tran) is an implementation if S 0 = {s 0 } is a singleton and Tran(s) = {M } is a singleton for every s ∈ S; clearly, NAA implementations are precisely LTS. We also define the inconsistent NAA to be ⊥ = (∅, ∅, ∅) and the universal NAA by = ({s}, {s}, 2 2 Σ×{s} ).

A relation R ⊆ S 1 × S 2 is a modal refinement between NAA (S 1 , S 0 1 , Tran 1 ), (S 2 , S 0 2 , Tran 2 ) 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.
We define and use the notions of initialised modal refinement, ≤ m , ≡ m , implementation, ≤ t , and ≡ t the same way as for DMTS.

Proposition 2. The class of NAA is preordered by modal refinement ≤ m , with bottom element ⊥ and top element .

Note that as implementations of all our three formalisms νHML, DMTS and NAA are LTS, it makes sense to use thorough refinement ≤ t and equivalence ≡ t across formalisms, so that we e.g. can write S ≤ t ∆ for a NAA S and a νHML formula ∆.

Equivalences

We proceed to show that νHML, DMTS and NAA are equally expressive: Theorem 3. For any set S of LTS, the following are equivalent:

1. There exists a νHML formula ∆ with ∆ = S. 2. There exists a finite NAA S with S = S. 3. There exists a finite DMTS S with S = S.

Furthermore, the latter two statements are equivalent even if we drop the finiteness constraints.

Note that we could drop the finiteness assumption about the set of variables of νHML formulae, while retaining the fact that ∆(x) is a finite HML formula. The result of Theorem 3 could then be extended with the statement that these possibly infinite νHML formulae are equivalent to general DMTS/NAA.

For a DMTS S = (S, S 0 , , -→), let Tran(s) = {M ⊆ Σ × S | ∃N : s -→ N, N ⊆ M ; ∀(a, t) ∈ M : s a t} and define the NAA dn(S) = (S, S 0 , Tran).

Conversely, for an NAA (S, S 0 , Tran), define the DMTS nd(S) = (T, T 0 , , -→) as follows:

-T = {M ∈ Tran(s) | s ∈ S}, T 0 = {M ∈ Tran(s 0 ) | s 0 ∈ S 0 }, --→ = {(M, {(a, M ) | M ∈ Tran(s )} | (a, s ) ∈ M }, - = {(t, a, t ) | t ∈ T, ∃(t, N ) ∈ -→ : (a, t ) ∈ N }.
Note that both nd and dn preserve finiteness. Both translation are exponential in their respective arguments. Lemma 4. For every DMTS S, S ≡ t dn(S). For every NAA S, S ≡ t nd(S).

For a set of pairs of actions and states M we use M a to denote the set {s | (a, s) ∈ M }. Let (S, S 0 , Tran) be a finite NAA and let s ∈ S, we then define

∆ Tran (s) = M ∈Tran(s) (a,t)∈M a t ∧ a∈Σ [a] u∈Ma u
We then define the νHML formula nh(S) = (S, S 0 , ∆ Tran ). Notice that variables in nh(S) are states of S.

Lemma 5. For all NAA S, S ≡ t nh(S).

Our translation from νHML to DMTS is based on the constructions in [START_REF] Boudol | Graphical versus logical specifications[END_REF]. First, we need a variant of a disjunctive normal form for HML formulae: Lemma 6. For any νHML formula (X 1 , X 0 1 , ∆ 1 ), there exists another formula (X 2 , X 0 2 , ∆ 2 ) with ∆ 1 = ∆ 2 and such that any formula ∆ 2 (x), for x ∈ X 2 , is tt or of the form ∆ 2 (x) = i∈I j∈Ji a ij x ij ∧ a∈Σ [a]y i,a for finite (possibly empty) index sets I and J i , i ∈ I, and all x ij , y i,a ∈ X 2 . Additionally we can assume that for all i ∈ I, j ∈ J i , a ∈ Σ, a ij = a implies x ij ⊆ y i,a .

Let now (X, X 0 , ∆) be a νHML formula in the form introduced above, then we define a DMTS hd(∆) = (S, S 0 , , -→) as follows:

-S = {(x, k) | x ∈ X, ∆(x) = i∈I φ i , k ∈ I = ∅} ∪ {⊥, }, -S 0 = {(x 0 , k) | x 0 ∈ X 0 }. -For each (x, k) ∈ S with ∆(x) = i∈I ( j∈Ji a ij x ij ∧ a∈Σ [a]y i,a
) and

I = ∅, • for each j ∈ J i , let Must j (x, k) = {(a ij , (x ij , i )) ∈ Σ × S}, • for each a ∈ Σ, let May a (x, k) = {(x , i ) ∈ S | x ⊆ y i,a }. -Let = {(s, a, s ) | s ∈ S, a ∈ Σ, s ∈ May a (s)} ∪ {( , a, ) | a ∈ Σ} and -→ = {(s, Must j (s)) | s = (x, i) ∈ S, j ∈ J i } ∪ {(⊥, ∅)}.
Lemma 7. For all νHML formulae ∆, ∆ ≡ t hd(∆).

Further, we remark that the overall translation from DMTS to νHML is quadratic and in the other direction inevitably exponential.

Example 8. Consider the νHML formula X = ( a ( b X ∧ [a]ff ) ∧ [b]ff ) ∨ [a]ff .
Changing the formula into the normal form of Lemma 6 introduces a new variable Y as illustrated below; X remains the sole initial variable. The translation hd then gives a DMTS with two initial states (the inconsistent state ⊥ and redundant may transitions such as x 1 a x 2 , x 2 b x 1 , etc. have been omitted):

X = ( x1 a Y ∧ [a]tt ∧ [b]ff ) ∨ ([a]ff ∧ [b]tt x2 ) Y = b X ∧ [a]ff ∧ [b]tt

Specification Theory

In this section, we introduce operations of conjunction, disjunction, structural composition and quotient for NAA, DMTS and νHML. Together, these operations yield a complete specification theory in the sense of [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF], which allows for compositional design and verification using both logical and structural operations. We remark that conjunction and disjunction are straightforward for logical formalisms such as νHML, whereas structural composition is more readily defined on behavioural formalisms such as (D)MTS. For the mixed formalism of NAA, disjunction is trivial as we permit multiple initial states, but conjunction requires some work. Note that our construction of conjunction works for nondeterministic systems in contrast to all the work in this area except for [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF][START_REF] Larsen | Equation solving using modal transition systems[END_REF].

Disjunction

The disjunction of NAA S 1 = (S 1 , S 0 1 , Tran 1 ) and

S 2 = (S 2 , S 0 2 , Tran 2 ) is S 1 ∨ S 2 = (S 1 ∪ S 2 , S 0 1 ∪ S 0 2 , Tran 1 ∪ Tran 2 ). Similarly, the disjunction of two DMTS S 1 = (S 1 , S 0 1 , 1 , -→ 1 ) and S 2 = (S 2 , S 0 2 , 2 , -→ 2 ) is S 1 ∨ S 2 = (S 1 ∪ S 2 , S 0 1 ∪ S 0 2 , 1 ∪ 2 , -→ 1 ∪ -→ 2 )
. It follows that disjunction respects the translation mappings dn and nd from the previous section.

Theorem 9. Let S 1 , S 2 , S 3 be NAA or DMTS. Then S 1 ∨ S 2 = S 1 ∪ S 2 . Further, S 1 ∨ S 2 ≤ m S 3 iff S 1 ≤ m S 3 and S 2 ≤ m S 3 . s 0 1 s 0 2 a a b b
We point out one important distinction between NAA and DMTS: NAA with a single initial state are equally expressive as general NAA, while for DMTS, this is not the case. The example on the right shows a DMTS (S, S 0 , , -→), with S = S 0 = {s 0 1 , s 0 2 }, s 0 1 -→ {(a, s 0 1 ), (a, s 0 2 )} and s 0 1 -→ {(b, s 0 1 ), (b, s 0 2 )} (and the corresponding maytransitions). Two initial states are necessary for capturing S . Lemma 10. For any NAA S there is a NAA T = (T, T 0 , Ψ ) with T 0 = {t 0 } a singleton and S ≡ m T .

Conjunction

Conjunction for DMTS is an extension of the construction from [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF] for multiple initial states. Given two DMTS (S 1 , S 0 1 ,

1 , -→ 1 ), (S 2 , S 0 2 , 2 , -→ 2 ), we define S 1 ∧ S 2 = (S, S 0 , , -→) with S = S 1 × S 2 , S 0 = S 0 1 × S 0 2 , and -(s 1 , s 2 ) a (t 1 , t 2 ) iff s 1 a 1 t 1 and s 2 a 2 t 2 , -for all s 1 -→ N 1 , (s 1 , s 2 ) -→ {(a, (t 1 , t 2 )) | (a, t 1 ) ∈ N 1 , (s 1 , s 2 ) a (t 1 , t 2 )}, -for all s 2 -→ N 2 , (s 1 , s 2 ) -→ {(a, (t 1 , t 2 )) | (a, t 2 ) ∈ N 2 , (s 1 , s 2 ) a (t 1 , t 2 )}.
To define conjunction for NAA, we need auxiliary projection functions π i : Σ × S 1 × S 2 → Σ × S i . These are defined by

π 1 (M ) ={(a, s 1 ) | ∃s 2 ∈ S 2 : (a, s 1 , s 2 ) ∈ M } π 2 (M ) ={(a, s 2 ) | ∃s 1 ∈ S 1 : (a, s 1 , s 2 ) ∈ M } Given NAA (S 1 , S 0 1 , Tran 1 ), (S 2 , S 0 2 , Tran 2 ), define S 1 ∧ S 2 = (S, S 0 , Tran), with S = S 1 × S 2 , S 0 = S 0 1 × S 0 2 and Tran((s 1 , s 2 )) = {M ⊆ Σ × S 1 × S 2 | π 1 (M ) ∈ Tran 1 (s 1 ), π 2 (M ) ∈ Tran 2 (s 2 )}. Lemma 11. For DMTS S 1 , S 2 , dn(S 1 ∧ S 2 ) = dn(S 1 ) ∧ dn(S 2 ).
For the translation from NAA to DMTS, nd(S 1 ∧ S 2 ) = nd(S 1 ) ∧ nd(S 2 ) does not necessarily hold, as the translation changes the state space. However, Theorem 12 below will ensure that nd(S 1 ∧ S 2 ) ≡ t nd(S 1 ) ∧ nd(S 2 ).

Theorem 12. Let S 1 , S 2 , S 3 be NAA or DMTS. Then S 1 ∧ S 2 = S 1 ∩ S 2 . Further, S 1 ≤ m S 2 ∧ S 3 iff S 1 ≤ m S 2 and S 1 ≤ m S 3 .
Theorem 13. With operations ∧ and ∨, the sets of DMTS and NAA form bounded distributive lattices up to ≡ m .

Structural Composition

We define structural composition for NAA. For NAA S 1 = (S 1 , S 0 1 , Tran 1 ), S 2 = (S 2 , S 0 2 , Tran 2 ), we define S 1 S 2 = (S, S 0 , Tran) with S = S 1 × S 2 , S 0 = S 0 1 × S 0 2 , and for all (s 1 , s 2 ) ∈ S, Tran(( We remark that structural composition on MTS [START_REF] Larsen | Modal specifications[END_REF] coincides with our NAA composition, so that for MTS S 1 , S 2 , dn(S 1 ) dn(S 2 ) = dn(S 1 S 2 ). On the other hand, structural composition for DMTS (with single initial states) as defined in [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF] is weaker than NAA composition, i.e. for DMTS S 1 , S 2 , and denoting by the composition from [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF], only dn(S 1 ) dn(S 2 ) ≤ t dn(S 1 S 2 ) holds. Consider for example the DMTS S and S in the figure below. When considering their NAA composition, the initial state is the pair (s 0 , t 0 ) with Tran((s 0 , t 0 )) = {∅, {(a, (s 2 , t 1 )), (a, (s 2 , t 2 ))}. Since this constraint cannot be represented as a disjunctive must, there is no DMTS with a single initial state which can represent the NAA composition precisely. Hence the DMTS composition of [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF] is a DMTS over-approximation of the NAA composition, and translating from DMTS to NAA before composing (and back again) will generally give a tighter specification. However, as noted already in [START_REF] Hüttel | The use of static constructs in a modal process logic[END_REF], MTS composition itself is an over-approximation, in the sense that there will generally be implementations I ∈ S 1 S 2 which cannot be written I = I 1 I 2 for I 1 ∈ S 1 and I 2 ∈ S 2 ; the same is the case for NAA and DMTS.

s 1 , s 2 )) = {M 1 M 2 | M 1 ∈ Tran 1 (s 1 ), M 2 ∈ Tran 2 (s 2 )}, where M 1 M 2 = {(a, (t 1 , t 2 )) | (a, t 1 ) ∈ M 1 , (a, t 2 ) ∈ M 2 }.

Quotient

We now present one of the central contributions of this paper, the construction of quotient. The quotient S/T is to be the most general specification that, when composed with T , refines S. In other words, it must satisfy the property that for all specifications X, X ≤ m S/T iff X T ≤ m S. Quotient has been defined for deterministic MTS and for deterministic acceptance automata in [START_REF] Raclet | Residual for component specifications[END_REF]; here we extend it to the nondeterministic case (i.e. NAA). The construction incurs an exponential blow-up, which however is local and depends on the degree of nondeterminism. We also provide a quotient construction for nondeterministic MTS; this is useful because MTS encodings for NAA can be very compact.

Let (S, S 0 , Tran S ), (T, T 0 , Tran T ) be two NAA. We define the quotient S/T = (Q, {q 0 }, Tran Q ). Let Q = 2 S×T Fin and q 0 = {(s 0 , t 0 ) | s 0 ∈ S 0 , t 0 ∈ T 0 }. States in Q will be written {s 1 /t 1 , . . . , s n /t n } instead of {(s 1 , t 1 ), . . . , (s n , t n )}.

In the following, we use the notation x ∈∈ z as a shortcut for the fact that there exists y with x ∈ y ∈ z. We first define Tran Q (∅) = 2 Σ×{∅} . This means that the empty set of pairs is the universal state . Now let q = {s 1 /t 1 , . . . , s n /t n } ∈ Q. We first define the auxiliary set of possible transitions pt(q) as follows. For x ∈ S ∪ T , let α(x) = {a ∈ Σ | ∃y : (a, y) ∈∈ Tran(x)} and γ(q

) = i α(s i ) ∪ (Σ \ α(t i )) . Let further π a (X) = {x | (a, x) ∈ X}.
Let now a ∈ γ(q). For all i ∈ {1, . . . , n}, let {t i,1 , . . . , t i,mi } = π a ( Tran T (t i )) be the possible next states from t i after an a-transition, and define pt a (q) = {s i,j /t i,j | i ∈ {1, . . . , n}, j ∈ {1, . . . , m i }} | ∀i ∈ {1, . . . , n} : ∀j ∈ {1, . . . , m i } : (a, s i,j ) ∈∈ Tran S (s i ) and pt(q) = a∈Σ ({a} × pt a (q)). Hence pt a (q) contains sets of possible next quotient states after an a-transition, each obtained by combining the t i,j with some permutation of possible next a-states in S. We then define

Tran Q (q) = {X ⊆ pt(q) | ∀i : ∀Y ∈ Tran T (t i ) : X Y ∈ Tran S (s i )},
where the operator is defined by {s 1 /t 1 , . . . , s k /t k } t = s and X Y = {(a, x y) | (a, x) ∈ X, (a, y) ∈ Y }. Hence Tran Q (q) contains all sets of (possible) transitions which are compatible with all t i in the sense that (the projection of) their parallel composition with any set Y ∈ Tran T (t i ) is in Tran S (s i ).

Theorem 16. For all NAA S, T and X, X T ≤ m S iff X ≤ m S/T . Theorem 17. With operations ∧, ∨, and /, the set of NAA forms a commutative residuated lattice up to ≡ m . This theorem makes clear the relation of NAA to linear logic [START_REF] Girard | Linear logic[END_REF]: except for completeness of the lattice induced by ∧ and ∨ (cf. Theorem 13), NAA form a commutative unital Girard quantale [START_REF] Yetter | Quantales and (noncommutative) linear logic[END_REF], the standard algebraic setting for linear logic. Completeness of the lattice can be obtained by allowing infinite conjunctions and disjunctions (and infinite NAA).

Quotient for MTS

We now give a quotient algorithm for the important special case of MTS, which results in a much more compact quotient than the NAA construction in the previous section. However, MTS are not closed under quotient; cf. [28, Thm. 5.5]. We show that the quotient of two MTS will generally be a DMTS.

Let (S, s 0 , S , -→ S ) and (T, t 0 , T , -→ T ) be nondeterministic MTS. We define the quotient S/T = (Q, {q 0 }, Q , -→ Q ). We let Q = 2 S×T Fin as before, and q 0 = {(s 0 , t 0 )}. The state ∅ ∈ Q is again universal, so we define ∅ a ∅ for all a ∈ Σ. There are no must transitions from ∅. Let α(s), γ(q) be as in the previous section. For convenience, we work with sets May a (s), for a ∈ Σ and states s, instead of may transitions, i.e. we have May a (s) = {t | s a t}.

Let q = {s 1 /t 1 , . . . , s n /t n } ∈ Q and a ∈ Σ. First we define the may transitions. If a ∈ γ(q) then for each i ∈ {1, . . . , n}, write May a (t i ) = {t i,1 , . . . , t i,mi }, and define May a (q) = {s i,j /t i,j | i ∈ {1, . . . , n}, j ∈ {1, . . . , m i }} | ∀i ∈ {1, . . . , n} : ∀j ∈ {1, . . . , m i } : s i,j ∈ May a (s i ) .

For the (disjunctive) must-transitions, we let, for every s i a -→ s , q -→ {(a, M ) ∈ {a} × May a (q) | ∃t : s /t ∈ M, t i a -→ t }.

Example 18. We illustrate the construction on an example. Let S and T be the MTS in the left part of Fig. 4. We construct S/T ; the end result is displayed in the right part of the figure.

First we construct the may-successors of s 0 /t 0 . Under b and c there are no constraints, hence we go to . For a, we have all permutations of assignments of successors of s to successors of t, namely {s 1 /t 1 , s 1 /t 2 }, {s 1 /t 1 , s 2 /t 2 }, {s 2 /t 1 , s 1 /t 2 } and {s 2 /t 1 , s 2 /t 2 }. Since there is a must-transition from s (to s 1 ), we create a disjunctive must-transition to all successors that can be used to yield a must-transition when composed with the must-transition from t to t 1 . These are all successors where t 1 is mapped to s 1 , hence the first two. However, {s 1 /t 1 , s 1 /t 2 } will turn out inconsistent, as it requires to refine s 1 by a composition with t 2 . As t 2 has no must under b, the composition has none either, hence the must of s 1 can never be matched. As a result, after pruning, the disjunctive must from {s 0 /t 0 } leads only to {s 1 /t 1 , s 2 /t 2 }. Further, {s 2 /t 1 , s 1 /t 2 } is inconsistent for the same reason, so that we only have one other may-transition under a from {s 0 /t 0 }. Now {s 1 /t 1 , s 2 /t 2 } is obliged to have a must under b so that it refines s 1 when composed with t 1 , but cannot have any c in order to match s 2 when composed with t 2 . Similarly, {s 2 /t 1 , s 2 /t 2 } has neither c nor b. One can easily verify that T (S/T ) ≡ m S in this case.

Note that the constructions may create inconsistent states, which have no implementation. In order to get a consistent system, it needs to be pruned. This is standard and the details can be found in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory[END_REF]. The pruning can be done in polynomial time.

Theorem 19. For all MTS S, T and X, X ≤ m S/T iff T X ≤ m S.

Conclusion and Future Work

In this paper we have introduced a general specification framework whose basis consists of three different but equally expressive formalisms: one of a graphical behavioural kind (DMTS), one logic-based (νHML) and one an intermediate language between the former two (NAA). We have shown that the framework possesses a rich algebraic structure that includes logical (conjunction, disjunction) and structural operations (parallel composition and quotient). Moreover, the construction of the quotient solves an open problem in the area of MTS. As for future work, we hope to establish the exact complexity of the quotient constructions. We conjecture that the exponential blow-up of the construction is in general unavoidable.

Fig. 3 .

 3 Fig.3. νHML formula, NAA and DMTS for the ("weak until") property "there is always an 'a' transition available, until a 'b' transition becomes enabled ", with Σ = {a, b, c}

Lemma 14 .

 14 Up to ≡ m , the operator on NAA is associative and commutative, distributes over ∨, and has unit U, where U is the LTS ({s}, s, -→) with s a -→ s for all a ∈ Σ. Theorem 15. For all NAA S 1 , S 2 , S 3 , S 4 , S 1 ≤ m S 3 and S 2 ≤ m S 4 imply S 1 S 2 ≤ m S 3 S 4 .

Fig. 4 .

 4 Fig. 4. Two nondeterministic MTS and their quotient