Many-Valued Institutions for Constraint Specification

Abstract

We advance a general technique for enriching logical systems with soft constraints, making them suitable for specifying complex software systems where parts are put together not just based on how they meet certain functional requirements but also on how they optimise certain constraints. This added expressive power is required, for example, for capturing quality attributes that need to be optimised or, more generally, for formalising what are usually called service-level agreements. More specifically, we show how institutions endowed with a graded semantic consequence can accommodate soft-constraint satisfaction problems. We illustrate our approach by showing how, in the context of service discovery, one can quantify the compatibility of two specifications and thus formalise the selection of the most promising provider of a required resource.

Work partially supported by funds from the Spanish Ministry for Economy and Competitiveness (MINECO) and the European Union (FEDER funds) under grant COMMAS (ref. TIN2013-46181-C2-1-R).

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The problem of supporting the process of building complex systems from simpler parts has deserved a lot of attention since the birth of software engineering, and has been addressed by formal methods of different kinds (e.g. [12]). One such family of formal methods is known under the general heading of ‘algebraic specification’ (e.g. [23]). In a nutshell, the method is based on the simple principle that parts of software applications (components, modules, and so on) should expose interfaces where they specify required and provided properties. Those parts can then be connected if their interfaces match (in the sense that required properties are met by those provided).

A well-known theory of algebraic specifications is based on the theory of ‘institutions’ [17]. Essentially, institutions provide logical languages for formulating the properties that will go on the interfaces of parts and an algebra of models that provide mathematical abstractions of the parts; properties and models are related in a way that supports compositionality, i.e. that the properties of a complex whole can be derived from those of its parts.

That theory is based on exact matches between interfaces, i.e. either the provided properties satisfy the required ones or they do not. Whereas this has served well the specification of functional requirements, software development has evolved in ways that require the specification of properties that can be met in more than one way, i.e. that express ‘soft’ constraints. A typical example is service-oriented software development where software applications (requesters) can choose among several application suppliers (providers) every time a need for a service arises; the requester first needs to discover a provider that can guarantee, through an interface, the fulfilment of certain requirements, and then to bind to a provider that optimises the satisfaction of certain constraints (e.g. shipment costs in relation to delivery time) establishing a ‘service-level agreement’. Another example arises in the context of software product lines, where the selection of features may require the optimisation of given quality attributes of the resulting software variant [18].

In this context, soft-constraint systems have been successfully employed for capturing such non-functional requirements in service-oriented architectures [20, 27], including the negotiation of service-level agreements [6], as well as in the context of software product lines (e.g. [2]). The two main approaches to soft constraint satisfaction problems, scsp [4] and vcsp [9, 24], generalise the classical crisp variant of constraint satisfaction problems (csp) by evaluating constraints over c-semirings and valuation structures, respectively.

Our aim in this paper is to extend the institution-based theory of algebraic specifications to address soft constraints. Although the idea of extending abstract data types with soft constraints was already outlined, essentially through examples, in [15], it lacks a rigorous formalisation within the setting of institutions. Such an extension is essential to provide a logic-independent foundation that, on the one hand, can be used to support different specification languages and, on the other hand, can be integrated in development environments that, like Hets [21], offer automated support for the specification and analysis of systems.

To this end, in Sect. 2, we first extend the traditional notion of institution along the lines of [10] by replacing the boolean space of truth values with residuated lattices [16], which offer a unifying truth structure for both idempotent c-semirings and valuation structures [3]. Using a simple example, we explain how first-order logic specifications can be extended with soft constraints, and then show how this extension can be generalised to define a logical system of soft constraints as a many-valued institution parameterised by a stratified logic [1]. Based on this construction, in Sect. 3, we formalise the mechanism of selecting a most promising provider of a needed resource in the context of service discovery and binding on the quantification of the compatibility of two constraint specifications as a value of a residuated lattice; we achieve this by defining a compatibility score using the concept of graded semantic consequence [10]. Lastly, in Sect. 4 we study the evolutionary behaviour of service applications. We show how our framework captures situations where different service components (constraint specifications) are based on different truth spaces, which arise in heterogeneous complex systems. We also take into account the dynamicity of preferences during the development of a system (the change of the truth structures, or of the preferences expressed as sentences of the specifications), and underline the uncertainties of predicting the evolutionary behaviour of service applications. The paper relies on basic knowledge of category theory, for example at the level of [11, 22].

2 Soft-Constraint Specification in Institutions

In this section, after briefly recalling the notion of institution, we focus on the construction of a particular type of institution that is suitable for defining soft csp specifications. As an example, we describe in more detail how constraint specifications can be written over the institution of first-order logic. This allows us to identify the properties and the additional structure that an institution $\mathcal {I}$ should have in order to deal with soft constraints, and to further define a many-valued institution $\mathrm {CSP}(\mathcal {I})$.

2.1 Institutions

The notion of institution was introduced by Goguen and Burstall [17] at the beginning of the 80’s to allow for studying concepts for structuring and modularising specifications, independently of the actual formalism to be used for writing the specifications. Intuitively, the notion of institution is an abstract view of the main ingredients of a logical or specification formalism. In particular, an institution consists of:

• A category of signatures, where signatures are the basic elements that we use for building formulas. For instance, in first-order logic, signatures are sets of sorts and function and predicate symbols together with their arity.

• A functor $\mathrm {Sen}$ that associates, to each signature $\varSigma$, the set of all the formulas that can be written using $\varSigma$. In the case of first-order logic, this would mean all the formulas that can be written using the predicate and function symbols in the signature, and including the standard logical connectives and quantifiers. $\mathrm {Sen}$ is a functor and not just a mapping, because we want to explicitly associate to each signature morphism $\varphi :\varSigma \rightarrow \varSigma '$ that translates symbols in $\varSigma$ into symbols in $\varSigma '$, the mapping $\mathrm {Sen}(\varphi )$ that translates formulas over $\varSigma$ into formulas over $\varSigma '$.

• A functor $\mathrm {Mod}$ that associates, to each signature $\varSigma$, the category of all its models. In the case of first-order logic, $\mathrm {Mod}(\varSigma )$ is the category of all $\varSigma$-algebras. Again, $\mathrm {Mod}$ is a functor and not just a mapping, because we want to explicitly associate to each signature morphism $\varphi :\varSigma \rightarrow \varSigma '$ that translates symbols in $\varSigma$ into symbols in $\varSigma '$, the reduct associated to that morphism. In particular, if $A'$ is a $\varSigma '$-algebra, its reduct along $\varphi :\varSigma \rightarrow \varSigma '$ would be a $\varSigma$-algebra $A$, where each symbol $s$ in $\varSigma$ is interpreted like the symbol $\varphi (s)$ in $A'$.

