Adrien Guery
email: adrien.guery@lmt.ens-cachan.fr

Félix Latourte

François Hild

Stéphane Roux

Analysis of E-Beam Microlithography and SEM Imaging Distortions

Keywords: SEM, microlithography patterning, digital image correlation, patterning distortions, imaging distortions

published or not. The documents may come   L'archive ouverte pluridisciplinaire

INTRODUCTION

Kinematic measurements are performed to study the mechanical behavior of materials. This can be done at the microstructure scale by using a Scanning Electron Microscope (SEM). Such spatially dense experimental information offers a wide scope of possibilities, such as for example the comparison with simulations to identify material parameters [START_REF] Héripré | Coupling between experimental measurements and polycrystal finite element calculations for micromechanical study of metallic materials[END_REF] associated with crystal plasticity constitutive equations [START_REF] Roters | Overview of constitutive laws, kinematics, homogenization and multiscale methods in crystal plasticity finite-element modeling: Theroy, experiments, applications[END_REF]. Yet, the imaging distortions induced by the SEM electromagnetic environment should be taken into account to ensure the accuracy of the experimental information [START_REF] Sutton | Metrology in a scanning electron microscope: theoretical developments and experimental validation[END_REF]. To perform kinematic measurements using Digital Image Correlation (DIC), a gray level pattern is required on the observed surface of the sample. When the natural texture of the material is not suitable, an artificial one may be deposited onto the surface. In the case of SEM imaging, a common practice is to resort to microgrid marking using e-beam microlithography [START_REF] Allais | Experimental characterization of the local strain field in an heterogeneous elastoplastic material[END_REF]. In this study, the same marking technique is employed, but has been tailored to create a numerically-generated random speckle, which presents the advantage (for DIC) to not induce spatially periodic patterns. Global distortions between the theoretical (or "reference") pattern and its SEM image, resulting from patterning and imaging, are measured by DIC. A partition method of these two contributions is performed using several SEM images of the pattern after a set of rotations of the sample in the SEM.

GLOBAL DISTORTIONS MEASUREMENT BY DIGITAL IMAGE CORRELATION

A gold speckle is deposited onto the surface of an in-situ specimen by a process of microlithography patterning. The material is 316LN austenitic stainless steel. The surface is prepared by mechanical polishing with colloidal silica finish. The process is divided into five main steps (see Figure 1). The principle consists of exposing a resist film, deposited onto the surface, with the electron beam of the SEM only at specific positions following a pattern design. For that purpose, a Raith Elphy Quantum commercial system is used to control the FEI Quanta FEG 600 SEM. After the dissolution of the exposed resist, a very thin layer of gold is deposited over the entire surface, and a final dissolution step of the resist film leaves gold only in the region that were first swept by the e-beam. In the present case, the speckle pattern is chosen to be a known distribution of diskshaped spots of random radius and position. The speckle covers a 400 µm side square surface. The displacement fields between the SEM image, denoted f , and the computer-generated image, g , of the pattern are measured using finite element based DIC [START_REF] Leclerc | Integrated digital image correlation for the identification of mechanical properties[END_REF], which is based on the conservation of the texture

    ) (z u z z   g f (1)
where z is the complex-valued coordinates of pixels in f , and u the sought displacement field. The minimization of the gray level residuals leads to the iterative solution of linear systems [START_REF] Besnard | Finite-Element" displacement fields analysis from digital images: Application to portevin-le chatelier bands[END_REF]     

s u M   (2) with     ) ( ) ( z ψ z ψ f f M j ROI i ij       (3) and     ) ( ) ( ~z ψ z f g f s i ROI i      (4)
where, at each iteration,   u  is a vector of the displacement corrections, and g ~the deformed image corrected by the current estimation of the displacement field. i ψ are chosen basis functions for the displacement discretization, in the present case an unstructured mesh of 3-noded triangular elements (about 40 pixel / 9.6 µm sides). With this DIC technique, a Root Mean Square (RMS) value of the displacement uncertainty of 0.02 pixel (or 5.0 nm) is measured (between 2 SEM images with no motion). In addition to rigid body motions, the obtained field includes distortions resulting from both patterning and imaging errors. The separation of these two contributions is not reachable so far.

PARTITION OF DISTORTIONS

A partition method of global distortions between patterning and imaging distortions is now presented. A set of ten rotations of an angle θ k ranging from 0° to 90° of the observed pattern is applied inside the SEM chamber (via the stage rotation) prior to imaging. Displacement fields, denoted u k , are then measured using DIC between the acquired images and the reference image of the pattern. Because large rotations are prescribed, the previous DIC formulation has been adapted considering finite transformation kinematics [START_REF] Guery | Characterization of SEM speckle pattern marking and imaging distortion by digital image correlation[END_REF]. The partition method consists of considering each displacement field u k as a composition of three transformations, namely, a patterning distortions field υ g , identical for each u k , a rotation of an angle θ k , and an imaging distortions field υ d , assumed to be time-independent. This procedure is described in Figure 3.

Fig. 3: Schematic of the partition of each of the k measurements of global distortions

The two unknown distortion fields are chosen to be described as a linear combination of polynomials expressed in the complex plane as

l k kl z z z d  ) ( with p l k l k     , 0 , 0 (5)
where z denotes the conjugate of z , and p the order of the series. Analytical expressions generally proposed in the literature [8] are described via this chosen basis too. A second order expansion of this polynomial basis appeared sufficient to describe both patterning and imaging distortions fields. Thus,   For each of the k displacement measurements, the deformed coordinate system in the reference image is given by

) ( 0 0 3 z u z z k k   (6)
With the proposed partition method, an approximation of

k 3 z , denoted k 3 ẑ , is proposed as   ) ,..., , ( ) ,..., , ( ˆ6 1 2 6 1 0 0 3 g g k g i d d d k a a e a a k z υ z υ z z     (7) with   k i d d d k e a a  ) ,..., , ( ˆ6 1 0 0 2 z υ z z   (8)
The error fields are then expressed as

k k k 3 3 ẑ z r   (9)
These fields are minimized in a weighted least squares criterion with respect to the sought coefficients   where ] [ k M is the DIC matrix associated to the measured degrees of freedom of u k , which is shown to be proportional to the inverse of the covariance matrix of measured degrees of freedom [START_REF] Besnard | Finite-Element" displacement fields analysis from digital images: Application to portevin-le chatelier bands[END_REF], and therefore appears adequate to weight the error fields in the least squares criterion. The problem is nonlinear because of large rotations. However, it becomes linear if considering one of the functions υ d or υ g as known, the other one is sought, and vice-versa. A few iterations are needed for converging to a minimum of the residual function. Figure 4 shows the change of the RMS error fields k r as a function of the measured rotation angle of the pattern between the first and the last iteration. , with a real amplitude) is not considered. Its amplitude is due to small magnification changes between the SEM image and the reference picture. Electron beam microlithography appears to involve smaller errors (in the 400 nm range) than SEM imaging does (in the 600 nm range). The imaging distortion magnitude is less than that observed by Sutton et al [START_REF] Sutton | Metrology in a scanning electron microscope: theoretical developments and experimental validation[END_REF] (of the order of 2.5 µm) but at a magnification about two times lower, and with a (very) different SEM. Moreover, the maximum levels of patterning errors are reached at the edges of the area of interest, which is consistent with the second step of the patterning process. The exposure of each elementary pattern (circular disks) is performed by electron beam deflection from the center of the square surface to mark, and thus it is expected to be less accurate far from the center. Last, the same experiment has been conducted with twice the previous magnification with a 100 µm side square speckle and very similar results have been obtained.

                 k k k k g g d d

CONCLUSIONS

A gold patterning process has been introduced to mark stainless steel surfaces with a numerically-generated random pattern using microlithography. Global distortions have been quantified using digital image correlation between an SEM image of the pattern and its corresponding reference image, including both patterning and SEM imaging biases. It has then been shown that it is possible to separate these two contributions by collecting several evaluations of this global distortion with various angles of rotation of the observed pattern. The patterning has been shown to involve lower errors than SEM imaging distortions. From these analyses, it would be relevant to check for any additional drifts due to SEM environment too. The subsequent use of SEM images for kinematic measurements requires a good characterization and quantification of the measurement errors.

Fig. 1 :

 1 Fig. 1: Surface gold patterning using e-beam microlithography: resin film deposition (a), electron beam exposure (b), exposed resist film development (c), gold deposition (d), residual resist film dissolution (e)

  Figure 2 (a) shows an SEM image of the imaged gold pattern using backscattered electron (BSE) detector at a working distance of 14 mm, with an acceleration voltage of 10 kV. Images are acquired with a physical size of 240 nm per pixel and stored in 16 bit format. Thanks to the histogram of gray levels of the SEM image, a reference image of the known distribution of spots is built. Its background is set as a homogeneous gray level read at the peak of the histogram corresponding to the uncovered alloy. Spots are set as a Gaussian-shaped distribution of gray levels whose mean value is read at the peak of the histogram related to the gold disks. Because the underlying microstructure of the material involves different gray levels (see Figure2(a)), this process is performed regionally after a simple first segmentation of the main regions.Figure 2 (b) shows the reference image obtained from the SEM image in Figure 2 (a).

Fig. 2 :

 2 Fig. 2: SEM image of the gold pattern using BSE detector (a), and corresponding reference image generated numerically (b).The scale bar is 200 µm

  .., denote the unknown complex-valued coefficients of the polynomial series describing υ d , respectively υ g .

Fig. 4 :

 4 Fig. 4: RMS value of the error fields expressed in pixels as a function of the measured rotation angle of the pattern in degrees. The physical size of one pixel is 240 nm

Fig. 5 :

 5 Fig. 5: Horizontal (a) and vertical (b) components of imaging distortions. Horizontal (c) and vertical (d) components of patterning errors. The fields are expressed in pixels, whose physical size is 240 nm


Nikola Beneš

Uli Fahrenberg
email: ulrich.fahrenberg@inria.fr

Jan Křetínský

Axel Legay

Louis-Marie Traonouez

Logical vs. Behavioural Specifications

Keywords: component-based design, refinement, logic, modal transition system, specification

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 νcalculus and the behavioural formalism of disjunctive modal transition systems. The translations preserve structural properties of the specification and allow us to perform logical operations on the behavioural specifications as well as behavioural compositions on logical formulae. The unification of both approaches provides additional methods for component-based stepwise design.

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 specification formalisms and their relationship. As an example, let us consider labelled transition systems and the property that "at all time points after executing req, 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(req ⇒ AX(work AW grant)) req grant, work, idle work grant or as a recursive system of equations in Hennessy-Milner logic [START_REF] Kim | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF] as

X = [grant, idle, work]X ∧ [req]Y Y = ( work Y ∨ grant X) ∧ [idle, req]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] Kim | Equation solving using modal transition systems[END_REF]. Figure 1 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 given in Fig. 2.

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] Kim | Modal specifications[END_REF], on the other hand, have a focus on compositional and incremental design. For a model consisting of several components, compositionality allows us to [START_REF] Aceto | On the specification of modal systems: A comparison of three frameworks[END_REF] infer properties of a system from the specifications of its components, and (2) decompose the problem of correctness for a system into verification problems for its components, which helps in overcoming the state space explosion problem. In this respect, logical specifications are somewhat lacking. Further, 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] Kim | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF] for a good account of composition and decomposition and other features which one would wish specifications to have. 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.

