Hongyang Qu

Chris Chilton

Marco Autili

Taolue Chen

Tingting Han

Paola Luk Áš Holík

Bengt Inverardi

Marta Jonsson

Marco Kwiatkowska

Hongyang Martinucci

Massimo Tivoli Qu

Reviewer

Val Érie Issarny

Ilaria Matteucci

Bernhard Steffen Connect

Keywords: Specification theory, conjunction, quotient, synthesis, assume-guarantee, data, quantitative verification, functional and non-functional requirements

In this deliverable we document the progress of WP2 during the third year of the CONNECT project.

We supply details of a compositional specification theory we have been working on for modelling connectors and components. This supports the operations of parallel composition, for examining the structural behaviour of networked systems, logical conjunction, for supporting independent development of components, and quotient for incremental development in the form of component/connector synthesis. Our framework, a portion of which is conceptually similar to interface automata, is unique in that we've provided the first definition of quotient that can act on components exhibiting non-determinism, as well as the first definition of conjunction on this flavour of model. A refinement preorder corresponding to safe-substitutivity allows for the seamless interchanging of components and connectors without violating environmental assumptions. Our formulation of refinement also ensures that the framework enjoys strong algebraic properties. These are necessary for reasoning about components and connectors in a compositional manner. Suitability of our specification theory is demonstrated by linking synthesis in WP3 with the quotienting operation in WP2. The technique relies on formulating a specification that does not allow communication mismatches to occur, and that also ensures the components to be connected make progress without deadlocking inopportunely. Such a mediator must also satisfy the constraints imposed by the system-wide ontology (i.e., ordering of actions and equivalence of actions). We demonstrate how this works in practice through a couple of examples.

An extension of the specification theory has also been documented in which synchronisation of actions facilitates the communication of data. The models of this framework are a cross between the Logic IOLTSs of our specification theory, and the register automata used by WP4. As for the original specification theory, this extended formalism supports parallel composition, conjunction and quotient. Through a number of examples, we demonstrate how the theory can be used for synthesising mediators of systems to be connected.

Quantitative assume-guarantee verification is also presented. The key achievement in the probabilistic setting is a complete assume-guarantee technique that can generate probabilistic assumptions automatically by a new L*-style learning method. This will be exploited as part of a future extended specification theory capable of handling probabilistic behaviour and non-functional properties.

The CONNECT project aims to develop a novel network infrastructure to allow heterogeneous networked systems to freely communicate with each other via on-the-fly synthesis of emergent connectors. The role of Work Package 2 (WP2) is to investigate the foundations and verification methods for composable connectors, so that support is provided for composition of networked systems, whilst enabling automated learning, reasoning and synthesis. This document provides an overview of the work undertaken by WP2 in the third year. The work is organised into two streams, (i) compositional theory of connector behaviours and (ii) compositional assume-guarantee verification for probabilistic automata, with the view to integrate these together.

For (i), we have formulated a specification theory for modelling components and connectors. The framework admits a substitutive refinement preorder, and provides the operations of parallel composition, for examining the structural behaviour of systems, conjunction (or shared refinement), for independent development, and quotient to synthesise components, for supporting incremental development. An extension with data has been provided for this specification theory. Integration with synthesis in WP3 is demonstrated by linking the algorithmic approach to connector synthesis developed in that work package with the quotient operator of the specification theory.

For (ii), we continued our work on assume-guarantee verification for probabilistic automata, extending the multi-objective approach to allow probabilistic liveness and expectations, which will be integrated with the quantitative specification theory over the course of the next year.

This deliverable addresses part of the issues concerning the work within Task 2.3, as described in the Description of Work (DoW). These issues are related to the definition of techniques for interoperability checking and protocol matching even in the presence of non-functional properties. Since Task 2.3 will end with the project, the rest of the work in Task 2.3 is left as future work. We recall that this work concerns the use of negotiation for achieving interoperability while still satisfying specified QoS properties and the evaluation of the related offline and online verification techniques.

In this chapter, we first recall the role of WP2 in the project (Section 1.1), and then address the review recommendations (Section 1.2). Next, we explain the research challenges and achievements of the third year (Section 1.3), before providing an outline structure of the deliverable (Section 1.4).

The role of work package WP2

The role of WP2 is to investigate the foundations and verification methods for composable connectors, so that support is provided for composition of networked systems, whilst enabling automated learning, reasoning and synthesis. The expected outcomes are formalisms, methods and software tools that can be used for the specification, design and development of connectors, allowing for both functional and non-functional properties to be expressed and verified. WP2 thus provides the theoretical underpinning for the work carried out in the other workpackages, in the sense that connectors specified in WP2 can be instantiated in WP3 (synthesis), WP4 (learning) and WP5 (dependability analysis).

The remit of WP2 is to develop compositional specification and verification techniques into a situation where they can be successfully applied to the modelling and reasoning of connector behaviours in a compositional manner. To achieve this goal, WP2 is structured into the four tasks:

• Task 2.1. Capturing functional and non-functional connector behaviours. This task aims to guide the project by formalising the notions of connector and component, characterising the types of interaction and identifying a verification approach, capable of capturing non-functional properties.

• Task 2.2. Compositional connector operators. The main thrust here is to formulate a compositional modelling and reasoning framework for components and connectors.

• Task 2.3. Rephrasing interoperability in terms of connector behaviours. The aim is to formulate techniques for interoperability checking, in the presence of dynamic behaviours and non-functional properties.

CONNECT 231167

• Task 2.4. Reasoning toolset. The focus here is on a quantitative verification framework for connectors and components, capable of handling dynamic scenarios and non-functional properties, which includes algorithms and prototype implementations.

We have organised the work into two parallel streams, respectively aimed at formulating (i) a compositional theory of connector behaviours, and (ii) compositional assume-guarantee verification for probabilistic automata. Such an approach facilitates progress across the full breadth of the tasks, while at the same time delivering reasoning methods and tools that are directly relevant to other workpackages, which rely on automata-like formalisms. The goal is to integrate the two streams together, which we are now beginning to do.

Work stream (i) is aimed at formulating a comprehensive framework for modelling, specifying, composing and reasoning about connector behaviours. The CONNECT consortium has selected a variant of interface automata as the underlying (stateful) model for interactive behaviours, which we refer to as Logic IOLTSs. A purely abstract specification notation consisting of traces is also provided, which is a stepping-stone to defining the substitutive trace-based refinement preorder. Our deviations from interface automata are motivated by the goal to provide a general theory with a range of operations, which can also support extensions with non-functional properties, and liveness. For each of the defined operators (parallel, conjunction, and quotient) we demonstrate congruence-like compositionality results, in addition to compositionality results linking the operational models to the abstract trace-based models. For maximum flexibility, we are concentrating on modelling arbitrary component behaviours, where connectors correspond to particular subclasses. To capture non-functional properties, we must generalise the theory to allow for quantitative behaviours. Such an extension will be coupled with the assume-guarantee framework for performing compositional verification.

For work stream (ii), we settled on probabilistic model checking as a means to formally analyze non-functional properties. In the deliverable D5.2 [START_REF]CONNECT Deliverable D5.2: Design of Approaches for dependability and initial prototypes[END_REF], we have demonstrated an application of these techniques to a CONNECT scenario. To support independent development of connectors, we are developing compositional assume-guarantee verification for probabilistic automata, which can support a range of non-functional properties. Compositional verification works by breaking a verification problem down into manageable sub-tasks, based on the structure of the system being analysed. In the assumeguarantee paradigm, in which properties (guarantees) of individual system components are verified under assumptions about their environment, desired properties of the combined system are then obtained by combining separate verification results using proof rules. We have adopted a compositional assumeguarantee framework for probabilistic automata based on the multi-objective approach. A broad range of non-functional properties can be expressed and verified in this framework.

The integration of the two streams will be achieved through integrating probabilistic automata and Logic IOLTSs, combined with an enhancement of the specification theory with assume-guarantee reasoning proof rules.

Review recommendations

• The relation between the calculus developed in WP2 and the synthesis work in WP3 is unclear.

We can use the theory of WP2 to prove technical results about the CONNECTors generated by WP3.

The framework proposed in WP2 supports modelling and reasoning about complex systems of components that interact with one another, whereas the work of WP3 is focused on generating actual mediators on-the-fly to support interoperability of networked systems. In WP2 we have used a directed model of communication, in which each interaction is under the control of one component, thus distinguishing fundamentally between input and output. This model is suitable for modelling asynchronous communication in distributed systems. WP3, on the other hand, has utilised a concurrent model whereby all components handshake on communications. Such an assumption simplifies, although certainly does not trivialise, the problem of generating mediators on-the-fly.

Although the frameworks of WP2 and WP3 have different communication semantics, the models used by WP3 can be ported across to the WP2 framework by explicitly representing the handshaking. In Chapter 3 of this deliverable, we demonstrate a mapping from components modelled as LTSs CONNECT 231167 of WP3 (see Chapter 3 of [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF]) to semantically equivalent models in the WP2 notation. As part of our work in WP2, we develop a quotienting operator for synthesising mediators of systems, where the systems can exhibit non-determinism. We prove that our mediators are free from communication mismatches, and moreover make progress so that the mediator guarantees meaningful communication takes place. Our synthesised mediator is also the most general. Through this, we can relate the models of WP3 to the technical results we have derived in WP2. As a result, we can show whether a mediator synthesised à la WP3 is the most general mediator, and check whether it is free from errors by using the theory built up in WP2. Thus in this deliverable, we demonstrate how the theory of WP2 can be used for justifying the practical aspects of WP3 concerned with mediator synthesis.

• It is unclear how the compositionality addressed in WP2 fits with the compositionality potentially needed for connector synthesis.

We have introduced a quotienting operation in the specification theory, for linking the inherent compositionality results of WP2 (stated in Chapter 2) to the synthesis of mediators in WP3. Through assume-guarantee reasoning, we will infer properties of synthesised mediators from the properties of the components to be mediated; this is, to some extent, what we mean by compositionality. Utilising such compositional properties relies on the semantic preserving mapping we introduce between models of WPs 2 and 3 (see Chapter 3).

From another perspective, the intention of WP2 is to develop a notation for modelling and reasoning about component and connector behaviours. It is therefore likely to have features and functionality that lie outside the main workflow of WPs 3-5.

• Choice of a theory in WP2 should be guided by its usefulness for CONNECT.

The specification theory is centred on the notion of components/connectors with operations on components to support composition, as well as independent (conjunction) and incremental (quotient) development. In Chapter 3, we have demonstrated the applicability of our theory to synthesis in WP3. An extension with data in Chapter 4 supports modelling in both WPs 3 and 4. The eventual probabilistic extension of the specification theory will link closely to modelling in WP5. Consequently, the theory is well-suited to the project's needs.

• Weakness of the algebra.

As part of our work in D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF], we tried to show that a basic collection of primitive connectors can be built up into complex connectors that cover the class of mediators. However, our work proved not to be so fruitful on this front, as in particular it was difficult to prevent the constructed mediator from generating communication mismatches. However, our preliminary findings of the algebra have led us to a greater understanding of how we can use such a collection of primitives, in the form of building ontological constraints.

In Chapter 3, we introduce a quotienting operator that can be used to generate abstract mediators in the notation of our specification theory. The purpose of the mediator is to allow communication between the supplied components that is free of communication mismatches and guarantees that suitable progress is made (i.e. the system does not deadlock prematurely). We achieve this by building a special component that captures the constraints imposed by the system ontology, which relates actions of components and may impose ordering constraints on actions. Although we have not elaborated on it in this deliverable, these ontological constraints can be built as the parallel composition of the algebraic primitives we introduced in D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF], treating them as observers (that is, all actions are inputs). It is then the responsibility of the quotienting operator to guarantee that the mediator will not generate any communication mismatches.

Thus in D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF] we adopted an approach where the algebra was used to specify and build mediators, whereas we have shifted direction now to the extent that primitives of the algebra are used for building constraints on what the mediator must do, while the quotient operator takes care of the actual synthesis.

Another comment by the reviewers concerned the fact that the underlying model of our algebra, namely interface automata, was weak in that it did not permit non-determinism or hidden actions. These restrictions were imposed at the time because the known definition of quotient, as given CONNECT 231167

in [START_REF] Bhaduri | Interface synthesis and protocol conversion[END_REF], could only be applied to deterministic systems. Our new specification theory relaxes these constraints, which has been made possible by devising a quotient operator that can be applied to non-deterministic systems.

• Develop stronger AG rules for probabilistic reasoning.

In the third year, we focused on completeness of assume-guarantee reasoning for probabilistic systems. The AG rules for reasoning about safety and liveness properties in D2.1 [START_REF]CONNECT Deliverable D2.1: Capturing functional and non-functional connector behaviours[END_REF] and D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF] are incomplete, as it is not always possible to find assumptions to apply those AG rules to reason about probabilistic systems. In this deliverable, we proposed a complete compositional reasoning technique by modelling assumptions as probabilistic finite automata (PFAs). Furthermore, PFAs assumptions can be automatically constructed in a similar fashion to the learning technique described in D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF].

Challenges and achievements for Year 3

The key challenge for Year 3 has been to develop a compositional theory for modelling and reasoning about components, whilst ensuring that it is fully integrated and usable by the remainder of the project. Despite being a non-trivial objective, we have developed a specification theory that aligns well with work packages 3, 4, and 5. Concerning the alignment with WP3, we have demonstrated through Chapter 3 a clean semantic preserving mapping between our theory in WP2 and the notation of extended LTSs used as part of synthesis in WP3 [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF]. Concerning alignment with WP4, we have developed an extension of our specification theory with data in Chapter 4: the process model defined there has the same form as the register automata defined in Deliverable 4.3 [START_REF]CONNECT Deliverable D4.3: Deployment of learning techniques[END_REF]. The differences are that for learning, register automata should be deterministic, and that inputs and outputs do not play the same roles in learning. The link with WP5 [START_REF]CONNECT Deliverable D5.3: Consolidated dependability framework. FET IP CONNECT EU project, FP7 grant agreement[END_REF] will come to fruition in the fourth year, when we produce a quantitative extension of our specification theory. One of the main achievements of WP2 for Year 3 is the formalization of a component, and connector, specification theory. The theory is described in Chapter 2. It allows us to rephrase interoperability between heterogeneous protocols in terms of connector behaviours, hence providing a solution to issues related to Task 2.3. A suitable interoperability notion has been defined within the work of WP3. In particular, by referring to Deliverable D3.3 [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF], with interoperability, we mean the ability of protocols to correctly communicate and coordinate, i.e., to correctly synchronize. In other words, two systems successfully interoperate if they correctly exchange compatible conversations or compatible traces. We focus on protocols that can potentially interoperate despite showing some differences. That is, communication and coordination between such protocols is possible in principle since they are semantically equivalent and complementary, but cannot be achieved seamlessly because of heterogeneity or diversities. Synchronization between protocols, thus, can be achieved under mediation, i.e., through a mediator that while managing mismatches, allows protocols to effectively exchange compatible traces (sequences of actions). A mediator is then a protocol that allows communication and coordination among compatible protocols by mediating their differences. Therefore, such a mediator serves as the locus where semantically equivalent and complementary actions are correctly synchronized thus enabling a mediated interoperability among protocols. Semantic equivalence of (heterogeneous) actions is managed by the use of ontologies.

With this notion of mediated interoperability in mind, our specification theory provides a declarative notation for describing components and connectors by means of trace sets, and its related operational semantics in terms of transition systems. The theory is equipped with both a suitable refinement relation hence allowing for safe replacing of components/connectors and composition operators for the construction of composite components/connectors out of smaller ones. Furthermore, a suitable quotient operator is defined hence supporting incremental development. Our specification theory also allows to represent specific ontology abstractions as "observers" (which are simply just components), so that ontology abstractions can be taken into account for connector synthesis purposes.

As it is detailed in Chapter 3, the quotient operator is particularly important in order to characterize the connector synthesis problem faced by WP3 as a quotient problem, hence showing, within the work of WP2, how we can use our theory for synthesizing connectors that act as component mediators. By reasoning in terms of quotient, we state correctness properties of the mediator synthesis such as soundness CONNECT 231167 and generality of the synthesized mediators, i.e., a synthesized mediator does not introduce inconsistent behavior, and any other equivalent mediator is a refinement of the synthesized one, respectively.

As described in Chapter 3, and in particular in Section 3.8, the mediator synthesis approach developed within WP3 fits within the theory formalized in this deliverable. In Section 3.8, we show that there exists a mapping between the theory of mediators described in [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF] and our specification theory. This allows us to state correctness of the WP3 mediator synthesis as inherited, under the described mapping, by the soundness and generality properties stated for mediators which are synthesized by means of quotient in our specification theory. Furthermore, we recall that the WP3 mediator theory uses ontologies for checking semantic equivalence among heterogenous sequences of actions during the mediator synthesis process. This is similar to our quotient procedure, that makes use of ontology abstractions. It is worthwhile to mention that such ontology abstractions can be represented as a composition of terms from the connector algebra defined in Deliverable D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF], under minor technical changes to the algebra that we avoid explicitly discussing here since they are not crucial for the purposes of this deliverable. For instance, in the example described in Section 3.6, a specific part of the ontology description could be given as a Plug "observer" connector of two Trans primitives by using the algebra notation. This means that, within the specification theory formalized in this deliverable, we can use the connector algebra (representing one of the main outcomes of WP2 during Year 2) to express the kind of ontological constraints that are needed to enable automated mediator synthesis.

A further link between WPs 2, 3, and 4, is established by the data-extension of our specification theory, described in Chapter 4. This extension links with the work on register automata (see Deliverable 4.3 [START_REF]CONNECT Deliverable D4.3: Deployment of learning techniques[END_REF]), in that register automata can be seen as a restricted form of processes with data. The extension also links with the work on synthesis in WP3, in that it allows to take constraints on data into account. Adding data constraints to the synthesis problem can in some cases provide an alternative to the use of ontologies for the purpose of matching actions between components: we illustrate this point by a couple of examples in Chapter 4.

Summing up, the specification theory that we describe in this deliverable, beyond providing a solution to issues related to Task 2.3, i.e., rephrasing interoperability in terms of connector behaviours, allows us to explicitly show the relationships between some previous work of WP2 (i.e., the connector algebra), current work of WP2 (i.e., a compositional specification theory for components and connectors suitable for automated mediator synthesis), and current work of WP3 (i.e., revised implementation of the mediator theory and related synthesis method). That is, the specification theory described in this deliverable allows us to address also the following reviewer comments from the second review: (i) "The relation between the calculus developed in WP2 based on interface automata targeted at verification and the synthesis work in WP3 is unclear." and (ii) "It is not obvious to the reviewers that this algebra can be exploited in WP3 which seems to be progressing well with the use of LTSs and does not seem to require this algebra."

Completeness is an important issue in compositional reasoning, which affects the usefulness of a compositional reasoning technique. A complete technique allows us to check the validity of a property by using this technique only. In this sense, the assume-guarantee rules presented in D2.1 [START_REF]CONNECT Deliverable D2.1: Capturing functional and non-functional connector behaviours[END_REF] and D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF] are incomplete. In Year 3, the key achievement in probabilistic compositional verification is a complete assume-guarantee technique, which can generate probabilistic assumptions automatically by a new L*style learning methods. In this technique, probabilistic assumptions are specified as probabilistic finite automata (PFAs), and hence our achievement includes a semi-algorithm for checking language inclusion for PFAs. Currently, this technique can only be applied to probabilistic systems represented by Discrete-Time Markov Chains (DTMCs). In addition to the complete reasoning technique, we also extended the learning technique in D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF] to generate assumptions for the AG rule (ASYM-N), which allows a system to be decomposed into more than two components, and investigate an alternative learning method NL* for automated assumption construction.

Outline

We begin by introducing our compositional specification theory in Chapter 2. Linking the specification theory to the work of synthesis in WP3 is elaborated on in Chapter 3, where we also demonstrate our specification theory on CONNECT-related examples. Chapter 4 details an extension of the specification theory with data. Chapter 5 presents work on the second strand of the work package that encompasses CONNECT 231167 developing probabilistic assume-guarantee reasoning techniques for probabilistic systems. Finally, we state the key conclusions of our work in Chapter 6 and also state the immediate tasks to be completed during the remainder of the project.

CONNECT 231167 18/86 2 Compositional specification theory for component behaviours

In this chapter we introduce a framework for modelling the behaviours of components. Based on our previous work, we choose not to distinguish CONNECTors from components. Chapter 3 shows how we can use our framework for synthesising CONNECTors that act as component mediators; thus that chapter will highlight the novel aspects of our work in terms of its application to CONNECTor synthesis. The work of this chapter is based predominantly on our recent paper accepted for publication at ESOP 2012 [START_REF] Chen | A Compositional Specification Theory for Component Behaviours[END_REF]. Our framework takes the form of a specification theory. We define an abstract (declarative) notation for describing components by means of trace sets, and provide an operational modelling notation in terms of transition systems. A refinement relation corresponding to substitutivity allows one to compare components, and unequivocally state when a component can be used safely in place of another. Operators of the specification theory allow for the construction of composite components out of smaller components.

Concerning the operators, we introduce parallel composition for examining how a number of components interact with one another. Conjunction, corresponding to shared refinement, allows for the combining of multiple component-specifications; it is essentially the greatest lower bound of refinement. Disjunction is defined as the least upper bound of refinement. Both conjunction and disjunction support independent development of components. Hiding can be used for abstraction, while renaming allows for the reuse of components in subtly different environments. The operator of quotient supports incremental development, by synthesising missing components given an overarching specification of the system.

Introduction

In our framework, components communicate by synchronising on input and output actions. A component comes equipped with an interface that specifies which actions it is willing to communicate on, as well as the type of the actions i.e., whether an action is an input or output in the component. Besides the interface, a component comes equipped with a behaviour that specifies the permitted temporal ordering of interactions between the component and its environment.

We do not insist that communication is handshaken. Therefore, we adopt synchronisation semantics in which outputs are non-blocking. If a component is willing to receive an input, this can only take place if the action is signalled by the environment. However, if a component wishes to emit an output, it can do so at its convenience, even if the environment is not willing to receive it (in which case an inconsistency would arise). This setting provides greater generality in modelling component-based systems, in comparison to the setting used by the CONNECT consortium in WPs 3-5. We note, however, that the set of allowable CONNECT-based systems is a sub-class of the connectors and components admitted by our framework.

An environment is said to be safe for a component, if any interaction between the component and environment does not permit the component to uncontrollably become inconsistent. In that respect, the environment must refuse to issue any input from which the component can encounter an inconsistency by a series of output actions. To support this principle in refinement, which corresponds to safe-substitutivity, we must allow a component to propagate its inconsistencies backwards over output actions. This is similar to the backward propagation of inconsistencies in parallel composition of interface automata, as defined by de Alfaro and Henzinger in [START_REF] Alfaro | Interface automata[END_REF]. Further detail on how this works in our setting will be elaborated in Section 2.2.1.

To highlight the novelty of our specification theory, we relate it to existing frameworks in the literature. Our models, in particular Logic IOLTSs, are inspired by the Logic LTS framework due to L üttgen and Vogler [START_REF] Nicola | Conjunction on processes: Full abstraction via ready-tree semantics[END_REF], a compositional theory that admits as specifications LTSs without I/O distinctions. Their inconsistency predicate is induced from inequality of ready-sets, rather than communication mismatches as in our case. Refinement is based on ready-simulation; alphabetised parallel and conjunction are considered, but not quotient.

The operational component model in our framework has been greatly influenced by I/O automata [START_REF] Lynch | An introduction to input/output automata[END_REF] and interface automata [START_REF] Alfaro | Interface automata[END_REF]: both are based on I/O LTSs, with the proviso that I/O automata must be input-enabled, meaning that each state of the automaton is willing to accept any input. We differ from I/O automata by not imposing input-enabledness and from interface automata by working with an explicit CONNECT 231167

19/86 representation of inconsistencies. Another difference is refinement, which for interface automata is defined in terms of alternating simulation, rather than traces; the original definition in [START_REF] Alfaro | Interface automata[END_REF] is simplified in [START_REF] Alfaro | Interface-based design[END_REF], but works only for input-deterministic interface automata. It should be noted that, unlike [START_REF] Alfaro | Interface automata[END_REF][START_REF] Alfaro | Interface-based design[END_REF], we use an associative variant of parallel composition, which combines an input and output into an output (as in [START_REF] Alfaro | Game models for open systems[END_REF]). Furthermore, we provide a definition of conjunction corresponding to shared refinement of interface automata, which substantially generalises that of [START_REF] Doyen | Interface theories with component reuse[END_REF] for synchronous components. Moreover, our quotienting operator on Logic IOLTSs generalises that in [START_REF] Bhaduri | Interface synthesis and protocol conversion[END_REF] defined only for deterministic components.

Our work thus addresses a number of the shortcomings of interface automata, as detailed by Legay et al. in [START_REF] Raclet | A modal interface theory for component-based design[END_REF].