• A satisfaction relation that, given a $\varSigma$-formula $\rho$ and a $\varSigma$-model $M$, tells us if $M$ satisfies $\rho$. Moreover, it is required that institutions (i.e. the formalisms that we consider valid) satisfy the satisfaction condition that states that satisfaction does not depend on the choice of signature, i.e. satisfaction is invariant under language translation.

Definition 1

(Institution). An institution $\mathcal {I}$ consists of

• a category $\mathrm {\mathbb {S}ig}^{\mathcal {I}}$ whose objects are called signatures,

• a sentence functor $\mathrm {Sen}^{\mathcal {I}} :\mathrm {\mathbb {S}ig}^{\mathcal {I}} \rightarrow \mathrm {\mathbb {S}et}$ giving for every signature $\varSigma$ the set $\mathrm {Sen}^{\mathcal {I}}(\varSigma )$ of $\varSigma$-sentences and for every signature morphism $\varphi$ the sentence translation map $\mathrm {Sen}^{\mathcal {I}}(\varphi )$,

• a model functor $\mathrm {Mod}^{\mathcal {I}} :(\mathrm {\mathbb {S}ig}^{\mathcal {I}})^{\mathrm {op}} \rightarrow \mathrm {\mathbb {C}at}$ defining for every signature $\varSigma$ the category $\mathrm {Mod}^{\mathcal {I}}(\varSigma )$ of $\varSigma$-models and $\varSigma$-model homomorphisms, and for every signature morphism $\varphi$ the reduct functor $\mathrm {Mod}^{\mathcal {I}}(\varphi )$,

• a satisfaction relation ${ \models ^{\mathcal {I}}_{\varSigma }} \subseteq {{|\mathrm {Mod}^{\mathcal {I}}(\varSigma )|} \times \mathrm {Sen}^{\mathcal {I}}(\varSigma )}$ for every signature $\varSigma$,