X = a tt ∧ [a]X ∧ [b]X a b
Figure 3: ν-calculus formula and DMTS for the invariance property "there is always an 'a' transition available", over the alphabet Σ = {a, b} Our Contribution Firstly, we show that Hennessy-Milner logic with greatest fixed points (the modal ν-calculus) and DMTS (with several initial states) are equally expressive, and we provide translations forth and back. Moreover, the translations preserve structural properties of the formulae/systems and enable us to freely combine the two formalisms. 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]) and a related 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], so that both turn out to be equivalent in expressiveness to ν-calculus and DMTS. The established connection also allows for a graphical representation of ν-calculus as DMTS. This extends the graphical representability of Hennessy-Milner logic (without fixed points) as modal transition systems [START_REF] Boudol | Graphical versus logical specifications[END_REF][START_REF] Kim | Modal specifications[END_REF].

X = b tt ∨ a tt ∧ [a]X ∧ [b]X ∧ [c]X
Example 1. Figures 3 and4 show examples of important basic properties expressed both as formulae in the modal ν-calculus and as DMTS. We refer to Section 2 for the formal definitions. Note that the DMTS in Fig. 4 has two initial states; we will show in Section 3.5 that allowing multiple initial states is essential for the correspondence between DMTS and the modal ν-calculus.

Secondly, we show that there are natural operations of conjunction and disjunction for DMTS that mimic the ones of ν-calculus. As we work with multiple initial states, disjunction is readily defined, and conjunction extends the one for DMTS with single initial state [START_REF] Beneš | Modal transition systems: Composition and LTL model checking[END_REF].

Thirdly, we introduce compositionality into the formalisms. For simplicity we assume CSP-style synchronisation of labels, but the construction can easily be generalised to other types of label synchronisation. We define a composition operator for specifications which soundly captures parallel composition of implementations, and we provide a solution to the open problem of the general quotient.

The intuition of quotient, or decomposition, is as follows. Given a specification S of a 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 . 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) DMTS. 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 composition and quotient, all four discussed formalisms form commutative residuated lattices [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. Moreover, they form complete specification theories in the sense of [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF]. Hence they support full compositionality and decomposition in the sense of [START_REF] Kim | 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.

Outline of the Paper

Section 2 introduces all the formalisms of DMTS, ν-calculus and the auxiliary formalisms of NAA and a new hybrid modal logic, which can serve as compact representation for NAA and is of interest in itself. In Section 3 the equivalence of the systems is discussed. In Section 4, we use our translations to turn the formalisms into complete specification theories. Section 5 discusses related work and Section 6 concludes.

Specification Formalisms

In this section we introduce the four specification formalisms with which this paper is concerned. 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 (finite) labelled transition systems (LTS) over Σ, i.e. structures I = (S, s 0 , -→) consisting of a finite set S of states, an initial state s 0 ∈ S, and a transition relation -→ ⊆ S × Σ × S.

Disjunctive Modal Transition Systems

Definition 1. 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-transition s -→ N stipulates a disjunctive requirement: at least one of the choices (a, t) ∈ N has to be implemented. A DMTS (S, S 0 , , -→) is an implementation if S 0 = {s 0 } is a singleton and -→ = {(s, {(a, t)}) | s a t}.

DMTS were introduced in [START_REF] Kim | Equation solving using modal transition systems[END_REF] in the context of equation solving. They are a natural closure of modal transition systems (MTS) [START_REF] Kim | Modal specifications[END_REF]. We say that a DMTS (S, S 0 , , -→) is a MTS if S 0 = {s 0 } is a singleton and for all s -→ N it holds that N = {(a, t)} is also a singleton. When speaking about MTS, we usually write s a -→ t instead of s -→ {(a, t)}. An LTS (S, s 0 , -→) can be translated to a DMTS implementation (S, S 0 , , -→ ) by setting S 0 = {s 0 }, = -→ and -→ = {(s, {(a, t)}) | s a -→ t}. This defines an embedding of LTS into DMTS whose image are precisely the DMTS implementations.

Definition 2. Let D 1 = (S 1 , S 0 1 , 1 , -→ 1 ) and 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 1 there is t 2 ∈ S 2 with s 2 a t 2 and (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.
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 (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 )
. Sometimes we will refer to the last property of a modal refinement relation,

∀s 0 1 ∈ S 0 1 : ∃s 0 2 ∈ S 0 2 : (s 0 1 , s 0 2 ) ∈ R, as being initialised.
Note that modal refinement is reflexive and transitive, i.e. a preorder on DMTS.

The set of implementations of a 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 ≤ t D 2 , if D 1 ⊆ D 2 . We write D 1 ≡ t D 2 if D 1 ≤ t D 2 and D 2 ≤ t 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 ≤ t 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š | Modal transition systems: Composition and LTL model checking[END_REF], but we will not need this here.

Proposition 3. For all DMTS D 1 , D 2 , D 1 ≤ m D 2 implies D 1 ≤ t D 2 .

The Modal ν-Calculus

We recall the syntax and semantics of the modal ν-calculus, the fragment of the modal µ-calculus [START_REF] Kozen | Results on the propositional µ-calculus[END_REF][START_REF] Scott | A theory of programs[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] Kim | 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] Kim | 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 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.

We are now going to introduce a normal form for ν-calculus expressions. The purpose of this normal form is twofold. One is to allow us to define modal refinement for ν-calculus, an analogue to the DMTS modal refinement that can be seen as a sound approximation of the logical implication, cf. Proposition 3. The second purpose is to facilitate a simple translation between DMTS and ν-calculus expressions, see Section 3.1 below. 1Lemma 4. 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 ≤ t y aij ,j .

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

∆ 2 (x) = i∈I ( j∈Ji a ij x ij ∧ a∈Σ [a]x i,a
). Now for each such formula, replace (recursively) x by new variables

{x i | i ∈ I} and set ∆ 2 (x i ) = j∈Ji a ij k xk ij ∧ a∈Σ [a] k xk i,a . Using initial variables X 0 2 = {x i | x ∈ X 0 1 }, the so-constructed ν-calculus expression is equivalent to the original one.
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 .

Definition 5. Let N 1 = (X 1 , X 0 1 , ∆ 1 ), N 2 = (X 2 , X 0 2 , ∆ 2 ) be ν-calculus expres- sions 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
• 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

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

We say that N 1 modally refines N 2 , denoted N 1 ≤ m N 2 , whenever there exists a modal 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 say that a ν-calculus expression (X, X 0 , ∆) in normal form is an implementation if X 0 = {x 0 } is a singleton, ♦(x) = {{(a, y)} | y ∈ a (x), a ∈ Σ} and a (x) = ∅ for all a / ∈ Σ, for all x ∈ X. We can translate an LTS (S, s 0 , -→) to a ν-calculus expression (S, S 0 , ∆) in normal form by setting S 0 = {s 0 } and ♦(s) = {{(a, t)} | s a -→ t} and a (s) = {t | s a -→ t} for all s ∈ S, a ∈ Σ. Like for DMTS, this defines an embedding of LTS into the modal ν-calculus whose image are precisely the ν-calculus implementations.

We will show below in Theorem 10 that for any LTS I and any ν-calculus expression N in normal form, I |= N iff I ≤ m N , hence the fixed-point semantics of [START_REF] Kim | Proof systems for satisfiability in Hennessy-Milner logic with recursion[END_REF] and our refinement semantics agree. As a corollary of this result, we get that modal refinement is a sound approximation to logical implication, i.e. that N 1 ≤ m N 2 implies that for all implementations I, (I |= N 1 ) ⇒ (I |= N 2 ).

Nondeterministic Acceptance Automata

Definition 6. A nondeterministic acceptance automaton (NAA) 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 ) = ∅.

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, these are deterministic. We extend the formalism into nondeterministic setting here. The following notion of modal refinement was introduced in [START_REF] Beneš | Parametric modal transition systems[END_REF].

Definition 7. Let A 1 = (S 1 , S 0 1 , Tran 1 ) and A 2 = (S 2 , S 0 2 , Tran 2 ) be NAA. 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 . (2)
We say that A 1 modally refines A 2 , and 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.
An NAA is an implementation if S 0 = {s 0 } is a singleton and, for all s ∈ S, Tran(s) = {M } is a singleton. An LTS (S, s 0 , -→) can be translated to an NAA by setting S 0 = {s 0 } and Tran(s) = {{(a, t) | s a -→ t}}. This defines an embedding of LTS into NAA whose image are precisely the NAA implementations.

Hybrid Modal Logic

As our fourth specification formalism, we introduce a hybrid modal logic, 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] Blackburn | Representation, reasoning, and relational structures: a hybrid logic manifesto[END_REF][START_REF] Prior | Papers on Time and Tense[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.

We can translate an LTS (S, s 0 , -→) to an L-expression (S, S 0 , Φ) by setting

S 0 = {s 0 } and Φ(s) = s a -→t a t ∧ s b -→u ¬ b u.
This defines an embedding of LTS into L-expressions whose image are precisely the L-implementations.

Definition 8. 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, y 1 ) ∈ M 1 : ∃(a, y 2 ) ∈ M 2 : (y 1 , y 2 ) ∈ R, • ∀(a, y 2 ) ∈ M 2 : ∃(a, y 1 ) ∈ M 1 : (y 1 , y 2 ) ∈ R. We say that E 1 modally refines E 2 , denoted E 1 ≤ m E 2 , whenever there exists 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.