There are a number of process-algebraic frameworks that deal with asynchronous I/O interaction. We mention a characterisation of I/O automata by De Nicola and Segala [START_REF] Nicola | A process algebraic view of input/output automata[END_REF], which is actually a generalisation (and also applicable to interface automata), since the inconsistent process Ω allows to distinguish between good and bad inputs. Similarly to our approach, refinement in [START_REF] Nicola | A process algebraic view of input/output automata[END_REF] is given by trace containment, but does not extend to inconsistent trace containment. This is because we allow a Logic IOLTS to become inconsistent after emitting an output, whereas a process can only become inconsistent through receiving a bad input. Finally, we remark that [START_REF] Nicola | A process algebraic view of input/output automata[END_REF] supports a number of operators of a specification theory, but does not deal with conjunction or quotient.

Our work is also related to the ioco theory in model based testing [START_REF] Tretmans | Model-based testing and some steps towards test-based modelling[END_REF]. The ioco relation is similar to our refinement, but lacks compositionality of operators, so is not well-suited to a specification theory for components.

There have been several CSP-based frameworks that deal with asynchronous communication; of these, the receptive process theory (RPT) [START_REF] Josephs | Receptive process theory[END_REF] utilises a model of concurrency similar to ours in that outputs are non-blocking. RPT also considers quotient (referred to as factorisation), but for the restricted class of delay-insensitive networks [START_REF] Josephs | Controllable delay-insensitive processes[END_REF] that differ from our setting.

A further class of component-based modelling formalisms is based on may/ must modalities. A specification theory for components has been devised in [START_REF] Raclet | Residual for component specifications[END_REF] based on modalities [START_REF] Raclet | Why are modalities good for Interface Theories?[END_REF][START_REF] Raclet | Modal Interfaces: Unifying Interface Automata and Modal Specifications[END_REF], but the definition of quotient is more restrictive than ours. Larsen et al. have made an effort in relating modal transition systems with interface automata [START_REF] Larsen | Modal I/O automata for interface and product line theories[END_REF]. The approach of modal I/O automata is based on a game-like definition of refinement, which we claim to be more complex than ours, see, e.g., the discussion of parallel composition in [START_REF] Raclet | Modal Interfaces: Unifying Interface Automata and Modal Specifications[END_REF]. The framework in [START_REF] Raclet | Modal Interfaces: Unifying Interface Automata and Modal Specifications[END_REF] can support reasoning about liveness properties which our framework does not (although they both support reasoning of safety properties). However, our framework can be easily extended by introducing quiescent states, and additionally considering containment of quiescent traces to reason about liveness.

CONNECTor synthesis in terms of quotient has been considered by Calvert and Lam in [START_REF] Calvert | Deriving a protocol converter: a top-down method[END_REF], however, their approach is more limited than ours. First of all, our quotient is defined on asynchronous systems without handshaking. Moreover, our quotient is the adjoint of parallel composition with respect to a substitutive refinement preorder that preserves non-inconsistency under all environmental contexts. Unlike the existing definition of quotient on interface automata [START_REF] Bhaduri | Interface synthesis and protocol conversion[END_REF], our definition does not require the components under consideration to be deterministic.

Relating the applications of quotient to CONNECT, Martinelli makes use of quotient-like techniques for reasoning about system security [START_REF] Martinelli | Analysis of security protocols as open systems[END_REF]. In his setting, a system can be thought of as a process with a hole, the latter can be used by an attacker to interact maliciously with the system. Ascertaining whether a security policy is upheld by the system is determined by considering all possible instantiations of the hole. Our use of quotient is different, as we are concerned with synthesising CONNECTors by means of quotient, rather than verifying properties of systems (although we can certainly infer properties of our synthesised CONNECTors). Chapter 3 explains in more detail how our quotient can be used for synthesising CON-NECTors for components having different interaction primitives, by handling ontological constraints. The work is novel from a methodological perspective, although it shares similarities with existing techniques and methods.

Declarative (trace-based) modelling framework

In this section, we model components abstractly by means of declarative specifications. We introduce a substitutive refinement preorder together with three compositional operators on declarative specifications.

CONNECT 231167 20/86

A declarative specification comes equipped with an interface, together with a set of behaviours over the interface. The interface is represented by a set of input actions and a set of output actions, which are necessarily disjoint, while the behaviour is characterised by traces. Outputs are under the control of the component, whereas inputs are issued by the environment. This means that, after any successful interaction between the component and the environment, the environment can issue any input i, even if it will be refused by the component. Naturally, if i is refused by the component after the trace t, we deem ti to be an inconsistent trace, since a communication mismatch has occurred. Given this treatment of inputs, we say that our theory is not input-enabled, even though T P is closed under input-extensions.

Definition 2.1 (Declarative specification)

Example A drinks machine dispenses either a tea or a coffee after a coin has been inserted. The drinks machine has sufficient water to produce only 2 drinks, after which a further coin insertion renders the machine inoperable. This behaviour can be encoded by the declarative specification DM = {£}, {t, c}, T, F 1 ∪ F 2 , where:

• T = {ǫ, £, £(c + t), £(c + t)£, £(c + t)£(c + t)} ∪ F 1 ∪ F 2 • F 1 = £(c + t)£(c + t)£(£ + c + t) * insertion of third coin after two dispensations • F 2 = (ǫ + £(c + t))££(£ + c + t) * insertion of second coin before dispensation.
As an issue of notation, for a trace t and set of actions A, write t ↾ A for the projection of t onto A. From hereon let P, Q and R be declarative specifications with signatures

A I P , A O P , T P , F P , A I Q , A O Q , T Q , F Q and A I R , A O R , T R , F R respectively.

Refinement

As refinement corresponds to safe substitutivity, for Q to be used in place of P we require that Q must exist safely in any environment that P can exist in safely. Whether an environment is safe for a specification depends on the sequences of message exchanges afforded by the component. If an environment can prevent a component from performing an inconsistent trace, then the environment is said to be safe. We do not insist that a component Q must have the same interface as the component P to be refined. Instead Q must be accepting of at least all of P's inputs, while restricting to a subset of P's outputs. This can be formalised by the covariant relationship A I P ⊆ A I Q on inputs and the contravariant constraint A O Q ⊆ A O P on outputs. In order to establish that refinement holds, we need to perform a weak form of alphabet equalisation on the inputs of the component to be refined. We refer to this operation as lifting. Informally, lifting extends the trace sets of P by explicitly refusing any input in A I Q \ A I P , after which it allows for arbitrary behaviour.

Definition 2.2 (Lifting)

Let P be a declarative specification, and let A I Q be a set of input actions. The lifting of trace sets T P and F P to A I Q , written as T P ↑ A I Q and F P ↑ A I Q respectively, is defined as:

• T P ↑ A I Q = T P ∪ {tit ′ : t ∈ T P , i ∈ A I Q \ A I P and t ′ ∈ (A I Q ∪ A P ) * }
CONNECT 231167

• F P ↑ A I Q = F P ∪ {tit ′ : t ∈ T P , i ∈ A I Q \ A I P and t ′ ∈ (A I Q ∪ A P ) * }.
Recall that an environment is safe for a component if the environment can prevent the component from performing an inconsistent trace. As outputs are under the control of the component itself, a safe environment must refuse to issue an input on any trace from which there is a sequence of output actions after the input that allows the trace to become inconsistent.

Under such an arrangement, for each declarative specification P we can define the safe declarative specification E(P) containing all of P's permissible and inconsistent traces, but also satisfying the additional property: if t ∈ T P and there exists t ′ ∈ (A O P ) * such that tt ′ ∈ F P , then t ∈ F E(P) . This has the effect of forcing all inconsistent traces to become inconsistent on the environment's issue of a bad input. If the environment respects this safe specification, by not issuing any input that results in an inconsistent trace, then the component can never encounter an inconsistent trace. Note that if ǫ ∈ F E(P) then there is no environment that can prevent P from performing an inconsistent trace. However, for uniformity we still refer to E(P) as the safe specification of P.

Definition 2.3 (Safe specification)

Let P be a declarative specification. The most general safe specification for P is a declarative specification E(P) = A I P , A O P , T E(P) , F E(P) , where T E(P) = T P ∪ F E(P) and

F E(P) = {tt ′ ∈ A * P : t ∈ T P and ∃t ′′ ∈ (A O P ) * • tt ′′ ∈ F P }.
We can now define our substitutive refinement preorder. From the safe specification associated with an arbitrary declarative specification, it is easy to see whether a declarative specification can be substituted safely in place of another. Note that F Q ⊆ F P ↑ A I Q would be too strong to use for the last clause, as we are only interested in trace containment up to the point where an environment can issue a bad input.

Definition 2.4 (Refinement)

For declarative specifications P and Q, Q is said to be a refinement of P, written Q ⊑ dec P, iff:

1. A I P ⊆ A I Q 2. A O Q ⊆ A O P 3. T E(Q) ⊆ T E(P) ↑ A I Q 4. F E(Q) ⊆ F E(P) ↑ A I Q .
Our trace-based definition of refinement respects the intuition behind de Alfaro and Henzinger's alternating refinement relation on interface automata, although theirs is simulation-based [START_REF] Alfaro | Interface automata[END_REF]. We believe that alternating simulation is too strong for checking of safe-substitutivity, as the environments compatible with a component should be independent of the component's resolution of non-determinism.

As our refinement is based on an extension of language inclusion, its complexity is in P, assuming regularity of the trace sets. Note that lifting maintains regularity.

Equivalence of declarative specifications in our framework is defined in terms of mutual refinement.

Definition 2.5 (Equivalence) Let P and Q be declarative specifications. Then P and Q are said to be equivalent, written P ≡ dec Q, iff P ⊑ dec Q and Q ⊑ dec P.

Lemma 2.6 (Preorder)

Refinement is both reflexive and transitive.

Parallel composition

The parallel composition operator on declarative specifications yields a declarative specification representing the combined effect of its operands running asynchronously. We do not consider synchronous parallel composition, as this does not make sense when dealing with non-blocking output actions. To preserve the effect that a single output from a component can be received by multiple components in the environment, we must define the parallel composition to repeatedly broadcast an output: this means that an input a? and output a! combine to form an output a! (as in certain variants of I/O automata), rather than a hidden action τ as is the case in Milner's CCS.

CONNECT 231167 22/86

Not all declarative specifications can be composed with one another; we restrict to those that are said to be composable. P and Q are composable for parallel composition only if

A O P ∩ A O Q = ∅.
This restriction is meaningful if we consider inputs on an interface as buttons and outputs as lights. Given two distinct components, it is not possible for them to share a common light, whereas it is possible to push their buttons at the same time. In practice, issues of composability can be avoided by employing renaming, if this is considered to be appropriate.

• A I P||Q = (A I P ∪ A I Q ) \ (A O P ∪ A O Q ) • A O P||Q = A O P ∪ A O Q • T P||Q = {t ∈ A * P||Q : t ↾ A P ∈ T P and t ↾ A Q ∈ T Q } ∪ F P||Q • F P||Q = {tt ′ ∈ A * P||Q : t ↾ A P ∈ F P and t ↾ A Q ∈ T Q , or t ↾ A P ∈ T P and t ↾ A Q ∈ F Q }.
Informally, a trace is permissible in P || Q if its projection onto A P is a trace of P and its projection onto A Q is a trace of Q. A trace is inconsistent if it has a prefix whose projection onto the alphabet of one of the components is inconsistent and the projection onto the alphabet of the other component is a permissible trace of that component.

We demonstrate the following result, a corollary of which is that mutual refinement is a congruence for parallel, subject to composability. Theorem 2.8 (Compositionality of parallel) Let P, Q and R be declarative specifications such that P and R are composable for parallel composition, and

A I Q ∩ A O R ⊆ A I P ∩ A O R . If Q ⊑ dec P, then Q || R ⊑ dec P || R.

Conjunction

The conjunction operator on declarative specifications can be thought of as finding a common implementation for a number of properties, each of which are represented by declarative specifications. Naturally, any implementation of these properties should be a refinement of each of the properties to be implemented. The conjunction (or shared refinement) of two declarative specifications P and Q is the coarsest declarative specification that refines both P and Q. Thus conjunction is the meet operator on the refinement preorder.

As remarked in Section 2.1, no definition of conjunction has been provided on interface automata, which are conceptually similar to the models of our framework. Henzinger et al. have previously provided a definition of conjunction with respect to alternating refinement [START_REF] Doyen | Interface theories with component reuse[END_REF], however this is only defined on a special type of synchronous component, rather than interface automata.

As for parallel composition, conjunction can only be performed on composable components. P and Q are composable for conjunction only if the sets

A I P ∪ A I Q and A O P ∪ A O Q are disjoint.
Definition 2.9 (Conjunction) Let P and Q be declarative specifications such that

A I P ∪ A I Q and A O P ∪ A O Q are disjoint. Then P ∧ Q is the declarative specification A I P∧Q , A O P∧Q , T P∧Q , F P∧Q
, where:

• A I P∧Q = A I P ∪ A I Q • A O P∧Q = A O P ∩ A O Q • T P∧Q = T P ↑ A I Q ∩ T Q ↑ A I P • F P∧Q = F P ↑ A I Q ∩ F Q ↑ A I P .
Conjunction has strong connections with the logical 'and' operator in Boolean algebra, as shown below.

Mutual refinement is a congruence for conjunction, subject to composability.

CONNECT 231167

Theorem 2.10 (Properties of conjunction)

• Conjunction is the greatest lower bound operator for ⊑ dec

• R ⊑ dec P and R ⊑ dec Q iff R ⊑ dec P ∧ Q • P ∧ Q ≡ dec Q iff Q ⊑ dec P.
Theorem 2.11 (Compositionality of conjunction) Let P, Q and R be declarative specifications such that P is composable with R for conjunction. If Q ⊑ dec P, then Q ∧ R ⊑ dec P ∧ R.

Quotient

The final operation that we consider on the specification theory is that of quotienting, which has strong connections to synthesis. Given a specification for a system R, together with a sub-component P implementing1 part of R, the quotient yields the coarsest specification for the remaining part of R to be implemented. Thus, the parallel composition of the quotient with P should be a refinement of the systemwide specification R. Therefore, quotient can be thought of as the adjoint of parallel composition.

A definition of quotient that acts on deterministic interface automata has been supplied by Bhaduri and Ramesh in [START_REF] Bhaduri | Interface synthesis and protocol conversion[END_REF]. As there is a close coupling between declarative specifications and deterministic interface automata, we should not be surprised that quotient is definable in our setting. However, contrasting their definition with ours reveals that the presentation is substantially different.

As P is a sub-component of R, we make the reasonable assumption that A P ⊆ A R . Moreover, a necessary condition for the existence of the quotient is that

A O P ⊆ A O R
, otherwise refinement will fail on the alphabet containment checks. Definition 2.12 (Quotient) Let P and R be declarative specifications such that

A O P ⊆ A O R and A P ⊆ A R . The quotient of P from R is the specification R/P with signature A I R/P , A O R/P , T R/P , F R/P
, where:

• A I R/P = A O P ∪ A I R • A O R/P = A O R \ A O P • T R/P = {t ∈ A * R : ∀t ′ a prefix of t • L(t ′ ) and ∀t ′′ ∈ A I R/P * • L(tt ′′ )} • F R/P = {t ∈ A * R : (t ↾ A P ∈ T P =⇒ t ∈ F E(R) ) and ∀t ′ a prefix of t • L(t ′ )} • L(t) = (t ↾ A P ∈ F P =⇒ t ∈ F E(R) ) and (t ↾ A P ∈ T P =⇒ t ∈ T R ).
The alphabet of the quotient contains all of the actions from A R and A P so that R/P can fully control P and emulate the behaviour of R. Yet still, simple examples reveal that there may not exist a component Q over an interface consisting of inputs A I R/P and outputs A O R/P such that P || Q ⊑ dec R. Unfortunately, the existence of the quotient cannot be ascertained by a syntactic check on the alphabets of P and R.

In Definition 2.12 we referred to R/P as a specification, but not a declarative specification. If T R/P is non-empty, then T R/P is a declarative specification, otherwise it is not. As the following theorem shows, if T R/P is non-empty (a condition of being a declarative specification), then the quotient exists, and if it is empty, then the quotient does not exist.

Theorem 2.13 (Existence of quotient) Let P and R be declarative specifications such that

A O P ⊆ A O R and A P ⊆ A R .
Then there exists a declarative specification Q with input actions A I R/P and output actions

A O R/P such that P || Q ⊑ dec R iff T R/P = ∅.
The next two theorems show that R/P satisfies the required properties of quotient when T R/P is non-empty, and that quotient is well-behaved with respect to refinement.

Theorem 2.14 (Properties of quotient) Let P and R be declarative specifications such that A

O P ⊆ A O R and A P ⊆ A R . If T R/P = ∅, then P || (R/P) ⊑ dec R and for any declarative specification Q over inputs A I R/P and outputs A O R/P such that P || Q ⊑ dec R it holds that Q ⊑ dec R/P.
Theorem 2.15 (Compositionality of quotient) Let P, Q and R be declarative specifications such that Q ⊑ dec P.

• If Q/R and P/R are defined, then Q/R ⊑ dec P/R.

• If R/Q and R/P are defined, and

(A I Q ∩ A O R ) \ A P = ∅, then R/Q ⊒ dec R/P.

Operational modelling framework

In this section we take an operational view of components, by specifying their allowable interactions in terms of Logic IOLTSs, an I/O version of labelled transition systems augmented by an inconsistency predicate on states. We remain faithful to the trace-based substitutive preorder, and cast refinement at the operational level in terms of declarative refinement. For any operational model, we can derive an equivalent declarative specification, meaning that the observable safe interactions between the models and an arbitrary environment are indistinguishable.

To support a compositional theory of components, we define the operations of parallel composition, conjunction and quotient directly on our operational models. We further show that compositionality results for the operators on the declarative framework carry over to the operational framework as well.

An explicit definition of implementation is not provided for our models, although there are a number of candidates. One such suggestion for the characterisation of implementations would be the set of specifications in which no inconsistent states are reachable. We leave this for the user to decide.

We can now define the operational models formally. For a set A, write A τ as shorthand for A ∪ {τ }, where it is assumed that τ ∈ A.

Definition 2.16 (IOLTS)

An I/O labelled transition system (IOLTS) P is a tuple S P , A I P , A O P , -→ P , where S P is a (possibly infinite) collection of processes (states), A I P and A O P are disjoint sets referred to as the inputs and outputs (the union of which we denote by A P ), and -→ P ⊆ S P ×A τ P ×S P is the transition relation. Note that since we do not insist on our components being fully input-enabled (unlike I/O automata [START_REF] Lynch | An introduction to input/output automata[END_REF]), meaning that at any stage a component can refuse to accept an input issued by the environment or another component, we must extend IOLTSs to reason about potential communication mismatches that occur during interactions. We accomplish this by augmenting IOLTSs with an inconsistency predicate for tracking mismatches. The resulting model, called a Logic IOLTS, takes its inspiration from the Logic LTSs of L üttgen and Vogler [START_REF] Nicola | Conjunction on processes: Full abstraction via ready-tree semantics[END_REF][START_REF] Vogler | Ready simulation for concurrency: It's logical![END_REF], although we have a different interpretation of inconsistency. Definition 2.17 (Logic IOLTS) A Logic IOLTS P is a tuple S P , A I P , A O P , -→ P , F P in which S P , A I P , A O P , -→ P is an IOLTS, and F P ⊆ S P is an inconsistency predicate on states satisfying the property: if p ∈ S P can diverge (meaning there is an infinite sequence of τ -transitions emanating from p), then p ∈ F P .

The inconsistency predicate annotates states that correspond to run-time errors such as communication mismatches, underspecification, or divergent behaviour. Regardless of why a state is inconsistent, we assume that on encountering an inconsistency, unspecified behaviour can ensue. Consequently, inconsistent states are resemblant of the process CHAOS from CSP [START_REF] Brookes | A theory of communicating sequential processes[END_REF].

Figure 2.1 shows a number of Logic IOLTSs represented pictorially. We adopt the convention of enclosing the transition system within a box corresponding to the interface of the component. Labelled arrows pointing at the interface correspond to inputs, whereas arrows emanating from the interface correspond to outputs. As a matter of clarity, we only represent the states that are reachable by a sequence of transitions from the process we are interested in. States annotated with an F are deemed to be inconsistent.

We introduce nomenclature for handling stability and hidden τ -transitions. A relation From hereon, let P = S P ,

ǫ =⇒ P ⊆ S P × S P is defined by p ǫ =⇒ P p ′ iff p( τ -→ P ) * p ′ . Generalising
A I P , A O P , -→ P , F P , Q = S Q , A I Q , A O Q , -→ Q , F Q and R = S R , A I R , A O R , -→ R , F R
be three Logic IOLTSs, and let p P , q Q and r R be processes in the Logic IOLTSs P, Q and R respectively.

Refinement

In keeping with the declarative framework, we wish refinement to correspond to safe-substitutivity. Hence, we cast refinement at the operational level in terms of refinement at the declarative level. To do this, we define a mapping • * from operational models to declarative models (Definition 2.20) that preserves the environments that the models can interact harmoniously with.

An essential feature of operational refinement is that the mapping from operational to declarative models preserves the safe traces of the component. For a declarative specification P, a trace t is said to be immediately-safe iff t is permissible, but not inconsistent (i.e., t lies within T P \ F P ). If t is contained within T P \ F E(P) , we say that t is safe. The calculation of the safe traces for a Logic IOLTS is slightly more involved, because it is necessary to deal with non-determinism and τ -transitions.

Definition 2.18 (Immediately-safe states)

The set of immediately-safe states that a process p P can be in after following the trace t is given by h p P (t), where h p P : A * P -→ 2 S P is defined as:

• h p P (ǫ) = ∅ if p P ǫ =⇒ P p ′ with p ′ ∈ F P {p ′ ∈ S P : p ǫ =⇒ P p ′ } otherwise • h p P (to) = ∅ if ∃p ′ ∈ h p P (t) such that p ′ ⊣o =⇒ P p ′′ with p ′′ ∈ F P {p ′′ ∈ S P : ∃p ′ ∈ h p P (t) • p ′ ⊣o =⇒ P p ′′ } otherwise when o ∈ A O P • h p P (ti) = ∅ if ∃p ′ ∈ h p P (t) such that p ′ ⊣i =⇒ P p ′′ with p ′′ ∈ F P , or p ′ i -→ P {p ′′ ∈ S P : ∃p ′ ∈ h p P (t) • p ′ ⊣i =⇒ P p ′′ } otherwise when i ∈ A I P .
Definition 2.19 (Safe traces) A trace t of p P is immediately-safe iff h p P (t) = ∅ and is safe iff h p E(P) (t) = ∅, where E propagates inconsistencies backwards over output and τ transitions. The set of immediately-safe traces of p P is denoted IST (p P ), while the set of safe traces is denoted ST (p P ).

An immediately-safe trace t of a process p characterises a permissible exchange between p and an arbitrary environment, such that t will never encounter an inconsistent state under any resolution of p's non-determinism. Relating this intuition to Definitions 2.18 and 2.19, suppose p and the environment can safely communicate on the trace t. If from some state that p is in after following t it can perform an output o, and every o it can output will never make the system inconsistent, then the environment must be willing to accept that output. Conversely, the environment can only safely issue an input i after t if i can be accepted from every state the process is in after following t, without making the system inconsistent. We must impose these restrictions to account for the fact that the process cannot be expected to know how to resolve its non-determinism prior to its communication with the environment.

Definition 2.20 (Model mapping) The model mapping function •

* from Logic IOLTSs to declarative specifications is defined by p P * = A I P , A O P , T p P * , F p P * , where: • Having defined a mapping from operational to declarative models, we can now define operational refinement in the obvious way.

• T p P * = {t : p P t =⇒ P } ∪ F ∪ F I CONNECT 231167 P p 1 p 2 p 3 a b a b ⊑ op Q q 1 q 2 q 3 a c a c R r 1 r 2 r 3 r 4 r 5 a a b c a b c ⊑ op S s 1 s 2 s 3 F s 4 F a a c a b c
F p P * = F ∪ F I • F = {tt ′ : p P t =⇒ P p ′ , p ′ ∈ F P and t ′ ∈ A * P } • F I = {tit ′ : p P t =⇒ P p ′ , i ∈ A I P , p ′ i -→ P and t ′ ∈ A * P }.

Definition 2.22 (Operational refinement)

Process q Q is said to be a refinement of process p P , written

q Q ⊑ op p P , iff q Q * ⊑ dec p P * .

Lemma 2.23 (Operational preorder) Refinement is reflexive and transitive.

Under the assumption of finiteness, we note that refinement checking is PSPACE-complete. This is similar to traces refinement in CSP, where the worst-case is rarely observed in practice. Definition 2.24 (Operational equivalence) Processes p P and q Q are said to be equivalent, written p P ≡ op q Q , iff q Q ⊑ op p P and p P ⊑ op q Q . Looking at the refinements in Figure 2.1, from q 1 the environment can safely issue a, after which it must be willing to accept c. Clearly a can be safely accepted by p 1 , and as p 2 does not issue a c output the environment will be perfectly happy. Moreover, as the environment is not permitted to issue a b in q 1 there is no harm in p 1 being able to handle this behaviour. Hence p 1 ⊑ op q 1 . Now, r 1 ⊑ op s 1 as r 1 is willing to accept the input a from the environment, which is not the case in s 1 . This is because we cannot trust s 1 to resolve its non-determinism on a in an optimistic way by always moving to s 2 .