such that the satisfaction condition $\mathrm {Mod}^{\mathcal {I}}(\varphi )(M') \models ^{\mathcal {I}}_{\varSigma } \rho \quad \text {iff} \quad M' \models ^{\mathcal {I}}_{\varSigma '} \mathrm {Sen}^{\mathcal {I}}(\varphi )(\rho )$ holds for any signature morphism $\varphi :\varSigma \rightarrow \varSigma '$, $\varSigma '$-model $M'$ and $\varSigma$-sentence $\rho$.

We may omit sub- or super-scripts when there is no risk of confusion. The sentence translation $\mathrm {Sen}^{\mathcal {I}}(\varphi )$ and the reduct functor $\mathrm {Mod}^{\mathcal {I}}(\varphi )$ may also be denoted by $\varphi (\_)$ and $\_\mathord {\upharpoonright }_{\varphi }$. When $M = M'\mathord {\upharpoonright }_{\varphi }$ we say that $M$ is a $\varphi$-reduct of $M'$ and that $M'$ is a $\varphi$-expansion of $M$.

A specification in an institution $\mathcal {I}$ is a pair $(\varSigma , E)$ consisting of a signature and a collection of sentences (axioms) in the language of that signature, i.e. $E\subseteq \mathrm {Sen}^{\mathcal {I}}(\varSigma )$ – what is usually called a (theory) presentation. A morphism of specifications $\phi :(\varSigma ,E) \rightarrow (\varSigma ',E')$ is a signature morphism $\phi :\varSigma \rightarrow \varSigma '$ such that $E' \models \phi (E)$, i.e. the axioms of $(\varSigma , E)$ are semantic consequences of $(\varSigma ', E')$ – such a morphism formalises the way $(\varSigma , E)$ is a part of $(\varSigma ', E')$. Presentations and their morphisms constitute a category, which we denote by $\mathbb {P}\mathrm {res}^{\mathcal {I}}$.

An example of a specification in first-order logic is given in Fig. 1 (written in a Casl-like syntax [8]) – the specification of residuated lattices, i.e. the first-order structures that satisfy the axioms of the specification are the residuated lattices, which play an essential role in this paper.¹

Fig. 1.

The specification $(\varSigma _{\mathbb {RL}}, E_{\mathbb {RL}})$ of residuated lattices

2.2 Generalising the Truth Space

As said above, institutions are an abstraction of logical formalisms, where you describe its main ingredients, in particular, when a given formula is satisfied (or is not satisfied) by a given model. However, when dealing with soft constraints, we need to allow for different degrees of satisfaction. This means, replacing the ‘true’/‘false’ structure of truth values by a more complex kind of structures. In this paper, we consider that these structures are residuated lattices. The choice for residuated lattices is motivated by the fact that the addition of a residual operation to semirings and valuation structures has been shown in [3, 7] to provide a unifying framework for soft csp: residuated lattices generalise both commutative idempotent semirings and fair valuation structures, which are the structures usually employed with local consistency techniques [5].

We actually need for the lattices to be complete (i.e. that a supremum and an infimum exists for every set of degrees of satisfaction).

Definition 2

(Complete Residuated Lattices). A complete residuated lattice $\mathcal {L} = (L, \le , \vee , \wedge , *, \rightarrow , 0, 1)$ is a complete lattice (with supremum $\vee$, infimum $\wedge$, smallest element $0$ and greatest element $1$) equipped with a monoidal structure (a commutative and associative binary operation $*$ having $1$ as identity) such that, for all elements $x,y,z \in L$, $(x *y) \le (x *z) \text { if } y \le z$, and $y \le (x \rightarrow z ) \text { iff } x *y \le z$.

A morphism $\lambda :\mathcal {L} \rightarrow \mathcal {L}'$ is a function $\lambda :L \rightarrow L'$ that is simultaneously a morphism of complete lattices and of commutative monoids, and is compatible with the residual $\rightarrow$. We denote the corresponding category by $\mathbb {RL}$.

Intuitively, the set $L$ provides the degrees of satisfaction (with $0$ as dissatisfaction and $1$ as total satisfaction) which are ordered according to $\vee$ or, equivalently, to $\wedge$: $a \le b$ iff $a \vee b = b$. The operation $*$ captures the accumulation of truth values that result from successive inferences, and $\rightarrow$ corresponds to the entailment between two degrees of satisfaction. To capture soft csp as a many-valued logical system, we therefore extend the notion of institution in keeping with [10]:

Definition 3

( $\mathbb {RL}$ -institution). An $\mathbb {RL}$ -institution $\mathcal {I}$ is defined as a tuple $(\mathrm {\mathbb {S}ig}^{\mathcal {I}}, \mathrm {Sen}^{\mathcal {I}}, \mathrm {Mod}^{\mathcal {I}}, \mathcal {RL}^{\mathcal {I}}, \models ^{\mathcal {I}})$ consisting of

• a category $\mathrm {\mathbb {S}ig}^{\mathcal {I}}$, a functor $\mathrm {Sen}^{\mathcal {I}}$, and a functor $\mathrm {Mod}^{\mathcal {I}}$ as for an institution,

• a truth space functor $\mathcal {RL}^{\mathcal {I}} :(\mathrm {\mathbb {S}ig}^{\mathcal {I}})^{\mathrm {op}} \rightarrow \mathbb {RL}$ giving for every signature a complete residuated lattice, and

• a many-valued satisfaction relation ${ \models ^{\mathcal {I}}_{\varSigma }} :{{|\mathrm {Mod}^{\mathcal {I}}(\varSigma )|} \times \mathrm {Sen}^{\mathcal {I}}(\varSigma ) \rightarrow \mathcal {RL}^{\mathcal {I}}(\varSigma )}$ for every signature $\varSigma$,

such that the equality $\bigl (\mathrm {Mod}^{\mathcal {I}}(\varphi )(M') \models ^{\mathcal {I}}_{\varSigma } \rho \bigr ) = \mathcal {RL}^{\mathcal {I}}(\varphi )\bigl (M' \models ^{\mathcal {I}}_{\varSigma '} \mathrm {Sen}^{\mathcal {I}}(\varphi )(\rho )\bigr )$ holds for any signature morphism $\varphi :\varSigma \rightarrow \varSigma '$, $\varSigma '$-model $M'$ and $\varSigma$-sentence $\rho$. The satisfaction relation extends to a consequence relation over $E, \varGamma \subseteq \mathrm {Sen}(\varSigma )$ as follows: $E \models ^{\mathcal {I}}_{\varSigma } \varGamma = \bigwedge \{(M \models ^{\mathcal {I}}_{\varSigma } E) \rightarrow (M \models ^{\mathcal {I}}_{\varSigma } \varGamma ) \mid M \in |{\mathrm {Mod}(\varSigma )}|\}$.

The rest of this section is dedicated to showing how, starting from an institution $\mathcal {I}$ that satisfies some structural properties, we can define an $\mathbb {RL}$-institution $\mathrm {CSP}(\mathcal {I})$ of soft-constraint satisfaction problems based on $\mathcal {I}$.

2.3 The First-Order Soft-Constraint $\mathbb {RL}$-institution

To specify systems using constraints, which we evaluate over residuated lattices, we consider only those presentations that extend $(\varSigma _{\mathbb {RL}},E_{\mathbb {RL}})$, that is presentations $(\varSigma , E)$ with $\varSigma _{\mathbb {RL}} \subseteq \varSigma$ and $E \models E_{\mathbb {RL}}$. This means that, on the one hand, every $(\varSigma , E)$-model has an underlying residuated lattice (its reduct as a $\varSigma _{\mathbb {RL}}$-model) and that, on the other hand, we can make use of the symbols in $\varSigma _{\mathbb {RL}}$ when writing the sentences of $E$. Moreover, we admit only morphisms of presentations $\varphi :(\varSigma ,E) \rightarrow (\varSigma ',E')$ that do not change the symbols of $\varSigma _{\mathbb {RL}}$.

Fig. 2.

The specifications $\textsc {BookData}$ and $\textsc {Customer}$

Example 4

Figure 2 depicts the specification of a customer’s book-buying preferences. $\textsc {Customer}$ extends the specification $\textsc {BookData}$, which concerns a book trader that stores a number of books and offers three kinds of delivery: standard, express and online; for every book, two operations return the language in which the book is written and the number of days associated with each delivery mode.

Customer also extends the specification of residuated lattices given in Fig. 1 and adds two new function symbols – languagePref and deliveryPref – both of sort Sat. Because every model of Sat is a residuated lattice, the two new function symbols can be used to express preferences through axioms of the specification: German is preferred to English and French to German; regardless of the book and delivery time, online delivery is preferred to express and to standard; standard delivery is preferred to express when express delivery takes three days or more and standard takes seven days or less.

In order to include constraints in specifications, we need a new syntactic category through which we can declare constraint variables, and we need constraint sentences through which we can express preferences over those variables that we wish to be optimised. For example, in the case of Customer, we could specify the following constraint variables and sentences:

A constraint sentence (or constraint for short) is a term of sort Sat. The specified constraints express the existence of preferences on the language in which the book is written, and the wish to optimise the method of delivery relatively to the expected delivery period. This optimisation is made relative to the axiomatisation of the preferences in Customer: given a model of Customer and a valuation $\chi$ of the constraint variables (i.e. a choice of a book and of a delivery mode), every constraint is assigned a value (degree of satisfaction) in the residuated lattice; the degree of satisfaction of a constraint in a model can then be defined as the supremum of all the degrees of satisfaction obtained by varying $\chi$, i.e. for all possible combinations of books and delivery modes, which in soft csp is known as the best level of consistency [5].

The extension of first-order logic with constraint sentences is best accommodated in what are called stratified institutions [1], which provide an elegant way of capturing the valuations of constraint variables through states of models:

Definition 5

(Stratified Institution). A stratified institution $\mathcal {I}$ is defined as a tuple $(\mathrm {\mathbb {S}ig}^{\mathcal {I}}, \mathrm {Sen}^{\mathcal {I}}, \mathrm {Mod}^{\mathcal {I}}, [\![\_]\!]^{\mathcal {I}}, \models ^{\mathcal {I}} )$ ² where

• $\mathrm {\mathbb {S}ig}^{\mathcal {I}}$, $\mathrm {Sen}^{\mathcal {I}}$ and $\mathrm {Mod}^{\mathcal {I}}$ are as for an institution,

• $[\![\_]\!]^{\mathcal {I}}$ is a stratification, i.e.  a collection of

  • functors $[\![\_]\!]^{\mathcal {I}}_{\varSigma } :\mathrm {Mod}^{\mathcal {I}}(\varSigma ) \rightarrow \mathrm {\mathbb {S}et}$ for every signature $\varSigma$, and

  • surjective³ natural transformations $[\![\_]\!]^{\mathcal {I}}_{\phi } :[\![\_]\!]^{\mathcal {I}}_{\varSigma '} \Rightarrow \mathrm {Mod}^{\mathcal {I}}(\phi ) \mathbin {;}[\![\_]\!]^{\mathcal {I}}_{\varSigma }$ for every signature morphism $\phi :\varSigma \rightarrow \varSigma '$,

• the satisfaction relation $M \models ^{m}_{\varSigma } \rho$ is parameterised by model states,

such that, for every $\phi :\varSigma \rightarrow \varSigma '$, $M' \in |{\mathrm {Mod}^{\mathcal {I}}(\varSigma ')}|$, $m' \in [\![{M'}]\!]^{\mathcal {I}}_{\varSigma '}$, $\rho \in \mathrm {Sen}^{\mathcal {I}}(\varSigma )$: $\mathrm {Mod}^{\mathcal {I}}(\phi )(M') \models ^{[\![{M'}]\!]^{\mathcal {I}}_{\phi }(m')}_{\varSigma } \rho \quad \text { iff } \quad M' \models _{\varSigma '}^{m'} \mathrm {Sen}^{\mathcal {I}}(\phi )(\rho )$.

The stratified version of the institution of first-order logic that we adopt, which will be denoted by $\underline{\mathrm {FOL}}$, has as signatures pairs $\langle \varSigma , V\rangle$ of a first-order signature $\varSigma$ and a set of sorted constraint variables $V$. The $\langle \varSigma , V\rangle$-sentences are simply sentences over $\varSigma$ with the constraint variables $V$ as constants (nullary operation symbols). The models of a signature $\langle \varSigma , V\rangle$ are the $\varSigma$-models, while the states of a model $M$ are the valuations $\chi :V \rightarrow M$, i.e., sorted functions from $V$ to the many-sorted carrier set of $M$. The satisfaction of a $\langle \varSigma , V\rangle$-sentence $\rho$ by a $\langle \varSigma , V\rangle$-model $M$ in a state $\chi \in [\![{M}]\!]_{\langle \varSigma , V \rangle }$ is defined as the satisfaction of $\rho$ in $(M,\chi )$, i.e. in the extension of $M$ with the interpretation $\chi$ of variables.

Notice that every specification in the institution of first-order logic defines a specification in $\underline{\mathrm {FOL}}$ by choosing an empty set of constraint variables, i.e. we identify a first-order specification such as $(\varSigma _{\mathbb {RL}},E_{\mathbb {RL}})$ with $(\langle \varSigma _{\mathbb {RL}},\emptyset \rangle ,E_{\mathbb {RL}})$.

We can now summarise the construction of the $\mathbb {RL}$-institution $\mathrm {CSP}(\underline{\mathrm {FOL}})$ of first-order soft-constraint satisfaction problems:

Signatures. A signature is a pair $(\mathcal {L}, \varDelta )$ of a complete residuated lattice $\mathcal {L}$ and an extension $\varDelta :(\varSigma _{\mathbb {RL}},E_{\mathbb {RL}}) \rightarrow (\langle \varSigma , V\rangle ,E)$ of the specification of residuated lattices. We include a residuated lattice as part of a signature in order to let specifiers decide on which space of degrees of satisfaction they want to work with. For simplicity we may denote $(\mathcal {L}, \varDelta :(\varSigma _{\mathbb {RL}},E_{\mathbb {RL}}) \rightarrow (\langle \varSigma , V\rangle ,E))$ by $(\mathcal {L},\varSigma , V,E)$.

Constraint Sentences. A constraint sentence (or constraint for short) for a signature $(\mathcal {L},\varSigma , V,E)$ is a $\langle \varSigma , V\rangle$-term of sort Sat.

Models. The models of $(\mathcal {L},\varSigma , V,E)$ are the models of $(\langle \varSigma , V\rangle ,E)$ whose reducts along $\varDelta$ are complete and admit a morphism into $\mathcal {L}$. Notice that it would be too restrictive to choose only those models of $(\langle \varSigma , V\rangle ,E)$ whose reducts over $\varSigma _{\mathbb {RL}}$ are $\mathcal {L}$ because we wish to support mappings between specifications that use different residuated lattices as their spaces of degrees of satisfaction. Formally, a model of $(\mathcal {L}, \varDelta :(\varSigma _{\mathbb {RL}},E_{\mathbb {RL}}) \rightarrow (\langle \varSigma , V\rangle ,E))$ is a pair (M, f) consisting of a model M of $(\langle \varSigma , V\rangle ,E)$ together with a morphism $f :M\mathord {\upharpoonright }_{\varDelta } \rightarrow \mathcal {L}$.

Satisfaction Relation. For every constraint signature $(\mathcal {L},\varSigma , V,E)$ and every model $M$, we define the value of $c$ over $M$ as the best level of consistency:

$$ \bigl ((M,f) \models _{(\mathcal {L},\varSigma , V,E)} c \bigr ) = f\bigl (\textstyle \bigvee _{\chi \in [\![{M}]\!]_{\varSigma }} \mathrm {eval}_{(M, \chi )}(c)\bigr ), $$

where $\mathrm {eval}_{(M, \chi )}(c)$ is the usual (inductively defined) interpretation of the first-order $\langle \varSigma ,V\rangle$-term $c$ in $(M,\chi )$. Note that $f$ translates the supremum to the residuated lattice $\mathcal {L}$ chosen by the specifier.

2.4 The $\mathrm {CSP}(\mathcal {I})$ $\mathbb {RL}$-institution of Soft CSP over $\mathcal {I}$

We now generalise the construction $\mathrm {CSP}(\underline{\mathrm {FOL}})$ to an arbitrary stratified institution $\mathcal {I} = (\mathrm {\mathbb {S}ig}^{\mathcal {I}}, \mathrm {Sen}^{\mathcal {I}}, \mathrm {Mod}^{\mathcal {I}}, [\![\_]\!]^{\mathcal {I}}, \models ^{\mathcal {I}} )$ that satisfies the following conditions:

• C1. To make residuated lattices available to the specifier, we require the existence of an $\mathcal {I}$-presentation $(\varSigma _{\mathbb {RL}}, E_{\mathbb {RL}})$ such that $\mathbb {RL}\subseteq \mathrm {Mod}^{\mathcal {I}}(\varSigma _{\mathbb {RL}}, E_{\mathbb {RL}})$. This does not restrict applicability as most institutions suitable for the domains where soft constraints are useful will provide the ability to specify data structures.

• C2. In order to be able to express constraints, we require the existence of a functor $\mathrm {C} :\mathrm {\mathbb {S}ig}^{\mathcal {I}} \rightarrow \mathrm {\mathbb {S}et}$ that provides the set of constraints for each signature. In addition, we assume that for every object $\varDelta :(\varSigma _{\mathbb {RL}}, E_{\mathbb {RL}}) \rightarrow (\varSigma , E)$ of the comma category $(\varSigma _{\mathbb {RL}}, E_{\mathbb {RL}})/\mathbb {P}\mathrm {res}^{\mathcal {I}}$ there exists a family of functors $|{\_}|_{\varSigma } :[\![\_]\!]_{\varSigma } \rightarrow [ \mathrm {C}(\varSigma ) \rightarrow \mathrm {Mod}^{\mathcal {I}}(\varDelta )]$ such that, for any signature morphism $\varphi :\varSigma \rightarrow \varSigma '$, $\varSigma '$-model $M'$, state $\chi ' \in [\![{M'}]\!]_{\varSigma '}$, and constraint $c \in \mathrm {C}(\varSigma )$, $|{M'\mathord {\upharpoonright }_{\varphi }}|_{\varSigma }([\![{M'}]\!]_{\varphi }(\chi '))(c) = |{M'}|_{\varSigma '}(\chi ')(\varphi (c))$.

On this basis, we define the logical system $\mathrm {CSP}(\mathcal {I})$ as follows:

• The category $\mathrm {\mathbb {S}ig}^{\mathrm {CSP}(\mathcal {I})}$ of constraint signatures is the product category of $\mathbb {RL}^{\mathrm {op}}$ and the comma category $(\varSigma _{\mathbb {RL}}, E_{\mathbb {RL}})/\mathbb {P}\mathrm {res}^{\mathcal {I}}$.

• $\mathrm {Sen}^{\mathrm {CSP}(\mathcal {I})}((\mathcal {L}, \varDelta :(\varSigma _{\mathbb {RL}}, E_{\mathbb {RL}}) \rightarrow (\varSigma , E)) = \mathrm {C}(\varSigma )$.

• $\mathrm {Mod}^{\mathrm {CSP}(\mathcal {I})}(\mathcal {L}, \varDelta ) = \mathrm {Mod}^{\mathcal {I}}(\varDelta )/\mathcal {L}$, with $\mathrm {Mod}^{\mathcal {I}}(\varDelta ) :\mathrm {Mod}^{\mathcal {I}}(\varDelta )^{-1}(\mathbb {RL}) \rightarrow \mathbb {RL}$.

• Given an $(\mathcal {L}, \varDelta )$-model $(M, f :M\mathord {\upharpoonright }_{\varDelta } \rightarrow \mathcal {L})$ and a sentence $\rho \in \mathrm {Sen}(\mathcal {L}, \varDelta )$, the satisfaction of $\rho$ by $(M,f)$ is defined as:

  $$\begin{aligned} \bigl ((M,f) \models _{(\mathcal {L},\varDelta )} \rho \bigr ) = f\bigl (\textstyle \bigvee _{\chi \in [\![{M}]\!]_{\varSigma }} |{M}|_{\varSigma }(\chi )(\rho )\bigr ) \end{aligned}$$

Theorem 6

For any stratified institution $\mathcal {I}$ satisfying the conditions C1 and C2 above, $\mathrm {CSP}(\mathcal {I})$ is an $\mathbb {RL}$-institution.

The following results are important for Sect. 3.

Proposition 7

$\mathrm {CSP}(\mathcal {I})$ inherits the following properties of $\mathcal {I}$:

• 1. If $\mathrm {\mathbb {S}ig}^{\mathcal {I}}$ is finitely cocomplete so is $\mathrm {\mathbb {S}ig}^{\mathrm {CSP}(\mathcal {I})}$.

• 2. If $\mathcal {I}$ has (weak) model amalgamation, so does $\mathrm {CSP}(\mathcal {I})$.

• 3. Given factorisation systems [19] $(\mathbb {E},\mathbb {M})$ for $\mathrm {\mathbb {S}ig}^{\mathcal {I}}$ and $(\mathbb {E}_{\mathbb {RL}}, \mathbb {M}_{\mathbb {RL}})$ for $\mathbb {RL}$, we obtain a factorisation system for $\mathrm {\mathbb {S}ig}^{\mathrm {CSP}(\mathcal {I})}$ by taking the epimorphisms to be the pairs of arrows in $\mathbb {M}_{\mathbb {RL}}$ and $(\varSigma _{\mathbb {RL}},E_{\mathbb {RL}})/\mathbb {E}^{\mathrm {pres}}$, and the monomorphisms to be the pairs of arrows in $\mathbb {E}_{\mathbb {RL}}$ and $(\varSigma _{\mathbb {RL}},E_{\mathbb {RL}})/\mathbb {M}^{\mathrm {pres}}$.

3 Soft Constraints for Service-Oriented Computing

As an application of our approach, we study how soft-constraint institutions can be used for formalising structures and processes specific to service-oriented computing: we describe service applications and modules by means of constraint specifications, and define the requirements of applications and the properties guaranteed by service modules as constraint sentences. Consequently, we obtain a series of new results on the way in which service applications evolve through the processes of service discovery, selection, and binding.

We fix an arbitrary $\mathbb {RL}$-institution $(\mathrm {\mathbb {S}ig}^{\mathcal {I}}, \mathrm {Sen}^{\mathcal {I}}, \mathrm {Mod}^{\mathcal {I}}, \mathcal {RL}^{\mathcal {I}}, \models ^{\mathcal {I}})$ – see Definition 3 – for which the category of signatures has pushouts, is equipped with a factorisation system, and for which the functor $\mathcal {RL}^{\mathcal {I}}$ preserves pullbacks. In particular, for a soft constraint institution $\mathrm {CSP}(\mathcal {I})$, it suffices that $\mathrm {\mathbb {S}ig}^{\mathcal {I}}$ has pushouts and admits a factorisation system (see Proposition 7). We use $\overline{n}$ to denote the set $\{1,\cdots ,n\}$.

In our framework of service-oriented computing, for simplicity, we consider that we have two kinds of units, service applications and service modules. Service applications can be seen as units that require some services. We may consider that they have an orchestration part, describing what the unit intends to do, and some interfaces describing the services required. In particular, interfaces are subspecifications of the given orchestration together with some property that describes the preferences of the unit to use a given service.

Definition 8

(Service Application). A service application $(\varSigma ,I,R)$ consists of a signature $\varSigma \in |{\mathrm {\mathbb {S}ig}}|$, called orchestration, together with a finite family $I = \{i_x\}_{x \in \overline{n}}$ of interfaces, that is, a family of monic signature morphisms $i_x :\varSigma _x \rightarrow \varSigma$ such that $\mathcal {RL}(\varSigma _x) = \mathcal {RL}(\varSigma )$, and their associated requirements $R = \{r_x \in \mathrm {Sen}(\varSigma _x)\}_{x \in \overline{n}}$. We will refer to a pair $(\varSigma _x, r_x)$ consisting of the domain of an interface and its corresponding requirement as a requires-specification.

Example 9

As part of our running example, we consider a service application $\mathcal {C} = (\varSigma , I, R)$ whose orchestration $\varSigma$ is Customer (as in Fig. 2), and whose single interface consists of the identity and the requirement

$$\begin{aligned} R&= \mathsf{{languagePref}}(\mathsf{{language}}(\mathsf{{book}})) \ \wedge \\&\qquad \qquad \qquad \quad \mathsf{{deliveryPref}}(\mathsf{{delivery}}, \mathsf{{book}}, \mathsf{{deliveryTime}}(\mathsf{{delivery}}, \mathsf{{book}})). \end{aligned}$$

Service modules are like service applications but, in addition, they provide functionalities or resources. In this sense, they have an orchestration part and some interfaces for the services required, as well as a provides interface.

Definition 10

(Service Module). A service module $(\varOmega ,P,J,Q)$ consists of an orchestration $\varOmega \in |{\mathrm {\mathbb {S}ig}}|$, a provides-property $P \in \mathrm {Sen}(\varOmega )$, a finite family $J = \{j_y\}_{y \in \overline{m}}$ of interfaces $j_y :\varOmega _y \rightarrow \varOmega$, and a family of associated requirements $Q = \{q_y \in \mathrm {Sen}(\varOmega _y)\}_{y \in \overline{m}}$.

Example 11

We define a service module $\mathcal {S} = (\varOmega , P, J, Q)$ for the application $\mathcal {C}$ given in Example 9 by taking $\varOmega$ as the specification Supplier in Fig. 3, the provides-property $P = \mathsf{{available}}(\mathsf{{book}}, \mathsf{{delivery}})$, and the requirement $Q = \mathsf{{deliverable}}(\mathsf{{book}}, \mathsf{{delivery}}, \mathsf{{days}})$ defined over $\varOmega$ (i.e. $J$ consists of an identity). The module guarantees the delivery of a book $b$ for a method $d$ within $\mathsf{{deliveryTime}}(b, d)$ days, but in turn it depends on another external delivery-service provider.

Fig. 3.

The specification $\textsc {Supplier}$ (The table is only a convenient abbreviation for a set of sentences that specify, for example, that the book “Schiele” is available in German with 3-day express delivery. The column “id” is just an annotation that we use to reference the rows.)

Definition 12

( $\alpha$ -Satisfiability of an Application). A service application $(\varSigma ,I,R)$ is $\alpha$ -satisfiable if all of its requirements can be satisfied at once with a value greater than $\alpha$, i.e. there exists a model of its orchestration that satisfies $R$ with at least the value $\alpha$: $\bigvee _{M \in |{\mathrm {Mod}(\varSigma )}|}\bigl (\bigwedge _{x \in \overline{n}} M \models i_x(r_x)\bigr ) \ge \alpha .$

Definition 13

( $\beta$ -Correctness of a Service Module). A service module $\mathcal {M} = (\varOmega ,P,J,Q)$ is said to be $\beta$ -correct if $P$ is a consequence of $Q$ with a value $\beta _{\mathcal {M}}$ greater than $\beta$. Formally, this means that $\beta _{\mathcal {M}} = \bigl (\{j_y(q_y)\}_{y \in \overline{m}} \models _{\varOmega } P\bigr ) \ge \beta$.

We now focus on the execution of service applications in the context of a fixed set $Rep$ of service modules – a service repository. Each execution step is triggered by the need to fulfil a requirement of the current application, which in the context of our work corresponds to a requires-specification. Similarly to conventional soft-constraint satisfaction problems, the goal is to maximize the satisfaction of the requirement. To this end, we distinguish three elementary processes: discovery, selection and binding.

Service Discovery. Let $\mathcal {A} = (\varSigma ,I,R)$ be a service application and $(\varSigma _k, r_k)$ one of its requires-specifications. Unlike the selection and binding processes, we model the discovery of new service modules to be bound to $\mathcal {A}$ in a minimal way: all we assume is that it provides a set of possible matches – pairs $(\mathcal {M}, \phi )$ of service modules $\mathcal {M} = (\varOmega ,P,J,Q)$ from $Rep$ and attachment morphisms $\phi :\varSigma _{k} \rightarrow \varOmega$. Note that the output of the discovery process only depends on the repository and the selected requires-specification, and not on the application itself.

Service Selection. In order to select from the set of discovered service modules the best module that satisfies the requirement, we compute for each match $(\mathcal {M}, \phi )$ provided by the discovery process the compatibility score between the provides-property $P$ guaranteed by the correctness of the service module $\mathcal {M}$ and of the requirement $r_k$ of the application. To this end, we first compute the pushout $(i, j)$ of the signature morphisms $i_k$ and $\phi$ linking the requires-specification $(\varSigma _k, r_k)$ to the orchestrations of the application and of the service module (see the diagram below), and then translate both the requirement and the provides-property to the vertex $\varSigma '$ of the pushout:

$$ \bigl (j(P) \models \mathrm {Sen}(i_k \mathbin {;}i)(r_k)\bigr ) = \bigwedge _{M \in |{\mathrm {Mod}(\varSigma ')}|} \bigl (M \models _{\varSigma '} j(P)\bigr ) \rightarrow \bigl (M \models _{\varSigma '} \mathrm {Sen}(i_k \mathbin {;}i)(r_k) \bigr ). $$

These values belong to different lattices (of different service providers), hence we have to further translate them to the lattice of the service application via the morphisms $\mathcal {RL}(\phi \mathbin {;}j)$ in order to be able to compare them. Here it is useful to note that $\mathcal {RL}(\phi \mathbin {;}j) = \mathcal {RL}(\phi )$ because $\mathcal {RL}(j)$ is an identity.

However, computing such compatibility scores is not enough: the selection of a best module for the distinguished requirement of the application must also take into account the correctness of the modules. Thus, for every match $(\mathcal {M}, \phi )$, we have to multiply the score $\mathcal {RL}(\phi )(j(P) \models \mathrm {Sen}(i_k \mathbin {;}i)(r_k))$ obtained as above with $\beta _{\mathcal {M}}$, the correctness of $\mathcal {M}$. Finally, we will select those service modules for which this product is maximal.

$$ sel ( Rep ,\mathcal {A},\varSigma _k,r_k) = {\mathop {\arg \,\max }\limits _{(\mathcal {M}, \phi ) }} \{\beta _{\mathcal {M}} *\mathcal {RL}(\phi )\bigl (j(P) \models \mathrm {Sen}(i_k \mathbin {;}i)(r_k)\bigr )\} $$

Example 14

Consider the repository $Rep = \{\mathcal {S,S'}\}$ where the new service module $\mathcal {S}' = (\varOmega ', P', J', Q')$ is such that $\varOmega '$ is as in Fig. 4, $P' = P$, and $Q' = Q$. When selecting a best supplier for the service application $\mathcal {C}$ from Example 9, the books that best fit the preferences are the online version of “Schiele” ($1.3$) for $\mathcal {S}$ and “Chagall – Ma vie” with an express delivery ($2.2$) for $\mathcal {S}'$. In principle, we would need to compute the compatibility scores between Customer and Supplier and OtherSupplier, respectively, using all possible models. However, due to the way the specifications are written, the choice of the best book for each supplier can be calculated directly from the axioms. First, the constraint variables book and delivery are limited to the interpretations defined by the tables. Second, the axioms of Customer that express specific preferences, such as for a language, make it feasible to determine the best books provided by each supplier for any model. With respect to language, Book $3$ is the least preferred, while 2.1 and 2.2 are the most preferred because languagePref(en) $\le$ languagePref(de) $\le$ languagePref(fr). In order to determine the best buying option, it suffices now to decide which variant of $2.1$ and $2.2$ is the most suitable for our constraints, which we do by comparing their delivery options: since express delivery is preferred to standard when the latter does not guarantee a delivery within seven days, the best choice is $2.2$, and thus the selection process chooses $\mathcal {S}'$ as the best supplier.

Fig. 4.

The specification $\textsc {OtherSupplier}$

Service Binding. After selecting a service module (non-deterministically from the set $sel ( Rep ,\mathcal {A},\varSigma _k,r_k)$), the application will commit to the chosen provider through a binding process which changes the application as follows:

• The new orchestration is the vertex $\varSigma '$ of the pushout $(i, j)$.

• Apart from the interface $i_k$ corresponding to the distinguished requirement, the interfaces of the application are preserved via a factorisation of the composition of the old interfaces and the morphism of orchestrations $i$: for $x \in \overline{n} \setminus \{k\}$, we obtain the interface $m^{\varSigma }_x :\varSigma '_x \rightarrow \varSigma '$ by taking the factorisation $e^{\varSigma }_x \mathbin {;}m^{\varSigma }_x$ of the composed morphism $i_x \mathbin {;}i$.

• The interface $i_k$ is replaced by the interfaces of the selected service module: for $y \in \overline{m}$, $m^{\varOmega }_y :\varOmega '_y \rightarrow \varSigma '$ is the monic in the factorisation of $j_y \mathbin {;}j$.

• The distinguished requirement $r_k$ is replaced by the requirements $\{e^{\varOmega }_{y}(q_y)\}_{y \in \overline{m} }$ of the selected module, while the other requirements of the application are kept: for $x \in \overline{n} \setminus \{k\}$, $r_x$ is translated to $e^{\varSigma }_x(r_x)$.

The final goal of binding a service application to different service modules is to obtain an application with all the requirements fulfilled. It is thus natural to be interested in determining a lower bound for the satisfiability of a service application based on the satisfiability of the application that results from the process of binding to a service module with a certain degree of correctness.

Proposition 15

(Correctness of Service Binding). Let $\mathcal {M} = (\varOmega ,P,J,Q)$ be a $\beta$-correct module that matches a service application $\mathcal {A} = (\varSigma , I, R)$ through a morphism $\phi :\varSigma _k \rightarrow \varOmega$. If the selection process guarantees that the compatibility score of the requirement $r_k$ of $\mathcal {A}$ and the provides-property $P$ of $\mathcal {M}$ is at least $\delta$, and if the resulting application $\mathcal {A}' = (\varSigma ', I', R')$ of their binding is $\alpha$-satisfiable, then $\mathcal {A}$ is $\zeta$-satisfiable with $\zeta = \mathcal {RL}(\phi )(\beta *\delta *\alpha )$.

4 History and Value Systems

In this section, we analyse two distinguishing features of our method of selecting a best service module: unlike previous boolean approaches [13, 14], it relies on arbitrary residuated lattices that may change through binding; moreover, it takes into account not only the properties of the supplier, but also the information encoded in the orchestration of the application. Each of these features raises new challenges in predicting which service modules will be bound to the application.

4.1 History Matters

The choice of a best supplier is usually not invariant to the change of the orchestration of an application. In this section, we identify those situations in which the information contained by the orchestration of a service application becomes irrelevant to the selection of a best service module.

Example 16

Consider the service application $\mathcal {C}' = (\varSigma ', I', R)$ with the orchestration $\varSigma '$ defined as the specification Customer of the application $\mathcal {C}$ from Example 9 to which we add the sentence

$$ \forall \, b :\mathsf{{Book}}, d :\mathsf{{Delivery}}, n :\mathsf{{Nat}}.\ \mathsf{{deliveryPref}}(d, b, n) = 0\,\mathsf{{if}}\,n > 7, $$

and having the same requirement $R$ as $\mathcal {C}$. If we repeat the selection process for $\mathcal {C}'$ and the repository $Rep = \{\mathcal {S},\mathcal {S}'\}$, the supplier $\mathcal {S}$ will be chosen instead of $\mathcal {S}'$. This is due to the fact that the delivery time for Book $2$ is greater than seven days, and thus it does not meet the time-limit imposed by the new application.

Proposition 17

Let $\mathcal {A} = (\varSigma , I, R)$ be a service application and $(\varSigma _k, r_k)$ a requires-specification written over an $\mathbb {RL}$-institution having the model-amalgamation property. If the interface $i_k :\varSigma _k \rightarrow \varSigma \in I$ is a signature morphism that admits model expansions, the compatibility score between the requirement $r_k$ of $\mathcal {A}$ and the provides-property of a service module $\mathcal {M} = (\varOmega , P, J, Q)$ can be evaluated directly with respect to the orchestration $\varOmega$ of $\mathcal {M}$, rather than having to first compute the pushout of the application and the module.

Fact 18

For a $\mathrm {CSP}(\mathcal {I})$ institution having the model-amalgamation property, a constraint signature morphism $\varphi :(\varDelta , \mathcal {L}) \rightarrow (\varDelta ', \mathcal {L}')$ in $\mathrm {\mathbb {S}ig}^{\mathrm {CSP}(\mathcal {I})}$, with underlying morphisms $\varphi _{ pr } :(\varSigma , E) \rightarrow (\varSigma ',E')$ and $\varphi _{ rl } :\mathcal {L}' \rightarrow \mathcal {L}$, admits model expansions whenever the morphism of presentations $\varphi _{pr}$ admits model expansions and the reduct $M \mathord {\upharpoonright }_{\varDelta }$ of any $(\varSigma , E)$-model $M$ is projective with respect to $\varphi _{ rl }$.

4.2 Changing the Truth Space

The choice of a residuated lattice affects both the compatibility score (between a requirement and a provides-property) and the correctness of a service module.

Example 19

Consider once again the service application $\mathcal {C}$ from Example 9 and two suppliers $\mathcal {S}_1$ and $\mathcal {S}_2$ whose orchestrations have the same underlying signature – $\textsc {SimpleSupplier}$ as in Fig. 5. Moreover, they have the same provides-property

$$\begin{aligned} P_1&= \mathsf{{available}}(\mathsf{{book}}, \mathsf{{delivery}}) \wedge (\mathsf{{available}}(\mathsf{{book}}, \mathsf{{delivery}}) \rightarrow \\&\qquad \qquad \qquad \quad \mathsf{{deliverable}}(\mathsf{{book}}, \mathsf{{delivery}}, \mathsf{{deliveryTime}}(\mathsf{{book}}, \mathsf{{delivery}}))) \end{aligned}$$

and no requirements. The residuated lattices of the orchestrations of $\mathcal {S}_1$ and $\mathcal {S}_2$ differ: both $\mathcal {S}_1$ and $\mathcal {C}$ are based on the same Heyting algebra $\mathcal {L}$ with the underlying set of truth values $[0,1]$, while $\mathcal {S}_2$ is based on the real-valued Łukasiewicz lattice $\L = ([0,1], \mathrm {min}, \mathrm {max}, *, \rightarrow , 0, 1)$, with $x *y = \mathrm {max}\{0,x+y-1\}$ and $x \rightarrow y = \mathrm {min}\{1,1 - x + y\}$, for any $x, y \in [0,1]$. The compatibility scores between the requirement $R = \mathsf{{deliveryTime}}(\mathsf{{book}}, \mathsf{{delivery}}, \mathsf{{deliveryTime}}(\mathsf{{book}}, \mathsf{{delivery}}))$ of the service application $\mathcal {C}$ and the provides-property $P_1$ of $\mathcal {S}_1$ and $\mathcal {S}_2$ will be $1$ and $0.5$, respectively. Consequently, for any match $\phi$ between $\mathcal {C}$ and $\mathcal {S}_2$ such that the morphism of residuated lattices $\mathcal {RL}(\phi ) :\L \rightarrow \mathcal {L}$ does not map $0.5$ to $1$, the selection process will only determine $\mathcal {S}_1$ as a best service module. Notice that, even when $\mathcal {S}_1$ and $\mathcal {S}_2$ have the same underlying residuated lattices, the selection process may still depend on the matches between $\mathcal {C}$ and the two modules.

Fig. 5.

The specification $\textsc {SimpleSupplier}$

Similarly, the correctness of a service module depends on its associated lattice.

Example 20

Let $\mathcal {S}_3$ be a service module based on the extension of SimpleSupplier with the sentence

$$\begin{aligned} \forall \, b :\mathsf{{Book}} , d :\mathsf{{Delivery}}.\ (\mathsf{{deliverable}}( b, d, \mathsf{{deliveryTime}}( b, d)) \rightarrow \mathsf{{available}}(b, d)) = 1. \end{aligned}$$

Its provides-property is $P = \mathsf{{available}}(\mathsf{{book}}, \mathsf{{delivery}})$, and it has only one requirement, deliverable(book, delivery, deliveryTime(book, delivery)). The correctness of the module $\mathcal {S}_3$ will depend on the residuated lattice of its orchestration: for any Heyting algebra, the module will be correct with the value $1$, while for the real-valued Łukasiewicz lattice, the module will only be $0.5$-correct. Of course, these values cannot be compared, as they belong to different lattices. Still, the first one is absolute, while the second is not.

5 Conclusions and Future Work

We have developed a general technique for extending arbitrary institutions with soft constraints that formalises and generalises the results presented in [15]. Our approach consists in adding constraints to specifications written over a base stratified institution that provides functional requirements. The proposed technique requires that the underlying stratified institution $\mathcal {I}$ is expressive enough to capture residuated lattices, which provide the space of degrees of satisfaction in which constraints are expressed, and that every signature of $\mathcal {I}$ provides constraint variables, constraint sentences, and mappings through which each valuation of the constraint variables determines an interpretation of the constraints as elements of the residuated lattice. Building on this formalisation, we have shown how the selection of a best supplier in the context of service discovery and binding can be defined in terms of graded semantic consequence, and we have studied the unpredictability of the evolution of service applications that originates from the change of the truth structures that underlie the service components.

In order to facilitate an implementation of our model-theoretical approach to choosing a best supplier, we intend to further examine sound and complete proof systems defined in terms of many-valued rules as in [10]. These could be used in the development of operational semantics for the execution of such service-oriented applications (i.e. of a model for dynamic reconfiguration of systems in the style of [14]) with evolving preferences and truth spaces. Towards that end, the logic-programming semantics of services recently proposed in [26] provides a starting point. Besides the obvious need to adapt the theory presented therein to our many-valued setting (which means replacing linear temporal sentences with soft constraint specifications), the main open question is how to generalise the orchestrations of client applications and service modules in order to capture the way in which the satisfaction of constraint sentences changes upon iterations of the processes of service discovery, selection and binding.

We also consider worthwhile investigating how a graded variant of institution-independent logic programming, which generalises service-oriented logic programming, can be defined in relation to the developments presented in [25]. This would necessitate adapting the institution-independent abstractions of the concepts of Herbrand model, unification, resolution and computed answer (with a given degree of confidence) to the many-valued nature of our setting.