Structural Equivalence

We proceed to show that our four specification formalisms are structurally equivalent. To this end, we shall expose six translations between them, see Fig. 5. Section 3.1 is concerned with dn and nd, Section 3.2 with al and la, and Section 3.3 with da and ad. We show in Theorems 9, 11 and 12 that all six translations preserve and reflect modal refinement.

X 1 = a Y ∧ [a]tt ∧ [b]ff X 2 = [a]ff ∧ [b]tt Y = b (X 1 ∨ X 2 ) ∧ [a]ff ∧ [b]tt X1 tt X2 Y a a b b b b a, b
∆(s) = N ∈♦(s) (a,t)∈N a t ∧ a∈Σ [a] t∈ a (s) t (3)
and define the (normal-form) ν-calculus expression dn(D) = (S, S 0 , ∆). 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 similar to the characteristic formulae of [START_REF] Kim | Modal specifications[END_REF].

Conversely, 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 nd(N ) = (X, X 0 , , -→). Note how this is a simple syntactic translation from boxes to disjunctive must-transitions and from diamonds to may-transitions. Also, the two translations are inverse to each other: dn(nd(N )) = N and nd(dn(D)) = D. The following theorem follows easily:

Example 2. Consider the ν-calculus formula X = a ( b X ∧ [a]ff ) ∧ [b]ff ∨ [a]ff .
Converting the formula into the normal form of Lemma 4 yields the result given in Fig. 6 (left), where both X 1 and X 2 are initial variables. The resulting DMTS is illustrated in Fig. 6 (right).

Theorem 9. For all DMTS D 1 , D 2 , D 1 ≤ m D 2 iff dn(D 1 ) ≤ m dn(D 2 ). For all ν-calculus expressions N 1 , N 2 in normal form, N 1 ≤ m N 2 iff nd(N 1 ) ≤ m nd(N 2 ).
As a corollary, we can now show that the fixed-point semantics and our refinement semantics for the modal ν-calculus agree: Write I = (I, i 0 , -→ I ), D = (S, S 0 , , -→), and dn(D) = (S, S 0 , ∆).

For states i ∈ I, s ∈ S, write i ≤ m s iff (I, i, -→ I ) ∈ (S, {s},
, -→) , i.e. if the LTS I with its initial state replaced by i implements the DMTS S with initial state s. Similarly, write i |= s iff (I, i, -→ I ) ∈ (S, {s}, ∆) .

We start with the only-if part. The proof is done by coinduction. We define the assignment σ : S → 2 I as follows:

σ(t) = {j ∈ I | j ≤ m t}. We need to show that for every s ∈ S, σ(s) ⊆ ∆(s) σ. Let i ∈ σ(s). As i ≤ m s, we know that (1) ∀s -→ N : ∃i a -→ I j, (a, t) ∈ N : j ≤ m t and (2) ∀i a -→ I j : ∃s a t : j ≤ m t.
Due to (1), we see that for all N ∈ ♦(s), there is i

a -→ I j and (a, t) ∈ N such that j ∈ σ(t) and i ∈ a t σ. Hence i ∈ N ∈♦(s) ( (a,t)∈N a t) σ = N ∈♦(s) ( (a,t)∈N a t) σ.
Due to (2), it holds that for every a ∈ Σ and every i a -→ I j, there is t ∈ a (s) such that j ∈ σ(t) ⊆ t∈ a (s) t σ. Hence i ∈ a∈Σ [a]( t∈ a (s) t) σ = a∈Σ [a]( t∈ a (s) t) σ. Altogether, we have shown that i ∈ ∆(s) . Clearly, there is s 0 ∈ S 0 such that i 0 ∈ σ(s 0 ). Therefore, I |= dn(D). For the other direction, define a relation R ⊆ I × S by R = {(j, t) | j |= t}. We show that R satisfies the conditions of modal refinement.

Let (i, s) ∈ R. As i |= s, we know that (1) ∀N ∈ ♦(s) : ∃(a, t) ∈ N : i |= a t and (2) ∀a ∈ Σ : i |= [a]( t∈ a (s) t).

By (1), we know that for all s -→ N , there is (a, t) ∈ N and i a -→ I j such that j |= t. By (2), it holds that for all i a -→ I j, there is s a t so that j |= t.

We have shown that i ≤ m s.

Clearly, there is s 0 ∈ S 0 for which (i 0 , s 0 ) ∈ R, hence I ≤ m D.

NAA vs. Hybrid Modal Logic

Also the translations between NAA and our hybrid modal logic are straightforward. For an NAA 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 NAA la(E) = (X, X 0 , Tran).

Theorem 11. For all NAA A 1 , A 2 , A 1 ≤ m A 2 iff al(A 1 ) ≤ m al(A 2 ). For all L-expressions E 1 , E 2 , E 1 ≤ m E 2 iff la(E 1 ) ≤ m la(E 2 ).
Proof. We show that for any NAA (S, S 0 , Tran) and any L-expression (S, S 0 , Φ), Tran(s) = Φ(s) for every s ∈ S, for both translations. For the second one, la, this is clear by definition, and for the first,

Φ(s) = M ∈Tran(s) (a,t)∈M a t ∧ (b,u) / ∈M ¬ b u = M ∈Tran(s) (a,t)∈M {M | (a, t) ∈ M } ∩ (b,u) / ∈M {M | (b, u) / ∈ M } = M ∈Tran(s) {M | ∀(a, t) ∈ M : (a, t) ∈ M } ∩ {M | ∀(b, u) / ∈ M : (b, u) / ∈ M } = M ∈Tran(s) {M | M ⊆ M } ∩ {M | M ⊆ M } = M ∈Tran(s) M = Tran(s)
as was to be shown.

DMTS vs. NAA

The translations between DMTS and NAA are somewhat more intricate. 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 NAA da(D) = (S, S 0 , Tran). 2For an NAA 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.

Theorem 12. For all DMTS D 1 , D 2 , D 1 ≤ m D 2 iff da(D 1 ) ≤ m da(D 2 ). For all NAA A 1 , A 2 , A 1 ≤ m A 2 iff ad(A 1 ) ≤ m ad(A 2 ). Proof. To show that D 1 ≤ m D 2 implies da(D 1 ) ≤ m da(D 2 ), write D 1 = (S 1 , S 0 1 , 1 , -→ 1 ), D 2 = (S 2 , S 0 2 , 2 , -→ 2 ).
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

M 2 = {(a, t 2 ) | s 2 a 2 t 2 , ∃(a, t 1 ) ∈ M 1 : (t 1 , t 2 ) ∈ R}. The condition ∀(a, t 2 ) ∈ M 2 : ∃(a, t 1 ) ∈ M 1 : (t 1 , t 2 ) ∈ R
in the definition of NAA 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 -→ 2 N 2 ; we need to show that N 2 ∩ M 2 = ∅.
By DMTS refinement, we have