Example To formally check p 1 ⊑ op q 1 , it is necessary to resort to the definition of refinement on declarative specifications (Definition 2.4). It can easily be checked that all of the conditions of that definition hold by considering the sets below, obtained by computing the model mapping of the processes p 1 and q 1 .

• F p1 * = F E( p1 * ) = (a + b)(a + b) + • F q1 * = F E( q1 * ) = (a + ac)a(a + c) * • T p1 * = (a + b) * • T q1 * = {ǫ, a, ac} ∪ (a + ac)a(a + c) * • X ↑ A I P = X ∪ (ǫ + a + ac + (aa + aca)(a + c) * )b(a + b + c) * for X ∈ {F q1 * , T q1 * }.
CONNECT 231167

Error-completion

In order to simplify the definitions of the operators in our specification theory for the operational framework, we introduce the error-completion of a Logic IOLTS. This is a transformation that leaves the mapping from a Logic IOLTS to a declarative specification unchanged. The error-completion of a Logic IOLTS provides an explicit operational representation for the inconsistent traces that would arise in mapping the Logic IOLTS to its corresponding declarative specification. Consequently, an error-completed Logic IOLTS is closed under input extensions. It is this property that simplifies the definitions of the operators in our framework. We do not say that an error-completed Logic IOLTS is input-enabled, however, as we can distinguish good inputs from bad inputs.

Definition 2.25 (Error-completion)

Let P be a Logic IOLTS, and assume f P ∈ S P . The error-completion of P is a Logic IOLTS P ⊥ = S P ⊥ , A I P , A O P , -→ P ⊥ , F P ⊥ , where:

• S P ⊥ = S P ∪ {f P } • -→ P ⊥ = -→ P ∪ {(f, a, f ) : f ∈ F P ⊥ and a ∈ A P } ∪ {(s, a, f P ) : a ∈ A I P and ∄s ′ • s a -→ P s ′ } • F P ⊥ = F P ∪ {f P }.
As remarked, the error-completion of a Logic IOLTS preserves the mapping from Logic IOLTSs to declarative specifications, as the next lemma shows. Note that the corresponding declarative specifications are equal, rather than declaratively equivalent.

Lemma 2.26 (Error-completion respects mappings) For any process p

P , p P * = p P⊥ * .
Besides simplifying the definition of the compositional operators in our specification theory, errorcompletion of a Logic IOLTS also simplifies the definition of the model mapping function.

• T p * = {t : p t =⇒ P ⊥ } • F p * = {tt ′ : p t =⇒ P ⊥ p ′ t ′ =⇒ P ⊥ and p ′ ∈ F P ⊥ }.

Parallel composition

As for declarative specifications, the parallel composition of Logic IOLTSs yields a Logic IOLTS representing the combined effect of its operands running asynchronously. We insist that any given output should be under the control of one component only. Therefore Logic IOLTSs P and Q are composable for parallel composition only if

A O P ∩ A O Q = ∅.
Definition 2.28 (Parallel composition) Let P and Q be Logic IOLTSs composable for parallel composition. Then the parallel composition of P and

Q is a Logic IOLTS P || Q = S, A I , A O , -→, F
, where:

• S = S P ⊥ || S Q ⊥ • A I = (A I P ∪ A I Q ) \ (A O P ∪ A O Q ) • A O = A O P ∪ A O Q • -→ is the smallest relation satisfying the following rules: P1. If p a -→ P ⊥ p ′ with a ∈ A τ P \ A Q , then p || q a -→ p ′ || q P2. If q a -→ Q ⊥ q ′ with a ∈ A τ Q \ A P , then p || q a -→ p || q ′ P3. If p a -→ P ⊥ p ′ and q a -→ Q ⊥ q ′ with a ∈ A P ∩ A Q , then p || q a -→ p ′ || q ′ .
CONNECT 231167

• F = (S P ⊥ || F Q ⊥ ) ∪ (F P ⊥ || S Q ⊥ ).
Conditions P1 to P3 ensure that the parallel composition of Logic IOLTSs interleave on independent actions and synchronise on common actions. For P3, given the parallel composability constraint, synchronisation can take place between an output and an input, or two inputs. Figure 2.2 shows how the parallel composition operator works in practice, although we omit non-enabled input transitions to inconsistent states. In particular, the example demonstrates how inconsistencies can be introduced through non-input enabledness, as in state r 6 corresponding to

p 6 || q 2 .
Reassuringly, parallel composition of Logic IOLTSs yields a Logic IOLTS. The following theorem shows the relationship between parallel composition on Logic IOLTSs and parallel composition on declarative specifications.

Theorem 2.29 (Parallel correspondences) Let P and Q be Logic IOLTSs composable for parallel composition. For processes p P and q Q , it holds that p P || q Q * = p P * || q Q * .

Conjunction

In keeping with conjunction of declarative specifications, Logic IOLTSs P and Q are composable for conjunction only if the sets

A I P ∪ A I Q and A O P ∪ A O Q are disjoint.
Definition 2.30 (Conjunction) Let P and Q be Logic IOLTSs composable for conjunction. Then the conjunction of P and

Q is a Logic IOLTS P ∧ Q = S, A I P ∪ A I Q , A O P ∩ A O Q , -→, F
, where:

• S = S P ⊥ ∧ S Q ⊥ • -→ is the smallest relation satisfying the following rules: C1. If a ∈ A O P ∩ A O Q , p a -→ P ⊥ p ′ and q a -→ Q ⊥ q ′ , then p ∧ q a -→ p ′ ∧ q ′ C2. If a ∈ A I P ∩ A I Q , p a -→ P ⊥ p ′ and q a -→ Q ⊥ q ′ , then p ∧ q a -→ p ′ ∧ q ′ C3. If a ∈ A I P \ A I Q and p a -→ P ⊥ p ′ , then p ∧ q a -→ p ′ ∧ f Q C4. If a ∈ A I Q \ A I P and q a -→ Q ⊥ q ′ , then p ∧ q a -→ f P ∧ q ′ C5. If p τ -→ P ⊥ p ′ , then p ∧ q τ -→ p ′ ∧ q C6. If q τ -→ Q ⊥ q ′ , then p ∧ q τ -→ p ∧ q ′ • F = F P ⊥ ∧ F Q ⊥ .
CONNECT 231167 29/86 The idea behind the definition of conjunction for p ∧ q is that p and q must synchronise on common actions, interleave on τ -transitions, and on encountering independent input actions behave like the respective component to which the action belongs. On encountering a state p ∧ q in which one of p ∈ F P or q ∈ F Q holds, let it be p, we know that whatever the behaviour of p ∧ q it will always be a refinement of p. So the most general refinement of p ∧ q will actually be q. This is supported by the fact that inconsistent states in the error-completed Logic IOLTS admit arbitrary behaviour.

∧ Q q 1 q 2 F q 3 q 4 F b c, e b b c e = P ∧ Q r 1 p 1 ∧ q 1 r 2 p 3 ∧ q 2 r 3 p 4 ∧ q 3 r 4 f P ∧ q 3 r 5 p 5 ∧ f Q r 6 f P ∧ q 4 F r 7 p 6 ∧ f Q b c
Figure 2.3 shows the conjunction of processes p 1 and q 1 in the Logic IOLTSs P and Q (although for clarity we omit inputs leading to inconsistent states). In state r 1 corresponding to p 1 ∧ q 1 , the b-output transitions of p 1 and q 1 synchronise. Independent output actions such as the a-transition in p 1 are not permitted to proceed, because it would not be the case that r 1 could be used safely in place of q 1 if this transition were to be permitted. State r 2 can evolve into r 3 by synchronising the c-inputs of p 3 and q 2 , while it can also evolve into r 4 by proceeding on the independent input e of q 2 . From this point, r 4 behaves like q 3 , because e is an input-violation of p 3 . Similar reasoning applies to r 3 's evolution into r 5 by receiving the d-input.

As for parallel composition, there is a correspondence between conjunction at the operational and declarative levels.

Theorem 2.31 (Conjunction correspondences)

Let P and Q be Logic IOLTSs composable for conjunction. For processes p P and q Q , it holds that p P ∧ q Q * = p P * ∧ q Q * .

Quotient

Non-determinism and τ -transitions arising in Logic IOLTSs make the definition of quotient more involved than the other operators we have considered on operational models. To ensure that the quotient is the coarsest specification, it is necessary to track the non-determinism of the system-wide specification and its partial implementation. This is because the non-determinism can affect the safe traces of a Logic IOLTS.

As for declarative specifications, we only compute the quotient of process p P from r R when

A O P ⊆ A O R and A P ⊆ A R .
The quotient is the coarsest specification q over an interface consisting of inputs

A O P ∪ A I R and outputs A O R \ A O P such that p P || q ⊑ op r R .
If such a q exists, we denote it by r R /p P . Our work in this section is more general than that of Bhaduri and Ramesh in [START_REF] Bhaduri | Interface synthesis and protocol conversion[END_REF], as we allow for our components to exhibit non-determinism and hidden transitions. Recall that in [START_REF] Bhaduri | Interface synthesis and protocol conversion[END_REF], the interface automata must be deterministic.

Before defining the quotient-construction, we introduce some functions and predicates that simplify the presentation.

Definition 2.32 For Logic IOLTS P, set of states S ⊆ S P ⊥ and action a ∈ A P , define:

• succ ǫ P (S) = {s ′ : s ǫ =⇒ P ⊥ s ′ with s ∈ S} CONNECT 231167
} • A I R/P = A O P ∪ A I R • A O R/P = A O R \ A O P
• -→ is the smallest relation satisfying the following rules:

Q1. R ′ /P ′ a -→ succ a R (R ′ )/succ a P (P ′ ) providing: (a) a ∈ A I P ∩ A I R implies succ a R (R ′ ) ∩ F E(R) = ∅ (b) a ∈ A O P ∩ A O R implies succ a R (R ′ ) ∩ F E(R) = ∅ and succ a P (P ′ ) = ∅ (c) a ∈ A I P ∩ A O R implies succ a P (P ′ ) ∩ F P = ∅ and succ a R (R ′ ) = ∅ Q2. R ′ /P ′ a -→ succ a R (R ′ )/P ′ providing: (a) a ∈ A I R \ A P implies succ a R (R ′ ) ∩ F E(R) = ∅ (b) a ∈ A O R \ A P implies succ a R (R ′ ) = ∅. • R ′ /P ′ ∈ F R/P iff
at least one of the following rules holds:

F1. R ′ = ∅ or P ′ = ∅ F2. F E(R ⊥ ) ∩ R ′ = ∅ or F P ⊥ ∩ P ′ = ∅ F3. R ′ /P ′ a -→ R ′′ /P ′′ with a ∈ A I R/P and R ′′ /P ′′ ∈ F R/P .
Definition 2.34 (Quotient) Let P and R be Logic IOLTSs such that A O P ⊆ A O R and A P ⊆ A R . The quotient of process p P from process r R , written r R /p P , is the process succ ǫ R (r R )/succ ǫ P (p P ) in the Logic IOLTS R//P obtained from R/P by removing all transitions immediately leading to a state in F R/P , and removing all states R/P such that R/P ∈ F R/P and R ∈ F E(R) . If succ ǫ R (r R )/succ ǫ P (p P ) is not contained in R//P, then the quotient is not defined.

As for declarative specifications, the quotient of p P from r R may not exist. The following theorem shows that definedness of the quotient according to the previous definition coincides precisely with the existence of such a quotient.

Theorem 2.35 (Existence of quotient) Let P and R be Logic IOLTSs such that

A O P ⊆ A O R and A P ⊆ A R . Then r R /p P is defined (i.e. r R ∈ F E(R) or r R /p P ∈ F R/P )
iff there exists a process q in a Logic IOLTS with inputs A I R/P and outputs A O R/P such that p P || q ⊑ op r R . Consequently, the constraint r R ∈ F E(R) and r R /p P ∈ F R/P gives a precise characterisation of whether the quotient exists or not. When the quotient does exist, it behaves in exactly the same way as for declarative specifications.

Theorem 2.36 (Quotient correspondences) Let P and R be Logic IOLTSs such that

A O P ⊆ A O R and A P ⊆ A R . If r R /p P ∈ F R/P or r R ∈ F E(R) , then r R /p P * = r R * / p P * .
Figure 2.4 provides an example in which processes p 1 and r 1 have no quotient. This tallies with Theorem 2.35, as we have {r 1 }/{p 1 } ∈ F R/P when r 1 ∈ F E(R) . On the other hand, quotients exist for the processes p 1 and r 1 of Figures 2.5 and 2.6. This is also supported by Theorem 2.35, as {r 1 }/{p 1 } ∈ F R/P for the processes in both figures.

For Figure 2.6, the quotient is the single consistent state {r 1 }/{p 1 }. This is because in going from R/P to R//P we remove the transition labelled by the output a between the processes {r 1 }/{p 1 } and {r 2 }/{p 2 , p 3 }, as the latter state is inconsistent. Maintaining this transition would yield an invalid quotient as p 1 || (r 1 /p 1 ) would be inconsistent when r 1 is consistent. It is safe to discard this transition only because it is an output. Recalling the definition of ⊑ op , for safe-substitutivity it is perfectly safe to suppress outputs on the left that would have occurred on the right.

R/P q 1 {r 1 }/{p 1 } q 2 {r 2 }/{p 2 , p 3 } a a b R//P q 1 r 1 /p 1 q 2 {r 2 }/{p 2 , p 3 } a a b

Summary and future work

We have developed a compositional specification theory for components that may be modelled operationally, closely mirroring actual implementations, or in an abstract manner by means of declarative specifications. Both frameworks admit a simple refinement relation, defined in terms of traces, which corresponds to safe-substitutivity. We define asynchronous parallel composition, conjunction and quotient, and prove that the induced equivalence is a congruence for these operations. It is straightforward to extend our framework with disjunction and hiding. CONNECT-centric examples demonstrating our specification theory are provided in Chapter 3. The simplicity of our formalism facilitates reasoning about the temporal ordering of interactions needed for assume-guarantee inference. We are in the process of formulating an AG framework for reasoning compositionally about components. This will support the preservation of safety and liveness properties under the operations of the specification theory. As the original framework only deals with finite-executions, the form of liveness to be considered will be based on quiescence. CONNECT 231167 32/86 CONNECT 231167

P p 1 p 2 p 3 p 4 a a b a b R r 1 r 2 r 3 a b a b R/P q 1 {r 1 }/{p 1 } F q 2 {r 2 }/{p 2 , p 3 } a a b R//P q 1 r 1 /p 1 F q 2 {r 2 }/{p 2 , p 3 } a b
3 Integration of the specification theory and synthesis

In this chapter we relate the specification theory introduced in Chapter 2 with the task of generating connectors. The latter must facilitate the successful interaction of multiple components that need to communicate with one another. The components are permitted to have incompatible behaviours and to utilise different interaction vocabularies. Therefore, to ensure that the connector generated is meaningful, we assume there is an ontology relating the actions of the components that need to communicate. Such an ontology can tell us about equivalence of actions, along with ordering constraints that the actions must satisfy.

The purpose of the connector is to resolve the communication mismatches inherent from the differing characteristics of the components. This essentially means that the connector functions as a mediator. The mediators generated by our theory are free from communication mismatches, but they also ensure that progress is made so that meaningful interaction takes place. Given a collection of components, our theory also allows one to deduce whether a mediator can exist or not.

Connector synthesis as quotient

As we are interested in using our theory developed in Chapter 2, we assume that the components needing to communicate are modelled as either declarative specifications or Logic IOLTSs (the choice is largely indifferent). The synthesis approach we document is applicable to any number of components needing to communicate, so for simplicity we assume that there are exactly two, which we denote by P and Q.

A mediator M for the successful interaction of P and Q can be found as a solution to the equation

P || M || Q ⊑ G,
where G is some specification stating what it means for P and Q to interact successfully, and ⊑ is the refinement relation defined in Chapter 2 (it is either ⊑ dec or ⊑ op depending on the model types). Thus, using the theory of Sections 2.2.4 and 2.3.5, it follows that the most general M can be found by quotient as G/(P || Q). Of course, as quotient is a partial operation, definedness of M is not guaranteed.

A problem with this formulation in CONNECT concerns the derivation of the goal G. Conceivably, G would deal with application-specific knowledge, but in CONNECT this is not generally available, other than in the form of the ontology that specifies relationships between interaction primitives. We therefore consider the task of formulating an abstract goal that specifies the general principles of interaction that we are interested in. Specifically, the goal G must ensure that the synthesised mediator M satisfies the following properties: G1. P || M || Q is not permitted to generate any communication inconsistencies G2. P || M || Q is only permitted to deadlock in composite states where all three of P, M and Q are permitted to deadlock G3. P || M || Q must satisfy the constraints imposed by the ontology.

The following sections explain precisely how we can synthesise a mediator to satisfy these properties by means of quotient.

Capturing ontological constraints

Given components P and Q needing to communicate, we assume that there is an ontology that relates actions of P with actions of Q and vice versa. This assumption is widespread through CONNECT, otherwise it is not possible to generate a connector that respects the semantics of the components it interfaces with. In our work for WP2, we assume that the ontology can specify two kinds of relationship on the communication primitives of the components: CONNECT 231167 2. Ordering of primitives. The ontology further tells us about the ordering of primitives that the composition of the components and mediator must respect. This allows us to enforce constraints of causality (since we do not explicitly model data, causality can not be inferred by dataflow constraints or similar). For example, an ack in Q should only be issued after a send has been emitted by P.

For each relationship in the ontology, we construct an observation component that has as interface the collection of primitives that appear in the relationship. As we treat the component as an observer, all of the actions are considered to be inputs. The behaviour of the observer respects the intuition of the relationship (we explain how the behaviour is derived in the points below). If the mediator or a component violates a constraint, the corresponding observer will generate an inconsistency. The component O respecting the combined effect of all of the ontological constraints is then defined as the parallel composition of the representations of the individual relationships. Note that this is always defined. We model an arbitrary observer Seq(c 1 . . . c m ) as a component in our framework. Its behaviour is characterised by Figure 3.1. In practice, other constraints besides equivalence and ordering of primitives can be represented by observers. Although we do not consider them in this report, they can be handled by our theory in the same way.

Modelling deadlock

A trace t of a declarative specification P is said to be quiescent if the component cannot produce further output without receiving stimulation from the environment.

A P ∪ A Q A P A Q Figure 3.2: Logic IOLTS representing the goal G
Yet, deadlock is not all bad news. For example, deadlock could signify successful termination of a component, or could indicate that the component requires interaction from the environment in order to proceed. We therefore classify deadlocked states as either good or bad, depending on whether we're happy for deadlock to occur or not.

Our synthesis framework ensures that the components and mediator will always make progress (i.e. will not deadlock), unless all of the components deadlock in a good way (desideratum G2). This means that we need a way of distinguishing good and bad deadlock in a component. To do this, we introduce a action that appears as an input in the interface of each component. Like in CSP, a action is used to signify successful termination. The behaviour of each component is extended so that a action can be observed at any point where the component is permitted to deadlock in a good state.

The mediator will have as an output action. This means that the mediator is only able to issue the in a composite state where all of the components are willing to receive it, otherwise an inconsistency will occur. The checking of deadlock follows implicitly from the synthesis procedure with quotient, after devising a suitable goal.

Note that this notion of progress is slightly weaker than that modelled by, e.g., liveness in the sense of linear temporal logic, since infinite computations are not required to achieve some particular goal. However, for components (or systems) that exhibit only finite computations, quiescence is a perfectly adequate way to model liveness.

Formulating the goal

We begin by assuming that P || M || Q is intended to be a closed system. This means that there are no inputs in the interface of P || M || Q. In this setting, we take as the goal a general specification G that states "no inconsistency will arise" and "deadlock can only occur after a has been seen". The goal can thus only become quiescent after seeing a action.

This can be formulated as the declarative specification A I , A O , T, F, Q , where:

• A I = ∅ • A O = A P ∪ A Q ∪ { } • T = (A O \ { }) * (ǫ + ) • F = ∅ • Q = (A O \ { }) * .
A pictorial representation of the goal as a Logic IOLTS is provided in Figure 3.2.

In the case that P || M || Q is an open system, the goal would be slightly more involved, as it would have to interleave the interactions with the environment. However, If we have a model of the environment E, we can use the same goal by considering P || M || Q || E, where we assume that E is just another component.

CONNECT 231167

If we do not have a model of the environment, it is not possible to guarantee that the mediator can avoid inconsistencies. This can only be done if the environment issues outputs only at the times when the components are willing to receive them. The most general safe environment will always issue an output, whenever the corresponding components are willing to receive it. If we wish to synthesise the mediator for the most general safest environment, this can be done by transforming the interfaces of P and Q such that open inputs become outputs. In this case, the parallel composition of the transformed components and the mediator would be a closed system, and so we can use the standard goal G.

The synthesis procedure

We can now state how to synthesise the mediator. Explanation on how our synthesis procedure relates to the synthesis algorithm in WP3 [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF] is provided in Section 3.8.

Given the goal G and ontological constraint O, we formulate the mediator synthesis problem as finding a most general mediator M such that P || M || O || Q ⊑ G. In our theory, M can be found as G/(P || Q || O), as per Definitions 2.12 and 2.33.

To check that the synthesised mediator M satisfies our desiderata, suppose that As a result, if there is a mediator M such that P || M || Q satisfies the desiderata we outlined in Section 3.1, then our algorithm based on quotient is guaranteed to find it. Moreover, by the Theorems in Sections 2.2.4 and 2.3.5, the mediator will always be the most general.

P

A simple messaging example

We begin by demonstrating our mediator synthesis procedure on a simple example, which is a variant of the instant messaging illustration we first considered in [START_REF] Autili | Towards a connector algebra[END_REF]. Our revised example is set within a humble train station. A despatching system holds details of the trains at the station, together with each train's destination list and departure platform. A number of dissemination systems interface with the despatcher to keep passengers informed about the status of each train. Such systems include electronic display boards and automated announcers. It is our intention to synthesise a connector for allowing a departure board to display information about a particular train.

Figure 3.3 models the behaviour of the despatcher, while Figure 3.4 models the behaviour of the departure board controller. Both models take the form of Logic IOLTSs, where square nodes are quiescent and circular nodes are non-quiescent. As the models have disjoint communication vocabularies, they are unable to interoperate with one another. Fortunately, however, an ontology tells us the relationships between the actions:

• req ≡ hand • done ≡ close

• done ack ≡ close ok

• text ≡ msg • src ≡ target.
Considering whether these actions are inputs or outputs in the respective models, we can derive a component O representing the ontological constraints as the parallel composition of the following Seq primitives:

• Seq(req, hand)

• Seq(auth ok, req ack)

• Seq(close, done)

• Seq(done ack, close ok)

• Seq(msg, text)

• Seq(target, src).

Example based on booking a packaged holiday

We now consider a slightly more involved example to demonstrate our synthesis procedure on that was first presented in the CONNECT publication [START_REF] Blair | The role of ontologies in emergent middleware: Supporting interoperability in complex distributed systems[END_REF]. The example involves two travel agencies: one based in the US and the other in the EU. The travel agencies have different booking systems, the technicalities being irrelevant for us in this section, although the full details can be consulted in [START_REF] Blair | The role of ontologies in emergent middleware: Supporting interoperability in complex distributed systems[END_REF]. We assume the existence of an ontology that relates the domain-specific concepts of the systems.

A client of the US system needs to interface with the EU booking system. It is thus our intention to synthesise a mediator that will allow the client to interact with the service. An added complication of this scenario is that the models of the clients and services deal with data. We show how we can encode data constraints within our notation so that the synthesised mediator respects the principles of data flow.

In keeping with the notation of WP3, we assume the transitions of models are labelled as:

• (op, In, Out), where op is a receptive operation, In is a list of data items that should be input and Out is a list of data items that should be output; or

• (op, In, Out), where op is an active operation, In is a list of data items that are to be output, and Out is a list of data items to be input.

Our setup in WP2 is unable to cope with these structured transitions atomically, so we give a transformation that respects the semantics. Each transition labelled with (op, In, Out) is represented by two consecutive transitions labelled opI?In and opO!Out. On the other hand, each transition labelled (op, In, Out) is represented by two consecutive transitions labelled by opI!In and opO?Out. Note that the ? and ! symbols indicate the I/O type of the actions opI and opO.

Modelling the components. We model the components (i.e. the US client and EU service) by Logic IOLTSs. Figure 3.7 shows the U S client, which first finds a complete holiday and then confirms it. The model for the EU service is too cumbersome to draw, so we give a characterisation in terms of the following LTSA description:

EUF = (selFlightI -> selFlightO -> makeResI -> makeResO -> END). EUH = (selHotelI -> selHotelO -> makeResI -> makeResO -> END). EUC = (selCarI -> selCarO -> makeResI -> makeResO -> END). ||EU = (EUF || EUH || EUC).
The EU service requires the user to select a flight, hotel and car in any order, before being permitted to make a reservation. Actions ending in an I are treated as inputs, while actions ending in an O are treated as outputs.