s 1 -→ 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 a 2 t 2 , hence (a, t 2 ) ∈ M 2 .
To prove that da(D

1 ) ≤ m da(D 2 ) implies D 1 ≤ m D 2 , let R ⊆ S 1 × S 2 be a modal refinement relation in the NAA sense and (s 1 , s 2 ) ∈ R. Let s 1 a 1 t 1 , then we cannot have s 1 -→ 1 ∅. Let M 1 = {(a, t 1 )} ∪ {N 1 | s 1 -→ 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 2 t 2 as was to be shown.

Let s 2 -→ 2 N 2 and assume, for the sake of contradiction, that there is no

s 1 -→ 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 -→ 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. Let M 1 = {(a N1 , t N1 ) | s 1 -→ 1 N 1 }, then M 1 ∈ Tran 1 (
(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 .

For the proof that

A 1 ≤ m A 2 implies ad(A 1 ) ≤ m ad(A 2 ), write A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), with DMTS translations (D 1 , D 0 1 , -→ 1 , 1 ), (D 2 , D 0 2 , -→ 2 , 2 ). We have a modal refinement relation (in the NAA sense) R ⊆ S 1 × S 2 . Define R ⊆ D 1 × D 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}. We show that R is a modal refinement in the DMTS sense. Let (M 1 , M 2 ) ∈ R . Let M 2 -→ 2 N 2 . By construction of -→ 2 , there is (a, t 2 ) ∈ M 2 such that N 2 = {(a, M 2 ) | M 2 ∈ Tran 2 (t 2 )}. Then (M 1 , M 2 ) ∈ R
implies that there must be (a, t 1 ) ∈ M 1 for which (t 1 , t 2 ) ∈ R, and we can define

N 1 = {(a, M 1 ) | M 1 ∈ Tran 1 (t 1 )}, whence M 1 -→ 1 N 1 .
We show that ∀(a, M 1 )

∈ N 1 : ∃(a, M 2 ) ∈ N 2 : (M 1 , M 2 ) ∈ R . Let (a, M 1 ) ∈ N 1 , then M 1 ∈ Tran 1 (t 1 ). From (t 1 , t 2 ) ∈ R we hence get M 2 ∈ Tran 2 (t 2 ), and then (a, M 2 ) ∈ N 2 by construction of N 2 and (M 1 , M 2 ) ∈ R due to the conditions of NAA refinement (applied to (t 1 , t 2 ) ∈ R). Let M 1 a 1 M 1 , then we have M 1 -→ 1 N 1 for which (a, M 1 ) ∈ N 1 by construction of 1 .
This in turn implies that there must be (a,

t 1 ) ∈ M 1 such that N 1 = {(a, M 1 ) | M 1 ∈ Tran 1 (t 1 )}, and then by (M 1 , M 2 ) ∈ R , we get (a, t 2 ) ∈ M 2 for which (t 1 , t 2 ) ∈ R. Let N 2 = {(a, M 2 ) | M 2 ∈ Tran 2 (t 2 )}, then M 2 -→ 2 N 2 and hence M 2 a 2 M 2 for all (a, M 2 ) ∈ N 2 .
On the other hand, the argument in the previous paragraph shows that there is (a, M 2 ) ∈ N 2 for which (M 1 , M 2 ) ∈ R .

We miss to show that R is initialised. Let M 0 1 ∈ D 0 1 , then we have s 0 1 ∈ S 0 1 with M 0 1 ∈ Tran 1 (s 0 1 ). As R is initialised, 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 NAA refinement conditions, whence

(M 0 1 , M 0 2 ) ∈ R . To see that ad(A 1 ) ≤ m ad(A 2 ) implies A 1 ≤ m A 2 , let R ⊆ D 1 × D 2 be a modal refinement relation in the DMTS sense and define R ⊆ S 1 × S 2 by R = {(s 1 , s 2 ) | ∀M 1 ∈ Tran 1 (s 1 ) : ∃M 2 ∈ Tran 2 (s 2 ) : (M 1 , M 2 ) ∈ R} ;
we will show that R is an NAA modal refinement.

Let (s 1 , s 2 ) ∈ R and M 1 ∈ Tran 1 (s 1 ), then by construction of R , we have

M 2 ∈ Tran 2 (s 2 ) with (M 1 , M 2 ) ∈ R. Let (a, t 2 ) ∈ M 2 and define N 2 = {(a, M 2 ) | M 2 ∈ Tran 2 (t 2 )}, then M 2 -→ 2 N 2 . Now (M 1 , M 2 ) ∈ R implies that there must be M 1 -→ 1 N 1 satisfying ∀(a, M 1 ) ∈ N 1 : ∃(a, M 2 ) ∈ N 2 : (M 1 , M 2 ) ∈ R. We have (a, t 1 ) ∈ M 1 such that N 1 = {(a, M 1 ) | M 1 ∈ Tran 1 (t 1 )}; we only miss to show that (t 1 , t 2 ) ∈ R . Let M 1 ∈ Tran 1 (t 1 ), then (a, M 1 ) ∈ N 1 , hence there is (a, M 2 ) ∈ N 2 with (M 1 , M 2 ) ∈ R, but (a, M 2 ) ∈ N 2 also entails M 2 ∈ Tran 2 (t 2 ).
Let (a, t 1 ) ∈ M 1 and define

N 1 = {(a, M 1 ) | M 1 ∈ Tran 1 (t 1 )}, then M 1 -→ 1 N 1 . Now let (a, M 1 ) ∈ N 1 , then M 1 a 1 M 1 , hence we have M 2 a 2 M 2 for some (M 1 , M 2 ) ∈ R by modal refinement. By construction of
2 , this implies that there is M 2 -→ 2 N 2 with (a, M 2 ) ∈ N 2 , and we have (a, t 2 ) ∈ M 2 for which

N 2 = {(a, M 2 ) | M 2 ∈ Tran 2 (t 2 )}. Now if M 1 ∈ Tran 1 (t 1 ), then (a, M 1 ) ∈ N 1 , hence there is (a, M 2 ) ∈ N 2 with (M 1 , M 2 ) ∈ R, but (a, M 2 ) ∈ N 2 also gives M 2 ∈ Tran 2 (t 2 ).
We miss to show that R is initialised. Let s 0 1 ∈ S 0 1 , then Tran 1 (s 0 1 ) = ∅, hence there is

M 0 1 ∈ Tran 1 (s 0 1 ). As R is initialised, this gets us M 0 2 ∈ D 2 with (M 0 1 , M 0 2 ) ∈ R, but M 0 2 ∈ Tran 2 (s 0
2 ) for some s 0 2 ∈ S 0 2 , and then (s 0 1 , s 0 2 ) ∈ R .

Corollary 13. For all DMTS D, ν-calculus expressions N , NAA A, and Lexpressions E, dn(D) ≡ t da(D) ≡ t D, nd(N ) ≡ t N , ad(A) ≡ t al(A) ≡ t A, and la(E) ≡ t E.

Translation Complexity

We have shown that our four specification formalisms are structurally equivalent, which will be useful for us from a theoretical point of view. From a practical point of view however, some of the translations may incur exponential blow-ups, hence care has to be taken. On the other hand, all our translations can be implemented in an on-the-fly manner, only creating states when necessary.

We already noticed that the translation of ν-calculus expressions into normal form may incur an exponential blow-up, so this also affects our translation from the modal ν-calculus to DMTS. When considering only normal-form expressions, the translations to and from DMTS incur no blow-ups.

When translating from NAA to our hybrid modal logic, we see that, due to the complementation (b, u) / ∈ M , the length of a formula Φ(s) is quadratic in the representation of Tran(s). For the reverse translation, the number of Tran constraints can be exponential in the number of states. The worst case is Φ(s) = tt, which gets translated to Tran(s) = 2 2 Σ×S . We note that there is a direct translation from DMTS to hybrid modal logic: for a DMTS D = (S, S 0 , , -→), define dl(D) = (S, S 0 , Φ) with

Φ(s) = s-→N (a,t)∈N a t ∧ s a u ¬ a u
for all s ∈ S. This translation is again quadratic, and da(D) = la(dl(D)).

The translations between DMTS and NAA may involve exponential blow-ups both ways. For the first translation, we can see this by considering the one-state DMTS ({s}, {s},

, -→) with = {(s, a, s) | a ∈ Σ} and -→ = ∅. Then Tran(s) = 2 2 Σ×S .
The fact that also the translation from NAA to DMTS may be exponential in space is evident from the definition. To see that this blow-up is unavoidable, we expose a special property of the Tran-sets arising in the DMTS-to-NAA translation.

Lemma 14. 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
• for all s -→ N , there is (a, t) ∈ M i ∩ N . Now as M ⊆ M 1 ∪ M 2
, it directly follows that for all (a, t) ∈ M , we have s a t. Moreover, since M 1 ⊆ M , we also have that for all s -→ N , there exists (a, t) ∈ M ∩ N . As a consequence, M ∈ Tran(s).

Using this, we can show the following. 3Lemma 15. There exists a one-state NAA A for which any DMTS D ≡ t A has at least 2 n-1 states, where n is the size of the alphabet Σ.

Proof. Let Σ = {a 1 , . . . , a n } and A = ({s 0 }, {s 0 }, Tran) the NAA with Tran(s 0 ) = {M ⊆ Σ × {s 0 } | ∃k : |M | = 2k} the transition constraint containing all disjunctive choices of even cardinality. Let D = (T, T 0 , , -→) be a DMTS with D ≡ t A; we claim that D must have at least 2 n-1 initial states.

Assume, for the purpose of contradiction, that

T 0 = {t 0 1 , . . . , t 0 m } with m < 2 n-1 . We must have m i=1 Tran T (t 0 i ) = {M ⊆ Σ × T | ∃k : |M | = 2k}
, so that there is an index j ∈ {1, . . . , m} for which Tran T (t 0 j ) = {M 1 , M 2 } contains two different disjunctive choices from Tran S (s 0 ). By Lemma 14, also M ∈ Tran T (t 0 j ) for any M with M 1 ⊆ M ⊆ M 1 ∪ M 2 . But M 1 ∪ M 2 has greater cardinality than M 1 , so that there will be an M ∈ Tran T (t 0 j ) with odd cardinality.

Figure 7 sums up the translation complexities.

DMTS

X / / L Q & & NAA X o o Q ν-calculus X / / ν-normal form L o o L O O hybrid modal logic X O O
Figure 7: Complexity of the translations between specification formalisms. "L" stands for linear (no blow-up), "Q" for quadratic blow-up, and "X" for exponential blow-up

Initial States

We finish this section with a justification for why we allow our specifications to have several (or possibly zero) initial states. The first lemma shows that for NAA, and up to thorough refinement, this is inessential; due to their close relationship, this also holds for L-expressions.

Lemma 16. For any NAA A 1 , there is an NAA A 2 = (S 2 , S 0 2 , Tran 2 ) with S 0 2 = {s 0 2 } a singleton and

A 1 ≡ t A 2 . Proof. Write A 1 = (S 1 , S 0 1 , Tran 1 ). If S 0 1 = ∅,
(s) = Tran 1 (s) for s ∈ S 1 , Tran 2 (s 0 2 ) = s 0 1 ∈S 0 1 Tran 1 (s 0 1 ). Let R = id S1 ∪ {(s 0 1 , s 0 2 ) | s 0 1 ∈ S 0 1 }, then R is easily seen to be a modal refinement A 1 ≤ m A 2 .
We show that A 2 ≤ t A 1 . Let I = (S, s 0 , -→) ∈ A 2 , then we have a modal refinement R 2 ⊆ S × S 2 , i.e. such that for all (s, s 2 ) ∈ R 2 , there exists

M 2 ∈ Tran 2 (s 2 ) for which ∀s a -→ t : ∃(a, t 2 ) ∈ M 2 : (t, t 2 ) ∈ R 2 , ∀(a, t 2 ) ∈ M 2 : ∃s a -→ t : (t, t 2 ) ∈ R 2 . (4)
Now (s 0 , s 0 2 ) ∈ R 2 implies that there must be M 2 ∈ Tran 2 (s 0 2 ) for which (4) holds, but by definition of Tran 2 (s 0 2 ), this entails that there is s 0 1 ∈ S 0 1 for which

M 2 ∈ Tran 1 (s 0 1 ). Define R 1 ⊆ S × S 1 by R 1 = {(s, s 2 ) | (s, s 2 ) ∈ R 2 , s = s 0 } ∪ {(s 0 , s 0 1 )} , then R 1 is a modal refinement I ≤ m A 1 .
In order to show that the above statement does not hold for DMTS, we expose a special property of DMTS with single initial states, cf. [7, Example 7.8]. Recall that for LTS I 1 = (S 1 , s 0 1 , -→ 1 ), I 2 = (S 2 , s 0 2 , -→ 2 ), their nondeterministic sum is given by I 1 + I 2 = (S, s 0 , -→) with S = S 1 ∪ S 2 ∪ {s 0 } (with the unions disjoint), where s 0 is a new state, and transitions s a -→ t iff s a -→ 1 t or s a -→ 2 t together with s 0 a -→ t for all t with s 0 Proof. Let i 0 1 and i 0 2 be the initial states of I 1 and I 2 , respectively. Let further i 0 be the initial state of I 1 + I 2 . Assume that we have modal refinements R 1 and R 2 such that

(i 0 1 , s 0 ) ∈ R 1 and (i 0 2 , s 0 ) ∈ R 2 . Let R = R 1 ∪ R 2 ∪ {(i 0 , s 0 )}. Clearly, R is a modal refinement witnessing I 1 + I 2 ≤ m D.
Now let D be the DMTS, with two initial states, depicted in Fig. 8, then D = {I 1 , I 2 } as also seen in Fig. 8, but I 1 + I 2 / ∈ D . Hence D is not thoroughly equivalent to any DMTS with a single initial state.

Applying the construction from the proof of Lemma 16 to the DMTS in Fig. 8 gives an NAA A 2 = (S 2 , {s 0 2 }, Tran 2 ) with Tran 2 (s 0 2 ) = {{(a, s 1 )}, {(b, t 1 }} (where s 1 and t 1 are the target states of the a and b transitions in D, respectively). This specifies an exclusive disjunction: one of a and b has to be implemented, but not both. This also serves to show that Lemma 17 does not hold for NAA.

Corollary 18. There is a DMTS D 1 for which there is no DMTS D 2 = (S 2 , S 0 2 , , -→) with S 0 2 = {s 0 2 } a singleton and

D 1 ≡ t D 2 .
Due to their close relationship with DMTS, this property also holds for ν-calculus expressions in normal form: there exist ν-calculus expressions which are not equivalent to any normal-form ν-calculus expression with a single initial variable. (Of course, omitting "normal form" would make this statement invalid; as disjunction is part of the syntax, any ν-calculus expression is thoroughly equivalent to one with only one initial variable.)

We also remark that the above argument can easily be extended to show that for any k ∈ N, there exists a DMTS with k + 1 initial states which is not thoroughly equivalent to any DMTS with at most k initial states. Using again the example in Fig. 8, we can also show that the statement in Lemma 16 does not hold when thorough equivalence is replaced by modal equivalence. Let A 1 = da(D), with initial states s 0 and t 0 , be the NAA translation of the DMTS in Fig. 8 and assume that there exists an NAA A 2 with single initial state s 0 2 for which A 2 ≤ m A 1 . Then there is a modal refinement R with (s 0 2 , s 0 ), (s 0 2 , t 0 ) ∈ R. Let M 2 ∈ Tran 2 (s 0 2 ), then by (s 0 2 , s 0 ) ∈ R, there must be some (a, t 2 ) ∈ M 2 with (t 2 , s 1 ) ∈ R. By (s 0 2 , t 0 ) ∈ R, this implies that there must be (a, t 1 ) ∈ Tran 1 (t 0 ), a contradiction.

Specification Theory

Behavioural specifications typically come equipped with operations which allow for compositional reasoning, viz. conjunction, composition and quotient, cf. [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF]. On deterministic MTS, these operations can be given easily using simple structural operational rules. For non-deterministic systems this is significantly harder.

We remark that composition and quotient operators are well-known from some logics, such as, e.g. linear [START_REF] Girard | Linear logic[END_REF] or spatial logic [START_REF] Caires | A spatial logic for concurrency[END_REF], and were extended to quite general contexts [START_REF] Cardelli | Modular Markovian logic[END_REF]. However, whereas these operators are part of the formal syntax in those logics, for us they are simply operations on logical expressions (or DMTS, or NAA). Consequently, composition is generally only a sound over-approximation of the semantic composition.

Given the structural equivalence of DMTS, the modal ν-calculus, NAA, and our hybrid modal logic exposed in the previous section, it suffices to introduce the operations for one of the four types of specifications. On the other hand, we will often state properties for all four types of specifications at the same time, letting S stand for a specification of any type.

Disjunction and Conjunction

Disjunction of specifications is easily defined as we allow multiple initial states.

For DMTS D 1 = (S 1 , S 0 1 , 1 , -→ 1 ), D 2 = (S 2 , S 0 2 , 2 , -→ 2 ), we can hence define D 1 ∨ D 2 = (S 1 ∪ S 2 , S 0 1 ∪ S 0 2 , 1 ∪ 2 , -→ 1 ∪ -→ 2 )
(with all unions disjoint). Similar definitions are available for the other types of specifications, and disjunction commutes with the translations.

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 -→ 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 -→ 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 )}.
For NAA, conjunction can be defined using auxiliary projection functions