Ontological constraints. The ontology states that a find trip request f indI must take place before the constituent parts of the trip can be selected (selF lightI, selCarI and selHotelI). Moreover, the results of finding a trip f indO can only be returned once the flight, car and hotel have been selected (selF lightO, selCarO and selHotelO have been seen). Confirming a trip conf I on the US client corresponds to making a reservation makeResI on the EU booking service, and the reservation acknowledgement makeResO of CONNECT 231167 the EU service corresponds to the US trip confirmation conf O. A further constraint states that a car can only be hired from the airport that the flight goes to. Thus, the flight result selF lightO, is required before the car can be selected selCarI.

The following points formally state the ontological constraints as according to the preceding text, together with the component representation: The component O representing the ontological constraints is obtained as the parallel composition of the Seq primitives listed above. Note that all of the actions are treated as inputs, as O is an observing component. Therefore, all states are quiescent and by input-enabledness, any trace over these actions that does not satisfy the ontological constraints is an inconsistent trace of the component.

Synthesis. The mediator M is obtained as the quotient G/(U S || O || EU ).

As usual, G is the Logic IOLTS shown in Section 3.4 taking the output set as the union of all actions in the components EU and U S. The Logic IOLTS of M generated using our quotienting procedure is shown in Figure 3.8. CONNECT 231167

Mapping the WP3 mediator theory into the WP2 specification theory

In the previous sections, we have shown how the specification theory defined in Chapter 2 can be used to formulate the mediator synthesis problem as a suitable quotienting problem, in which ontological constraints and an abstract goal specification are taken into account. Since the mediator synthesis problem has been deeply investigated within the work of WP3, we show the relationships between the specification theory of WP2 and the mediator theory of WP3. Demonstrating integration of the work packages is achieved by giving a mapping from the mediator theory of WP3 to our specification theory. This allows the work of WP3 to inherit the interesting results of the specification theory. More verbosely, it allows one to state that a mediator synthesized à la WP3 is correct. That is, the mediator does not introduce communication mismatches or deadlocks, and is most general.

In our work, WP2 has opted for a model of concurrency that does not rely on handshaking between components, to better support distributed systems with asynchronous communication. This has culminated in an I/O model of concurrency where outputs are under the control of the component to which they belong, while inputs are controlled by the environment. WP3, on the other hand, has assumed that input and output actions must always handshake between components, much like in CSP and CCS. The WP2 model of concurrency is more general than that used by WP3, as handshaking can be explicitly encoded by synchronisation of common input actions. We utilise this property in giving our mapping.

The discussion hereafter requires a basic knowledge of the work described in Chapter 2 of Deliverable D3.3 [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF]. In the following, we try to keep the discussion self-contained, and where that is not possible we provide the reader with references to the specific content of [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF].

Aligning the action sets. WP3 utilises extended LTSs (cf. Definition 2, Chapter 2 of [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF]) for modelling components, which are standard LTSs augmented with final states. Transitions can either be hidden, in which case they are labelled with τ , or are visible and support the communication of data. Let l range over action labels, id 1 , . . . , id m , od 1 , . . . , od n range over data values, and ? and ! be the label prefixes used to denote input actions and output actions respectively. A visible transition of an extended LTS has one of the following forms:

• expectation of action with data and production of return data -all actions of the form ?l(id 1 . . . id m ,od 1 . . . od n ) where both l and id 1 , . . . , id m are expected as input, and od 1 , . . . , od n are produced as output;

• production of action with data and expectation of return data -all actions of the form !l(id 1 . . . id m ,od 1 . . . od n ) where both l and id 1 , . . . , id m are produced as output, and od 1 , . . . , od n are expected as input.

Since Logic IOLTSs (as in Chapter 2) do not deal with data parameters (although an extension has been developed in Chapter 4), we give an explicit representation of each instantiation of the data variables as separate transitions. Thus, analogously to what is done in Section 3.7, we give a transformation that respects the action semantics:

• expectation of action with data and production of return data -each transition labeled with ?l(id 1 . . . id m ,od 1 . . . od n ) is represented by two consecutive transitions labeled with lI id 1 . . . id m of type input and lO od 1 . . . od n of type output;

• production of action with data and expectation of return data -each transition labeled with !l(id 1 . . . id m ,od 1 . . . od n ) is represented by two consecutive transitions labeled with lI id 1 . . . id m of type output and lO od 1 . . . od n of type input.

From extended LTSs to Logic IOLTSs. As our quotient procedure works on Logic IOLTSs, we need to give a semantic preserving mapping from extended LTSs to Logic IOLTSs. Besides converting actions as mentioned previously, we also need to ensure that parallel composition of extended LTSs corresponds to parallel composition on the semantically equivalent Logic IOLTSs. We can achieve this by forcing the CONNECT 231167

Logic IOLTSs to handshake on each communication. Handshaking can be enforced by requiring each action in a component to be preceded by a special handshaking action that is always of type input. The mapping L ensures that each transition of the original extended LTS is split into three parts. The first part corresponds to handshaking so that synchronisation only takes place if all relevant parties agree. After handshaking, the first collection of data items id 1 . . . id m are communicated. Once this has taken place, the data items od 1 . . . od n are transmitted. We indicate that a component is safe to deadlock in a final state by allowing it to perform the -transition. Note that none of the states are inconsistent.

Relating this mapping to WP3, Figure 3.9 shows the transformed extended LTS of the Blue component from Figure 3.6 of D3.3 [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF]. Due to the extensive interface of the component, we indicate the I/O type of actions by the ? and ! symbols after the action name. Note that towards the bottom of the figure, we introduce actions prefixed PlaceOrder2, while in the original model of D3.3 the operation of the corresponding action with data is PlaceOrder. A discrepancy arises between our formalism and that of WP3, in that we assume an action with data has a particular data type. However, in WP3 this is not the case, and moreover is unnecessary as an action with data is treated as an atomic action for synchronisation purposes. As PlaceOrder arises twice with different data types in the original Blue model, we must distinguish the two instances in our formalism, which is why we use PlaceOrder2 for the second such occurrence. Discussion with WP3 is underway to see if we can standardise our approaches.

Formulating the ontological constraints. The mediator synthesis problem in WP2 takes as input the components that need to communicate, together with a component representing the constraints imposed by the ontology. In WP3, however, the ontological constraints are deduced as part of the synthesis algorithm. Thus, in order to map the WP3 mediator synthesis problem to that in WP2, the derived ontological constraints from WP3 need to be fed into WP2. Although we omit the detail here, it suffices to know that the synthesis algorithm in WP3 can be amended to generate these ontological constraints for us.

CONNECT 231167

Obtaining the mediator. Equipped with the ontological constraints represented by a component O, together with the components P and Q represented by Logic IOLTSs L(P) and L(Q), we can obtain the Logic IOLTS mediator M as the unique solution of G/(L(P) || O || L(Q)), if a solution exists, otherwise there is no mediator. As in Section 3.4, the goal has as the output set A L(P) ∪ A L(Q) , and the input set is empty. A trace can only become quiescent in G after a has been witnessed, and there are no inconsistent traces. This formulation of the goal G correlates with the notion of coordination policies (i.e., goal) provided by the WP3 mediator theory [START_REF]CONNECT Deliverable D3.3: Dynamic connector synthesis: revised prototype implementation. FET IP CONNECT EU project, FP7 grant agreement[END_REF].

If the mediator M does not exist for L(P) and L(Q), then there is no mediator allowing P and Q to successfully communicate with one another. If M does exist, then the most general mediator allowing P and Q to communicate is the extended LTS M ′ , obtained from M by collapsing actions back down into the form used by WP3, and stripping out all handshaking and -labelled transitions. Note that in the mediator, the split-form of transitions may not be consecutive, so cannot be collapsed back into a single transition. This fits with the WP3 theory, whereby each transition ?l(id 1 . . . id m , od 1 . . . od n ) or !l(id 1 . . . id m , od 1 . . . od n ) is permitted to be represented by split transitions of the form ?l(id 1 . . . id m , -) and ?l(-, od 1 . . . od n ), or !l(id 1 . . . id m , -) and !l(-, od 1 . . . od n ) respectively.

Summary

In this chapter, we have formalised the mediator synthesis problem as an application of finding the quotient of a collection of components to communicate from a goal specification that guarantees absence of communication mismatches and premature deadlock. We have executed our methodology on two examples, one involving simple messaging, and the other based on the CONNECT-oriented travel agency example of [START_REF] Blair | The role of ontologies in emergent middleware: Supporting interoperability in complex distributed systems[END_REF]. We have linked the work of WPs 2 and 3 by giving a mapping from the extended LTSs of WP3 to the Logic IOLTSs of WP2, which allows us to compare the mediators synthesised by the two approaches. From this we can tell whether the mediator synthesised by WP3 is the most general, and whether it is free of communication errors.

CONNECT 231167 4 Data extension of the specification theory

In this chapter, we extend the formalism for specifying components, presented in Chapter 2, by introducing the ability to model and reason about data. Data can occur as parameters of actions that are used for communication, and can also be stored in variables. The result is a model that covers the register automata developed in WP4 (see Chapter 2 of D4.3 and [START_REF] Cassel | A succinct canonical register automaton model[END_REF]). This model can be used for learning (as we show in Chapter 3 of D 4.3 and [START_REF] Howar | Inferring Canonical Register Automata[END_REF]) and for synthesis of mediators (see D3.3 and this chapter). Our extension is more general than the register automata of WP4 in that it need not impose restrictions (determinism, canonicity) where this is not necessary. The treatment of data in our extension can also be seen as inspired by the treatment of data in I/O-automata [START_REF] Lynch | An introduction to input/output automata[END_REF][START_REF] Jonsson | Compositional specification and verification of distributed systems[END_REF], but the semantical notions (refinement, consistency, etc.) will remain aligned with the theory of logical I/O transition systems presented in Chapter 2. We will present operations for parallel composition and conjunction: these are rather straight-forward adaptations of the corresponding operations in the finitary case. Refinement between two specifications is undecidable in the general case, but sufficient techniques for the problem can be adapted from simulation relations between infinite-state transition systems (e.g., [START_REF] Lynch | An introduction to input/output automata[END_REF][START_REF] Jonsson | Compositional specification and verification of distributed systems[END_REF]).

Continuing the analogy with Chapter 2, we also present an operation of quotient, which can be seen as an inverse of the parallel composition operation. We provide a technique for generating quotients, which provides an algorithm under assumptions that are met in many practical situations. In our data extension, the quotient is not computable for general nondeterministic specifications. However, for the deterministic case, a quotient can be calculated by a fixpoint calculation adapted from controller synthesis (e.g., [START_REF] Thomas | Languages, automata, and logic[END_REF]), based on computations of pre-and postconditions.

In Section 4.4, we illustrate how this operation can be used to formulate (and solve) the problem of generating a most general mediator on the basis of register automata obtained, e.g., by learning. The main purpose of including an application to mediator synthesis is to demonstrate how the algebra developed in this deliverable provides unifying links with the developments of WP3 and WP4. From a CONNECT perspective, the contribution of Section 4.4 (an also of Chapter 3) is to show that the specification theory developed in WP2 can be used to formulate the mediator synthesis problem. We also provide a framework for synthesizing a most general mediator (in a certain technical sense). Note, however, that this procedure may be of unnecessary high complexity and produce unnecessarily general mediators. More specific and efficient approaches to the synthesis problem are presented in Deliverable D3.3. Moreover, the approach in Section 4.4 assumes that suitable information about the relationship between communication primitives and data of two networked components have been extracted, e.g., from an ontology; we do not here consider the problem of how to perform this extraction. In contrast, the approaches presented in Deliverable D3.3 are able to work directly on the information provided by some ontology.

Note on Related Work

Relationships between our specification theory (without data) and previous literature are discussed in Chapter 2. There has been no published work which systematically extends interface automata with data. On the other hand, our data extension follows lines similar to definitions of I/O-automata (e.g., [START_REF] Lynch | An introduction to input/output automata[END_REF][START_REF] Jonsson | Compositional specification and verification of distributed systems[END_REF] and follow-up works). These works do not consider the quotient operation or something analogous.

Concerning our application of the quotient operation for mediator synthesis, there is a related line of work on web service composition, represented by works such as [START_REF] Bertoli | Automated composition of web services via planning in asynchronous domains[END_REF][START_REF] Guermouche | A mediator based approach for services composition[END_REF][START_REF] Berardi | Automatic composition of transition-based semantic web services with messaging[END_REF][START_REF] Hull | E-services: a look behind the curtain[END_REF]. Here, components that represent web services are specified in some formalism as automata that exchange data values. Specifications can be given in different forms, typically in terms of control states that may and must be reached, and in som cases also including dependencies of data values. In contrast to the work presented in this chapter, that line of work is not a part of an overall coherent specification framework. Also, the work does not aim to specify a "best" or "most general" mediator, but merely search for some mediator that fulfills the specified purpose.

A close work is [START_REF] Bertoli | Automated composition of web services via planning in asynchronous domains[END_REF], which presents a the synthesis algorithm based on backward search, which is an adaptation of classical algorithms for solving games over finite graphs (games on finite graphs have been extensively studied, see e.g. [START_REF] Gurevich | Trees, automata, and games[END_REF][START_REF] Gr Ädel | Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar[END_REF][START_REF] Emerson | Tree automata, mu-calculus and determinacy[END_REF][START_REF] Zielonka | Infinite games on finitely coloured graphs with applications to automata on infinite trees[END_REF][START_REF] Thomas | Languages, automata, and logic[END_REF][START_REF] Chatterjee | Algorithms for omega-regular games with imperfect information[END_REF]). A specified property is a combination of safety and reachability, given as a combination of target states together with unsafe states. The algorithm produces loop-free controllers that guarantee that the composed system reaches a target state while avoiding unsafe states. In contrast, our specification is a combination of a safety condition and a deadlock freeness CONNECT 231167 condition; these two kinds of specifications are of incomparable expressive power. One advantage of our type of specification is that synthesized controllers may contain loops. Another difference is that [START_REF] Bertoli | Automated composition of web services via planning in asynchronous domains[END_REF] underapproximates infinite data domains by finite ones, arguing that to achieve enough precision, it is in practical cases enough to use finite domains of very small sizes. We combine the game solving with a knowledge level reasoning similar to [START_REF] Pistore | Automated composition of web services by planning at the knowledge level[END_REF] where the precise values of variables are abstracted into a set of important relations between them, here equalities and inequalities, called knowledge. Since specifications relate values of variables only in terms of equalities and inequalities and since the data are not manipulated in other means than testing equality and sending/receiving, this abstraction is precise. We believe that this kind of abstraction also results in smaller state spaces. For instance, a state of the quotient where the knowledge contains the equality x = y would correspond to a set of states containing a state with x = val and y = val for every value val from the domain of x and y. In knowledge [START_REF] Pistore | Automated composition of web services by planning at the knowledge level[END_REF], it is only discussed how to compute postconditions and perform symbolic forward exploration of state space on the level of knowledge. Our contribution is that we show how to compute preconditions and perform symbolic backward exploration needed for the computation of bad states.

As another remark, we note that Chapter 3 and Section 4.4 use two different techniques for achieving proper synchronization between components, both of which can be regarded as extractable from ontology information. The approach in Chapter 3 extracts explicit ordering between actions, whereas the approach in Section 4.4 extracts ordering which is implicitly defined by data constraints. A related contrasting between such approaches has been made in [START_REF] Marconi | Implicit vs. explicit data-flow requirements in web service composition goals[END_REF]. According to [START_REF] Marconi | Implicit vs. explicit data-flow requirements in web service composition goals[END_REF], none of the two approaches clearly wins: explicit approaches tend to scale better and are easier to write, implicit approaches offer higher degree of reuse and abstraction and clearer separation of components from the composition goal.

Processes: Operational Specifications with Data

In this section, we define our operational model of Logic IOLTS, which also includes data. We will refer to such objects as processes w. data or data-processes.

We assume a finite collection of unbounded domains of data values -each domain is called a sort -and a set of actions. Each action has a certain arity, which is a tuple of sorts that determines which combinations of parameters it may take. A symbol is a term of the form α(d 1 , . . . , d n ), where α is an action, and d 1 , . . . , d n are data values in the appropriate sorts. For a set I of actions, let Σ I be the set of data symbols with an action in I.

We assume a set of (sorted) variables, ranged over by x, y, z, etc., and a set of formal parameters ranged over by p. A parameterized symbol is of form α(p 1 , . . . , p n ), where α is an action, and p 1 , . . . , p n are distinct formal parameters. We assume that each action always uses the same fixed tuple of formal parameters when forming parameterized symbols. A guard is a conjunction of equalities and negated equalities over variables and formal parameters.

Remark: Our theory can with modest effort be extended to cover richer sets of functions and predicates, rather than just equalities and negated equalities. In this version, we restrict to equalities.

Let us define our notion of data-processes (i.e., Logic IOLTS with data), which is actually very similar to the register automata defined in Chapter 2 of D4.3 (see also [START_REF] Cassel | A succinct canonical register automaton model[END_REF]). Definition 4.1 A data-process P is a tuple P = (I P , O P , L P , ℓ 0 P , X P , δ P , ϕ F P ), where • I P is a finite set of input actions,

• O P is a finite set of output actions,

• L P is a finite set of locations,

• ℓ 0 P ∈ L P is the initial location • X P is a set of (sorted) variables, each of which has a defined initial value.

• δ P is a finite set of transitions, each of which is of form ℓ, stmt, ℓ ′ where stmt is a statement of form g ; α(p 1 , . . . , p n ); y 1 , . . . , y k := z 1 , . . . , z k , where CONNECT 231167

We can now reuse the definitions in Section 2.3, and define a mapping • D from data-processes to declarative specifications (see Definition 2.1) by P D = P Op * . In the following, we will often use the set of safe traces ST P , defined in Definition 2.19, as a characterization of the behavior of a process.

For future development, we will sometimes use an alternative, but equivalent, definition of refinement, which is phrased in terms of the sets of safe traces of Q and P, by adapting the definition of alternating simulation [START_REF] Alfaro | Interface automata[END_REF]. Proposition 4.3 Assume that P and Q are processes with nonempty sets of safe traces. Then Q ⊑ dec P iff: I P ⊆ I Q , and O Q ⊆ O P , and • whenever t is a safe trace of both P and Q (i.e., t ∈ ST P ∩ ST Q ), then

-for any input symbol i, if ti ∈ ST P then ti ∈ ST Q , -for any output symbol o, if to ∈ ST Q then to ∈ ST P . ⊓ ⊔
Thus, the extensional semantics can be characterized by the set of safe traces.

There are different (incomplete) techniques for establishing Q ⊑ dec P when Q and P are dataprocesses, including simulation [START_REF] Jonsson | Compositional specification and verification of distributed systems[END_REF]. We note that in general, the problem of checking Q ⊑ dec P is undecidable. This follows from the undecidability of checking universality for register automata [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF].

Parallel Composition

Let us now adapt the definition of parallel composition (Definition 2.28) to data-processes. Intuitively, the parallel composition operator yields the combined effect of its operands running asynchronously. We use a model of communication in which an output from a component can be received by multiple components in the environment: this means that we use a broadcast model of communication. An input ?a( d) and output !a( d) combine to form an output !a( d) (as in certain variants of I/O automata), rather than a hidden action τ as is the case in Milner's CCS. Note that the attributes ? and ! on actions (as in !a()) are not part of the actions, they serve only to remind that the action in question is an input or output in the considered context.

Two data-processes P = (I P , O P , L P , ℓ 0 P , X P , δ P , ϕ F P ) and

Q = (I Q , O Q , L Q , ℓ 0 Q , X Q , δ Q , ϕ F Q ) are com- posable if O P ∩ O Q = ∅ and X P ∩ X Q = ∅.
As a building block for the definition of parallel composition on data-processes, let us define the parallel composition of two statements stmt 1 = g 1 ; α(p); y 1 := z 1 and stmt 2 = g 2 ; α(p); y 2 := z 2 with the same action α, in two processes with disjoint sets of variables, as

stmt 1 stmt 2 = g 1 ∧ g 2 ; α(p); y 1 , y 2 := z 1 , z 2 .
In the special case where stmt 1 is an output statement of form g 1 ; α(x); y 1 := z 1 stmt 2 is an input statement of form α(p); y 1 := p 1 , then stmt 1 stmt 2 can be written as g 1 ; α(x); y 1 , y 2 := z 1 , p 1 [x/p]. For an action α and a process P, let g α P,ℓ P denote the disjunction of the guards of the outgoing α-statements from ℓ P : if there is no such statement, then g α P,ℓ P is defined as false. We are now ready for the definition of parallel composition. But first, given processes P and Q let us define a mapping, denoted Incompat P||Q from pairs of locations of P and Q to boolean combinations of equalities and inequalities over the state variables of P and Q, such that Incompat P||Q ( ℓ P , ℓ Q ) is true if P in location ℓ P can produce an output symbol for which Q does not have a matching input step, or vice versa. Formally, we can represent Incompat P||Q ( ℓ P , ℓ Q ) as a disjunction, which for each synchronizing action α ∈ O P ∩ I Q contains the disjunct g α P,ℓ P ∧ ¬g α Q,ℓ Q , and symmetrically for each synchronizing action α ∈ O Q ∩ I P contains the disjunct g α Q,ℓ Q ∧ ¬g α P,ℓ P .

Definition 4.4

The parallel composition of two composable data-processes P = (I P , O P , L P , ℓ 0 P , X P , δ P , ϕ F P ) and

Q = (I Q , O Q , L Q , ℓ 0 Q , X Q , δ Q , ϕ F Q ), denoted P Q, is obtained as P Q = (I P||Q , O P||Q , L P||Q , ℓ 0 P||Q , X P||Q , δ P||Q , ϕ F P||Q )
, where

• I P||Q = (I P ∪ I Q ) \ O P||Q , CONNECT 231167 50/86 • O P||Q = O P ∪ O Q , • L P||Q = L P × L Q , • ℓ 0 P||Q = ℓ 0 P , ℓ 0 Q , • X P||Q = X P ∪ X Q ,
• δ P||Q is obtained from δ P and δ Q by two forms of transitions.

-If ℓ P , stmt, ℓ ′ P ∈ δ P has an action which is not an action of Q, (i.e., it is non-synchronizing),

then ℓ P , ℓ Q , stmt, ℓ ′ P , ℓ Q ∈ δ P||Q for any location ℓ Q ∈ L Q . -Symmetrically, if ℓ Q , stmt, ℓ ′ Q ∈ δ
has an action which is not an action of P, then ℓ P , ℓ Q , stmt, ℓ P , ℓ ′ Q ∈ δ P||Q for any location ℓ P ∈ L P .

-

If ℓ P , stmt P , ℓ ′ P ∈ δ P and ℓ Q , stmt Q , ℓ ′ Q ∈ δ Q have the same action, i.e., they synchronize, then ℓ P , ℓ Q , stmt P stmt Q , ℓ ′ P , ℓ ′ Q ∈-→. • ϕ F P||Q is defined by ϕ F P||Q ( ℓ P , ℓ Q ) = ϕ F P (ℓ P ) ∨ ϕ F Q (ℓ Q ) ∨ Incompat P||Q ( ℓ P , ℓ Q ). ⊓ ⊔
We remark that this form of parallel composition is slightly different from the form of Definition 2.28. In particular, Definition 2.28 does not include a term that correspond to the "incompatibility" predicate. This is because Definition 2.28 assumes that the processes to be composed are error-completed, which implies that incompatibility of a composed state is simply the disjunction of the inconsistency predicates on the two components.

Definition of Parallel Composition in Terms of Safe Traces

As a preparation for the definition of Quotient in Section 4.4, we will show how parallel composition can be defined on the basis of safe traces of participating data-processes.

Extend the definition of Incompat P||Q to traces of P || Q by saying that Incompat P||Q (t) is true if there is a state ℓ P , ℓ Q , σ of P || Q such that ℓ 0,P , ℓ 0,Q ℓ 0 , σ 0 t =⇒ P ℓ P , ℓ Q , σ , where ℓ 0,P , ℓ 0,Q , σ 0 is the initial state of P || Q, and such that σ |= Incompat P||Q ( ℓ P , ℓ Q ).

For a trace t and a set I of actions, define t ↾ I as the subsequence of t consisting of symbols in Σ I . Define ST P || ST Q as the set of traces t ∈ (Σ

I P||Q ∪ Σ O P||Q ) * with t ↾ (I P ∪ O P ) ∈ ST P and t ↾ (I Q ∪ O Q ) ∈ ST Q . Then

Conjunction

In this section we define a conjunctive operator on data-processes that corresponds to the meet operation on the refinement preorder. Although our formulation shares similarities with Definition 2.30, we do not consider the error-completion of components in this chapter, so we must explicitly handle non-enabled inputs. Let P = (I P , O P , L P , ℓ 0 P , X P , δ P , ϕ F P ) and

Q = (I Q , O Q , L Q , ℓ 0 Q , X Q , δ Q , ϕ F Q )
be two data-processes, and let stmt P = g P ; α P (p P ); y P := z P and stmt Q = g Q ; α Q (p Q ); y Q := z Q be statements of P and Q respectively. We say that P and Q are composable for conjunction only if [START_REF] Berardi | Automatic composition of transition-based semantic web services with messaging[END_REF] The conjunction of two composable data-processes P and Q, denoted P ∧ Q, is the dataprocess (I P∧Q , O P∧Q , L P∧Q , ℓ 0 P∧Q , X P∧Q , δ P∧Q , ϕ F P∧Q ), where:

I P ∪ I Q is disjoint from O P ∪ O Q , and X P ∩ X Q = ∅. Definition 4.
• I P∧Q = I P ∪ I Q CONNECT 231167 51/86 • O P∧Q = O P ∩ O Q • L P∧Q = (L P × L Q ) ∪ L P ∪ L Q • ℓ 0 P∧Q = ℓ 0 P if ¬ϕ F P (ℓ 0 P ) ∧ ϕ F Q (ℓ 0 Q ), ℓ 0 Q if ϕ F P (ℓ 0 P ) ∧ ¬ϕ F Q (ℓ 0 Q ), and ℓ 0 P , ℓ 0 Q otherwise • X P∧Q = X P ∪ X Q
• δ P∧Q is the smallest set satisfying:

-If ℓ P , stmt P , ℓ ′ P ∈ δ P , ℓ Q , stmt Q , ℓ ′ Q ∈ δ Q , α P = α Q , ¬ϕ F P (ℓ P ) and ¬ϕ F Q (ℓ Q ), then ℓ P , ℓ Q , stmt P || stmtQ, ℓ ′ P , ℓ ′ Q ∈ δ P||Q -If ℓ P , stmt P , ℓ ′ P ∈ δ P , α P ∈ I P ∩I Q then ℓ P , ℓ Q , (g P ∧¬g α P Q,ℓ Q ) ; α P (p P ); y P := z P , ℓ ′ P ∈ δ P||Q -If ℓ Q , stmt Q , ℓ ′ Q ∈ δ Q , α Q ∈ I P ∩ I Q then ℓ P , ℓ Q , (g ′ P ∧ ¬g α Q P,ℓ P ); α Q (p Q ); y Q := z Q , ℓ ′ Q ∈ δ P||Q -If ℓ P , stmt P , ℓ ′ P ∈ δ P , and α P ∈ I P \ I Q or ϕ F Q (ℓ Q ), then ℓ P , ℓ Q , stmt P , ℓ ′ P ∈ δ P||Q -If ℓ Q , stmt Q , ℓ ′ Q ∈ δ Q , and α Q ∈ I Q \ I P or ϕ F P (ℓ P ), then ℓ P , ℓ Q , stmt Q , ℓ ′ Q ∈ δ P||Q -If ℓ P , stmt P , ℓ ′ P ∈ δ P and α P ∈ I P∧Q ∪ O P∧Q , then ℓ P , stmt P , ℓ ′ P ∈ δ P||Q -If ℓ Q , stmt Q , ℓ ′ Q ∈ δ Q and α Q ∈ I P∧Q ∪ O P∧Q , then ℓ Q , stmt Q , ℓ ′ Q ∈ δ P||Q .
• ϕ F P||Q is defined by:

-ϕ F P||Q ( ℓ P , ℓ Q ) ⇐⇒ ϕ F P (ℓ P ) ∧ ϕ F Q (ℓ Q ) -ϕ F P||Q (ℓ P ) ⇐⇒ ϕ F P (ℓ P ) -ϕ F P||Q (ℓ Q ) ⇐⇒ ϕ F Q (ℓ Q ). ⊓ ⊔

Quotient

In analogy with the development in Section 2.2.4, we consider the quotient operation, which can be seen as an "inverse" of parallel composition and therefore has a connection to synthesis. Given a specification for a system R, together with a component P implementing part of R, the quotient, denoted R \ P, yields the least refined (in the sense of ⊑) process for the remaining part of R, i.e., such that P || (R \ P) ⊑ R. Therefore, quotient can be thought of as an adjoint of parallel composition.

Looking at the treatment of sets of actions in Definition 4.4, we see that a necessary requirement for the existence of a quotient is that O P ⊆ O R . Then, the set of output actions of the quotient must be O R \ O P . However, there is some freedom for the set I R\P of input actions of the quotient. From Definition 4.4, we take as a natural choice I R\P to be (O P ∪ I R ), since a quotient with these actions will always exist if there is one with a smaller set, and since the subsequently presented technique to produce a quotient will not have to consider the difficulties that come with actions that are not visible by the quotient.

Say that a symbol α( d) may be disabled after a trace t if t is the sequence of symbols in a computation, which ends in a state where α( d) is not enabled. I.e., if there is a state ℓ, σ , such that ℓ 0 , σ 0 t =⇒ P ℓ, σ , where ℓ 0 , σ 0 is the initial state, and such that α( d) is not enabled in ℓ, σ .

We can now construct the safe traces of the quotient R \ P by first defining the situations that should be avoided when P is composed with R \ P. As follows from Proposition 4.3, these are that after some safe trace t of R, 1. for an input symbol i of R, the symbol i may be disabled after t ↾ (I P ∪ O P ) in P, and 2. for an output symbol o of P, the trace to ↾ (I P ∪ O P ) is a safe trace of P but the trace to is not a safe trace of R.

Let us define the set F P✄R as the set of safe traces of R for which one of the above situations occur. The safe traces ST R\P of the quotient can now be obtained as the maximal prefix-closed subset of ST R such that if t ∈ ST R\P , then CONNECT 231167 52/86

• t ∈ F P✄R , and

• if to ∈ ST R for some output action o ∈ Σ (O R \O P ) , then to ∈ ST R\P .
This construction is similar in spirit to the one defined for deterministic interface automata without data by Bhaduri and Ramesh [START_REF] Bhaduri | Interface synthesis and protocol conversion[END_REF]. The alphabet of the quotient contains all of the actions of R and P so that R \ P can control as much as possible P and emulate the behaviour of R. Yet still, simple examples reveal that there may not exist a component Q over an interface consisting of input actions I R\P and output actions O R\P such that P || Q ⊑ dec R. Unfortunately, the existence of the quotient cannot be ascertained by a syntactic check on the alphabets of P and R.

In fact, for data-processes the question whether there exists a quotient is undecidable. This follows from the result that checking refinement between data-processes is undecidable (which follows from [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF]).

Reformulating the Quotient Problem as a Synthesis Problem

Let us in this section provide a more constructive construction of the quotient, as a process of the generic form proposed in Definition 4.1. In the treatment in this subsection, we often use Q to refer to the quotient R \ P.

Due to the undecidability result referred to at the end of the previous section, our construction of qoutient will assume that processes P and R are deterministic (this concept will soon be defined). In this case, we will construct the quotient Q as the least refined deterministic process, whose set of safe traces satisfies the condition stated at the end of the previous subsection. To make these conditions more concrete, we will first rephrase the problem of finding a qoutient Q into a problem of finding a most general process Q whose parallel composition with a given process is guaranteed not to reach an inconsistent state. This "given process", which we denote P ✄ R, is constructed from P and R by synchronizing their actions, in a way similar to, but not the same as, the parallel composition of P and R. The resulting synthesis problem has a simpler structure, and can be addressed by adapting techniques from controller synthesis. We therefore think that this reformulation is a way to make our approach clearer.

Let us now perform these things.

Definition 4.7

We define a process P to be deterministic if for every location, guards of different transititons starting from the location with the same action are mutually exclusive. Formally, for any two transitions ℓ , g 1 ; α(p); ȳ1 := z1 , ℓ ′ 1 , ℓ , g 2 ; α(¯p);¯y 2 :=¯z 2 , ℓ ′ 2 ∈ δP and for any valuation σ of variables of X P and parameters of p, it holds that σ |= ¬g 1 ∨ ¬g 2 .

⊓ ⊔

Let us remark that the restriction to deterministic processes is not as severe as one might first think. For instance, it is possible to model processes that nondeterministically generate identifiers, sequence numbers, etc. by suitable modeling techniques. Consider for instance, a process which nondeterministically selects an identifier, assigns it to a variable id and then transmits it in an action showid(p), where p is id. We can represent this behavior by a single transition which is labeled by true ; showid(p) ; id := p .

Note that the transition has no guard (or more precisely, the guard is true). Thus the parameter of showid can be an arbitrary identifier. We have just slightly remodeled the process so that id is assigned in connection with the transition, rather than before the transition; the external behavior remains the same. We use this modeling idiom in several of the examples of Section 4.5.

We will from now on consider the quotient construction R \ P for the case that both R and P are deterministic.

The structure of our construction is the following. We first construct a new process, denoted P ✄ R, which "summarizes" the requirements on Q that are imposed by P and R. The process P ✄ R has the CONNECT 231167 property that the problem of finding a process Q such that P || Q ⊑ R is transformed into the (conceptually simpler) problem of finding a process Q which interacts with P ✄ R without causing an inconsistency. We thereafter show how to find such a Q by adaptation of controller synthesis techniques.

We construct the process P ✄R as the process obtained by running P and R in parallel, synchronizing on common symbols.

As a first step, given processes P and R, let us define a mapping NotRefine P✄R from pairs of locations of P and R to predicates such that NotRefine P✄R ( ℓ P , ℓ R ) is true in the situations that should be avoided, according to Criterion 1 or 2 above. We can represent NotRefine P✄R ( ℓ P , ℓ R ) as a disjunction, which for input action α ∈ I R of R with α ∈ I P contains the disjunct g α R,ℓ R ∧ ¬g α P,ℓ P , and which for each output action α ∈ O P of P contains the disjunct g α P,ℓ P ∧ ¬g α R,ℓ R .

Definition 4.8

The synchronization P ✄ R of two processes P = (I P , O P , L P , ℓ 0 P , X P , δ P , ϕ F P ) and R =

(I R , O R , L R , ℓ 0 R , X R , δ R , ϕ F R ), is obtained as P ✄ R = (I P✄R , O P✄R , L P✄R , ℓ 0 P✄R , X P✄R , δ P✄R , ϕ F P✄R )
, where

• I P✄R = O R \ O P , • O P✄R = O P ∪ I R , • L P✄R = L P × L R , • ℓ 0 P✄R = ℓ 0 P , ℓ 0 R , • X P✄R = X P ∪ X R ,
• δ P✄R is obtained from δ P and δ R by two forms of transitions.

-If ℓ R , stmt, ℓ ′ R ∈ δ R has an action which is not an action of P, then ℓ P , ℓ R , stmt, ℓ P , ℓ ′ R ∈ δ P✄R for any location ℓ P ∈ L P .

-If ℓ P , stmt P , ℓ ′ P ∈ δ P and ℓ R , stmt R , ℓ ′ R ∈ δ R have the same action, i.e., they synchronize, then ℓ P , ℓ R , stmt P stmt R , ℓ ′ P , ℓ ′ R ∈ δ P✄R .

• ϕ F P✄R is defined as

ϕ F P✄R ( ℓ P , ℓ R ) = ϕ F P ( ℓ P ) ∧ ¬ϕ F R ( ℓ R ) ∨ NotRefine P✄R ( ℓ P , ℓ R ) .

⊓ ⊔

Having defined the auxiliary process P ✄ R, we can now reformulate the quotient problem into a more standard synthesis problem Definition 4.9 We say that processes P and Q collaborate harmoniously if I Q = O P and O Q = I P , and P || Q has a nonempty set of safe traces.

Intuitively, P and Q collaborate harmoniously if neither P nor Q will produce an output symbol which the other process is not prepared to receive, or which causes some process to reach an inconsistency. We now get Proposition 4.10 Let P and R be as assumed above, such that

(I P ∪ O P ) ⊆ (I R ∪ O R ) and O P ⊆ O R . Let Q be a process with I Q = O P ∪ I R and O Q = O R \ O P . Then P || Q ⊑ R iff (P ✄ R) and Q collaborate harmoniously. ⊓ ⊔ CONNECT 231167

Solving the Synthesis Problem

If P and R are as above, then it follows that (P ✄ R) is deterministic. Due to Proposition 4.10, we will from now on consider the following synthesis problem:

Given a deterministic process P, find the least refined process Q such that P and Q collaborate harmoniously.

To be able to collaborate harmoniously, Q should maintain as much relevant information as possible about the "current states" of P. More precisely, from the past sequence of exchanged symbols, Q can infer the current location of P and values of its variables. A most general Q should keep track of this information, since any piece of it may become important when performing an output action. A process Q which has remembered more of this information can do "better" choices than a process which has remembered less, and so can be at least as general. The restriction to deterministic processes guarantees that Q can maintain complete information about the location and values of variables of P.

Our solution to the synthesis problem is essentially obtained using two constructions. We first define a control skeleton S for Q. It stores the location of P in its control location (i.e., its locations are locations of P), its input and output actions are O P and I P , it contains a primed variable x ′ for each variable x of P, and in every location ℓ P , it may perform transitions which synchronise with actions that P can perform in ℓ P . It copies the guards of P and the assignments performed by P (but replaces occurrences of variables of P in the guards by their primed counterpart). This means that when S synchronises with an input statement of P, it transmits an arbitrary value (it does not guard the formal parameters by any additional guard). When S synchronises with an output statement of P, it records newly generated values created and sent by P. For instance, in the case the statement of P is of the form !α(p); x := x, S stores p to the primed variable x ′ . The control skeleton is formally defined as the process S = (I S , O S , L S , ℓ 0 S , X S , δ S , ϕ F S ), where

• I S = O P , • O S = I P , • L S = L P , • ℓ 0 S = ℓ 0 P , • X S = {x ′ | x ∈ X P },
• ϕ F S assigns false to every location of S, • δ P contains a transition ℓ, g ′ ; α(p 1 , . . . , p n ), ℓ ′ ; x′ :=¯z ′ for every transition ℓ, g; α(p 1 , . . . , p n ); x := z, ℓ ′ of P where g ′ , x ′ , and z ′ are obtained from g, x, and z by replacing occurrences of variables of X P by their primed versions.

Q will be later obtained from S by refining its transitions by additional guards that ensure that P || Q avoids inconsistent traces. To achieve this, the guards on transitions of Q should prevent computations of P || Q to reach a bad state, which is either an inconsistent state or a state from where Q cannot prevent P || Q to reach a bad state. Since we are interested in the least refined process Q, we want to add as weak guards as possible.

We will show how to compute a characterisation of bad states in a form of a function Bad which assigns to every state ℓ P of P a boolean formula Bad (ℓ P ) over equalities and inequalities over X P . A state ℓ P , ℓ S , σ of P || S is bad iff σ restricted to X P satisfies Bad (ℓ P ).

Computing Bad States

Calculation of Bad is the key step in the synthesis process. It corresponds to computation of a controller invariant for Q. It is done by starting from the set of inconsistent states given by the mapping ϕ F P . From the set of inconsistent states, we derive the set of bad states, which is done by taking predecessors of inconsistent and also bad states under statements that are not output statements of S. Predecessor computation is performed as follows. Let ϕ be a knowledge predicate. Then

pre(x := y ; ϕ) = ϕ[y/x] pre(g; ϕ) = ϕ ∧ g CONNECT 231167 55/86
We can put the above rules together to derive the precondition of a statement as follows.

pre(g; α(p); y

:= z ; ϕ) = ∃p . (g ∧ ϕ[z/y])
Application of an existential quantifier here involves two steps, saturation and elimination. Assume that ϕ is a formula in disjunctive normal form (DNF) over equalities and inequalities over a set of variables. Formula ∃(x 1 , . . . , x n ) . ϕ is obtained by transforming every clause of ϕ in the following way:

1. Saturation: (a) saturate equalities, i.e. compute the transitive and reflexive closure of the equality relation =; (b) saturate inequalities, i.e. include an inequality x = y whenever there is some z with x = z ∧ z = y.

2. Elimination: remove all predicates involving some of x 1 , . . . , x n .

We can now give an algorithm for computing Bad , presented as Algorithm 1. Having computed Bad , we compute Q from S. We first obtain safe as the complement of Bad . Then Q is the process

Q = (I Q , O Q , L Q , ℓ 0 Q , X Q , δ Q , ϕ F Q ) where • I Q = O S , • O Q = I S , • L Q = L S , • ℓ 0 Q = ℓ 0 S ,
• X Q = X S , and

• ϕ F Q = ϕ F S .
The input transitions of Q are the same as the input transitions of S. Output transitions of Q will be obtained from output transitions of S by equipping them with additional guards which keep computations of P || Q within safe. For every output transition ℓ P , stmt, ℓ ′ P of S, there is a unique corresponding input transition ℓ P , stmt ′ , ℓ ′ P of P. Let stmt || stmt ′ be of form g; α(p); y := z. We calculate the precondition wrt. safe(ℓ ′ P ) as ψ ∃X P . g ∧ safe(ℓ ′ P )[z/y]. Thereafter, the transition ℓ P , ψ ∧ stmt ′ , ℓ ′ P is added to Q.

Pruning Q

The Q obtained by the above method satisfies the requirement for being a least refined process such that P and Q collaborate harmoniously. However, it may contain a significant amount of redundancy. Some of its states can never be reached, some transitions can never be taken, and some parts of conditions within guards are true for every computation reaching the source location of the transition.

To obtain a more optimal solution, we will prune the redundant parts of Q. We compute the function Reach that for every state ℓ P , ℓ Q of P || Q returns a formula Reach( ℓ P , ℓ Q ) such that there exists CONNECT 231167 56/86 a computation of P || Q reaching a state ℓ P , ℓ Q , σ iff σ satisfies Reach( ℓ P , ℓ Q ). The algorithm for computing Reach is given below. Then, for every state ℓ Q of Q, we will compute

Reach(ℓ Q ) = ∃X P . ℓ P ∈L P Reach( ℓ P , ℓ Q )
The formula Reach(ℓ Q ) characterises all possible valuations of variables of Q that can appear in a computation of P || Q together with ℓ Q . We then prune Q as follows:

• remove states ℓ Q such that Reach(ℓ Q ) = false • remove transitions ℓ Q , g; α(p); y := z, ℓ ′ Q such that Reach(ℓ Q ) ⇒ ¬g • For each transition ℓ Q , g; α(p); y := z, ℓ ′
Q , we replace the guard g by Reach(ℓ Q ) ⇒ g (and possibly transform this formula to DNF and remove redundant literals and clauses).

We will compute values of Reach for states of P || Q by abstract postcondition computation on P || Q starting from the strongest condition that holds in its initial state. To do this, we will need to compute postconditions for predicates with respect to the different forms of synchronization statements in processes. Let ϕ be a formula over equalities and inequalities over X P||Q . Then

post(x := y ; ϕ) = (∃x.ϕ) ∧ x = y post(g; ϕ) = ϕ ∧ g
We can put the above rules together to derive the postcondition of a statement as follows.

post(g; α(p); y

:= z ; ϕ) = ∃p . (∃y . (g ∧ ϕ) ∧ y = z)
Let ϕ 0 be the strongest predicate satisfied by the initial valuation of P || Q. The computation of Reach is then carried out by Algorithm 2.

Algorithm 2: Computing Reach

Initialise Reach as ϕ 0 for ℓ 0 P , ℓ 0 Q and false otherwise;

1 repeat 2
Reach prev := Reach;

3 forall transitions ℓ P , ℓ Q , stmt, ℓ ′ P , ℓ ′ Q of P || Q do 4 Reach( ℓ ′ P , ℓ ′ Q ) := Reach( ℓ ′ P , ℓ ′ Q ) ∨ post(stmt; Reach( ℓ P , ℓ Q )) 5 until Reach = Reach prev ; 6

Modelling Deadlock

In analogy with the treatment in Chapter 3, we also extend our framework so that it allows specification of deadlock freeness properties and subsequently synthesis of quotients that guarantee the deadlock freeness properties. We say that a state ℓ, σ of a computation of a process P is deadlock if no output transition can be taken from ℓ in the current valuation σ without reaching a bad state. Formally, we specify deadlock as the predicate Deadlock Bad P parametrised by Bad as follows

Deadlock Bad P (ℓ) ℓ , g;α( p);x:=ȳ , ℓ ′ ∈δ P α∈I P ∀p . g =⇒ Bad (ℓ ′ )[ȳ/x]
(Deadlock Bad P (ℓ) is automatically true if ℓ has no output transitions). We specify in which situations a process is allowed to deadlock by providing a specification of the so called quiescent states. Similarly as ϕ F P , the map Quiescent P maps each location to a boolean combination of equalities and negated equalities over variables in X P . A consistent computation is not allowed to reach a deadlock state which is not quiescent. That means that a computation is now inconsistent if it contains a state ℓ, σ such that

σ |= ϕ F P (ℓ) ∨ Deadlock Bad P (ℓ) ∧ ¬Quiescent P (ℓ) .
CONNECT 231167

l 0 l 1 l 2 l 3 l 4 m 0 m 1 m 2 m 3
CFRing XMPP CONNECT 231167 processes reach their terminal states, we define Quiescent R to be false for r 0 , r 1 and true for r 2 . We follow the scheme of the previous sections, and compute first the process CFRing || XMPP showed in Figure 4.3 which inherits all the transitions of CFRing and XMPP unsynchronized. We are looking for the least refined process Q such that (CFRing || XMPP ) || Q ⊑ R. The next step is the construction of the process P = (CFRing || XMPP ) ✄ R, which is shown in Figure 4.4. Notice that its only quiescent state is l 4 , m 3 , r 2 . This is, Quiescent P ( l 4 , m 3 , r 2 ) = true and it evaluates to false for all the other locations of P. Q will now be obtained as the least refined process such that Q || P cannot reach an inconsistent state. The inconsistent states here are only those which are deadlock and not quiescent. Since Bad (ℓ P ) is initially false for all locations of P, the computation starts by evaluating Deadlock Bad P . Let us pick the location ℓ = l 3 , m 2 , r 1 . Deadlock Bad P (ℓ) evaluates initially to the disjunction ϕ = id1 = id2 ∨ msg1 = msg2 which falsifies the guard of the only output transition of ℓ (leading to l 4 , m 4 , r 2 ). We set Bad (ℓ) to ϕ and we then propagate Bad (ℓ) = ϕ backwards via output transitions of P. We compute the precondition of ϕ with respect to the transition from ℓ ′ = l 2 , m 2 , r 1 to ℓ. We see that it becomes true (particularly, the disjunct id2 = id1 is first transformed into id2 = p which is then turned into true by the existential quantification over p). We set Bad (ℓ ′ ) to true which means that Q must avoid visiting ℓ ′ in all situations. Notice that it is indeed the case that if Q allows XMPP to reach state m 2 (where the value of msg2 is already fixed) before msg1 is generated by CFRing, then Q cannot guarantee msg1 = msg2 at the end of the communication which may lead to an undesired deadlock. Let us now look at the precondition of ϕ wrt. the transition from l 3 , m 1 , r 1 . Since Bad (ℓ) is now ϕ, Deadlock Bad P ( l 3 , m 1 , r 1 ) evaluates to id2 = id1 (particularly, the disjunct msg1 = msg2 turns into msg1 = p which after the universal quantification over p becomes false). Intuitively, this reflects the fact that when CFRing is in state l 3 and XMPP in state m 1 , the values of id1 and id2 should be already equal since they cannot become equal otherwise. The rest of the symbolic backward computation of Bad is carried out analogously.

r 0 r 1 r 2 R !start() !msgout(p) !msgin(p) !id(p) !who(p) p 1 = p 3 ∧ p 2 = p 4 ; ! (p 1 , p 2 , p 3 , p 4 )
l 0 , m 0 l 1 , m 0 l 2 , m 0 l 3 , m 0 l 0 , m 1 l 1 , m 1 l 2 , m 1 l 3 , m 1 l 0 , m 2 l 1 , m 2 l 2 , m 2 l 3 , m 2
The construction of Q starts by assembling its control skeleton S depicted in Figure 4.5. Guards are then added to its transitions to guarantee that any computation stays in safe. Finally, we prune unreachable states, useless transitions, and redundant guard conditions as described in Section 4.4.2. The resulting mediator Q is in Figure 4.6.

Booking Seats

The next example is given as an incompatible client Client and a server Server shown in Figure 4.7 which are meant to implement a service for booking seats in a theatre. Our task is again to synthesize a mediator Q. The goal is to achieve that both processes arrive to the end of the transaction and when this happens, they agree on all important values. This is specified by process R in Figure 4 CONNECT 231167 as true for r 2 and false otherwise. As before, we take P = (Client || Server ) ✄ R and construct Q as the least refined process such that (P ✄ R) || Q cannot reach an inconsistent state. The mediator Q obtained by our synthesis algorithm from Section 4.4.2 is in Figure 4.9.

.8. Quiescent R is defined CONNECT 231167 l 0 , m 0 , r 0 l 1 , m 0 , r 1 l 2 , m 0 , r 1 l 3 , m 0 , r 1 l 1 , m 1 , r 1 l 2 , m 1 , r 1 l 3 , m 1 , r 1 l 1 , m 2 , r 1 l 2 , m 2 , r 1 l 3 , m 2 ,
l 0 , m 0 , r 0 l 1 , m 0 , r 1 l 2 , m 0 , r 1 l 3 , m 0 , r 1 l 1 , m 1 , r 1 l 2 , m 1 , r 1 l 3 , m 1 , r 1 l 1 , m 2 , r 1 l 2 , m 2 , r 1 l 3 , m 2 ,

E-Commerce