π i : Σ × S 1 × S 2 → Σ × S i given 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 } . Then for NAA A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), we let A 1 ∧ A 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 )}.
We can also define conjunction for L-expressions, using similar auxiliary mappings on formulae. For sets X 1 , X 2 and i ∈ {1, 2}, we define ρ

i : L(X i ) → L(X 1 × X 2 ) inductively, by • ρ i (tt) = tt, ρ i (ff ) = ff , ρ i (¬φ) = ¬ρ i (φ), ρ i (φ i ∧ φ 2 ) = ρ i (φ i ) ∧ ρ i (φ 2 ), • ρ 1 ( a x 1 ) = x2∈X2 a (x 1 , x 2 ), • ρ 2 ( a x 2 ) = x1∈X1 a (x 1 , x 2 ). Then for L-expressions (X 1 , X 0 1 , Φ 1 ), (X 2 , X 0 2 , Φ 2 ), X 1 ∧ X 2 = (X 1 × X 2 , X 0 1 × X 0 2 , Φ) with Φ((x 1 , x 2 )) = ρ 1 (Φ 1 (x 1 )) ∧ ρ 2 (Φ 2 (x 2 )). Lemma 19. For all DMTS D 1 , D 2 , NAA A 1 , A 2 , and L-expressions E 1 , E 2 , da(D 1 ∧ D 2 ) = da(D 1 ) ∧ da(D 2 ), ad(A 1 ∧ A 2 ) ≡ m ad(A 1 ) ∧ ad(A 2 ), al(A 1 ∧ A 2 ) = al(A 1 ) ∧ al(A 2 ), and la(E 1 ∧ E 2 ) = la(E 1 ) ∧ la(E 2 ).
Note that above we only claim modal equivalence, not equality, for the ad translation; this is due to the change of state space during the translation and follows easily from Theorem 20 below.

Proof. The last two claims follow easily once one notices that for

i ∈ {1, 2} and all M , M |= ρ i (φ) iff π i (M ) |= φ. To show the first claim, let D 1 = (S 1 , S 0 1 , 1 , -→ 1 ) and D 2 = (S 2 , S 0 2 , 2 , -→ 2 ) be DMTS, with NAA trans- lations Let da(D 1 ) = (S 1 , S 0 1 , Tran 1 ) and da(D 2 ) = (S 2 , S 0 2 , Tran 2 ). Write A ∧ = da(D 1 ∧ D 2 ) and A ∧ = da(D 1 ) ∧ da(D 2 ); we show that A ∧ = A ∧ .
First, remark that A ∧ and A ∧ have precisely the same state space S 1 × S 2 and initial states S 0 1 × S 0 2 . We now show that they have the same transition constraints. Let Tran ∧ (resp. Tran ∧ ) be the transition constraints mapping of

A ∧ (resp. A ∧ ). Let (s 1 , s 2 ) ∈ S 1 × S 2 and M ∈ Tran ∧ (s 1 , s 2 ).
By construction of Tran ∧ , there must be

M 1 ∈ Tran 1 (s 1 ) and M 2 ∈ Tran 2 (s 2 ) such that π 1 (M ) = M 1 and π 2 (M ) = M 2 . We show that M ∈ Tran ∧ (s 1 , s 2 ). Let (a, (t 1 , t 2 )) ∈ M . Since π 1 (M ) = M 1 and π 2 (M ) = M 2 , we have (a, t 1 ) ∈ M 1 and (a, t 2 ) ∈ M 2 .
As a consequence, there are transitions s 1 a t 1 and s 2 a t 2 in D 1 and D 2 , respectively. Thus, by construction, there is a transition We have shown that M ∈ Tran ∧ (s 1 , s 2 ). Similarly, we can show that for all M ∈ Tran ∧ (s 1 , s 2 ), we also have M ∈ Tran ∧ (s 1 , s 2 ). We can thus conclude that Tran ∧ = Tran ∧ , hence A ∧ = A ∧ .