The following example is slightly more complex than previous ones. We are given a client and a customer service applications in Figure 4.10 that together are supposed to implement an e-commerce service, but are incompatible. The client Blue first starts by sending its id and expects to receive an id of a new order. Then it orders a number of items in some quantities using the AddOrder action, provides its payment informations using P laceOrder action, and expects all items together with its quantities to be confirmed by the customer service. It blocks in the case that it does not receive the right confirmation. The client then announces that he is ready to quit the transaction and expects to receive the result of the payment transaction Result.

The customer service M oon expects to receive the clients id, then it sends a confirmation and sends an id of a new order, together with a client verification. It is then prepared to repeat a loop in which it 1) receives an order of an item, 2) receives a quantity in which the item is ordered, and 3) confirms that the item in the given quantity is ordered. After that, it receives payment information, it arranges the payment via a third party service (which is invisible to the client and not modelled here), and sends the result of the payment transaction.

Ideally, we would like to model the scenario where the client can order any number of items. However, our modelling mechanism allows only processes with a finite number of variables. This scenario would require processes with unbounded number of variables both for specification of Blue and M oon services and for specification, as well as for mediator. We must restrict ourselves to the case where the number of ordered items is bounded by a constant n, which becomes a parameter of the synthesis problem.

We assume that variables of the same sort are initialised with the same initial values ⊥. For instance, all variables item 1 , item 2 , Item 1 , Item 2 have the same initial value ⊥.

The specification (parameterised by the maximum number of ordered items n) is given by the process R(n) in Figure 4.11. Quiescent R is defined as true for r 2 and false otherwise. Similarly as in the previous examples, R captures that both sides finish the transaction and that at the end of the transaction, both sides agree on all the important values.

The synthesised mediator for the case when n = 2 is shown in Figure 4.12. It was obtained as the least refined process Q(2) such that ((Blue(2) || M oon(2)) ✄ R(2)) || Q(2) does not generate an inconsistent trace and subsequently pruned as described in Section 4.4.2. The figure displays only the component of states of Q(2) which is a states of Blue(2) || M oon [START_REF] Abadi | Conjoining specifications[END_REF].

The mediator first brings the system to the point when Blue has ordered its first item (the state b 1 2 , m 0 3a ). It can now decide to start forwarding the first order to M oon (vertical transitions). At the same time, it has to be ready to receive either the second order or the credit card details from Blue (the horizontal transitions). If Blue ordered also the second item, the mediator will forward the second order to M oon after it has forwarded the first one. The mediator will send the payment credit card details to M oon only a after it has received it from Blue and after it has forwarded all orders of Blue (this is taken care of by the guard of the statement stmt * d ). It waits for Blue to confirm all orders. Sending confirmations to Blue is independent from receiving confirmations from M oon since to send the right confirmations, the mediator only needs to know what was ordered by Blue. The communication with Blue and M oon can be interleaved in many ways.

Summary and Future Work

We have extended the compositional specification theory in Chapter 2 with data, using mechanisms that have been naturally adapted from similar other works in the literature. The resulting theory naturally bridges the models developed and used in WP4 (see Chapter 2 of D4.3), and can also be used to formulate the synthesis problem addressed in WP3, as we illustrated on some examples. A major contribution is the integration of these elements in a single specification framework. As future work, it remains to implement and evaluate the most important mechanisms of the theory, as well as to extend the framework for solving of quotients to more general specifications. The extension can be done along two dimensions. One is to handle nondeterministic processes, which brings the problem of uncertainty -the connector cannot be completely sure about the state of the controlled system. Another dimension is to extend the speficiation framework to cover liveness properties. Such extensions have been considered for the finite-state case in the literature (see, e.g., [START_REF] Chatterjee | Algorithms for omega-regular games with imperfect information[END_REF]), but their adaption to handle data appears nontrivial. . . , Q n , OId, CCN, R, i 1 , . . . , i n , q i , . . . , q n , oid, ccn, r) As mentioned in the Introduction, the work of this work package is organised into two streams: (i) compositional theory of connector behaviours, and (ii) compositional assume-guarantee verification for probabilistic automata, with the view to integrate these together. This chapter provides an overview of the progress in the work stream (ii).

∧ n i=1 p i+2n+3 = item id i ∧ ∧ n i=1 p i+3n+3 = quant i ∧ p 4n+4 =
?stmt !stmt ′ 2 !stmt ′ 1 ?Quit(p) ?stmt !stmt ′ 2 !stmt ′ 1 ?Quit(p) ?stmt !stmt ′ 2 !stmt ′ 1 ?Quit(p) ?stmt !stmt ′ 2 !stmt ′ 1 ?Quit(p) !stmt ′ 2 !stmt ′ 1 ?Quit(p) !stmt 1 a !stmt 1 b ?stmt 1 c !stmt 1 a !stmt 1 b ?stmt 1 c !stmt 1 a !stmt 1 b ?stmt 1 c !stmt 1 a !stmt 1 b ?stmt 1 c !stmt 1 a !stmt 1 b ?stmt 1 c !stmt 1 a !stmt 1 b ?stmt 1 c !stmt 2
?stmt ?stmt ?stmt ?stmt !stmt * d !stmt * d !stmt * d Q(2) stmt = P laceOrder(p 1 , p 2 ); CCN := p 2 stmt i = AddT oOrder(p 1 , p 2 , p 3 ); I i , Q i := p 2 , p 3 stmt ′ i = ReceiveConf irmation(OId, I i , Q i ) stmt i a = p 1 = oid; process item(p 1 , p 2 ); i i := p 2 stmt i b = p = Q i ; set quantity; (p)q i := p stmt i c = conf irm item; (p 1 , p 2 , p 3 ) stmt d = close order(p 1 , p 2 ); ccn := p 2 stmt * d = I 1 ∧ q 2 = Q 2 ∧ i 2 = I 2 ; close order(p 1 , p 2 ); ccn := p 2
Probabilistic verification techniques have been applied to the formal modelling and analysis of a wide range of systems, from communication protocols such as Bluetooth, to nanoscale computing devices, to biological cellular processes. In order to tackle the inherent challenge of scalability and independent development, compositional approaches to verification are sorely needed. An example is assume-guarantee reasoning, where each component of a system is analysed independently, using assumptions about the other components that it interacts with. In the previous deliverables D2. 1 [21] and D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF], we have already proposed an assume-guarantee framework for probabilistic automata and its extensions. In D2.1, assumptions are probabilistic safety properties (e.g. "event A always occurs before event B with probability at least 0.98") and D2.2 generalises this to boolean combinations of ω-regular and reward properties. In both cases, this yields efficiently checkable assumptions and the approaches were successfully implemented and applied to some large case studies, including CONNECT-relevant examples.

As mentioned in Section 2.4, we are in the process of formulating an assume-guarantee framework for the specification theory presented in Chapter 2. We shall also develop a quantitative extension of the specification theory based on discrete-probabilities. Once this has been completed, we shall marry the quantitative assume-guarantee techniques presented in this chapter with the those we are working on in the non-quantitative case, and apply them to the probabilistic specification theory. This will be a key priority of WP2 in the remaining period of the project.

In this chapter, we present recent developments in work stream (ii) concerning compositional assumeguarantee verification techniques for probabilistic automata. In particular, we describe in Section 5.1 extensions to techniques for automatically generating probabilistic assumptions that can be used as the basis for compositional reasoning. In Section 5.2, our focus is on using a more expressive class of assumptions. We present novel techniques [START_REF] Feng | Learning-based compositional verification for synchronous probabilistic systems[END_REF] for compositional probabilistic verification of synchronous systems in which assumptions are probabilistic finite automata (PFAs) [START_REF] Rabin | Probabilistic automata[END_REF]. Probabilistic safety property assumptions in D2.1 can only capture a limited amount of information about a component, restricting the cases where assume-guarantee reasoning can be applied. Therefore, the framework in D2.1 is incomplete in the sense that, if the property being verified is true, there does not necessarily exist an assumption that can be used to verify it compositionally. In contrast, our new approach is complete. Furthermore, as in D2.2, we use a novel L*-inspired learning algorithm to automatically generate assumptions. The assumeguarantee method has been implemented and applied to a number of examples, including communication protocols of relevance to CONNECT, but it relies on semi-algorithms, with no guarantee of termination, and its performance is not competitive compared to the method reported in D2.2; see [START_REF] Feng | Learning-based compositional verification for synchronous probabilistic systems[END_REF] for more detail.

We emphasise that the use of learning in WP2 differs from that in WP4; we are using learning to fully automate compositional reasoning, by learning assumptions that suffice to derive the required conclusion.

Extensions to the learning approach

Preliminaries

In the deliverable D2.1 [START_REF]CONNECT Deliverable D2.1: Capturing functional and non-functional connector behaviours[END_REF], we reported a probabilistic assume-guarantee framework, in which probabilistic safety properties can be verified in a compositional way. An assume-guarantee triple now takes the form A ≥p A M i G ≥p G where M i is a PA and A ≥p A , G ≥p G are two probabilistic safety properties; the former is a probabilistic assumption, the latter a property to be checked. This is interpreted as follows: In order to produce conjectures, L* needs answers to membership queries about whether certain traces t should be in the language being generated. For this, we use the following check: t M 2 |= G ≥p G , which can be seen as an analogue of the corresponding one for the non-probabilistic case. Intuitively, the idea is that if, under a single possible behaviour t of M 1 , M 2 satisfies the property, then t should be included in the assumption A. There may be situations where this scheme leads to an assumption that cannot be used to verify the property. This is because it is possible that there are multiple traces which do not violate property G ≥p G individually but, when combined, cause G ≥p G to be false. In practice, though, this approach seems to work well in most cases.

A ≥p A M i G ≥p G is true if,
A final aspect of L* that needs discussion is counterexamples. In [START_REF] Cobleigh | Learning assumptions for compositional verification[END_REF][START_REF] Pasareanu | Learning to divide and conquer: Applying the L* algorithm to automate assume-guarantee reasoning[END_REF], when the response to an equivalence query is "no", a counterexample in the form of a trace is returned to L*. In our case, there are two differences in this respect. Firstly, a counterexample may constitute multiple traces; this is because the results of the model checking queries executed by the teacher yield probabilistic counterexamples [START_REF] Han | Counterexample generation in probabilistic model checking[END_REF], which comprise multiple paths (again, see [START_REF] Feng | Compositional verification of probabilistic systems using learning[END_REF] for precise details). Secondly, situations may arise where no such counterexample can be generated (recall that there is no guarantee that an assumption can eventually be created). In this case, since no trace can be returned to L*, we terminate the learning algorithm, returning the current tightest bounds on Pr min M1 M2 (G) that have been computed so far. We summarise in Figure 5.1 the overall structure of the L*-based algorithm for generating probabilistic assumptions. The left-hand side shows the basic L* algorithm. This interacts, through queries, with the teacher, shown on the right-hand side. The teacher responds to queries as described above. Notice that the equivalence query, which analyses a particular conjectured assumption A has four possible outcomes: the first two are when A can be used to show either that M 1 M 2 |= G ≥p G or M 1 M 2 |= G ≥p G ; the third is when a counterexample (comprising one or more traces) is passed back to L*; and the fourth is when no counterexample can be generated so the algorithm returns the tightest bounds computed so far for Pr min M1 M2 (G). The above approach was successfully used in [START_REF] Feng | Compositional verification of probabilistic systems using learning[END_REF] to automatically generate probabilistic assumptions for several large case studies. Furthermore, these assumptions were much smaller than the corresponding components that they represented, leading to gains in performance. In this section, we present some recent extensions to that work.

An Alternative Learning Method: NL*

We investigate the use of an alternative learning algorithm to generate probabilistic assumptions. Whereas L* learns a minimal DFA for a regular language, the algorithm NL* [START_REF] Bollig | Angluin-style learning of NFA[END_REF] learns a minimal residual finite-state automaton (RFSA). RFSAs are a subclass of nondeterministic finite automata. For the same regular language L, the minimal RFSA that accepts L can be exponentially more succinct than the corresponding minimal DFA. In fact, for the purposes of probabilistic model checking, the RFSA needs to be determinised anyway [START_REF] Alfaro | Formal Verification of Probabilistic Systems[END_REF]. However, the hope is that the smaller size of the RFSA may lead to a faster CONNECT 231167 learning procedure. NL* works in a similar fashion to L*, making it straightforward to substitute into the learning loop shown in Figure 5.1.

According to the experimental results in [START_REF] Feng | Automated learning of probabilistic assumptions for compositional reasoning[END_REF], the NL* algorithms successfully generated a correct (and small) assumption in all cases with the exception of one model. The results shows that the L*-based method is faster than NL* in most cases. However, on several of the larger models, NL* has better performance due to a smaller number of equivalence queries. NL* needs more membership queries, but these are less costly.

Learning Multiple Assumptions: Rule (ASYM-N)

In this section, we consider another extension of the probabilistic assumption generation scheme of Section 5.1.1, adapting it to the proof rule (ASYM-N) of [START_REF]CONNECT Deliverable D2.1: Capturing functional and non-functional connector behaviours[END_REF]. This is motivated by the observation that, for several of the case studies in the previous section, scalability is limited because one of the two components comprises several sub-components. As the number of sub-components increases, model checking becomes infeasible due to the size of the state space. The (ASYM-N) proof rule allows decomposition of the system into more than 2 components:

true M 1 A 1 ≥p1 A 1 ≥p1 M 2 A 2 ≥p2 . . . A n-1 ≥pn-1 M n G ≥p G true M 1 . . . M n G ≥p G (ASYM-N)
Adapting our probabilistic assumption generation process to (ASYM-N) works by learning assumptions for the rule in a recursive fashion, with each step requiring a separate instantiation of the learning algorithm for (ASYM), as is done for the non-probabilistic version of a similar rule in [START_REF] Pasareanu | Learning to divide and conquer: Applying the L* algorithm to automate assume-guarantee reasoning[END_REF]. The experimental results shown in [START_REF] Feng | Automated learning of probabilistic assumptions for compositional reasoning[END_REF] demonstrate that, using the rule (ASYM-N), we can successfully learn small assumptions and perform compositional verification in several cases where the rule (ASYM) runs out of memory. Furthermore, in two instances, (ASYM-N) permits verification of models which cannot be checked in a non-compositional fashion.

Learning-based Compositional Verification for Synchronous Probabilistic Systems

In this section, we present novel techniques for automated compositional verification of synchronous probabilistic systems. First, we give an assume-guarantee framework for verifying probabilistic safety properties of systems modelled as discrete-time Markov chains (DTMC). Assumptions about system components are represented as probabilistic finite automata (PFAs) and the relationship between components and assumptions is captured by weak language inclusion. More concretely, PFAs represent weighted languages, mapping finite words to probabilities. An assumption about a system component M is represented by a PFA that gives upper bounds on the probabilities of traces being observed in M . This is an inherently linear-time relation, which is well-known to be difficult to adapt to compositional techniques for systems that exhibit both probabilistic and nondeterministic behaviour [START_REF] Segala | Modelling and Verification of Randomized Distributed Real Time Systems[END_REF]. So, in the present work, we restrict our attention to fully probabilistic systems. To do so, we model components as probabilistic I/O systems (PIOSs), which, when combined through synchronous parallel composition, result in a (fully probabilistic) discrete-time Markov chain. The relation between a PIOS M and a PFA A representing an assumption about M is captured by weak language inclusion. Based on this, we give an asymmetric proof rule for verifying probabilistic safety properties on a DTMC composed of two PIOSs.

In order to implement our approach, we give an algorithm to check weak language inclusion, reducing it to the existing notion of (strong) language inclusion for PFAs. Although checking PFA language equivalence (that each word maps to the same probability) is decidable in polynomial time [START_REF] Tzeng | A polynomial-time algorithm for the equivalence of probabilistic automata[END_REF][START_REF] Doyen | Equivalence of labeled Markov chains[END_REF], checking language inclusion is undecidable [START_REF] Blondel | Undecidable problems for probabilistic automata of fixed dimension[END_REF]. We propose a semi-algorithm, inspired by [START_REF] Tzeng | A polynomial-time algorithm for the equivalence of probabilistic automata[END_REF], to check language inclusion; in the case where the check fails, a minimal counterexample is produced. We also develop a CONNECT 231167 novel technique for learning PFAs, which we use to automatically generate assumptions. Our algorithm, like L*, is based on active learning, posing queries in an interactive fashion about the PFA to be generated.

In the rest of the section, we first briefly describe probabilistic finite automata and discrete-time Markov chains in Section 5.2.1, and define an assume-guarantee framework for synchronous probabilistic systems in Section 5.2.2. Next, we develop a semi-algorithm to check language inclusion for PFAs in Section 5.2.3 and a learning algorithm, similar to the L* algorithm, for constructing PFAs as assumptions in Section 5.2.4. In Section 5.2.5, we integrate the techniques in Sections 5.2.3 and 5.2.4 into the framework described in Section 5.2.2.

Preliminaries

We use SDist(S) to denote the set of probability sub-distributions over set S, η s for the point distribution on s∈S, and µ 1 ×µ 2 for the product distribution of µ 1 and µ 2 . A PFA A defines a mapping Pr A : α * →[0, 1] giving the probability of accepting each finite word w ∈ α * . Intuitively, the probability Pr A (w) for a word w = a 1 • • • a n is determined by tracing paths through A that correspond to w, with P(a)[s, s ′ ] giving the probability to move from s to s ′ on reading a. More precisely, we let ι be an S-indexed 0-1 row vector with ι[s] = 1 if and only if s = s, κ be an S-indexed column vector of 1s and P(w) = P(a 1 )• • •P(a n ). Then, we define Pr A (w) = ιP(w) κ.

Definition 5.2 (Language inclusion/equivalence) Given two

PFAs A 1 and A 2 with the same alphabet α, we say A 1 and A 2 are related by (strong) language inclusion (resp. language equivalence), denoted A 1 ⊑ A 2 (resp. A 1 ≡ A 2 ), if for every word w ∈ α * , Pr A1 (w) Pr A2 (w) (resp. Pr A1 (w) = Pr A2 (w)).

Definition 5.3 (DTMC)

A discrete-time Markov chain (DTMC) is a tuple D=(S, s, α, δ), where S is a finite set of states, s ∈ S is an initial state, α is an alphabet of action labels and δ : S × (α ∪ {τ }) → SDist(S) is a (partial) probabilistic transition function, such that, for any s, δ(s, a) is defined for at most one a ∈ α ∪ {τ }. If δ(s, a) = µ, the DTMC can make a transition, labelled with action a, and move to state s ′ with probability µ(s ′ ). We denote such transitions by s a -→ µ (or s a -→ s ′ ). The DTMC deadlocks when δ(s, a) is not defined for any a, which we denote by s →. We use action label τ to denote a "silent" (or "internal") transition. A (finite or infinite) path through D is a sequence of transitions θ = s 0 a0 → s 1 a1 → • • • with s 0 = s. In this deliverable, we consider probabilistic safety properties G p , where G is a regular safety property [START_REF] Baier | Principles of Model Checking[END_REF], defining a set of "good" executions, and p ∈ [0, 1] is a probability bound. Model checking G p reduces to solving a linear equation system [START_REF] Baier | Principles of Model Checking[END_REF].

Assume-Guarantee for Synchronous Probabilistic Systems

We now define a compositional verification framework for fully probabilistic systems. Components are modelled by probabilistic I/O systems (PIOSs). These exhibit (input) nondeterminism but, when composed synchronously in parallel, result in a DTMC. From any state s of a PIOS M , there is either a single transition with an output, hidden or τ action, or k transitions, each with one action from a particular bundle α I,i comprising k input actions. Transitions and paths in PIOSs are defined as for DTMCs. The probability of a finite path θ = s 0 a0 --→ s 1 • • • an-1 ----→ s n in M is given by Pr M (θ) = n-1 i=0 δ(s i , a i )(s i+1 ). Since PIOSs only have nondeterminism on input actions, the probability for a word w ∈ (α ∪ {τ }) * is well defined: letting wd (θ) denote the word a 0 . . . a n-1 of actions from path θ, we have Pr M (w) = wd(θ)=w Pr M (θ). Then, letting st : (α ∪ {τ }) * α → α * be the function that removes all τ s, we define the probability Pr M τ (w ′ ) for a τ -free word w ′ ∈ α * as Pr M τ (w) = w=st(w ′ ) Pr M (w ′ ). Example 1. Figure 5.2 depicts two PIOSs M 1 and M 2 . M 1 is a data communicator which chooses (probabilistically) to either send or receive data. This simple example only models receiving; choosing to send results in a failure. M 1 tells M 2 , a data generator, that it is ready to receive using action ready. M 2 should then send a sequence of packets, modelled by the alternating actions d0 and d1 . If Notice PIOS M 1 M 2 has only τ or hidden actions and can thus be considered a DTMC.

We next introduce our notion of assumptions about PIOSs, for which we use a specific class of PFAs and weak language inclusion, which relaxes the definition of language inclusion for PFAs introduced earlier by ignoring τ actions. A valid assumption A for M is one that satisfies M ⊑ w A. We can reduce the problem of checking whether this is true to the problem of checking (strong) language inclusion between two PFAs (see Section 5.2.3) by the following proposition. We will also need to perform a conversion in the opposite direction, translating an assumption PFA A into a (weak language) equivalent PIOS, which we denote pios(A).

Definition 5.9 (Assumption-to-PIOS conversion)

Given assumption A = (S, s, α, P), and action partition α = ( m i=1 α I,i ) ⊎ α O ⊎ α H , its conversion to a PIOS is defined as pios(A) = (S ′ , s, α, δ), where S ′ = S ⊎ {s a |s ∈ S, a ∈ α H ∪ α O } ⊎ {s i |s ∈ S, 1≤i≤m} and δ is constructed as follows. For any transition s a -→ s ′ , let p denote P(a)[s, s ′ ] and p max (s) and p max i (s) be as defined in Definition 5.6. Then:

• if a ∈ α O ∪ α H , then δ(s, τ )(s a ) = p p max (s) and δ(s a , a)(s ′ ) = p max (s);

• if a ∈ α I,i (for 1 i m), then δ(s, τ )(s i ) = p max i (s) p max (s) and δ(s i , a)(s ′ ) = p• p max (s)

p max i (s) .
Example 2. Consider PIOS M 1 from Example 1. Figure 5.3 shows a valid assumption A for M 1 (i.e. M 1 ⊑ w A) and the corresponding PIOS pios(A). In A, state q 0 has two output actions leading to respective sub-distributions. Thus A is not a PIOS. In pios(A), a τ transition and the states q ready 0 and q fail 0 (abbreviated to q r 0 and q f 0 ) are added. Now, we describe how to perform compositional verification using our framework. We focus on verifying G p on a DTMC M 1 M 2 where M i are PIOSs. For simplicity, we will assume that the property refers only to input/output actions of M 1 and M 2 and assume that all hidden actions of M 1 and M 2 have been renamed as τ actions, which affects neither the parallel composition M 1 M 2 nor the probability of satisfying G.

An assume-guarantee triple A M G p means "whenever component M is part of a system satisfying the assumption A, the system is guaranteed to satisfy G p ". Definition 5.10 (Assume-guarantee triple) If M is a PIOS with alphabet α, A is an assumption about M and G p is a probabilistic safety property, then A M G p is an assume-guarantee triple, with the following meaning:

A M G p ⇔ ∀M ′ . (M ′ ⊑ w A =⇒ M ′ M |= G p ).
Using the translation pios(A) from PFA to PIOS described above, checking whether a triple is true reduces to standard probabilistic model checking (see Section 5.2.1).

Proposition 5.11

For A, M and G p as given in Definition 5.10, the assume-guarantee triple A M G p holds if and only if pios(A) M |= G p .

Finally, we give an asymmetric assume-guarantee proof rule (in the style of those from [START_REF] Pasareanu | Learning to divide and conquer: Applying the L* algorithm to automate assume-guarantee reasoning[END_REF][START_REF] Kwiatkowska | Assume-guarantee verification for probabilistic systems[END_REF]) for verifying a system M 1 M 2 compositionally.

Theorem 5.12 Let M 1 , M 2 be PIOSs, A an assumption for M 1 and G p a probabilistic safety property for M 1 M 2 . Then the following proof rule holds:

M 1 ⊑ w A and A M 2 G p M 1 M 2 |= G p (ASYM-PIOS)
CONNECT 231167

we stop the learning loop, concluding that M 1 ||M 2 |= G p . If, on the other hand, C is a spurious counterexample, we can always extract, from C a counterexample (word) c such that the learning algorithm can update its observation table. Full details can be found in [START_REF] Feng | Learning-based compositional verification for synchronous probabilistic systems[END_REF]. From the arguments above, we can show that, when the learning loop terminates, it always yields a correct result. It should be pointed out, though, that since the loop is driven by the learning algorithm of Section 5.2.4, whose termination we cannot prove, we are also unable to guarantee that the loop finishes. Furthermore, weak language inclusion checks use the semi-algorithm of Section 5.2.3, which is not guaranteed to terminate.

Conclusions and future work

In the first section, we have described some recent improvements and extensions to the learning framework for probabilistic assume-guarantee verification. There are a variety of possible directions for future research in this area. One is to extend our techniques for learning probabilistic assumptions to the assume-guarantee framework in [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF], which additionally includes ω-regular and expected reward properties. Here, the ω-regular language learning algorithms of [START_REF] Farzan | Extending automated compositional verification to the full class of omega-regular languages[END_REF][START_REF] Chaki | Automated assume-guarantee reasoning for omega-regular systems and specifications[END_REF] may provide a useful starting point. There are also possibilities to enhance the underlying compositional verification framework. This includes developing efficient techniques to work with richer classes of probabilistic assumptions and extending the approach to handle more expressive types of probabilistic models, such as those that incorporate continuous-time behaviour.

In the second section, we have presented a novel assume-guarantee framework where multicomponent systems are modelled by discrete-time Markov chains, components are probabilistic I/O systems and assumptions are probabilistic finite automata. Based on new techniques for checking PFA language inclusion and active learning of PFAs, we have built a fully-automated implementation of the framework that generates assumptions and then performs compositional verification. Unfortunately, the method relies on semi-algorithms, with no guarantee of termination, and its performance is not competitive compared to the method reported in D2.2; see [START_REF] Feng | Learning-based compositional verification for synchronous probabilistic systems[END_REF] for more detail. Future work in this area will include investigating more alternative representations for assumptions, exploring ways to extend our techniques to models with nondeterminism and investigating termination conditions for the language inclusion check and PFA learning.

CONNECT 231167 79/86

Conclusion and future work

A key contribution of WP2 in the third year is the formulation of a comprehensive specification theory for modelling components. This is a bedrock for the work package in that, come the end of the project, the reasoning frameworks introduced in WP2 should all be based on this specification theory. The specification theory itself introduces formal notions such as refinement for comparing components and determining when they can be substituted for one another. The operation of parallel composition allows users to examine the structure of composed component-based systems, while conjunction supports independent development, a necessary feature for supporting compositionality in CONNECT. The operation of quotient supports the principles of synthesis, and can be used for proving technical results about the properties of mediators synthesised à la WP3, such as deadlock and error freedom.

We have successfully demonstrated through Chapter 3 that the specification theory introduced is not an abstract notation disconnected from CONNECT, but can be used as a genuine modelling framework of the project. We have given a simple semantic preserving mapping from the extended LTSs of WP3 to the Logic IOLTSs of our specification theory. This allows the other work packages to exploit the compositionality results we have presented in Chapter 2, with respect to the refinement preorder.

To better support modelling across the project, we have introduced in Chapter 4 an extension of the specification theory with data, which should assist greatly with the modelling of components in both WPs 3 and 4. To broach the work of WP5, it is our intention to commence work on a quantitative specification theory based on discrete probabilistic behaviours, with reward structures for capturing non-functional properties. Such models will be easily adoptable by WP5 so that quantitative analysis techniques can be applied to examine the performance aspects of systems.

Besides a unified modelling approach across the project, we also intend to develop frameworks for reasoning compositionally about components, primarily in the form of assume-guarantee specifications. We have made a start on such a framework in the non-quantitative case, although due to its infancy we do not document it in this report. So far we have devised a reasoning framework for safety properties, and we have proposed a framework for liveness based on quiescence. Concerning the safety framework, we have also formulated AG rules for the operations of parallel composition and conjunction, and have produced the associated soundness proofs. Formulation of a rule for quotient, which will be necessary for showing strong integration and linking with WP3, is still in progress. We will resume work on this framework over the remainder of the project.

Work on compositional reasoning for probabilistic systems has already commenced independently (see Chapter 5), with formulation of a fully-automated assume-guarantee technique for DTMCs, including automatic generation of probabilistic assumptions represented as PFAs, a semi-algorithm for checking language inclusions on PFAs, and a new L*-style learning methods for PFAs. The learning framework for assumption generation in D2.2 has been extended to support the (ASYM-N) rule and included another learning algorithm. Over the course of the final year, it is our intention to link our compositional reasoning techniques to the probabilistic extension of the specification theory.

We also plan to investigate an approach that enhances the connector synthesis by considering nonfunctional aspects. The approach, by leveraging non-functional estimation and (multi-objective) optimization techniques, selects the best connector with respect to specified non-functional requirements for the system to be connected. The synthesized connector is selected among the possible ones that are correct w.r.t. functional aspects (i.e., a refinement of the most general one) but different w.r.t non-functional perspectives. In this case the approach estimates the non-functional aspects of the possible alternative connectors and then decides which to provide. In case more than one non-functional aspect is considered, a trade-off analysis (based on multi-objective function optimization) needs to be executed. The devised approach could also enhance our specification theory by defining a specific operator for this aim. More specifically, the proposed specification theory could be enhanced to allow the specification of nonfunctional characteristics of actions (inside a connector) and connectors as whole. Moreover, several compositional operators considering in the connector composition the non-functional aspects could be defined. By considering the approach for synthesis characterized in this deliverable, we envisage two different operator types, one able to calculate the non-functional characteristics of the possible (functional equivalent) connectors and another that is able to select a connector functionally equivalent to the most general one but that optimizes a specific (multi-objective) function.

CONNECT 231167

Figure 2 . 1 :

 21 Figure 2.1: Refinement of Logic IOLTSs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 2 . 2 :

 22 Figure 2.2: Example of parallel composition on Logic IOLTSs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 2 . 3 :

 23 Figure 2.3: Example of conjunction on Logic IOLTSs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 2 . 4 :

 24 Figure 2.4: Example showing non-existence of quotient on Logic IOLTSs.. . . . . . . . . . . . . . . . . . . . . . . . .

Figure 2 . 5 :

 25 Figure 2.5: Example of quotient on Logic IOLTSs with no inconsistencies. . . . . . . . . . . . . . . . . . . . . . . . .

Figure 2 . 6 :

 26 Figure 2.6: Example of quotient on Logic IOLTSs with inconsistencies. . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 3 . 1 :

 31 Figure 3.1: Component denoting Seq(c 1 . . . c m ). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 3 . 2 :

 32 Figure 3.2: Logic IOLTS representing the goal G . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 3 . 3 :

 33 Figure 3.3: Model of the despatcher. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 3 . 4 :

 34 Figure 3.4: Model of the departure board controller. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 3 . 5 :

 35 Figure 3.5: The parallel composition of the despatcher, the display and O.. . . . . . . . . . . . . . . . . . . . . . . .

Figure 3 . 6 :

 36 Figure 3.6: The quotient-synthesised connector. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 3 . 7 :

 37 Figure 3.7: Model of the US client: U S. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 3 . 8 :

 38 Figure 3.8: The mediator for the holiday booking example. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 3 . 9 :

 39 Figure 3.9: Logic IOLTS obtained by transforming the Blue extended LTS. . . . . . . . . . . . . . . . . . . . . . . .

Figure 4 . 1 :

 41 Figure 4.1: Mediator synthesis problem for CFRing and XMPP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 4 . 2 :

 42 Figure 4.2: Specification of the synthesis problem with messaging in the form of the process R. . . . . .

Figure 4 . 3 :

 43 Figure 4.3: The process CFRing || XMPP . The statements of the transitions marked by vertical arrows are defined by the labels on the left margin of the figure. The statements of the transitions marked by horizontal arrows are defined by the labels on the top margin of the figure. . . . . . . . . . . . . .

Figure 4 . 4 :

 44 Figure 4.4: The process P = (CFRing || XMPP ) ✄ R. The statements of the transitions marked by vertical and horizontal arrows are defined by the labels on the top and the left margin of the figure (as in Figure 4.3). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 4 . 5 :

 45 Figure 4.5: The skeleton S of Q. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 4 . 6 :

 46 Figure 4.6: The resulting mediator Q for the application with messaging.. . . . . . . . . . . . . . . . . . . . . . . . .

Figure 4 . 7 :

 47 Figure 4.7: Incompatible client Client and server Server of an application for booking seats. . . . . . . . .

Figure 4 . 8 :Figure 4 . 9 :

 4849 Figure 4.8: Specification of the synthesis problem with booking seats in the form of the process R. . .

Figure 4 . 10 :

 410 Figure 4.10: Client Blue and customer service M oon in an e-commerce service, parameterized by the maximum number of ordered items n. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 4 . 11 :

 411 Figure 4.11: Specification of the synthesis problem where the number of ordered items is bounded by n is given by the process R(n). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 4 . 12 :

 412 Figure 4.12: Resulting mediator Q for the e-commerce service with n = 2 . . . . . . . . . . . . . . . . . . . . . . . .

Figure 5 . 1 :

 51 Figure 5.1: Overview of probabilistic assumption generation [39], using an adaption of L*: generates assumption A ≥p A for verification of M 1 M 2 |= G ≥p G using rule (ASYM). . . . . . . . . . . . . . . . . . . . . . .

Figure 5 . 2 :

 52 Figure 5.2: Running example: two PIOSs M 1 and M 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 5 . 3 :

 53 Figure 5.3: Assumption A and its PIOS conversion pios(A). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 5 . 4 :

 54 Figure 5.4: Semi-algorithm for deciding PFA language inclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 5 . 5 :

 55 Figure 5.5: L*-style learning algorithm for PFAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 5 . 6 :

 56 Figure 5.6: L*-style PFA learning loop for probabilistic assumption generation. . . . . . . . . . . . . . . . . . . .

Definition 2 . 7 (

 27 Parallel composition) Let P and Q be declarative specifications such that A O P and A O Q are disjoint. Then P || Q is the declarative specification A I P||Q , A O P||Q , T P||Q , F P||Q , where:

ǫ

  =⇒ P for visible actions a ∈ A, we obtain p a =⇒ P p ′ CONNECT 231167 iff there exist p a and p ′ a such that p ǫ =⇒ P p a a -→ P p ′ a ǫ =⇒ P p ′ , and p ⊣a =⇒ P p ′ iff there exists p a such that p a -→ P p a ǫ =⇒ P p ′ . The extension to words w = a 1 . . . a n is defined in the natural way by p w =⇒ P p ′ iff p a1 =⇒ P . . . an =⇒ P p ′ . Furthermore, for a compositional operator ⊕, and sets A and B, we write A ⊕ B for the set {a ⊕ b : a ∈ A and b ∈ B}. This allows us to use a process-algebraic notation for states.

Figure 2 . 1 :

 21 Figure 2.1: Refinement of Logic IOLTSs.

Theorem 2 . 21 (

 221 Model mapping preserves safe traces) For an arbitrary process p P , IST (p P ) = T p P * \ F p P * and ST (p P ) = T p P * \ F E( p P * ) .

Lemma 2 . 27 (

 227 Simplified model mapping) Let p be a process in Logic IOLTS P ⊥ . Then p * = A I P , A O P , T p * , F p * , where:

Figure 2 . 2 :

 22 Figure 2.2: Example of parallel composition on Logic IOLTSs.

Figure 2 . 3 :

 23 Figure 2.3: Example of conjunction on Logic IOLTSs.

q 1 Figure 2 . 4 :

 124 Figure 2.4: Example showing non-existence of quotient on Logic IOLTSs.

Figure 2 . 5 :

 25 Figure 2.5: Example of quotient on Logic IOLTSs with no inconsistencies.

Figure 2 . 6 :

 26 Figure 2.6: Example of quotient on Logic IOLTSs with inconsistencies.

Figure 3 . 1 : 1 .

 311 Figure 3.1: Component denoting Seq(c 1 . . . c m )

•

  Modelling equivalences. Let a ≡ b 1 . . . b n be any equivalence relationship in the ontology (for n ≥ 1), where it is assumed without loss of generality that a is a primitive of P and b 1 , . . . , b n are primitives of Q. We require that b 1 , . . . , b n are either all inputs in Q or are all outputs in Q. We further require that exactly one of a and b 1 is an output in the respective alphabets of P and Q. Now, if a ∈ A O P and b 1 ∈ A I Q , then a ≡ b 1 . . . b n is represented by Seq(ab 1 . . . b n ). Otherwise, if a ∈ A I P and b 1 ∈ A O Q , then a ≡ b 1 . . . b n is represented by Seq(b 1 . . . b n a). • Modelling orderings. Let a 1 precedesa 2 precedes . . . precedesa n be an ordering relationship in the ontology. Then the representation of this ordering is given by Seq(a 1 a 2 . . . a n ).

  || M || Q raises an inconsistency. Then certainly P || M || Q || O generates an inconsistency, but this means that P || M || Q || O ⊑ G on account of inconsistency containment as G has no inconsistencies. Therefore the quotient technique would not have generated M. Instead suppose that P || M || Q deadlocks at a point where we do not allow it to. Then P || M || Q is in a quiescent state and a action has not been seen. Then by the same reasoning as for inconsistencies, we know P || M || O || Q must deadlock in a quiescent state (as O is an observer so only deals with input actions) and a could not have been encountered as all components must synchronise on the action. But then P || M || Q || O ⊑ G because of quiescence containment, and so M would not have been synthesised by our quotienting technique. Finally, suppose that P || M || Q does not respect one of the ontological constraints represented by Seq(c 1 . . . c m ). If {c 1 , . . . , c m } = A, then there is a trace t of P || M || Q such that t ↾ A becomes inconsistent in Seq(c 1 . . . c m ). Let A O be the set of actions arising in O, then t ↾ A O is inconsistent in O. Hence t is inconsistent in P || M || O || Q. But then it must be the case that P || M || O || Q ⊑ G because of inconsistency containment. Consequently, M could not have been synthesised by our quotienting procedure.

Figure 3 . 4 :

 34 Figure 3.4: Model of the departure board controller.

Figure 3 .Figure 3 . 5 :Figure 3 . 6 :Figure 3 . 7 :

 3353637 Figure 3.5 shows the parallel composition of the despatcher, the display and the ontological constraints component O. As O is an observer, meaning that all actions are inputs, the effect of taking Despatcher || Display || O is to make any path in Despatcher || Display inconsistent if it violates the ordering constraints of O. Thus in Figure 3.5, inconsistencies arise whenever a second target is observed before seeing a src action, as this violates the constraint Seq(target, src). Now by the quotienting procedure, we derive the mediator M as G/(Despatcher || Display || O), where G is given as defined in Section 3.4, taking A O = A Despatcher ∪ A Display . The resulting M is shown in Figure 3.6.

Figure 3 . 8 :

 38 Figure 3.8: The mediator for the holiday booking example.

1 .

 1 f indI precedes selF lightI , Seq(f indI, selF lightI) 2. f indI precedes selHotelI , Seq(f indI, selHotelI) 3. f indI precedes selCarI , Seq(f indI, selCarI) 4. selF lightO precedes f indO , Seq(selF lightO, f indO) 5. selHotelO precedes f indO , Seq(selHotelO, f indO) 6. selCarO precedes f indO , Seq(selCarO, f indO) 7. makeResI ≡ conf I , Seq(conf I, makeResI) 8. makeResO ≡ conf O , Seq(makeResO, conf O) 9. selF lightO precedes selCarI , Seq(selF lightO, selCarI).

Figure 3 . 9 :

 39 Figure 3.9: Logic IOLTS obtained by transforming the Blue extended LTS.

Algorithm 1 : 1 repeat 2 3 forall 5 until

 11235 Computing Bad Bad := ϕ F P ; Bad prev := Bad ; output transitions ℓ P , stmt, ℓ ′ P of P do 4 Bad (ℓ P ) := Bad (ℓ P ) ∨ pre(stmt; Bad (ℓ ′ P )) Bad = Bad prev ;

4 )Figure 4 . 1 :

 441 Figure 4.1: Mediator synthesis problem for CFRing and XMPP

Figure 4 . 2 :

 42 Figure 4.2: Specification of the synthesis problem with messaging in the form of the process R.

l 4 , m 3 CFRing||XMPP 1 =Figure 4 . 3 :

 3143 Figure 4.3: The process CFRing || XMPP . The statements of the transitions marked by vertical arrows are defined by the labels on the left margin of the figure. The statements of the transitions marked by horizontal arrows are defined by the labels on the top margin of the figure.

r 1 l 4 , m 3 4 )Figure 4 . 4 :

 143444 Figure 4.4: The process P = (CFRing || XMPP ) ✄ R. The statements of the transitions marked by vertical and horizontal arrows are defined by the labels on the top and the left margin of the figure (as in Figure 4.3).

r 1 l 4 4 )Figure 4 . 5 : 1 , m 0 , r 1 l 2 , m 0 , r 1 l 3 , m 0 , r 1 l 3 , m 1 , r 1 l 3 , m 2 , r 1 l 4 , m 3 Figure 4 . 6 :

 14445123131314346 Figure 4.5: The skeleton S of Q.

2 ! 1 = 2 ! 1 = 2 !Figure 4 . 7 :

 2121247 Figure 4.7: Incompatible client Client and server Server of an application for booking seats..

Figure 4 . 8 :

 48 Figure 4.8: Specification of the synthesis problem with booking seats in the form of the process R.

1 3, 5 , r 1 4, 5 , r 1 4, 6 , r 1 4, 7 , r 1 5, 7 , r 1 6, 7 , r 1 6, 8 , r 1 6, 9 , r 1 7, 9 , r 1 8, 10 , r 2 Q 2 ! 2 ? 3 p 1 = 2 ? 3 p 1 = 2 ?Figure 4 . 9 : 6 !? 6 ? 1 a!

 15151617171718191911022231231249661 Figure 4.9: Synthesized mediator Q for the application with booking seats.