(s 1 , s 2 ) a (t 1 , t 2 ) in D 1 ∧ D 2 . Let (s 1 , s 2 ) -→ N in D 1 ∧ D 2 . By construction, N is such that either (1) there exists N 1 such that s 1 -→ N 1 in D 1 and N = {(a, (t 1 , t 2 )) | (a, t 1 ) ∈ N 1 , (s 1 , s 2 ) a (
Theorem 20. For all specifications S 1 , S 2 , S 3 ,

• S 1 ∨ S 2 ≤ m S 3 iff S 1 ≤ m S 3 and S 2 ≤ m S 3 , • S 1 ≤ m S 2 ∧ S 3 iff S 1 ≤ m S 2 and S 1 ≤ m S 3 , • S 1 ∨ S 2 = S 1 ∪ S 2 , and S 1 ∧ S 2 = S 1 ∩ S 2 . Proof. The proof that S 1 ∨ S 2 ≤ m S 3 iff S 1 ≤ m S 3 and S 2 ≤ m S 3 is trivial: any modal refinement R ⊆ (S 1 ∪ S 2 ) × S 3 splits into two refinements R 1 ⊆ S 1 × S 3 , R 2 ⊆ S 2 × S 3 and vice versa.
For the proof of the second claim, which we show for DMTS, we prove the back direction first. Let

R 2 ⊆ S 1 × S 2 , R 3 ⊆ S 1 × S 3 be (DMTS) modal refinements and define R = {(s 1 , (s 2 , s 3 )) | (s 1 , s 2 ) ∈ R 1 , (s 1 , s 3 ) ∈ R 3 } ⊆ S 1 × (S 2 × S 3 ). Then R is initialised. Now let (s 1 , (s 2 , s 3 )) ∈ R, then (s 1 , s 2 ) ∈ R 2 and (s 1 , s 3 ) ∈ R 3 . Assume that s 1 a 1 t 1 , then by S 1 ≤ m S 2 , we have s 2 a 2 t 2 with (t 1 , t 2 ) ∈ R 2 . Similarly, by S 1 ≤ m S 3 , we have s 3 a 3 t 3 with (t 1 , t 3 ) ∈ R 3 . But then also (t 1 , (t 2 , t 3 )) ∈ R, and (s 2 , s 3 ) a (t 2 , t 3 ) by definition.
Assume that (s 2 , s 3 ) -→ N . Without loss of generality we can assume that there is

s 2 -→ 2 N 2 such that N = {(a, (t 2 , t 3 )) | (a, t 2 ) ∈ N 2 , s 3 a 3 t 3 }. By S 1 ≤ m S 2 , we have s 1 -→ 1 N 1 such that ∀(a, t 1 ) ∈ N 1 : ∃(a, t 2 ) ∈ N 2 : (t 1 , t 2 ) ∈ R 2 .
Let (a, t 1 ) ∈ N 1 , then also s 1 a 1 t 1 , so by S 1 ≤ m S 3 , there is s 3

a 3 t 3 with (t 1 , t 3 ) ∈ R 3 . By the above, we also have (a, t 2 ) ∈ N 2 such that (t 1 , t 2 ) ∈ R 2 , but then (a, (t 2 , t 3 )) ∈ N and (t 1 , (t 2 , t 3 )) ∈ R.
For the other direction of the second claim, let R ⊆ S 1 ×(S 2 ×S 3 ) be a (DMTS) modal refinement. We show that S 1 ≤ m S 2 , the proof of

S 1 ≤ m S 3 being entirely analogous. Define R 2 = {(s 1 , s 2 ) | ∃s 3 ∈ S 3 : (s 1 , (s 2 , s 3 )) ∈ R} ⊆ S 1 × S 2 , then R 2 is initialised. Let (s 1 , s 2 ) ∈ R 2 , then we must have s 3 ∈ S 3 such that (s 1 , (s 2 , s 3 )) ∈ R. Assume that s 1 a 1 t 1 , then also (s 2 , s 3 ) a (t 2 , t 3 ) and (t 1 , (t 2 , t 3 )) ∈ R. By construction we have s 2 a 2 t 2 and s 3 a 3 t 3 , but then (t 1 , t 2 ) ∈ R 2 . Assume that s 2 -→ 2 N 2 , then by construction, (s 2 , s 3 ) -→ N = {(a, (t 2 , t 3 )) | (a, t 2 ) ∈ N 2 , s 3 a 3 t 3 }. By S 1 ≤ m S 2 ∧ S 3 , we have s 1 -→ 1 N 1 such that ∀(a, t 1 ) ∈ N 1 : ∃(a, (t 2 , t 3 )) ∈ N : (t 1 , (t 2 , t 3 )) ∈ R.
Let (a, t 1 ) ∈ N 1 , then we have (a, (t 2 , t 3 )) ∈ N for which (t 1 , (t 2 , t 3 )) ∈ R. By construction of N , this implies that there are (a, t 2 ) ∈ N 2 and s 3

a 3 t 3 , but then (t 1 , t 2 ) ∈ R.
As to the last claims of the theorem, S 1 ∧S 2 = S 1 ∩ S 2 is clear from what we just proved: for all implementations I, I ≤ m S 1 ∧ S 2 iff I ≤ m S 1 and I ≤ m S 2 . For the other part, it is clear by construction that for any implementation I, any witness R for I ≤ m S 1 is also a witness for I ≤ m S 1 ∨ S 2 , and similarly for S 2 , hence S 1 ∪ S 2 ⊆ S 1 ∨ S 2 .

To show the other inclusion, we note that an initialised refinement R witnessing I ≤ m S 1 ∨ S 2 must relate the initial state of I either to an initial state of S 1 or to an initial state of S 2 . In the first case, and by disjointness, R witnesses I ≤ m S 1 , in the second, I ≤ m S 2 . Note how it is essential here that implementations have but one initial state; this part of the proof would break down if we were to allow several initial states for implementations.

Corollary 21. With operations ∨ and ∧, each of our four classes of specifications forms a bounded distributive lattice up to ≡ m .

Proof. The bottom elements (up to ≡ m ) in the lattices are given by specifications with empty initial state sets. The top elements are the DMTS ({s 0 }, {s 0 }, {(s 0 , a, s 0 ) | a ∈ Σ}, ∅) and its respective translations.

We miss to verify distributivity. Let

A i = (S i , S 0 i , Tran i ), for i = 1, 2, 3, be NAA. The set of variables of both A 1 ∧ (A 2 ∨ A 3 ) and (A 1 ∧ A 2 ) ∨ (A 1 ∧ A 3 ) is S 1 × (S 2 ∪ S 3 ) = S 1 × S 2 ∪ S 1 × S 3
, and one easily sees that the identity relation is a two-sided modal refinement. Things are similar for the other distributive law.

Composition

The composition operator for a specification theory is to mimic, at specification level, the parallel composition of implementations. That is to say, if is a Figure 9: DMTS S and T whose composition cannot be captured precisely 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 . (5)
For simplicity, we use CSP-style synchronisation for parallel 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 22. There is no operator , for any of our specification formalisms, which satisfies (5).

Proof. We show that there exist DMTS S and T such that there is no DMTS D with D = S T := {I J | I ∈ S , J ∈ T }. They are given in Figure 9; S has initial state s, while T has initial state t. Note that in fact, S and T are MTS, i.e. no disjunctive must transitions are used.

We make the following observations about implementations of S and T . They always contain one or more infinite runs labelled with a's with one-step b or c branches. Moreover, all infinite runs in these implementations are of this form. To each infinite a-run of an implementation we assign its signature, that is a word over 2 {b,c} that describes the one-step branches. This means that every implementation of S has runs with signatures from {{b}, {b, c}} ω , while every implementation of T has runs with signatures from {{c}, {b, c}} ω .

We now construct an implementation state space as illustrated in Figure 10. Consider the implementations I 1 , I 2 , . . . that share the same state space and have the initial state i 1 , i 2 , . . . , respectively. The implementation I n has only one a-run with the signature ∅ n {b, c}∅ ω . Note that I n is the composition of an implementation of S that has only one a-run with the signature {b} n {b, c}{b} ω and an implementation of T that has only one a-run with the signature {c} n {b, c}{c} ω .

Assume now that there exists a DMTS D with D = S T . As all I n belong to D and there is only a finite number of initial states of D, there has to be at least one initial state of D, say d, such that there exists a modal refinement R containing both (i k , d) and (i l , d) for some numbers k < l. Let D d be created from D by changing the set of initial states to the singleton {d}. As both I k ≤ m D d and I l ≤ m D d and D d has only one initial state, we know by Lemma 17 that also

j i 0 i 1 i 2 • • • in • • • a b c a a a a a a
I kl • • • • • • • • • • • • • • • • • •
I kl = I k + I l ≤ m D d .
The unfolding of this implementation is illustrated in Figure 11.

We now argue that I kl / ∈ S T . We actually show that it cannot even be bisimilar to any I J with I ∈ S and J ∈ T . Let us assume that there exist such I and J . We make the following observations:

• I has to contain at least one a-run with signature {b} k {b, c}{b} ω . Otherwise, it would be impossible to create the I k part of I kl .

• J has to contain at least one a-run with signature {c} l {b, c}{c} ω . Otherwise, it would be impossible to create the I l part of I kl .

However, these observations mean that I J contains at least one a-run with signature ∅ k {c}∅ l-k-1 {b}∅ ω . It is thus not bisimilar to I kl .

Given that we cannot have [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory[END_REF], the revised goal is to have a sound composition operator for which the right-to-left inclusion holds in [START_REF] Beneš | Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory[END_REF]. For NAA A 1 = (S 1 , S 0 1 , Tran 1 ), A 2 = (S 2 , S 0 2 , Tran 2 ), we define A 1 A 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(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 }.
Composition for DMTS is defined using the translations to and from NAA; note that this may incur an exponential blow-up. Lemma 23. 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 ∈ Σ.

Proof. Associativity and commutativity are clear. To show distributivity over ∨, let A i = (S i , S 0 i , Tran i ), for i = 1, 2, 3, be NAA. We prove that A 1 (A 1 ∨ A 3 ) ≡ m A 1 A 2 ∨ A 1 A 3 ; right-distributivity will follow by commutativity. The state spaces of both sides are S 1 × S 2 ∪ S 1 × S 3 , and it is easily verified that the identity relation is a two-sided modal refinement.

For the claim that A U ≡ m A for all NAA A = (S, S 0 , Tran), let u be the unique state of U and define R = {((s, u), s) | s ∈ S} ⊆ S × U × 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 Here, s = {(a, (t

M 1 ∈ Tran(s), then M = M 1 (Σ × {u}) = {(a, (t, u)) | (a, t) ∈ M 1 } ∈ Tran(s, u),
and the same argument applies.

The next theorem is one of independent implementability, as it ensures that a composition of refinements is a refinement of compositions: Remark that NAA composition is more precise than the composition for MTS introduced in [START_REF] Kim | Modal specifications[END_REF]. The MTS composition is given by the following rules:

(s 1 , s 2 ) a (t 1 , t 2 ) whenever s 1 a t 1 and s 2 a t 2 , (s 1 , s 2 ) a -→ (t 1 , t 2 ) when- ever s 1 a -→ t 1 and s 2 a -→ t 2 .
The difference between the two compositions is illustrated in Fig. 13. The figure shows two MTS and their MTS composition; for their NAA composition, Tran(s, t) = {(a, (s 1 , t 1 ))}, {(a, (s 1 , t 1 )), (a, (s 1 , t 2 ))}, {(a, (s 1 , t 1 )), (a, (s 2 , t 1 ))}, {(a, (s 1 , t 1 )), (a, (s 1 , t 2 )), (a, (s 2 , t 1 )), (a, (s 2 , t 2 ))} . [START_REF] Beneš | Parametric modal transition systems[END_REF] The NAA translation of their MTS composition has eight transition constraints instead of four; note how the four constraints in [START_REF] Beneš | Parametric modal transition systems[END_REF] precisely correspond to the four implementation choices for s 0 and t 0 . It can easily be shown that generally, NAA composition is a refinement of MTS composition. The following lemma shows a stronger relationship, namely that the MTS composition is a conservative approximation of the NAA composition.

Lemma 25. Let M 1 , M 2 , M 3 be MTS and let M and A be the MTS and NAA composition, respectively. It holds that

M 1 M M 2 ≤ m M 3 iff M 1 A M 2 ≤ m M 3 . Proof. Let M i = (S 0 i , {s 0 i }, i , -→ i ) be MTS for i = 1, 2, 3.
In the following, we use the notation s 1 A s 2 to denote the states (s 1 , s 2 ) of M 1 A M 2 and similarly for M .

For a MTS translated into NAA, the Tran sets have a special structure, namely that for all states s, Tran(s) always has a maximal element {(a, t) | s a t} and a minimal element {(a, t) | s a -→ t} (with respect to set inclusion; cf. Lemma 14 for the similar property for DMTS). Furthermore, we note that Tran(s 1 A s 2 ) ⊆ Tran(s 1 M s 2 ) and, moreover, Tran(s 1 A s 2 ) also has a minimal and a maximal element and these elements correspond to the minimal and maximal element of Tran(s 1 M s 2 ).

The fact that M 1 A M 2 ≤ m M 1 M M 2 follows from the observation about the inclusion relation between Tran sets directly. This proves the 'only-if' part of the lemma.

To prove the 'if' part of the lemma, we let

R = {(s 1 M s 2 , s 3 ) | s 1 A s 2 ≤ m s 3 } and show that it is a modal refinement relation witnessing M 1 M M 2 ≤ m M 3 . Let (s 1 M s 2 , s 3 ) ∈ R. • Let s 1 M s 2 a t 1 M t 2 .
Then (a, t 1 M t 2 ) belongs to the maximal element of Tran(s 1 M s 2 ), which is also in Tran(s 1 A s 2 ). Due to s 1 A s 2 ≤ m s 3 we have some N ∈ Tran(s 3 ) with (a, t 3 ) ∈ N such that t 1 A t 2 ≤ m t 3 . Thus s 3 a t 3 and (t 1 M t 2 , t 3 ) ∈ R.

• Let s 3 a -→ t 3 . Then all elements of Tran(s 3 ) contain (a, t 3 ). If we now chose the minimal element M ∈ Tran(s 1 A s 2 ) then it has to contain (a, t 1 A t 2 ) such that (t 1 A t 2 ≤ m t 3 ). This means that s 1 M s 2 a -→ t 1 and (t 1 M t 2 , t 3 ) ∈ R.

Quotient

The quotient operator for a specification theory is used to synthesise specifications for components of a 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 I 1 I 2 ∈ S . (7)
Furthermore, S/S 1 is to be as permissive as possible.

Quotient for MTS

Before we describe the general construction of the quotient, we start with a simpler construction that works for the important special case of MTS. However, MTS are not closed under quotient, cf. [34, Thm. 5.5]; we show that the quotient of two MTS will generally be a DMTS.

Recall that MTS have only one initial state and all their must transitions are singletons. Let M 1 = (S 1 , s 0 1 , 1 , -→ 1 ) and M 2 = (S 2 , s 0 2 , 2 , -→ 2 ) be MTS. We define M 1 /M 2 = (S, s 0 , , -→) with S = 2 S1×S2 , s 0 = {(s 0 1 , s 0 2 )}, and the transition relations given as follows.

We first define ∅ a ∅ for all a ∈ Σ. There are no must transitions from ∅.

For s = {(s 1 1 , s 1 2 ), . . . , (s n 1 , s n 2 )} ∈ S we say that a ∈ Σ is permissible from s if for all i = 1, . . . , n either s i For a permissible from s and i ∈ {1, . . . , n}, let {t i,1 2 , . . . , t i,mi

2 } = {t 2 ∈ S 2 | s 2
a t 2 } be an enumeration of the possible states in S 2 after an a-transition.

We then define pt a (s) = {(t i,j 1 , t i,j 2 ) | i = 1, . . . , n, j = 1, . . . , m i } ∀i : ∀j :

s i 1 a t i,j 1
) . The transitions of s are now given as follows: for every a permissible from s and every t ∈ pt a (s), let s a t. Furthermore, for every s

i 1 a -→ t 1 let s -→ {(a, M ) ∈ {a} × pt a (s) | ∃t 2 : (t 1 , t 2 ) ∈ M, s i 2 a -→ t 2 }.
Recall from Lemma 25 that the MTS composition is a conservative approximation to the NAA compositions. This means that the following theorem holds regardless of which of the two compositions is used.

Theorem 26. For all MTS specifications M 1 , M 2 and M 3 , M 1 M 2 ≤ m M 3 iff M 2 ≤ m M 3 /M 1 .
Proof. In this proof only, let denote MTS composition.

Write M i = (S i , s 0 i , i , -→ i ) for i = 1, 2, 3. We use the following notation to help distinguish states of M 1 M 2 and M 3 /M 1 . The states of M 1 M 2 are denoted by s 1 s 2 instead of (s 1 , s 2 ) while the states of M 3 /M 1 are denoted by {s 3 /s 1 , . . .} instead of {(s 3 , s 1 ), . . .}. We also note that for states of M 3 /M 1 , s ⊇ t implies s ≤ m t due to the construction. Now assume that M 2 ≤ m M 3 /M 1 and let R = {(s 1 s 2 , s 3 ) | s 2 ≤ m {s 3 /s 1 }}. We show that R is a witness for M 1 M 2 ≤ m M 3 , i.e. that it satisfies the conditions of Definition 2. Let (s 1 s 2 , s 3 ) ∈ R.

• Let s 1 s 2 a t 1 t 2 . As s 2 ≤ m {s 3 /s 1 } this means that {s 3 /s 1 } a {t 1 3 /t 1 1 , . . . , t k 3 /t k 1 } = t and t 2 ≤ m t. Due to the construction of {s 3 /s 1 }, we know that there is an index j for which t j 1 = t 1 and s 3 a t j 3 . Let t 3 = t j 3 . As t ⊇ {t 3 /t 1 }, x ≤ m {s /t }. Therefore, (t 1 t 2 , t 3 ) ∈ R.

• Let s 3 a -→ t 3 . This means that {s 3 /s 1 } -→ U . As s 2 ≤ m {s 3 /s 1 }, we know that s 2 a -→ t 2 and t 2 ≤ m u for some (a, u) ∈ U . Due to the construction of U we know that there exists t 3 /t 1 ∈ u. Again, as

u ⊇ {t 3 /t 1 }, t 2 ≤ m {t 3 /t 1 }. Therefore, (t 1 t 2 , t 3 ) ∈ R.
Assume, for the other direction of the proof, that • Let s -→ U and let s i Heathrow airport. Besides, MTS classes are advocated as an appropriate base for interface theories by Raclet et al. in [START_REF] Raclet | Why are modalities good for interface theories?[END_REF] and for product line theories in Nyman's [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 by Uchitel and Chechik in [START_REF] Uchitel | Merging partial behavioural models[END_REF] and methods for supervisory control of MTS shown by Darondeau et al. 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] Børjesson | Generality in design and compositional verification using TAV[END_REF][START_REF] Nicolás | MTSA: Eclipse support for modal transition systems construction, analysis and elaboration[END_REF][START_REF] Křetínský | MoTraS: A tool for modal transition systems and their extensions[END_REF].

M 1 M 2 ≤ m M 3 . Define R = {(s 2 , {s 1 3 /s 1 1 , . . . , s n 3 /s n 1 }) | ∀i = 1, . . . , n : s i t 0 t1 a t2 a • b • c s 0 s1 a s2 a • b s 0 /t 0 {s1/t1, s2/t2} a {s2/t1, s2/t2}
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] Kim | Equation solving using modal transition systems[END_REF], Fecher and Schmidt's 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 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]. Our results show that all these formalisms are at most as expressive as DMTS.

Larsen has shown in [START_REF] Kim | Modal specifications[END_REF] that any finite acyclic MTS is equivalent to a HML formula (without recursion or fixed points), the characteristic formula of the given MTS, cf. (3). 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. 4 Here we extend these results to ν-calculus formulae, and show that any such formula is equivalent to a DMTS, solving a problem left open in [START_REF] Kim | Equation solving using modal transition systems[END_REF]. Hence the modal ν-calculus supports full compositionality and decomposition in the sense of [START_REF] Kim | 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] Kim | Modal specifications[END_REF][START_REF] Kim | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF]. Recently, the graphical representability of a variant of alternating simulation called covariant-contravariant simulation has been studied in [START_REF] Aceto | On the specification of modal systems: A comparison of three frameworks[END_REF].

Quotients are related to decomposition of processes and properties, an issue which has received considerable attention through the years. In [START_REF] Kim | 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] Kim | 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 ν-calculus property Q. 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. Other extensions use infinite conjunctions [START_REF] Fokkink | Compositionality of Hennessy-Milner logic by structural operational semantics[END_REF], probabilistic processes [START_REF] Gebler | Compositionality of probabilistic Hennessy-Milner logic through structural operational semantics[END_REF] or processes with continuous time and space [START_REF] Cardelli | Modular Markovian logic[END_REF].

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[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 these logics, & and 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 ν-calculus, 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. To the best of our knowledge, there are no other such reductions of quotient for the synchronisation type of composition in the context of specifications.

Conclusion

In this paper we have introduced a general specification framework whose basis consists of four different but equally expressive formalisms: one of a graphical behavioural kind (DMTS), one logic-based (ν-calculus) and two intermediate languages between the former two (NAA and hybrid modal logic). We have shown their structural equivalence.

The established connection implies several consequences. On the one hand, it allows for a graphical representation of ν-calculus. Further, composition on DMTS can be transferred to the modal ν-calculus, hence turning it into a modal process algebra. On the other hand, such a correspondence identifies a class of modal transition systems with a natural expressive power and provides another justification of this formalism. Further, this class is closed under both conjunction and disjunction, a requirement raised by component-based design methods. However, it is not closed under complement and difference. 5 Nevertheless, since DMTS are closed under conjunction, disjunction and composition, we still have a positive Boolean process algebra.

Altogether, we have shown that the framework possesses a rich algebraic structure that includes logical (conjunction, disjunction) and behavioural operations (parallel composition and quotient) and forms a complete specification theory in the sense of [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF][START_REF] Kim | Ideal specification formalism = expressivity + compositionality + decidability + testability +[END_REF].

Moreover, the construction of the quotient solves an open problem in the area of MTS. All attempts to find the quotient for variants of MTS so far have been limited to the much simpler deterministic case [START_REF] Raclet | Residual for component specifications[END_REF]. Here we have given the first solution to the quotient on nondeterministic MTS: firstly a solution to the general case of nondeterministic DMTS and, secondly, an exponentially better algorithm for nondeterministic MTS. Due to the established correspondence, the quotient can be applied also to ν-calculus formulae. 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.

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. Further, we plan to implement the operations detailed here within the graphical tool MoTraS [START_REF] Křetínský | MoTraS: A tool for modal transition systems and their extensions[END_REF].

Figure 1 :Figure 2 :

 12 Figure 1: DMTS corresponding to the CTL property AG(req ⇒ AX(work AW grant))

Figure 4 :

 4 Figure 4: ν-calculus formula and DMTS for the ("weak until") property "there is always an 'a' transition available, until a 'b' transition becomes enabled", over the alphabet Σ = {a, b, c}

Figure 5 :

 5 Figure 5: Six translations between specification formalisms

Figure 6 :

 6 Figure 6: ν-calculus expression in normal form and its DMTS translation, cf. Example 2. The state corresponding to ff is inconsistent and not shown

Theorem 10 .

 10 For any LTS I and any ν-calculus expression N in normal form, I |= N iff I ≤ m N . Proof. We show that I ≤ m D iff I |= dn(D) for any DMTS D; the claim then follows because I ≤ m N iff I ≤ m nd(N ) iff I |= dn(nd(N )) = N .

1 a-→ 1 t or s 0 2 a-→ 2 t. Lemma 17 .

 1217 If D = (S, {s 0 }, , -→) is a DMTS with a single initial state and I 1 , I 2 ∈ D , then also I 1 + I 2 ∈ D .

2 bFigure 8 :

 28 Figure 8: DMTS D with two initial states and its two implementations I 1 , I 2

Figure 10 :

 10 Figure 10: Implementation state space illustrating the proof of Theorem 22

Figure 11 :

 11 Figure 11: The nondeterministic sum of I k and I l , unfolded

Figure 12 :

 12 Figure 12: Two DMTS and the reachable parts of the DMTS translation of their composition.Here, s = {(a, (t 1 , t 2 )), (a, (t 1 , u 2 ))}, t = {(a, (t 1 , t 2 ))} and u = ∅

Theorem 24 .

 24 For all specifications 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 . Proof. Let S 1 ≤ m S 3 and S 2 ≤ m S 4 , then S 1 ∨ S 3 ≡ m S 3 and S 2 ∨ S 4 ≡ m S 4 . By distributivity, S 3 S 4 ≡ m (S 1 ∨ S 3 ) (S 2 ∨ S 4 ) ≡ m S 1 S 2 ∨ S 1 S 3 ∨ S 3 S 2 ∨ S 3 S 4 , thus S 1 S 2 ∨ S 1 S 3 ∨ S 3 S 2 ≤ m S 3 S 4 . But S 1 S 2 ≤ m S 1 S 2 ∨ S 1 S 3 ∨ S 3 S 2 , finishing the argument. Example 3. An example of composition is shown in Fig. 12. Here the DMTS translation of D 1 D 2 has two initial states; it can be shown that no DMTS with a single initial state is thoroughly equivalent.

1 a or s i 2 a

 12 .

Figure 14 :

 14 Figure 14: Two nondeterministic MTS and their quotient

  s 1 ) by construction. Hence we have M 2 ∈ Tran 2 (s 2 ) satisfying the conditions in the definition of NAA refinement. By construction of Tran 2

  1 , t 2 )), (a, (t 1 , u 2 ))}, t = {(a, (t 1 , t 2 ))} and u = ∅

						s 1 , t 1
	a	s 1	a	t 1	a	s 1 , t 2
	s 0	t 0		s 0 , t 0	a
	a	s 2	a	t 2	a a	s 2 , t 1
						s 2 , t 2
	Figure 13: Two MTS and their MTS composition according to [33]

Note that this normal form is different from the one introduced in[START_REF] Beneš | Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory[END_REF]. The original normal form did not allow for modal refinement and was less apt for the ν-calculus to DMTS translation.

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

We wish to thank Ilya Bogdanov for discussions on this subject[START_REF]Covering of a partial order by upwards convex sets[END_REF].

a t i,j 3 with t i,j 1 t 2 ≤ m t i,j 3 . We fix these t i,j 3 . Let t = {t i,j 3 /t i,j 1 | i ∈ {1, . . . , n}, j ∈ {1, . . . , m i }}. Clearly, s a t and (t 2 , t) ∈ R.

A HML formula is prime if implying a disjunction means implying one of the alternatives.

Previous results on difference[START_REF] Sassolas | Exploring inconsistencies between modal transition systems[END_REF] are incorrect due to a mistake in[START_REF] Fischbein | On correct and complete strong merging of partial behaviour models[END_REF] on conjunction of MTS, see[31, p. 36].

Acknowledgement. The authors are indebted to several anonymous reviewers who provided very useful comments and suggestions, in particular regarding related work.

Example 4. We illustrate the construction on an example. Let S and T be the MTS in the left part of Fig. 14. 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

Since there is a must-transition from s 0 (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 0 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.

Quotient for NAA

We now introduce the general quotient operator for NAA. The construction is similar to the previous one, with the notions of permissibility and pt a (s) adapted to the more general setting.

Let

, and Tran given as follows:

Let

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 ) : (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 ).