2 c′ 2 !stmt ′ 1 ?

 221 !stmt d !stmt d !stmt d !stmt d ?close order ′ (p); r := p ?close order ′ (p); r := p ?close order ′ (p); r := p ?close order ′ (p); r := p !stmt Quit(p) p = r; !Quit(p); R := p ! (I 1 , . . . , I n , Q i , .

Figure 4 . 12 :

 412 Figure 4.12: Resulting mediator Q for the e-commerce service with n = 2 .

Figure 5 . 1 :

 51 Figure 5.1: Overview of probabilistic assumption generation [39], using an adaption of L*: generates assumption A ≥p A for verification of M 1 M 2 |= G ≥p G using rule (ASYM).

Definition 5 . 1 (

 51 PFA) A probabilistic finite automaton (PFA) is a tuple A = (S, s, α, P), where S is a finite set of states, s ∈ S is an initial state, α is an alphabet and P : α → (S × S → [0, 1]) is a function mapping actions to transition probability matrices. For each a ∈ α and s ∈ S, s ′ ∈S P(a)[s, s ′ ] ∈ [0, 1].

Definition 5 . 4 ( 1 initFigure 5 . 2 :

 54152 Figure 5.2: Running example: two PIOSs M 1 and M 2 .

Definition 5 . 5 ( 1 a→ µ 1 , s 2 a→ µ 2 , 1 b1→ µ 1 , s 2 b2→ µ 2 1 b1→ µ 1 , s 2 a→

 5511221122112 M 1 has failed, it sends a message fail . M 2 also has an initialisation step (init), which can fail. With probability 0.8, it is ready to receive signals from M 1 ; otherwise, it just tries to send packets anyway. Input/output actions for M 1 , M 2 are labelled with ?/! in the figure; all other actions are hidden. Each PIOS has a single input action bundle:α I,1 1 = {d0 , d1 }, α I,1 2 = {ready, fail }. Given PIOSs M 1 , M 2 with alphabets α 1 , α 2 , we say M 1 and M 2 are composable if α I 1 =α O 2 , α O 1 =α I 2 and α H 1 ∩ α H 2 =∅and define their parallel composition as follows. Parallel composition) The parallel composition of composable PIOSs M i = (S i , s i , α i , δ i ) for i=1, 2 is given by the PIOSM 1 ||M 2 = (S 1 ×S 2 , (s 1 , s 2 ), α, δ), where α = α H = α I 1 ∪ α O 1 ∪ (α H 1 ∪ {⊥}) * (α H 2 ∪ {⊥}) and, for b i ∈ α H i ∪ τ and a ∈ α I 1 ∪ α O 1 , δ is defined such that (s 1 , s 2 ) γ → µ 1 ×µ 2 iffone of the following holds: (i) s γ = a; (ii) s , γ = b 1 * b 2 ; (iii) s (or s 2 →), µ 2 = η s2 , γ = b 1 * ⊥; (iv) s 1 a → (or s 1 →), s 2 b2 → µ 2 , µ 1 = η s1 , γ = ⊥ * b 2 .

Definition 5 . 6 (Definition 5 . 7 (

 5657 Assumption) Let M be a PIOS with alphabet α = α I ⊎ α O ⊎ α H and input action bundles α I = m i=1 α I,i . An assumption A about M is a PFA A = (S, s, α, P) satisfying, for each state s ∈ S: (i) either all or none of the actions in a bundle α I,i (1 i m) are enabled in s; (ii) p max (s) ∈ [0, 1], where:p max (s) def = a∈α O ∪α H s ′ ∈S P(a)[s, s ′ ]+ Weak language inclusion/equivalence) For PIOS M with alphabet α and an assumption A about M , we say that M and A are related by weak language inclusion (resp. equivalence), denoted M ⊑ w A (resp. M ≡ w A), if for every word w ∈ α * , Pr M τ (w) Pr A (w) (resp. Pr M τ (w) = Pr A (w)).

Figure 5 . 3 :Proposition 5 . 8

 5358 Figure 5.3: Assumption A and its PIOS conversion pios(A).

  A declarative specification P is a tuple A I

	P , A O P , T P , F P in P are disjoint sets referred to as inputs and outputs respectively (the union of which is P and A O which A I denoted by A P ), T P ⊆ A * P is a non-empty set of permissible traces, and F P ⊆ A * P is a set of inconsistent
	traces. The trace sets must satisfy the constraints:
	1. F P ⊆ T P
	2. If t ∈ T P and i ∈ A I P , then ti ∈ T P
	3. T P is prefix closed
	4. If t ∈ F P and t ′ ∈ A * P , then tt ′ ∈ F P .

  Let P and R be Logic IOLTSs such that A O P ⊆ A O R and A P ⊆ A R . The quotient of P from R is the Logic IOLTS R/P = S R/P , A I R/P , A O R/P , -→, F R/P , where: • S R/P = {R/P : R ⊆ S R ⊥ and P ⊆ S P ⊥

• succ a P (S) = {s ′ : s ⊣a =⇒ P ⊥ s ′ with s ∈ S}. Definition 2.33 (Quotient Logic IOLTS)

  Thus t is quiescent if t ∈ T P and o ∈ A O P implies to ∈ T P . In the case of Logic IOLTSs, a state p P is quiescent if o ∈ A O P implies p P o =⇒ P . A trace t of p P is quiescent if there exists some quiescent state p P ′ such that p P t =⇒ P p P ′ . Thus quiescence on non-deterministic systems has may-like semantics.We use the concept of quiescence to indicate when a component is deadlocked. Formally, a component can deadlock after a trace t if t is a quiescent trace of the component. Therefore, a deadlocked component is one that can become blocked waiting for input.

	CONNECT 231167	36/86

  Definition 3.1 Let P = S P , L P , -→ P , F P , s 0 P be an extended LTS. The mapping L from extended LTSs to Logic IOLTSs is defined by L(P) = S L(P) , A I -{lI id 1 . . . id m : ?l(id 1 . . . id m , od 1 . . . od n ) ∈ L P } -{lO od 1 . . . od n : !l(id 1 . . . id m , od 1 . . . od n ) ∈ L

	L(P) , A O L(P) , -→ L(P) , ∅ , where:
	• S L(P) = S P ∪ {s ′ a , s ′′	′ a , s ′′ a , s ∈ S P
	• A I L(P) is the smallest set containing:

a : s ∈ S P , and ?a(. . . ) ∈ L P or !a(. . . ) ∈ L P } ∪ {s }, assuming s P } -{hand a : ?a(. . . ) ∈ L P or !a(. . .

) ∈ L P } -{ } • A O L(P)

is the smallest set containing:

-{lO od 1 . . . od n : ?l(id 1 . . . id m , od 1 . . . od n ) ∈ L P } -{lI id 1 . . . id m : !l(id 1 . . . id m , od 1 . . . od n ) ∈ L P } • -→ L(P)

is the smallest set containing: -{(s, hand a, t ′ a ) : (s, ?a(. . . ), t) ∈-→ P or (s, !a(. . . ), t) ∈-→ P } -{(t ′ a , aI id 1 . . . id m , t ′′ a ), (t ′′ a , aO od 1 . . . od n , t) : (s, ?a(id 1 . . . id m , od 1 . . . od n ), t) ∈-→ P } -{(t ′ a , aI id 1 . . . id m , t ′′ a ), (t ′′ a , aO od 1 . . . od n , t) : (s, !a(id 1 . . . id m , od 1 . . . od n ), t) ∈-→ P } -{(s, τ, t) : (s, τ, t) ∈-→ P }. -{(s, , s ) : s ∈ F P }.

  we have the following proposition Proposition 4.5 ST P||Q is the maximal prefix-closed subset of ST P || ST Q such that • whenever t ∈ ST P||Q , then Incompat P||Q (t) is false, and • whenever t ∈ ST P||Q and to ∈ (ST P || ST Q ) where o ∈ Σ (O P ∪O Q ) , then to ∈ ST P||Q .⊓ ⊔

Figure 4.11: Specification of the synthesis problem where the number of ordered items is bounded by n is given by the process

  order id∧ p 4n+5 = credit card number∧ p 4n+6 = result; ? (p 1 , . . . , p 4n+6 ) stmt = p 1 = OrderId; P laceOrder(p 1 , p 2 ); CreditCardN umber := p 2 stmt i = p 1 = OrderId; AddT oOrder(p 1 , p 2 , p 3 ); ItemId i , Quantity i := p 2 , p 3 OrderId ∧ p 2 = ItemId i ∧ p 3 = Quantity i ; ReceiveConf irmation(p 1 , p 2 , p 3 ) stmt i a = p 1 = order id i ; process item(p 1 , p 2 );item id i := p 2 stmt i b = set quantity(p);quantity i := p stmt i c = conf irm item(order id i , item id i , quantity i ) stmt d = p 1 = order id; close order(p 1 , p 2 );credit card numner := p 2 (p), !P laceOrder(p 1 , p 2 , p 3 ), !AddT oOrder(p 1 , p 2 , p 3 ), ReceiveConf irmation(p 1 , p 2 , p 3 ), !Quit(p), Quit ′ (p) !login(p), !login ′ (p), !create roder(p 1 , p 2 , p 3 ), !process item(p 1 , p 2 ), !set quantity(p), !conf irm item(p 1 , p 2 , p 3 ) !close order(p 1 , p 2 , p 3 ), !close order ′ (p) ∧ 2n+3 i=1 p i = p i+2n+3 ;! (p 1 , . . . , p 4n+6 )

				p = CId;		?create order	p = oid;
		?StartOrder(p);	!login ′ (p);		(p 1 , p 2 );	!StartOrder ′ (p);
		CId := p		cid := p	?login(p)	oid, cv := p 1 , p 2	OId := p
						?stmt 1
	stmt ′ i =	r 0 r 1 r 2 R !StartOrder(p) !StartOrder ′ R(n). ?stmt 2 ?stmt !stmt ′ 2 !stmt ′ 1 ?stmt 2 ?stmt !stmt ′ 2 !stmt ′ 1 ?stmt 2 ?stmt !stmt ′ 2 !stmt ′ 1 p 1 = Blue(n) ?Quit(p) ?Quit(p) ?Quit(p) ?stmt 2	M oon(n)
		b 4 , m 5	3 , m 5
		b 5 , m 5
	Figure 4.10: Client Blue and customer service M oon in an e-commerce service, parameterized by
	the maximum number of ordered items n. b 6 , m 6	.

  for all adversaries σ of M i such that Pr σ Mi (A) ≥ p A holds, Pr σ Mi (G) ≥ p G also holds. Crucially, verifying whether this is true reduces to a multi-objective model checking problem[START_REF] Etessami | Multi-objective model checking of Markov decision processes[END_REF][START_REF]CONNECT Deliverable D2.1: Capturing functional and non-functional connector behaviours[END_REF], which can be carried out efficiently by solving an LP problem. The proof rule used earlier now

	L* algorithm	Teacher
	cex. c CONNECT 231167 t M 2 |= G ≥pG ? (i) M 1 |= A ≥pA (ii) A ≥pA M 2 G ≥pG Update table trace t conj. A Membership query Membership query (analyse trace t) yes/no Try to find p A such that A ≥pA satisfies: conjecture Generate (analyse conjecture A) no yes done? Check: Update table Inputs: M 1 , M 2 G ≥pG Equivalence query	Pr min M1 M2 (G) ∈ [l, u] Outputs: (+ counterexample) Bounds: M 1 M 2 |= G ≥pG Property true: M 1 M 2 |= G ≥pG (+ assump. A ≥pA ) Property false:

We have not given a precise meaning to the term implementation nor sub-component; that is left up to the user of our specification theory. If the reader finds this unnerving, think of P as an arbitrary component.

List of Figures

g is a guard over X P and p 1 , . . . , p n , -α(p 1 , . . . , p n ) is a parameterized symbol with α ∈ (I P ∪ O P ), -y 1 , . . . , y k are distinct variables in X P , and z 1 , . . . , z k is a tuple, consisting of variables in X P and formal parameters in p 1 , . . . , p n .

• ϕ F P , the inconsistency predicate, maps each location to a boolean combination of equalities and negated equalities over variables in X P .

⊓ ⊔

We will write p for p 1 , . . . , p n , d for d 1 , . . . , d n , ȳ for y 1 , . . . , y k , and z for z 1 , . . . , z k . Intuitively, a data-process is at any point in time in a state, given by a location and an assignment to its variables. The data-process can perform a statement of form g; α(p); ȳ := z provided that the guard g[ d/p] evaluates to true in the current state; it then synchronizes via the symbol α( d), binds the formal parameters p to data values d, and simultaneously assigns new values to the variables ȳ according to the multiple assignment statement. A statement is performed atomically.

We will often use the terms input (output) transition and input (output) statement, when the involved action is an input (output) action. For convenience, input and output statements have the same basic form, even though the data values that are bound to the formal parameters are chosen by the environment in input statements, and by the data-process itself in output statements. In input statements, the guard is often true to reflect that the environment chooses the parameter values. However, a guard can also be used to reflect constraints on data values that the data-process is prepared to receive. In output statements, the parameters p are often taken directly from the variables of the data-process. We therefore introduce the notation g; !α(x 1 , . . . , x n ); ȳ := z as a shorthand for (g ∧ p 1 = x 1 ∧ • • • p n = x n ; !α(p 1 , . . . , p n ); ȳ := z.

The semantics of a data-process is defined by showing how a data-process can be mapped to an (infinite-state) Logic IOLTS, as defined in Definition 2.16. For a set X of variables, an X-valuation is an assignment of data values in the appropriate domains to the variables in X, respecting sorts. Valuations are extended to expressions in the natural way. For a valuation σ and a boolean combination of equalities over variables and data values g, we write σ |= g to denote that σ(g) evaluates to true.

A state of P is a pair ℓ, σ where ℓ ∈ L P and σ is a X P -valuation. The initial state of P is ℓ 0 P , σ 0 , where ℓ 0 P is the initial location and σ 0 is the X P -valuation that maps all variables to their initial values. A step of P, denoted by ℓ, σ α( d) ---→ ℓ ′ , σ ′ , transfers P from ℓ, σ to ℓ ′ , σ ′ while performing the (input or output) symbol α( d). It is derived from a transition ℓ, stmt, ℓ ′ ∈ δ P , with stmt of the form g; α(p 1 , . . . , p n ); y 1 , . . . , y k := z 1 , . . . , z k , such that

• σ ′ (y i ) = d j when z i is the parameter p j , for i = 1, . . . , k, and

We can now define the semantics of data-processes by mapping them to logic IOLTSs: Definition 4.2 Definition the mapping • Op from data-processes to logic IOLTSs as follows. For P = (I P , O P , L P , ℓ 0 P , X P , δ P , ϕ F P ), we define P Op as the logic IOLTS P Op = S P , Σ I P , Σ O P , -→ P , F P , where • S P is the set of states of P, The treatment of parallel composition and quotient stays the same as before with the difference that we define:

Applications to the Synthesis of Mediators

To demonstrate our formulation in practice, we choose three examples. First, the presented concepts are demonstrated in detail on a simple example with messaging protocols. Then we present an example with protocols for booking seats in a theatre and a slightly more complicated example with an e-commerce service.

In all the examples, we assume the input processes to be preprocessed so that the inner structure of communicated values is not important. For example, suppose that our task is to synchronise a mediator for a client and a server in an e-commerce application. The client orders an item using an output action !order(item object) where item object is an object consisting of two values: value item specifying the ordered item and value quantity specifying how many of items the client orders. On the other hand, the service receives an order in a sequence of two actions, ?OrderItem(p); Item := p and ?SetQuantity(p); Quantity := p. The mediator should guarantee that the service gets the clients orders with right values of items and quantities. In this case, the preprocessing phase replaces the action !order(item object) by !order(item, quantity) in order to make the components of item object visible for the synthesis algorithm.

Messaging Protocol

The scenario consists of two mismatching messaging protocols, CFRing and XMPP , both of which need to communicate with one another through a mediator that we must construct.

The safe traces of the messaging clients are represented by the two processes shown in Figure 4.1. In the description, we omit guards of transitions that are true. All variables of every sort are initialised by a special value ⊥. There is a value ⊥ for every sort of variables.

• The process CFRing has input actions start, output actions msgout and id, variables msg1 and id1, and locations {l 0 , l 1 , l 2 , l 3 , l 4 }.

• The process XMPP has input actions msgin and who, variables msg2 and id2, and locations {m 0 , m 1 , m 2 , m 3 }.

We specify the composed system by a process R shown in Figure 4.2 which initially performs the action start, thereafter can perform any sequence of actions msgout, msgin, id, and who, and which thereafter outputs the action , which will synchronise with the actions of the two processes only if they properly agree on the values of the variables. To specify that the communication should stop only when both CONNECT 231167 becomes:

thus reducing the problem of checking property G ≥p G on M 1 M 2 to two smaller sub-problems: (i) verifying a probabilistic safety property on M 1 ; and (ii) checking an assume-guarantee triple for M 2 .

In [START_REF]CONNECT Deliverable D2.1: Capturing functional and non-functional connector behaviours[END_REF], this proof rule, along with several others, are proved and then used to perform compositional verification on a set of large case studies. This includes cases where non-compositional verification is either slower or infeasible. In the deliverable D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF], this framework is extended to permit the use of more expressive assumptions (and properties): quantitative multi-objective properties, essentially Boolean combinations of probabilistic safety, ω-regular and expected total reward properties. An example of an expressible assumption is "with probability 1, component M i always eventually sends a message and the expected time to do so is at most 10 time-units." Again, the framework is implemented through multi-objective model checking and applied to several case studies.

In this section, we focus on the use of probabilistic safety properties, as in [START_REF]CONNECT Deliverable D2.1: Capturing functional and non-functional connector behaviours[END_REF]. Although these have limited expressivity, an advantage is that the generation of such assumptions can be automated by adapting the L*-based techniques developed for non-probabilistic compositional verification [START_REF] Cobleigh | Learning assumptions for compositional verification[END_REF][START_REF] Pasareanu | Learning to divide and conquer: Applying the L* algorithm to automate assume-guarantee reasoning[END_REF].

The approach was reported in D2.2 [START_REF]CONNECT Deliverable D2.2: Compositional algebra of connectors. FET IP CONNECT EU project, FP7 grant[END_REF] and has been applied to several large case studies. In D2.2, we consider the assume-guarantee proof rule (ASYM), which is used to check that the parallel composition of two PAs M 1 and M 2 satisfies a property G ≥p G . To do this, we need an assumption A ≥p A , which will be generated automatically.

The first key point to make is that, although we are required to learn a probabilistic assumption, i.e. a probabilistic safety property A ≥p A , we can essentially reduce this task to the problem of learning a non-probabilistic assumption, i.e. the corresponding safety property A. The reasoning behind this is as follows.

We need the probabilistic assumption A ≥p A to be such that both premises of the proof rule (ASYM) hold: (i) M 1 |= A ≥p A ; and (ii) A ≥p A M 2 G ≥p G . However, if (i) holds for a particular value of p A , then it also holds for any lower value of p A . Conversely, if (ii) holds for some p A , it then must hold for any higher value. Thus, given a safety property A, we can determine an appropriate probability bound p A (if one exists) by finding the lowest value of p A (if any) such that (ii) holds and checking it against (i). Alternatively, we can find the highest value of p A such that (i) holds (this is just Pr min M1 (A) in fact) and seeing if this suffices for (ii). A benefit of the latter is that, even if M 1 M 2 |= G ≥p G cannot be shown to be true with this particular assumption, we still obtain a lower bound on Pr min M1 M2 (G). Furthermore, with an additional simple check, an upper bound can also be generated.

In D2.2, we described an approach for adapting the L*-based approach [START_REF] Cobleigh | Learning assumptions for compositional verification[END_REF][START_REF] Pasareanu | Learning to divide and conquer: Applying the L* algorithm to automate assume-guarantee reasoning[END_REF], which generates nonprobabilistic assumptions, to our setting. The underlying idea beind the use of L* in [START_REF] Cobleigh | Learning assumptions for compositional verification[END_REF][START_REF] Pasareanu | Learning to divide and conquer: Applying the L* algorithm to automate assume-guarantee reasoning[END_REF] is the notion of weakest assumption: this will always exist and, if the property G being verified is true, will permit a compositional verification. It is used as the target language for L* and forms the basis of the membership and equivalence queries. In practice, however, this language is often not the one that is finally generated since intermediate conjectured assumptions may suffice, either to show that the property is true or that it is false.

An important difference in the probabilistic assume-guarantee framework of [START_REF]CONNECT Deliverable D2.1: Capturing functional and non-functional connector behaviours[END_REF] is that it is incomplete, meaning that, even if the property G ≥p G holds, there may be no probabilistic assumption A ≥p A for which the rule (ASYM) can be used to prove the property correct. So, there can be no equivalent notion of weakest assumption to be used as a target language. However, we can adopt a similar approach whereby we use L* to generate a sequence of conjectured assumptions A and, for each one, potentially show that G ≥p G is either true or false. Furthermore, as described above, each assumption A yields a lower and an upper bound on Pr min M1 M2 (G). We can retain these values as the learning algorithm progresses, keeping the highest lower bound and lowest upper bound discovered to report back to the user. 1 This means that, even if the algorithm terminates early (without concluding that G ≥p G is true or false), it produces useful quantitative information about the property of interest. 1 Note that the sequence of assumptions generated is not monotonic, e.g. it does not yield a sequence of increasing lower bounds on Pr min

CONNECT 231167 Thus, given an appropriate assumption A about M 1 , we can decompose the verification of M 1 M 2 into two sub-problems: checking weak language inclusion between M 1 and A; and checking that A M 2 G p . The former, as shown in Proposition 5.8, reduces to (strong) language inclusion on PFAs, which we discuss in the next section. The latter, as shown in Proposition 5.11, requires construction of the DTMC pios(A) M 2 and then application of standard probabilistic model checking techniques.

Example 3. Consider probabilistic safety property G 0.9 , where G means "fail never occurs". We can check this on running example M 1 M 2 using assumption A from Example 2. Since M 1 ⊑ w A, we just need to check that pios(A)||M 2 |= G 0.9 . As pios(A)||M 2 has a single path (q 0 t 0 ) τ * init,0.08 --------→ (q 2 t 1 ) fail,1 ----→ (q 4 t 1 ) • • • containing fail with probability 0.08, G 0.9 is satisfied (since 1 -0.08 0.9) and we are done.

Completeness.

Our framework is complete in the sense that, if M 1 M 2 |= G p , we can always find an assumption A to apply Theorem 5.12 by converting M 1 to a PFA.

Deciding Language Inclusion for PFAs

As discussed above, verifying whether a component satisfies an assumption in our framework reduces to checking language inclusion between PFAs, i.e. deciding whether two PFAs A 1 and A 2 over the same alphabet α satisfy A 1 ⊑ A 2 . In this section, we propose a semi-algorithm for performing this check. If A 1 ⊑ A 2 does not hold, then the algorithm is guaranteed to terminate and return a lexicographically minimal word as a counterexample; but if A 1 ⊑ A 2 does hold, then the algorithm may not terminate. The latter case is unavoidable since the problem is undecidable (see [START_REF] Feng | Learning-based compositional verification for synchronous probabilistic systems[END_REF]). for all a ∈ α do 5:

Require: PFAs

υ ′ 1 := υ 1 P 1 (a); υ ′ 2 := υ 2 P 2 (a); w ′ := wa

We also define ι i and κ i as in Section 5.2.1. Inspired by the language equivalence decision algorithm in [START_REF] Tzeng | A polynomial-time algorithm for the equivalence of probabilistic automata[END_REF], our method proceeds by expanding a tree. Each node of the tree is of the form ( υ 1 , υ 2 , w), where w is a word and υ i = ι i P i (w) (for i = 1, 2) is the vector of probabilities of reaching each state via word w in A i . Note that υ i κ i is the probability of PFA A i accepting the word w. The root of the tree is ( ι 1 , ι 2 , ε), where ε is the empty word. As shown in Figure 5.4, we use a queue of tree nodes, which expands the tree in breadth-first order. In addition, we maintain a set V of non-leaf nodes, which initially only contains the root. The main difference between our method and [START_REF] Tzeng | A polynomial-time algorithm for the equivalence of probabilistic automata[END_REF] is that we adopt different criteria to decide when to add a node to the non-leaf set V . In [START_REF] Tzeng | A polynomial-time algorithm for the equivalence of probabilistic automata[END_REF], the set V is maintained by calculating the span of vector space. However, for the language inclusion check, we cannot simply use the same criteria.

In each iteration, we remove a node ( υ 1 , υ 2 , w) from the head of queue. We then expand the tree by appending a set of its child nodes ( υ ′ 1 , υ ′ 2 , w ′ ), where υ ′ 1 := υ 1 P 1 (a), υ ′ 2 := υ 2 P 2 (a) and w ′ := wa for all actions a ∈ α. If there is a node

), then the algorithm terminates and returns w ′ as a counterexample for A 1 ⊑ A 2 . Otherwise, we check if we can prune each child node ( υ ′ 1 , υ ′ 2 , w ′ ) (i.e. make it a leaf node) by seeing if it satisfies either of the following two criteria: (C1) υ ′ 1 κ 1 = 0; (C2) There exist |V | non-negative rational numbers ρ i such that, for all

where ≤ and ≥ denote pointwise comparisons between vectors.

Criterion (C1) is included because it is never possible to find a counterexample word with accepting probability less than υ ′ 1 κ 1 = 0. Criterion (C2) is included because any node satisfying it would guarantee υ ′ 1 κ 1 ≤ υ ′ 2 κ 2 ; moreover, if the algorithm terminates and a node satisfies (C2), all of its descendants also satisfy (C2). We can thus make it a leaf node. In practice, (C2) can easily be checked using an SMT solver. If a node cannot be pruned, we add it to the tail of queue and to the non-leaf set V. The algorithm terminates if queue becomes empty, concluding that

Correctness and termination. The correctness of the semi-algorithm in Figure 5.4 is shown formally in [START_REF] Feng | Learning-based compositional verification for synchronous probabilistic systems[END_REF]. A guarantee of termination, on the other hand, cannot be expected due to the undecidability of the underlying problem.

L*-Style Learning for PFAs

In this section, we propose a novel method to learn a PFA for a target weighted language generated by an unknown PFA. It works in a similar style to the well-known L* algorithm [START_REF] Angluin | Learning regular sets from queries and counterexamples[END_REF] for learning regular languages: it constructs an observation table (of acceptance probabilities for each word) based on two types of queries posed to a teacher. Membership queries ask the probability of accepting a particular word in the target PFA; equivalence queries ask whether a hypothesised PFA yields exactly the target language.

Figure 5.5 shows the learning algorithm. It builds an observation table (P, E, T ), where P is a finite, non-empty, prefix-closed set of words, E is a finite, non-empty, suffix-closed set of words and T : ((P ∪ P • α)•E) → [0, 1] maps each word to its accepting probability in the target language ( • denotes concatenation over sets). The rows of table (P, E, T ) are labelled by elements in the prefix set P ∪ P •α and the columns are labelled by elements in the suffix set E. The value T (u•e) of the entry at row u and column e is the acceptance probability of the word u•e. We use row(u) to represent the |E|-dimensional row vector in the table labelled by the prefix u ∈ (P ∪ P •α).

Inspired by [START_REF] Bergadano | Learning behaviors of automata from multiplicity and equivalence queries[END_REF], which gives an L*-style algorithm for learning multiplicity automata, we define the notions of closed and consistent observation tables by establishing linear dependencies between row vectors. Observation table (P, E, T ) is closed if, for all u∈P and a∈α, there exist non-negative rational coefficients φ i such that row(u • a) = ui∈P φ i row(u i ) and consistent if, for any rational coefficients ψ i , ∀e ∈ E. ui∈P ψ i T (u i •e) = 0 implies ∀a ∈ α, e ∈ E. ui∈P ψ i T (u i •a•e) = 0. The need for coefficients to be non-negative (for closed) is a stronger condition than in [START_REF] Bergadano | Learning behaviors of automata from multiplicity and equivalence queries[END_REF].

As shown in Figure 5.5, the observation table is filled with the results of membership queries until it is both closed and consistent. At each step, if (P, E, T ) is not closed (resp. consistent), then the algorithm finds u ∈ P, a ∈ α (resp. a ∈ α, e ∈ E) that make it not closed (resp. consistent), according to the definitions above, and adds u.a (resp. a.e) to the table. When (P, E, T ) is closed and consistent, the learning algorithm builds a hypothesis PFA A (see below) and poses an equivalence query. If the teacher answers "no" (that A does not yield the target language), a counterexample c ∈ α * is given, for which Pr A (c) is incorrect. The algorithm adds c and all its prefixes to P , updates the observation table and continues to check if the table is closed and consistent. If the teacher answers "yes", the algorithm terminates and returns A.

Construction of a hypothesis PFA A = (S, s, α, P), from a closed and consistent table (P, E, T ), proceeds as follows. First, we find a subset of P , denoted con(P ), such that every element of {row(u)|u ∈ P } can be represented as a conical combination of elements in {row(v)|v ∈ con(P )}, i.e. there are nonnegative rational coefficients λ i such that, for all u ∈ P , row(u) = vi∈con(P ) λ i row(v i ). The set of states in the PFA is then S = {s 0 , . . . , s n-1 }, where each state s i corresponds to a row vector in {row(v)|v ∈ con(P )} and the initial state s corresponds to row(ε). To obtain P(a) for each a ∈ α, we compute, for s i ∈ S, rational coefficients γ j such that row(s i • a) = sj ∈S γ j row(s j ) and then define P(a)[s i , s j ] := γ j • (T (s j • ε)/T (s i • ε)).

Correctness and termination.

When the learning algorithm terminates, it returns a correct PFA, as guaranteed by the equivalence query check. Unfortunately, we cannot prove the termination of our method. For L*, the corresponding proof uses the existence of a unique minimal DFA for a regular language. However, an analogous property does not exist for weighted languages and PFAs. According to [START_REF] Bergadano | Learning behaviors of automata from multiplicity and equivalence queries[END_REF], the smallest multiplicity automaton can be learnt given a weighted language. However, as shown in [START_REF] Denis | Learning classes of probabilistic automata[END_REF], converting CONNECT 231167

Require:

The alphabet α of a target weighted language generated by an unknown PFA. Ensure: A PFA accepting the target language.

1: initialise the observation table (P, E, T ), letting P = E = {ε}, where ε is the empty word 2: fill T by asking membership queries for ε and each action a ∈ α 3: while (P, E, T ) is not closed or not consistent do 4:

if (P, E, T ) is not closed then find u ∈ P, a ∈ α that make (P, E, T ) not closed 5:

add u • a to P , and extend T to (P ∪ P • α) • E using membership queries 6:

if (P, E, T ) is not consistent then find a ∈ α, e ∈ E that make (P, E, T ) not consistent 7:

add a • e to E, and extend T to (P ∪ P • α) • E using membership queries 8: construct a hypothesised PFA A and ask an equivalence query 9: if answer = no, with a counterexample c then add c and all its prefixes to P

Update table

Membership query

Update table

Generate conjecture

Inputs: Outputs:

Property false:

(analyse word w)

Equivalence query a multiplicity automaton to a PFA (even for the subclass that define stochastic languages) is not always possible.

Learning Assumptions for Compositional Verification

Finally, we build upon the techniques introduced in Sections 5.2.3 and 5.2.4 to produce a fully-automated implementation of the assume-guarantee framework proposed in Section 5.2.2. In particular, we use PFA learning to automatically generate assumptions to perform compositional verification. Figure 5.6 summarises the overall structure of our approach, which aims to verify (or refute) M 1 M 2 |= G p for two PIOSs M 1 , M 2 and a probabilistic safety property G p . This is done using proof rule (ASYM-PIOS) from Section 5.2.2, with the required assumption PFA A about component M 1 being generated through learning. The left-hand side of the figure shows the learning algorithm of Section 5.2.4, which drives the whole process; the right-hand side shows the teacher. The teacher answers membership queries (about word w) by computing the probability Pr M1 τ (w) of word w in M 1 . It answers equivalence queries (about conjectured PFA A) by checking if A satisfies both premises of rule (ASYM-PIOS): (i) M 1 ⊑ w A, and (ii) A M 2 G p . The first is done using Proposition 5.8 and the algorithm in Section 5.2.3. The second is done using Proposition 5.11, which reduces to probabilistic model checking of the DTMC pios(A) M 2 .

If both premises are true, we can conclude that M 1 M 2 |= G p holds. Otherwise, the teacher needs to provide a counterexample c for the learning algorithm to update the observation table and proceed. If premise (i) failed, then c is taken as the word showing the violation of (weak) language inclusion. If premise (ii) failed, we try to extract c from the results of model checking. We extract a probabilistic counterexample [START_REF] Han | Counterexample generation in probabilistic model checking[END_REF] C: a set of paths showing pios(A)||M 2 |= G p . Following the same approach as [START_REF] Feng | Compositional verification of probabilistic systems using learning[END_REF], we transform C into a (small) fragment of M 1 (denoted M C 1 ) and check whether M C 1 ||M 2 |= G p . If so, CONNECT 231167