Proof. We show the proof for NAA. Let

We assume that the elements of Tran 1 (s 1 ) are pairwise disjoint for each s 1 ∈ S 1 ; this can be achieved by, if necessary, splitting states.

We also use the notation introduced in the proof of Theorem 26, i.e. s 1 s 2 instead of (s 1 , s 2 ) when speaking about states of A 1 A 2 and {s 3 /s 1 , . . .} instead of {(s 3 , s 1 ), . . .} when speaking about states of A 3 /A 1 . We further note that by construction, s ⊇ t implies s ≤ m t for all s, t ∈ 2 S3×S1 . Now assume that

) and M 2 ∈ Tran 2 (s 2 ). As s 2 ≤ m {s 3 /s 1 }, we can pair M 2 with an M / ∈ Tran / ({s 3 /s 1 }), i.e. such that the conditions in (2) are satisfied (see Definition 7).

Let M 3 = M / M 1 . We show that (2) holds for the pair M , M 3 : Assume, for the other direction of the proof, that

) such that (2) holds for the pair M i,j , M i,j 3 .

Now define

We need to show that M ∈ Tran / (s).

Let i ∈ {1, . . . , n} and M i,j 1 ∈ Tran 1 (s i 1 ); we claim that M M i,j 1 and M i,j 3 are related as in [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF]. Let (a, t 3 ) ∈ M M i,j 1 , then t 3 /t 1 ∈ t, (a, t 1 ) ∈ M i,j 1 and (a, t) ∈ M . By disjointness, j = δ i (a, t 1 ), hence by definition of M , (a, t 3 ) ∈ M i,j 3 as was to be shown.

For the reverse inclusion, let (a, t 3 ) ∈ M i,j 3 . By [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] and definition of M i,j , there are (a, t 1 ) ∈ M i,j 1 and (a, t 2 ) ∈ M 2 for which t 1 t 2 ≤ m t 3 . Thus j = δ i (a, t 1 ), so that there must be (a, t) ∈ M for which t 3 /t 1 ∈ t, but then also (a, t 3 ) ∈ M M i,j

1 . We show that M 2 and M are related as in [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF].

• Let (a, t 2 ) ∈ M 2 . For every i = 1, . . . , n, M 1 ∈ Tran 1 (t i 1 ) and (a, t 1 ) ∈ M , we can use [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] to choose an element (a, τ i (a, t 1 )) ∈ M i,δi(a,t1) 3 for which

• Let (a, t) ∈ M , then we have (a, t 2 ) ∈ M 2 satisfying the conditions in [START_REF] Beneš | Process algebra for modal transition systemses[END_REF].

Hence t 1 t 2 ≤ m t 3 for all t 3 /t 1 ∈ t, so that (t 2 , t) ∈ R.

As a corollary, we get (7): If I 2 ∈ S/S 1 , i.e. I 2 ≤ m S/S 1 , then S 1 I 2 ≤ m S, which using I 1 ≤ m S 1 and Theorem 24 implies I 1 I 2 ≤ m S 1 I 2 ≤ m S. The reverse implication in Theorem 27 implies that S/S 1 is as permissive as possible.

Corollary 28. With operations ∧, ∨, and /, each of our four classes of specifications forms a commutative residuated lattice up to ≡ m .

Proof. We have already seen in Corollary 21 that the class of NAA forms a lattice, up to ≡ m , under ∧ and ∨, and by Theorem 27, / is the residual, up to ≡ m , of . All other properties (such as distributivity of over ∨ or N ⊥ ≡ m ⊥) follow.

Related Work

The modal ν-calculus is equivalent to the Hennessy-Milner logic with greatest fixed points, which arises from Hennessy-Milner logic (HML) [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF] by introducing variables and greatest fixed points. If also least fixed points are allowed, one arrives at the full modal µ-calculus [START_REF] Kozen | Results on the propositional µ-calculus[END_REF][START_REF] Vaughan | A decidable mu-calculus: Preliminary report[END_REF][START_REF] Scott | A theory of programs[END_REF]. Janin and Walukiewicz have in [START_REF] Janin | Automata for the modal mu-calculus and related results[END_REF] introduced an automata-like representation for the modal µ-calculus which seems related to our NAA.

DMTS have been proposed as solutions to algebraic process equations in Larsen and Xinxin's [START_REF] Kim | 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] Kim | 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 with Bruns' [START_REF] Bruns | An industrial application of modal process logic[END_REF] where MTS have been used for an air-traffic system at