Philippe Coló
email: philippe.colo@ensae-paristech.fr

Hélène Le Cadre
email: helene.lecadre@mines-paristech.fr

Computing an Aggregator's Long Term Profit under Uncertain Behavior of the Agents

Keywords: Sequential Games, Core, Hierarchical Learning

In the retail electricity market, consumers can subscribe a contract with a conventional retailer or cooperate through an aggregator who takes forward positions in the wholesale electricity market, modeled as a twotiered system. We characterize analytically the core of the game and give conditions for its non emptiness. Then we propose a Machine Learning algorithm to forecast the consumers' demand and use these forecasts as inputs to optimize the aggregator's pricing strategy. The viability of the aggregator's pricing strategy is finally evaluated on a case study containing the power consumptions of 370 Portuguese consumers over four years.

Introduction

Up to now, conventional consumers have a contractual relation with a retail electricity provider that supplies them electricity at a price defined through contract mechanisms (such as flat rate, HP/HC, Blue/White/Red, Time of Use, etc.). The arrival of aggregators could encourage consumers to become smarter. In France, various business models for the aggregator coexist: for example, the electricity provision from Enercoop relies exclusively on a cooperative network of local renewable producers; Grid Pocket uses behavioral economics and the analysis of the consumers' data patterns to optimize his clients' daily power consumption so as to reduce their energy bill; Energy Pool also aims at reducing his clients' energy bill but through the intelligent scheduling of the daily loads.

In this paper, smart consumers are members of a smart load balancing group that is managed by an aggregator. The group size might evolve dynamically and will be denoted G(t) at period t. The aggregator buys electricity in the dayahead (wholesale) electricity market. From the market operator point of view, the aggregator is a single buyer of electricity. In our model, the aggregator takes forward positions in the day-ahead market which coincide with the aggregation of his clients' forward positions. If real-time consumption differs from day-ahead estimation, the aggregator, and through him the smart coalition of consumers, is charged for this difference at a higher unit price. However, the aggregator might compensate overestimation errors of his clients by underestimation and vice versa. He might make profit through two different ways: firstly, by his classical activity of selling energy which gives rise to an activity profit. Secondly, by following the covering mechanism described above, leading to a covering profit. The sum of both gives the aggregator's total profit.

We define a coalition of consumers as a set of end users who agree on a joint demand profile to be contracted in the wholesale electricity market with the mediation of an aggregator. We let N be the set containing all the consumers (both the aggregator's and the conventional retailer's clients), of cardinality N ∈ N * .

Over each day, each consumer has exactly one base load, that cannot be shifted, and several shiftable loads. The scheduling of the shiftable loads, which is out of the scope of this paper, might be based on decentralized control [START_REF] Meyn | Ancillary Services to the Grid using Intelligent Deferrable Loads[END_REF], priority mechanisms or economic incentives such as rebates. Under this latter mechanism, consumers can be refunded provided they agree to defer their loads in case of peak demands to fill valleys where power consumption is lower.

In this paper, we assume that only the base load may differ from the estimated one since all the shiftable loads are assumed to be scheduled automatically [START_REF] Vasirani | Smart Consumer Load Balancing: State of the Art an an Empirical Evaluation in the Spanish Electricity Market[END_REF] and focus exclusively on the base load management over a long term period such as months.

We start by describing the interactions between the aggregator and the electricity market, utility functions and judgment accuracy issues in Section 2. In Section 3, we give our main analytical results. Finally, in Section 4, the viability of the aggregator's pricing strategy is evaluated in a case study.

Utility functions and uncertainty representation

We let p f (t) be the day-ahead wholesale market price and p 0 (t) be the real-time wholesale market price at period t. In the balancing, we introduce p + (t), the unit penalty when excess power must be sold by the aggregator and p -(t), the unit penalty when more power must be purchased by the aggregator. Following the French Transmission System Operator's balancing rules 1 , we have the relations: p 0 (t) < p -(t) and p + (t) < p 0 (t) at any period t. Smart consumer i is penalized on the basis of the difference between his estimated demand (in the day ahead) di (t) and the realization of his demand (in real time) d i (t) depending on whether he has chosen a long or short position. We now describe more precisely the penalty mechanism. In case of a long position, the forecast of consumer i is higher than the realization of his demand. The aggregator must sell the total excess power bought in the day-ahead market, in the balancing market, at price position, the forecast of consumer i is smaller than the realization of his demand.

The aggregator buys the total missing power on the balancing. Consumer i is penalized on the basis of p -(t) per missing power unit leading to: p -(t) di (t) -

d i (t) - .
The aggregator simply transfers the cost of buying the missing power to her clients having short positions. We assume that there is a noise deforming the welfare provided by a power unit. We let µ * i (t) ∼ f (θ * i ) be the noise affecting consumer i's evaluation of the provider *'s offer where θ i is a parameter characterizing this density function (its mean for example). We assume that at any period t, µ agg i (t) and µ ret i (t) are independent. Furthermore, noises are assumed to be independent and identically distributed (iid) between two distinct consumers and and there is no time dependence between two consecutive noises. This modeling allows us to quantify the intrinsic preferences of the agents when comparing the welfare brought by each provider.

In the following, we let: y agg (i, t) = ωµ agg i (t)-p agg (t) be the surplus created by the aggregator at period t by providing any consumer i with one power unit, where p agg (t) is the unit price charged by the aggregator and ω > 0 is the welfare created by that power unit. Symmetrically for the retailer: y ret (i, t) = ωµ ret i (t)-p ret (t) denotes the surplus created by the retailer, where p agg (t) is the unit price charged by the aggregator. We define the utility function for consumer i depending on which provider * he subscribes, as follows: . We let ∆µ i = µ ret i (t) -µ agg i (t) be the difference between the noises introduced by consumer i regarding his evaluation of the retailer and the aggregator's offers and F ∆µi be the associated cumulative distribution function.

U * i (t) = y * (i,

A sequential game

Π C (t) is the aggregator's covering profit resulting from the covering of opposite positions among his clients and Π A (t) is the aggregator's activity profit: Π A (t) = i∈G(t) d i (t)p agg (t). The aggregator's objective is to maximize the expectation of his total profit over T periods: max E T t=1 Π A (t) + Π C (t) such that 0 ≤ p agg (t) ≤ p, ∀t = 1, ..., T where p > 0 is a price cap fixed on the providers' retail price.

Similarly the conventional retailer's objective is: max

E T t=1 i∈N -G(t) p ret (t)d i (t) such that 0 ≤ p ret (t) ≤ p, ∀t = 1, ..., T.
The solving of these sequential optimization problems gives rise to sequences of prices p * (t) t=1,...,T

. We now describe the game that takes place at each period:

1) Each consumer enters the decision process or remains inert according to a parameter β. When consumers are used to a certain provider for one of their needs, they will not always consider alternative options. This tendency takes into account the general preferences of economic agents to choose the status quo: putting oneself together in order to make a decision has a cost in itself.

2) The consumers who have entered the decision process, choose one provider depending on the providers' prices and of the intrinsic preferences of the consumers.

To solve the two steps game for the base loads, we will proceed backwards. One major concern regarding Step 2) is whether the optimal price fixed by the aggregator guarantees the stability of his coalition. In the following, we will characterize analytically how the aggregator should share his cost among his clients to stabilize his coalition.

Definition of the cost of the coalition: We let i (t) = di (t) -d i (t) be the error between the forecasted demand and the real demand of consumer i. To enable analytical tractability, we assume that: i (t) ∼ N (0; σ 2 i ) is error distributed according to a Gaussian density function centered in zero and of standard deviation σ i > 0. The i (t) are iid, there is no time dependence between two consecutive errors and µ * i (t) is independent of any i (t). In turn i∈G(t) i (t) is distributed according to a Gaussian density function centered in zero and of variance i∈G(t) σ 2 i > 0. According to the stylized market design introduced in [START_REF] Cadre | Wind Farm Portfolio Optimization under Network Capacity Constraints[END_REF], the cost of coalition G(t) for the aggregator at time period t is:

c G(t) = p f (t) i∈G(t) di (t) + p -(t) i∈G(t) i (t) - -p + (t) i∈G(t) i (t) + (1)
The cooperative game that we consider is with Transferable Utility (TU) because the coalitional value/cost, c G(t) , defined in Equation ( 1) can be divided amongst the aggregator's clients in any way that the aggregator's clients choose. We introduce the notion of core which characterizes the stability of the coalition made of the aggregator's clients. For TU game, the core is defined as the set of imputations z agg (i, t)

i∈G(t)
such that no consumer has an incentive to switch from the aggregator to the conventional retailer. In other words, the core is a set of joint strategies with which all consumers want to cooperate in a smart consumer group and any deviating coalition (i.e., consumers switching to the conventional retailer) cannot guarantee higher utilities to all of its members. With this respect, the core strategies are stable.

We assume that for any consumer i, the opposite of his expected utility is associated to a unique imputation: z * (i, t) = -E U * i (t) . Using U * i (t) definition, consumer i's imputation is completely determined by the provider's price, estimated demand and game parameters: z * (i, t) = -ωθ * i di (t) + p agg (t) di (t).

Definition of the core: The imputation z agg (i, t)

i∈G(t)
is in the core if, and only if:

j∈G(t) z agg (j, t) = E c G(t) GR z agg (i, t) ≤ z ret (i, t), ∀i ∈ G(t) IR
GR stands for Group Rationality and IR, for Individual Rationality. Our game follows a γ-model [START_REF] Mochaourab | Coalitional Games in MISO Interference Channels: Epsilon-Core and Coalition Structure Stable Set[END_REF]: all consumers outside a coalition subscribe to the conventional retailer's offer and build single player coalitions without direct participation to the market. The game is with characteristic function V (., t) defined as follows:

V (G, t) E c G(t) if Card G(t) ≥ 2 and V (i, t)
E c ret (i, t) , ∀i ∈ N where the cost charged by the conventional retailer is

c ret (i, t) = p ret (t)d i (t).
Non emptiness of the core: Characterizing the aggregator's coalition stability is equivalent to prove that the core of the associated TU game is non empty. To check that the core is non empty, we rely on the Bondareva-Shapley Theorem i.e., we need to prove that the TU game is balanced.

Proposition 1. The core is non empty if, and only if: min i∈N di (t)

≥ 1 N p f (t) p ret (t) j∈N dj (t) + 1 N p -(t)-p + (t) p ret (t) j∈N σ 2 j .
Proof of Proposition 1. We recall that the TU game is balanced if, and only if:

i λ ret (i)E[c ret (i, t)] + λ agg E[c G(t) ] ≥ E[c G(t) ] (2)
for all the collections of weights λ ret (i)

i , λ agg such that λ ret (i) ∈ [0; 1], ∀i, λ agg ∈ [0; 1] and λ ret (i) + λ agg = 1, ∀i. This implies that λ agg = 1 -λ ret (i), ∀i; a fortiori: λ agg = 1-1 N i λ ret (i).
By substitution in Inequality (2), we infer that it is equivalent to:

i λ ret (i) E[c ret (i, t)] -1 N E[c G(t)
] ≥ 0 for all the collections of weights λ ret (i) i , λ agg defined above. According to the Bondareva-Shapley Theorem, the core of our TU game is non empty if, and only if,

E[c ret (i, t)]-1 N E[c G(t) ] ≥ 0, ∀i.
Therefore, we need to check whether this relation holds. Analytically, we have:

E[c ret (i, t)]-1 N E[c G(t) ] = E p ret (t)d i (t) - 1 N E p f (t) j dj (t) + p -(t) j ( dj (t) -d j (t)) - -p + (t) j ( dj (t) -d j (t)) + .
The first term of the equation can be rewritten as: p ret (t) di (t). Furthermore we recall that any real x can be decomposed as a linear combination of its positive and negative parts: x = x + -x -. This implies that:

E[c ret (i, t)] - 1 N E[c G(t) ] = p ret (t) - 1 N p f (t) di (t) - 1 N p f (t) j =i dj (t) - 1 N p -(t) E j ( dj (t) -d j (t)) =0 + 1 N p + (t) -p -(t) <0 E j ( dj (t) -d j (t)) + (3)
Equation ( 3) can be rewritten as follows:

E[c ret (i, t)] -1 N E[c G(t) ] ≥ 0, ∀i ∈ N ⇔ p ret (t) di (t) -1 N p f (t) j∈N dj (t) + 1 N (p + (t) -p -(t)) j∈N σ 2 j ≥ 0, ∀i ∈ N . This is equivalent to: min i∈N di (t) ≥ 1 N p f (t) p ret (t) j∈N dj (t) + 1 N p -(t) -p + (t) p ret (t) j∈N σ 2 j
Fairness: The Shapley value attributes to each consumer in the coalition an imputation which is a function of its marginal contribution to the coalition. To check the axiom of Pareto optimality, the Shapley value is averaged over all the interactions that each consumer can have with other consumers in the coalition. Formally, the Shapley value associated with consumer i ∈ G(t) is:

ϕ i (V, t) = G⊆G(t),i∈G (Card(G(t))-Card(G))!(Card(G)-1)! Card(G(t))! V (G) -V (G -{i}) .
In the framework of our γ-model, it can easily be computed analytically:

ϕ i (V, t) = 1 Card(G(t)) p f (t) di (t) + 1 √ 2π p -(t) -p + (t) j∈G(t) σ 2 j - j∈G(t) σ 2 j + 1
Card(G(t)) p ret (t) di (t). It is straightforward to show that our TU game is not convex 3 . As such we have no guarantee that the Shapley value belongs to the core. But we now give conditions for the Shapley value to be in the core. GR being checked immediately by definition of the Shapley value, we now focus on IR i.e., ϕ i (V, t) ≤ z ret (i, t), ∀i ∈ G(t) which give the following condition on the consumers' data and game parameters.

Proposition 2. The Shapley value of the TU game belongs to the core if, and only if:

di (t) j∈G(t) σ 2 j - j∈G(t)-{i} σ 2 j ≤ 1 √ 2π p -(t) -p + (t) p f (t) + 1 -Card(G(t)) p ret (t)
, ∀i ∈ G(t)

Inertia and its consequences: In Step 1), inertia is captured by a parameter β ∈ [0; 1] which denotes, at every period, the probability for the consumer to get himself into the situation of making a decision on his energy supplier. We will assume β = 0 and β = 1, meaning we are neither in a situation of monopoly, nor in a situation of competition à la Bertrand. This first step will have a consequence on the aggregator's pricing policy.

The introduction of inertia changes the demand dynamics i.e., we have:

i∈G(t) d i (t) = (1 -β) i∈G(t-1) d i (t) + β i∈N d i (t)s(i, t)
where s(i, t) ∈ [0; 1] is the probability that at the beginning of period t consumer i enters a decision process on the choice of his energy retailer and chooses the aggregator. s(i, t) can be computed analytically:

s(i, t) = P z ret (i, t) > z agg (i, t) = F ∆µi p ret (t)-p agg (t) ω .

Simulations

Solving this sequential optimization game described in Section 3 requires to forecast the demand of each individual consumer over horizon T . To that purpose we use a hierarchical learning algorithm: At the lower level, we run in parallel three experts Support Vector Regression (SVR), Neural Network (NN) and Conditional External Regret. While SVR and NN produce point forecast, Regret produces a probabilistic forecast of the consumers' demand. We therefore sample a forecast according to the estimated density function. We observe that the NN achieves excellent performance. This can be explained by the high dependence of the data on features such as hour, day, month, season, etc. We observe that to achieve pretty good performance the Regret [START_REF] Cesa-Bianchi | Prediction, Learning, And Games[END_REF] has to be run on a larger training set than the two other algorithms. Based on the data characteristics, we implement (at the lower level) a Conditional External Regret algorithm. More precisely, we classify a priori the forecasted densities obtained through External Regret based on features such as the day, week and season. At the upper level, the aggregator runs an External Regret algorithm which associated a weight to the forecasts produced by each of the three experts. The combinations of these experts' forecasts gives the aggregator's forecast of each individual consumer demand. Note that the weights associated with each expert are updated following the rule described in [START_REF] Cesa-Bianchi | Prediction, Learning, And Games[END_REF]. We run our algorithm on a database containing the power consumption of 370 Portugese consumers that can be either residentials or industrials 4 . We take as parameters: ω = 1, which enables us to normalize our surplus, and consider two scenarios β = 0.3 and β = 0.9. The power consumption of each individual is monitored every 15 minutes on a 4 year basis (to be precise, from the 1-st of January 2011 to December 31, 2014). In the data base, consumers are classified in 8 categories: retail/shopping, continuous laboring, weekly laboring, hotel businesses, catering industry, schools, logistics and others.

Figure 1 :

 1 Figure 1: We plot the dynamics of the providers' profit over 24 months for β = 0.3 in (a) and β = 0.9 in (b).

http://rei.revues.org/4053 [Online September

2015]

For any real x, we set: x + max{0; x} and x -min{0; x}

We recall the convexity definition: let G and G be two coalitions such that G ⊂ G , Card(G) ≥ 2 and let i ∈ N \G , to prove that the game is convex we need to check that:V G ∪ {i}, t -V G , t < V G ∪ {i}, t -V G, t .

Trindade A., artur.trindade@elergone.pt, Elergone, NORTE-07-0202-FEDER-038564, https://archive.ics.uci.edu/ml/datasets.html[Online September 2015]

To test the hierarchical learning algorithm performance, we use it to forecast the individual consumption of one consumer over one month, having trained the each algorithm and the hierarchical learning algorithm over a whole year (the granularity of the measurements being of 15 minutes). We report the resulting Mean Square Errors (MSEs) in Table 1.

In Figure 1, we represent the dynamics of the providers' profit evaluated on our 24 month test set for two scenarios of inertia: β = 0.3 in (a) and β = 0.9 in (b). We observe that the aggregator's profit always remains positive for both values of inertia parameter.

Conclusion

We consider a two-tiered electricity market where consumers can either buy power from a conventional retailer or through an aggregator who purchases power from the electricity market and then distributes it (for a subscription price) to his clients. In this article, we propose a coalition-based game-theoretic formulation of the problem, determine the game's core, and then provide a hierarchical learning algorithm for planning the aggregator's pricing strategy.

Extensions will be made by considering more general probabilistic models of error generation and characterizing the core and Shapley value under each model.


Pierre-Cyrille Héam
email: pcheam@lsv.ens-cachan.frokouchnarenko

Olga Kouchnarenko

Jérôme Voinot
email: jvoinot@lifc.univ-fcomte.fr

Component Simulation-based Substitutivity Managing QoS and Composition Issues

Keywords: Substitutivity, Component, Simulation, weighted automata, Quality of Service 1

Several scientic bottlenecks have been identied in existing component-based approaches.

Among them, we focus on the identication of a relevant abstraction for the component expression and verication of properties like substitutivity: When is it possible to formally accept or reject the substitution of a component in a composition? This paper suggests integer weighted automata to tackle this problem when considering a new factor Quality of Service (QoS). Four notions of simulation-based substitutivity managing QoS aspects are proposed, and related complexity issues on integer weighted automata are investigated.

Furthermore, the paper denes composition operators: sequential, strict-sequential and parallel compositions, bringing path costs into the analysis. New results on the compatibility of proposed substitutivity notions w.r.t. sequential and parallel composition operators are established.

Introduction

This paper is dedicated to the verication of substitutivity of components modelled by integer weighted automata while considering a new factor Quality of Service (QoS). In this context modelling and verifying both functional and non-functional properties is possible.

For these verication problems, we provide new theoretical decidability results. Furthermore, the paper denes composition operators: sequential, strict-sequential and parallel compositions, bringing path costs into the analysis. We point out how compatible proposed substitutivity notions and sequential and parallel composition operators really are.

Component-based development provides signicant advantages portability, adaptability, re-usability, etc. when developing, e.g., Java Card smart card applications or when composing Web services within Service Component Architecture (SCA). Several scientic bottlenecks have been identied in existing component-based approaches. Among them, 1 This work is partially funded by the French ANR projects ARA COPS and ACI TACOS.

we focus on the identication of a relevant abstraction for the component expression and verication. When is it possible to accept or reject the substitution of a component in a composition? Moreover, with the increasing importance of QoS in the design of componentoriented applications, like Web services, it is of great interest for users and developers to be able to determine, possibly dynamically, that a Web service performs the same tasks as another possibly failing service, with comparable/higher quality.

Contributions

Most of prior and current works on component and service composition focus on either the functional aspect or the QoS aspect alone, it is very dicult to address both. This paper takes an approach of modelling components and services and QoS descriptions by integer weighted nite state automata, and studies the complexity of substitutivity of one such automaton by another.

More precisely, the present paper makes the following contributions: The rst contribution is formal denitions of four (partial) substitutivity and (partial) strong substitutivity problems based on a simulation of automata taking path costs into account. For these substitutivity problems new decision/complexity results for dierent classes of integer weighted automata are presented.

The second contribution is formal denitions of composition operators: sequential, strictsequential and parallel compositions, bringing path costs into the analysis. New results on the compatibility of proposed substitutivity notions with relation to sequential and parallel composition operators are established.

The third contribution concerns some practical issues on service and component substitutivity. We briey situate component substitutivity w.r.t. various compositions in the context of a new type of urban, possibly driverless, vehicles.

These examples illustrate why the topic is very important in practice, especially given the need to bring costs into consideration.

Notice that the rst contribution was presented in [START_REF] Héam | Component simulation-based substitutivity managing QoS aspects[END_REF]. The second contribution is completely new. The third contribution follows and develops the examples in [START_REF] Héam | Component simulation-based substitutivity managing QoS aspects[END_REF].

Related Work

Weighted automata, trace-equivalence, simulations. Weighted automata an extension of integer weighted automata is a formalism widely used in computer science for applications in images compression [START_REF] Culik | Generalized weighted nite automata based image compression[END_REF][START_REF] Katritzke | Enhancements of partitioning techniques for image compression using weighted nite automata[END_REF], speech-to-text processing [MPR02, [START_REF] Mohri | Weighted automata in text and speech processing[END_REF][START_REF] Buchsbaum | An approximate determinization algorithm for weighted nite-state automata[END_REF] or discrete event systems [START_REF] Gaubert | Performance Evaluation of (max,+) Automata[END_REF]. These large application areas make them intensively studied from the theoretical point of view [START_REF] Krob | The Equality Problem for Rational Series with Multiplicities in the Tropical Semiring is Undecidable[END_REF][START_REF] Weber | Finite-valued Distance Automata[END_REF][START_REF] Hashiguchi | Decidability of the Equivalence Problem for Finitely Ambiguous Finance Automata[END_REF][START_REF] Klimann | Deciding unambiguity and sequentiality from a nitely ambiguous max-plus automaton[END_REF]. See [START_REF] Berstel | Rational Series and Their Languages[END_REF] for more detail on weighted automata.

To compare processes or components, trace equivalences are in general not expressive enough and there are stronger equivalence relations permitting to consider deadlocks, livelocks, branching behaviours, causality, etc. Among them, the strong bisimulation equivalence by Milner [START_REF] Milner | A Calculus of Communicating Systems[END_REF] and Park [START_REF] Park | Concurrency and automata on innite sequences[END_REF] is widely used in computer science because of its numerous advantages: It preserves branching behaviours and, consequently, most of the dynamic properties; there is a link between the strong bisimulation and modal logics [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF];

this is a congruence for a number of composition operators, e.g. parallel composition, prexing by an action, etc. The reader is referred to the survey [vG01] on simulation-preorder relations.

Bisimulation relations over weighted automata were investigated in [START_REF] Buchholz | Weak bisimulation for (max/+) automata and related models[END_REF]. In that paper authors consider that a max/plus automaton simulates another one if it can perform at the same moment the same action with the same weight. Our main purpose is to handle QoS aspects which are global notions over components. This is why in our paper, unlike [START_REF] Buchholz | Weak bisimulation for (max/+) automata and related models[END_REF], weights are related to successful paths of automata.

In the recent survey [START_REF] Beek | Formal methods for service composition[END_REF], the authors pointed out that, let us quote, automatabased models are increasingly being used to formally describe, compose, and verify service compositions. The role of automata-based analysis is also emphasised in [BABC + 09] for distributed components (Fractal, GCM and ProActive components). The main advantage of numerous works on component/service composition based on the use of automata or Labeled Transition Systems (LTSs) (see for instance [FUMK07,[START_REF] Mateescu | Formal modeling and discrete-time analysis of BPEL Web services[END_REF]) is that their formal basis allows automatic tool support. However, extending automata (nite state automata, timed automata, I/O automata, team automata, etc.) with costs makes various verication problems undecidable in general [START_REF] Bouyer | On the optimal reachability problem of weighted timed automata[END_REF]. In this framework, the present work denes four component/service substitutivity notions based on simulation relations of integer weighted automata, and provides constructive proofs for deciding substitutivity verication problems over those automata. Moreover, the article shows that the proposed notions are compatible with sequential and parallel composition operators which are essential for building new applications.

Modelling of QoS and of non functional properties of systems. Within the SCA initiative 2 , a recent set of specications describes a language-neutral model for building applications and systems using a Service-Oriented Architecture. SCA is claimed to be extendable and user friendly with:

• multiple implementation types including Java, C++, BPEL, PHP, Spring, etc.

• multiple bindings including Webservice, JMS, EJB, JSON RPC, etc.

• multiple hosting environments such as Tomcat, Jetty, Geronimo, OSGI, etc.

The policy framework provided with SCA supports specications of constraints, capabilities and QoS expectations, from component design to concrete deployment.

Recently, minimum-cost delegation in service composition through the integration of existing services was studied in [START_REF] Gerede | Minimum-cost delegation in service composition[END_REF]. [START_REF] Brada | Specication-Based Component Substitutability and Revision Identication[END_REF]. Our work is close to that in [START_REF] Cerná | Component substitutability via equivalencies of component-interaction automata[END_REF], where the authors addressed component substitutability using equivalences between component-interaction automata, which are dened 2 The rst ocial specication of SCA providing hierarchical components is the 1.0 version, published in march 2007.

with respect to a given set of observable labels. In the present work, in addition to a set of labels, path costs are taken into account when comparing integer weighted automata.

In [START_REF] Beyer | Web service interfaces[END_REF][START_REF] Beyer | An application of web-service interfaces[END_REF], the authors dened three substitutivity notions over interface automata modelling Web services. First two notions deal with signatures and propositional constraints on the consistency between various method calls and return values. They are stateless and cannot be handled in our framework. The third substitutivity notion on protocol interfaces is based on a simulation relation over labelled transition systems like in the present paper. It is shown to be polynomial time decidable but it does not manage costs.

Dierent solutions have been proposed to allow taking QoS into account while specifying Web services and their compositions [LKD + 03, Tia05, d'A06, BRL07, HKV07]. In [START_REF] Héam | How to Handle QoS Aspects in Web Services Substitutivity Verication[END_REF] the substitutivity problem has been investigated for the trace equivalence over integer weighted automata.

In [START_REF] Lohmann | Operating guidelines for nite-state services[END_REF][START_REF] Ch | Deciding service composition and substitutability using extended operating guidelines[END_REF] the authors studied the correct interaction between services modelled by open nets (uncoloured Petri nets with interfaces). The behaviour semantics of a set of open nets is given by annotated automata. These works on the correct interaction between services have been mainly inspired by the notion of soundness for workow nets [vdA98]. Extending an annotated automaton with global constraints over its states proposed in [START_REF] Ch | Deciding service composition and substitutability using extended operating guidelines[END_REF] gives an operating guideline to characterise all correctly interacting partners of a service.

Then simulation relations are used for deciding service composition and substitutability.

In [START_REF] Lohmann | Comparing and evaluating Petri net semantics for BPEL[END_REF] the authors compared and evaluated two dierent Petri net semantics for BPEL. Both implemented semantics abstract from data (messages and the content of variables). The properties that can be veried on the resulting models are (based on) soundness [vdA98], relaxed soundness [START_REF] Dehnert | Bridging the gap between business models and workow specications[END_REF], and also temporal logic properties.

The recent work in [START_REF] Chaki | Verication of evolving software via component substitutability analysis[END_REF] is dedicated to the verication of a dynamic substitutability problem: can a component replace another component during an execution? The verication approach is based on recent model-checking techniques. Notice that action costs are not taken into account in [START_REF] Chaki | Verication of evolving software via component substitutability analysis[END_REF]. In that setting, i.e. without considering costs, their substitutivity notion is stronger than the notion dened in the present paper.

The integration of (abstractions of ) QoS properties into component models is supported several component-based approaches and tools, such as KLAPER [START_REF] Grassi | Klaper: An intermediate language for model-driven predictive analysis of performance and reliability[END_REF], Palladio [START_REF] Becker | Model-based performance prediction with the palladio component model[END_REF] and RoboCop [START_REF] Alexandre | Evaluation of static properties for component-based architectures[END_REF]. As these component models do not dene any renement notion, they are clearly distinguishable form our work. However, these models already provide very well validated abstractions on performance. Let us notice that the protocol for using a component is often context-dependent. It is due to automated component adaptation and architectural dependency analysis. Parametric contracts [START_REF] Reussner | Automatic component protocol adaptation with the coconut/j tool suite[END_REF][START_REF] Reussner | Modelling parametric contracts and the state space of composite components by graph grammars[END_REF] for software components allow addressing this aspect and were successfully used for automated protocol adaptation and quality of service prediction.

Finally, in [START_REF] Moschoyiannis | Modelling component behaviour with concurrent automata[END_REF][START_REF] Küster | Concurrent logic and automata combined: A semantics for components[END_REF] authors show how to use automata and concurrent logic to model component-based systems. In these works, nite automata are derived from UML descriptions and synchronisations are performed using interface constraints.

Layout of the paper

The remainder of the paper is organised as follows. A motivating example is given in Sect. 2. Section 3 recalls integer weighted automata and denes four simulation-oriented substitutivity notions based on them. The verication issues on components substitutivity are presented in Sect. 4 and 5. Section 6 puts the substitutivity problems in the composition context. Section 7 exposes how the theoretical results would be exploited in practice. Finally, Section 8 concludes and gives some prospectives. Context. The TACOS project3 concerns the development of a new type of urban vehicles with new functionalities and services. The project follows the Cybercar concept, a public transport system with fully or partially automated driving capabilities, aimed at replacing the private car. One of the major cornerstones is the development, the validation and the certication of vehicles, like Cristal or Cycab.

A positioning system is a critical part of a land transportation system. Many positioning systems have been proposed over the past few years. Among them, let's quote GPS, GALILEO or GLONASS positioning systems which belong to the Global Navigation Satellite Systems (GNSS, for short). However, currently only some mobile terminals (laptops, PDAs, cell phones, etc.) are embedded with GNSS receivers. In addition, positioning systems are often dedicated to a particular environment; e.g., the GNSS systems generally do not work indoors. To solve these problems, numerous alternatives relying on dierent technologies, have arisen (see [SE06, EFPC04, HNS03, RMG05, OG00] for more details on issues related to positioning systems).

The present section and Section 7 briey describe how such heterogeneous positioning systems, encapsulated as components, called localisation components, are used together to provide positioning data satisfying some non functional requirements. Note that positioning data can be given in dierent formats. The most used format is the geographic one, like that usually obtained from a GPS positioning system. But other systems give semantic location data, like 'You are near the station Place Stanislas'.

In this framework, let us consider the two following positioning components where Wireless networks are exploited to extend the use of the GNSS. Their abstract representations are given by nite automata in The abstracted value may depend on an environment where the available power or the power consumption must be taken into account/reduced. For example, once the geographic location obtained, a vehicle whose available power is not enough to reach the next station because of a critical environment, must compute semantic location data to oer to its passengers. Then C1 performs the action c to acknowledge that its positioning task is successfully executed.

• Component C2 works similarly but after having done rst b 1 , it can perform actions b 1 or b 2 as many times as it is required. For example, depending on the speed of the vehicle, the localisation system must give the position more or less frequently.

Obviously, the C1 component can be functionally substituted by C2. Furthermore, when considering, e.g., energy costs over components represented by nite automata C3 and C4 in Fig. 2, the cost of each action is put on each transition.

For both C3 and C4, receiving a positioning request a costs 1 energy unit and performing c costs 3 energy units. However, for C3 each action b 1 and b 2 costs 2 energy units. For C4, performing the b 1 action costs only 1 energy unit but all b 2 actions cost 4 energy units.

The intuition behind this modelling is as follows. C3 has a low-cache memory allowing it to locally compute actions b 1 and b 2 . C4 has a high performance low-cache memory that allows it to locally compute action b 1 with a cost of 1 energy unit. C4 also has a local hard drive that makes b 2 computations possible. However, reading and writing on hard drives has a high energy cost of 4 energy units. In this situation, we do not want to say that C4 can substitute C3 since performing ab 1 b 2 c on C3 has the cost of 8 energy units whereas the same sequence of actions costs 9 energy units on C4.

Simulation-based Component Substitutivity

Theoretical Background

In this paper, Σ denotes a nite set of actions. We rst introduce the notion of integer weighted automata. To simplify the presentation the results are given for integer weighted automata but can be easily extended to any weights in a semi-ring. Denition 1. A nite integer weighted automaton A over Σ is a quintuplet

A = (Q, Σ, E, I, F ) where Q is the nite set of states, E ⊆ Q × Σ × Z × Q is the set of transitions, I ⊆ Q is the set of initial
states, and F ⊆ Q is the set of nal states. Finite integer weighted automata are often simply called automata in the sequel. Notice that there is a restriction on E: for every action a, every pair of states p, q, there exists in E at most one transition of the form (p, a, c, q), also written p a,c -→ A q. Now we formally dene an execution of a integer weighted automaton and related notions.

A partial execution or a path of a nite integer weighted automaton A is a sequence π = (p 0 , a 0 , c 0 , q 0 ), (p 1 , a 1 , c 1 , q 1 ), . . . , (p n , a n , c n , q n ) of transitions of A such that for every 0 ≤ i < n, q i = p i+1 . If we add the conditions: p 0 is an initial state, q n is a nal state, then we call π an execution or a successful path. The trace/label tr(π) of the (partial) execution π is the word a 0 a 1 . . . a n , and the cost of the (partial) execution π is the sum of the c i 's: cost A (π) = n i=0 c i . For instance, (1, a, 0, 1), (1, a, 0, 1), (1, b, 1, 2), (2, a, 2, 1) is a successful path of A exe1 , whose trace is aaba and whose weight is 0 + 0 + 1 + 2 = 3.

A state p of a integer weighted automaton is accessible/reachable (resp. co-accessible/coreachable) if there exists a path from an initial state to p (resp. from p to a nal state). For instance, in the automaton depicted in Fig. 10, the state 2, 3 is not accessible. Basically, given A, L(A) denotes its set of execution traces.

An automaton is trim if its states are all both accessible and co-accessible. It is well known that for every automaton A, there exists a trim automaton with the same set of successful executions. Moreover, computing this trim automaton can be done in polynomial time. For instance, the trim automaton in Fig. 11 is obtained from the automaton in Fig. 10.

An automaton A is nitely ambiguous if there exists a positive integer k such that for every word w there exists at most k successful paths in A labelled by w. For example, the automaton A exe2 is nitely ambiguous whereas the automaton A exe1 is not: the word ba n b is accepted by n dierent successful paths, depending when the transition from 2 to 1 is red.

Denition 2. Let

A 1 = (Q 1 , A, E 1 , I 1 , F 1 ) and A 2 = (Q 2 , A, E 2 , I 2 , F 2 ) be two automata. A binary relation A1,A2 ⊆ Q 1 × Q 2 is a simulation if (p 1 , p 2 ) ∈ A1,A2 implies, for all a in A and all c 1 in Q, i) for every q 1 ∈ Q 1 , if (p 1 , a, c 1 , q 1 ) ∈ E 1 then there exist q 2 ∈ Q 2 and c 2 ∈ Q such that (p 2 , a, c 2 , q 2 ) ∈ E 2 and (q 1 , q 2 ) ∈ A1,A2 , and ii) if p 1 is nal, then p 2 is nal too.
If there is no ambiguity on A 1 and A 2 , we just say that p 2 -simulates p 1 , written p 1 p 2 , when there is a simulation containing (p 1 , p 2 ). It is easy to see that the largest simulation on Q 1 × Q 2 exists. To simplify the notations, the largest simulation on

Q 1 × Q 2 is also denoted by A1,A2 .
The above relation is extended to paths of A 1 and A 2 in the following way: an execution π 2 of A 2 -simulates an execution π 1 of A 1 if and only if they have the same label (and consequently the same length) and for every i, π

1 [i] π 2 [i]. Finally, we write A 1
A 2 if for every co-accessible initial state i 1 of A 1 there exists an initial state i 2 of A 2 such that i 1 i 2 . For our example in Sect. 2, it is easy to see that C3 C4.

Modelling Substitutivity

A problem occurring while managing components/services is to determine that a component/service performs the same tasks as another possibly failing service, with comparable or higher quality. More formally, for two Web services modelled by their integer weighted automata A 1 and A 2 , the problem is to decide whether A 2 can have the same behaviour as A 1 with a similar or higher quality. To address this problem, four notions of simulation-based substitutivity managing QoS aspects are proposed in this section.

The notion of substitutivity means that a service S 1 can be substituted by a service S 2 if S 2 has a way to act as S 1 and the cost of this way is comparable or better that the cost in S 1 . Intuitively, the substitutivity is an existential notion: for each sequence of actions that can be done by S 1 , there exists in S 2 an equivalent sequence of actions with a smaller cost. The notion of strong substitutivity means that a service S 1 can be substituted by a service S 2 if S 2 has a way to act as S 1 , and whatever the way chosen by S 2 to act as S 1 is, its quality is similar or higher. Intuitively, the strong substitutivity notion requires a stronger universal quantication ensuring that not only S 2 can do better that S 1 , but that it will always do better.

Substitutivity Problem

Input: Two automata A 1 and A 2 . Output: True if for every successful path π 1 of A 1 there exists a successful path π 2 of A 2 such that π 1 π 2 and cost A2 (π 2 ) ≤ cost A1 (π 1 ), false otherwise.

We write A 1 A 2 when A 1 and A 2 satisfy the substitutivity problem.

Strong Substitutivity Problem Input: Two automata A 1 and A 2 . Output: True if for every successful path π 1 of A 1 there exists a successful path π 2 of A 2 such that π 1 π 2 and for every π 2 of A 2 such that π 1 π 2 , cost A2 (π 2 ) ≤ cost A1 (π 1 ), false otherwise.

We write A 1 st A 2 when A 1 and A 2 satisfy the strong substitutivity problem.

It is sometime fruitful to compare successful executions costs only on subtraces. This leads to the following partial substitutivity problems that are similar to the ones above. For these problems, we want to compare parts of executions, not paths that cannot be related to a successful path. Consequently, automata are required to be trim, and comparisons are done for all paths, not only for successful paths.

Partial Substitutivity Problem Input: Two trim automata A 1 and A 2 . Output: True if for every path π 1 of A 1 there exists a path π 2 of A 2 such that π 1 π 2 and cost A2 (π 2 ) ≤ cost A1 (π 1 ), false otherwise.

We note A 1 p A 2 when A 1 and A 2 satisfy the partial substitutivity problem.

Partial Strong Substitutivity Problem

Input: Two trim automata A 1 and A 2 . Output: True if for every path π 1 of A 1 there exists a path π 2 of A 2 such that π 1 π 2 and for every π 2 of A 2 such that π 1 π 2 , cost A2 (π 2 ) ≤ cost A1 (π 1 ), false otherwise.

We write A 1 st p A 2 when A 1 and A 2 satisfy the partial strong substitutivity problem. Notice that in the above denitions we choose that cost(π 2 ) ≤ cost(π 1 ) modelling that the lower is the cost the better is the service, what is intuitive for connection time or nancial cost. One can give a dual denition if the lower is the cost the worse is the service by changing cost(π 2 ) ≤ cost(π 1 ) into cost(π 2 ) ≥ cost(π 1 ). All notions, algorithms, etc. described in this paper may be trivially adapted to this dual denition. In order to not overload the reader, we do not consider that case.

We end this section by recalling some results on decision procedures for nite integer weighted automata.

Theorem 3. Given two integer weighted automata A 1 and A 2 , it is

• undecidable to test whether for every u ∈ L(A 1 ), cost A1 (u) ≤ cost A2 (u) [START_REF] Krob | The Equality Problem for Rational Series with Multiplicities in the Tropical Semiring is Undecidable[END_REF]; the same problem is decidable if A 1 and A 2 are both nitely ambiguous [HIJ02, Web94],

• undecidable to test whether for every u ∈ L(A 1 ), there exists an execution

π of label u in A 1 such that cost A1 (π) ≥ 0 (resp. cost A1 (π) ≤ 0) [Kro94],
• decidable in polynomial time to test whether for every

u ∈ L(A 1 ), cost A1 (u) ≤ cost A2 (u) if A 1 and A 2 are both nitely ambiguous [HIJ02, Web94],
• decidable in polynomial time to test whether A 1 is nitely ambiguous [START_REF] Weber | On the degree of ambiguity of nite automata[END_REF].

• PSPACE-complete to decide whether

L(A 1 ) ⊆ L(A 2 ) [AHU74, BJ06].

Strong Substitutivity Problems

This section provides decidability results for the strong substitutivity and the partial strong substitutivity problems.

Lemma 4. One has A 1 A 2 if and only if for every successful path π 1 of A 1 there exists a successful path π 2 of A 2 such that π 1 π 2 .

Proof.

Assume rst that for every successful path π 1 of A 1 there exists a successful path π 2 of A 2 such that π 1 π 2 . Let i 1 be a co-accessible state of A 1 . By denition of co-accessibility, there exists a successful path π 1 in A 1 starting from i 1 . By hypothesis, there exists a successful path

π 2 of A 2 such that π 1 π 2 . Therefore, π 1 [1] π 2 [1]. But π 1 [1] = i 1 and since π 2 is a successful path, π 2 [1] is an initial state of A 2 . Consequently, A 1 A 2 . Assume now that A 1 A 2 . Let π 1 be a successful path of A 1 . Since π 1 [1] is an initial state and since A 1 A 2 , there exists an initial state q 1 in A 2 such that π 1 [1] q 1 . Therefore, if we denote by (π 1 [1], a 1 , c 1 , π 1 [2]
) the rst transition of π 1 , there exists a state q 2 in A 2 and d 1 ∈ Z, such that (q 1 , a 1 , d 1 , q 2 ) is a transition of A 2 and π 1 [2] q 2 . Iterating this construction, one can, by a direct induction, build a successful path π 2 of A 2 such that π 1 π 2 , which concludes the proof.

2

Theorem 5. The strong substitutivity problem is P-complete.

Proof.

Let

A 1 = (Q 1 , A, E 1 , I 1 , F 1 ) and A 2 = (Q 2 , A, E 2 , I 2 , F 2 ) be two automata. We denote by B the automaton (Q, A, E, I, F ) where -Q = {(q 1 , q 2 ) ∈ Q 1 × Q 2 | q 1 q 2 }, -E = {((p 1 , p 2 ), a, c, (q 1 , q 2 )) | (p 1 , a, c 1 , q 1 ) ∈ E 1 , (p 2 , a, c 2 , q 2 ) ∈ E 2 , c = c 1 -c 2 , a ∈ A}, -I = (I 1 × I 2 ) ∩ Q and F = (F 1 × F 2 ) ∩ Q.
We claim that A 1 st A 2 if and only if A 1 A 2 and for every successful path π of B, cost B (π) ≥ 0.

(⇒) Assume that A 1 st A 2 . By Lemma 4, for every successful path of A 1 there exists an

-related path in A 2 . Thus A 1 A 2 . Consider now a successful path π in B, π = (p 0 , a 1 , α 1 , p 1 ), (p 1 , a 2 , α 2 , p 2 ) . . . (p n-1 , a n , α n , p n ).
By denition of B, there exist p 0 , p 1 , . . . , p n states of A 1 , q 0 , q 1 , . . . , q n states of A 2 , integers c 1 , c 2 , . . . , c n , d 1 , d 2 , . . . , d n such that

π 1 = (p 0 , a 1 , c 1 , p 1 ), (p 1 , a 2 , c 2 , p 2 ), . . . , (p n-1 , a n , c n , p n ) is a successful path in A 1 , π 2 = (q 0 , a 1 , d 1 , q 1 ), (q 1 , a 2 , d 2 , q 2 ), . . . , (q n-1 , a n , d n , q n ) is a successful path in A 2 , for every 1 ≤ i ≤ n, α i = c i -d i , for every 0 ≤ i ≤ n, p i = (p i , q i ) and p i q i .
Thus, one has π 1 π 2 . Therefore, since A 1 and A 2 satisfy the strong substitutivity problem, the following inequality holds:

n i=1 d i ≤ n i=1 c i . Consequently, cost B (π) = n i=1 α i ≥ 0.
(⇐) Assume now that A 1 and A 2 satisfy A 1 A 2 and for every successful path π of B, cost B (π) ≥ 0.

Since A 1 A 2 , by Lemma 4, for every successful path in A 1 there exists a -related successful path in A 2 .

Finally, consider two successful paths

π 1 = (p 0 , a 1 , c 1 , p 1 ), (p 1 , a 2 , c 2 , p 2 ), . . . , (p n-1 , a n , c n , p n ) in A 1 and π 2 = (q 0 , a 1 , d 1 , q 1 ), (q 1 , a 2 , d 2 , q 2 ), . . . , (q n-1 , a n , d n , q n ) in A 2 such that π 1 π 2 .
By denition there exists an successful path π in B,

π = (p 0 , a 1 , α 1 , p 1 ), (p 1 , a 2 , α 2 , p 2 ) . . . (p n-1 , a n , α n , p n ). such that for every 1 ≤ i ≤ n, α i = c i -d i , for every 0 ≤ i ≤ n, p i = (p i , q i ) and p i q i .
Moreover, by hypotheses, one has cost B (π) ≥ 0:

cost(π) = n i=1 α i ≥ 0. Consequently, n i=1 d i ≤ n i=1 c i .
It follows that cost A2 (π 2 ) ≤ cost A1 (π 1 ), proving the claim.

Deciding whether A 1 A 2 is known to be P-complete [START_REF] Sawa | P-hardness of equivalence testing on nite-state processes[END_REF][START_REF] Sawa | Behavioural equivalences on nite-state systems are ptime-hard[END_REF]. Now deciding whether for every successful path π of B, cost B (π) ≥ 0 is a basic polynomial problem on weighted graphs which can be solved for instance by Bellman-Ford's algorithm.

The P-completeness is trivially obtained using the claim on automata with nil weights and the P-completeness of testing whether A 1 A 2 .

2

Theorem 6. The partial strong substitutivity problem is P-complete.

Proof.

Let A 1 and A 2 be two trim automata. Let B be the automaton constructed as in the proof of Theorem 5. We claim that A 1 st p A 2 if and only if A 1 A 2 and if every transition of B has a positive weight.

The proof is quite similar to the one of Theorem 5: if A 1 and A 2 satisfy the partial strong substitutivity problem, then using the property on paths of length 1, each transition of B has to be positively weighted. Conversely, if every transition of B has a positive weight, it is clear by a direct induction on paths lengths, that A 1 and A 2 satisfy the partial strong substitutivity problem.

The P-completeness is also trivially obtained using the claim on automata with nil weights and the P-completeness of testing whether A 1 A 2 .

2

Substitutivity Problems

This section provides decidability results for the substitutivity and the partial substitutivity problems.

Theorem 7. The substitutivity problem is polynomial time decidable if A 2 is nitely ambiguous.

Proof.

Let A 2 = (Q 2 , Σ, E 2 , I 2 , F 2 ) a nitely ambiguous integer weighted automaton and A 1 = (Q 1 , Σ, E 1 , I 1 , F 1 ) be a integer weighted automaton. Set A 3 = (Q 1 , Σ × Q 1 × Q 1 , E 3 , I 1 , F 1 ) and A 4 = (Q 2 , Σ × Q 1 × Q 1 , E 4 , I 2 , F 2 ) where: • E 3 = {(p, [a, p, q], c, q) | (p, a, c, q) ∈ E 1 }, • E 4 = {(p, [a, r, s], c, q) | (p, a, c, q) ∈ E 2 , ∃x ∈ Z, (r, a, x, s) ∈ E 1 , r, s ∈ Q 1 and r
p and s q}.

Notice that A 3 is unambiguous and that A 4 is nitely ambiguous. Indeed, if u = [a 1 , q 1 , q 2 ][a 2 , q 2 , q 3 ] . . . [a n , q n , q n+1 ] is accepted by A 3 , then there is a unique execution (q 1 , a 1 , c 1 , q 2 ) . . . (q n , a n , c n , q n+1 ) labelled by u because of restriction on E in Sect. 3. Now assume that A 2 is -ambiguous and that the word u = [a 1 , q 1 , q 2 ][a 2 , q 2 , q 3 ] . . . [a n , q n , q n+1 ] is accepted by A 4 . Since there are at most executions in A 2 accepting a 1 a 2 . . . a n , there is at most executions in A 4 accepting u. Thus A 4 is nitely ambiguous. Let B = A 3 × (-A 4 ), where -A 4 is obtained from A 4 by multiplying the weight of each transition by -1.

We claim that A 1 A 2 if and only if A 1 A 2 and for every u ∈ L(B), there exists an execution π in B such that cost B (π) ≥ 0.

(⇒) Assume rst that A 1 A 2 . Then A 1 A 2 . Now let u ∈ L(B).
By denition of the product, one also has u ∈ L(A 3 ). Consequently, there exists an execution π 3 in A 3 of label u of the form π 3 = (q 1 , [a 1 , q 1 , q 2 ], c 1 , q 2 ), (q 2 , [a 2 , q 2 , q 3 ], c 2 , q 3 ) . . . (q n , [a n , q n , q n+1 ], c n , q n+1 ).

Consequently, by construction of A 3 ,

π 1 = (q 1 , a 1 , c 1 , q 2 ), (q 2 , a 2 , c 2 , q 3 ) . . . (q n , a n , c n , q n+1 ) is an execution in A 1 .
Since A 1 A 2 , there exists an execution π 2 in A 2 of label a 1 a 2 . . . a n such that cost A2 (π 2 ) ≤ cost A1 (π 1 ) and π 1 π 2 .

(1) Set

π 2 = (p 1 , a 1 , d 1 , p 2 ), (p 2 , a 2 , d 2 , p 3 ) . . . (p n , a n , d n , p n+1 ). Now, by construction of A 4 , π 4 = (p 1 , [a 1 , q 1 , q 2 ], d 1 , p 2 ), (p 2 , [a 2 , q 2 , q 3 ], d 2 , p 3 ) . . . (p n , [a n , q n , q n+1 ], d n , p n+1 )
is an execution of A 4 . Since cost A2 (π 2 ) = cost A4 (π 4 ) and cost A1 (π 1 ) = cost A3 (π 3 ) and by (1), the execution π in B corresponding to π 3 and π 4 has label u and a positive cost.

(⇐) Let assume now that A 1 and A 2 satisfy A 1 A 2 and for every u ∈ L(B), there exists an execution π in B such that cost B (π) ≥ 0.

Let π 1 = (q 1 , a 1 , c 1 , q 2 ), (q 2 , a 2 , c 2 , q 3 ) . . . (q n , a n , c n , q n+1 ) be an execution of A 1 . By construction of A 3 , one has in A 3 the following execution π 3 = (q 1 , [a 1 , q 1 , q 2 ], c 1 , q 2 ), (q 2 , [a 2 , q 2 , q 3 ], c 2 , q 3 ) . . . (q n , [a n , q n , q n+1 ], c n , q n+1 ).

Consequently, since A 1 A 2 , there exists a successful path π 4 in A 4 such that π 3 π 4 . It follows that u = [a 1 , q 1 , q 2 ][a 2 , q 2 , q 3 ] . . . [a n , q n , q n+1 ] is in L(B). By hypothesis, there exists an execution π in B of label u such that cost B (π) ≥ 0.

(

) 2
Let π 3 and π 4 be the corresponding executions of respectively A 3 and A 4 corresponding to π. Using (2), one has: cost A4 (π 4 ) ≤ cost A3 (π 3 ).

Therefore, since A 3 is unambiguous, π 3 = π 3 and one has:

cost A4 (π 4 ) ≤ cost A3 (π 3 ). (3)
Set

π 4 = (p 1 , [a 1 , q 1 , q 2 ], d 1 , p 2 ), (p 2 , [a 2 , q 2 , q 3 ], d 2 , p 3 ) . . . (p n , [a n , q n , q n+1 ], d n , p n+1 ).
By construction of A 4 , there exists an execution π 2 of A 2 of the form:

π 2 = (p 1 , a 1 , d 1 , p 2 ), (p 2 , a 2 , d 2 , p 3 ) . . . (p n , a n , d n , p n+1 ).
Since cost A4 (π 4 ) = cost A2 (π 2 ) and by (3) one has:

cost A2 (π 2 ) ≤ cost A3 (π 3 ).
Since by construction π 2 π 1 , the proof of the claim is completed.

This nishes the proof of the theorem, the polynomial time decidability resulting from Theorem 3.

2

Theorem 8. The partial substitutivity problem is decidable in polynomial time.

Proof.

Let A 1 and A 2 be two trim automata. We claim that automata A 1 p A 2 if for every transition (p 1 , a, c 1 , q 1 ) of A 1 there exists a transition (p 2 , a, c 2 , q 2 ) of A 2 such that c 2 ≤ c 1 , p 1 p 2 and q 1 q 2 . Indeed, if A 1 p A 2 then, using the property on paths of length 1, one has the desired result. Conversely, if for every transition (p 1 , a, c 1 , q 1 ) of A 1 there exists a transition (p 2 , a, c 2 , q 2 ) of A 2 such that c 2 ≤ c 1 , p 1 p 2 and q 1 q 2 , a direct induction on paths lengths shows that A 1 p A 2 .

Computing relation can be done in polynomial time. Next, it suces to check the above property by a simple walk of the transitions list. 2

Substitutivity and Composition

In this section we put the substitutivity problems introduced in this paper in the composition context. We dene three natural composition operators: sequential, strict-sequential and parallel compositions. To motivate composition operators, let us mention ATP rules formalising BPEL in [START_REF] Mateescu | Formal modeling and discrete-time analysis of BPEL Web services[END_REF], in discrete-time. Another example comes from applications where CSP controllers are used for B machines modelling the components. Indeed, in CSP B approach, the CSP sequential and parallel composition operators are allowed [START_REF] Evans | Interactive tool support for csp || b consistency checking[END_REF] to control B machines. A lot of process algebraic approaches allow such composition operators.

In addition to these well-known operators, we consider the strict sequential composition operator allowing to observe when the control goes from the rst component to the second one. This operator is useful, e.g., for the architectural description of the composite Fractal components [BABC + 09]. Notice also that our parallel composition operator is the same as the operator studied in [START_REF] Chaki | Verication of evolving software via component substitutability analysis[END_REF], but in addition our operator handles action costs.

We demonstrate that considering path costs when verifying simulation relations in a composition manner, does have a cost: some (but not all) substitutivity notions introduced in this paper are not compatible with several composition operators. New positive composition results are also provided.

= (Q 1 , A 1 , E 1 , I 1 , F 1 ) and A 2 = (Q 2 , A 2 , E 2 , I 2 , F 2 ) be two integer weighted automata. The sequential composition of A 1 and A 2 , denoted A 1 .A 2 , is the au- tomaton A 12 = (Q 12 , A 12 , E 12 , I 12 , F 12 )
where

• Q 12 = {(p 1 , p 2 ) | p 1 ∈ Q 1 , p 2 ∈ I 2 } ∪ Q 2 , • A 12 = A 1 ∪ A 2 , • I 12 = {(p 1 , p 2 ) | p 1 ∈ I 1 , p 2 ∈ I 2 }, • F 12 = F 2 ,
and where the transition relation E 12 obeys the following rules:

[SEQ1] p 1 a1,c1 -→ A1 q 1 (p 1 , p 2 ) a1,c1 -→ A1.A2 (q 1 , p 2 ) [SEQ2] p 2 a2,c2 -→ A2 q 2 (p 1 , p 2 ) a2,c2 -→ A1.A2 q 2 p 1 ∈ F 1 [SEQ3] p 2 a2,c2 -→ A2 q 2 p 2 a2,c2 -→ A1.A2 q 2 States of the form (p 1 , p 2 ), with p 1 ∈ Q 1 and p 2 ∈ Q 2 are called composed states.
This denition means that all moves of sequential composition are moves of either A 1 , or of A 2 if A 1 is in a nal state, or of A 2 if the state is a non composed one.

Given the two automata A exe1 and A exe2 depicted in Fig. 3, their sequential composition A exe1 .A exe2 is given in Fig. 4. Lemma 10. Let A 1 , A 2 , A 3 , A 4 be four automata such that there exist two simulation relations 1 and 2 , and A 1 1 A 3 and A 2 2 A 4 . We dene the relation R between the states of A 1 .A 2 and the states of A 3 .A 4 by • (p 1 , p 2 )R(p 3 , p 4 ) if and only if (p 1 1 p 3 ) and (p 2 2 p 4 ) and,

• p 2 Rp 4 if and only if p 2 2 p 4 and,

• there is neither state of the form (p 1 , p 2 ) related by R to a state of A 4 , nor state of A 2 related by R to a state of the form (q 3 , q 4 ). • For non composed states, since every transition from a non composed state of A 1 .A 2 targets, by the rule [SEQ3], a non composed state of A 1 .A 2 , the condition i) of Denition 2 is satised for states of A 2 and A 4 .

p 1 q 1 a 1 , c 1 p 3 q 3 A 3 A 1 a 1 , c 3 ≺ ≺ Figure 5: Proof of Lemma 11. p 2 q 2 a 2 , c 2 p 4 q 4 A 4 A 2 a 2 , c 4 ≺ ≺
• For composed states, assume that p 1 1 p 3 and p 2 2 p 4 . Two kinds of transitions can be red from (p 1 , p 2 ).

If there is a transition (p 1 , a 1 , c 1 , q 1 ) in A 1 , then by [SEQ1] there is a transition in A 1 .A 2 of the form ((p 1 , p 2 ), a 1 , c 1 , (q 1 , p 2 )) (see Fig. 5). Since p 1 1 p 3 , by Denition 2 there is a transition (p 3 , a 1 , c 3 , q 3 ) in A 3 such that q 1 1 q 3 . Thus (q 1 , p 2 )R(q 3 , p 4 ).

If there is a transition (p 2 , a 2 , c 2 , q 2 ) in A 2 , then by [SEQ2] there is a transition

((p 1 , p 2 ), a 2 , c 2 , q 2 ) in A 1 .
A 2 (see Fig. 6). Since p 2 2 p 4 , by Denition 2 there is a transition (p 4 , a 2 , c 4 , q 4 ) in A 4 such that q 2 2 q 4 . Therefore q 2 Rq 4 , proving the lemma.

2

Proposition 11. Let A 1 , A 2 , A 3 , A 4 be nite trim automata.

If A 1 A 3 and A 2 A 4 [resp. A 1 p A 3 and A 2 p A 4 ], then the pair A 1 .A 2 A 3 .A 4 [resp. A 1 .A 2 p A 3 .A 4 ].
Proof.

Let π be a successful path of A 1 .A 2 . By denition of the sequential product, π can be decomposed into π = π 1 , ((p 1 , p 2 ), a 2 , c 2 , q 2 ), π 2 , where π 1 is a path built up using only composed states, and (p 2 , a 2 , c 2 , q 2 ), π 2 is a successful path of A 2 . Let ϕ be the projection that maps each transition ((p 1 , p 2 ), a, c, (q 1 , q 2 )) of A 1 .A 2 between composed states to (p 1 , a, c, q 1 ). The function ϕ can be naturally extended to paths. Decompositions are illustrated in Fig. 7: the rst line represents the decomposition of π and the second line the decomposition using ϕ.

-, p 2 start p 1 , p 2 π 1 q 2 a 2 , c 2 A 2 A 1 × {p 2 } π 2 p 2 start p 2 ϕ(π 1 ) q 2 a 2 , c 2 A 2 A 1 π 2
By [SEQ1], ϕ(π 1 ) is a successful path of A 1 . Since A 1 A 3 , there exists a path π 3 of A 3 such that π 1 1 π 3 and cost(π 3 ) ≤ cost(π 3 ). Similarly, since A 2 A 4 , there exists a path π 4 such that ((p 2 , a 2 , c 2 , q 2 ), π 2 ) 2 π 4 and cost((p 2 , a 2 , c 2 , q 2 ), π 2 ) ≤ cost(π 4 ). Let q 4 be the starting state of π 4 , p f be the ending state of π 3 , and k be the length of π 3 (which is also the length of π 1 ). The sequence π of transitions of A 3 .A 4 dened by: if i is smaller than or equal to k, and if the i-th transition of π 3 is (r i , a i , c i , r i+1 ), then the i-th transition of π is ((r i , q 4 ), b i , d i , (r i+1 , q 4 )). If i is equal to k + 1, then the i-th transition of π is ((p f , q 4 ), a 2 , c 2 , q 2 ). For the values of i greater than k + 1, the i-th transition of π is the (i + k)-th transition of π 4 . Using [SEQ1], [SEQ2] and [SEQ3], one can easily check that π is a successful path of A 3 .A 4 such that that cost(π ) ≤ cost(π). Moreover, by Lemma 10, π π , proving the lemma for the substitutivity problem.

The proof still works for the partial substitutivity problem.

2

Unfortunately, Proposition 11 does not hold for (partial) strong substitutivity problems. Indeed, let us consider the following four automata:

A 1 = ({p 1 }, {a}, {(p 1 , a, 1, p 1 )}, {p 1 }, {p 1 }), A 3 = ({q 1 }, {a}, {(q 1 , a, 0, q 1 )}, {q 1 }, {q 1 }), A 2 = ({p 2 }, {a}, {(p 2 , a, 4, p 2 )}, {p 2 }, {p 2 }), A 4 = ({q 2 }, {a}, {(q 2 , a, 3, q 2 )}, {q 2 }, {q 2 }),
Pairs of automata A 1 , A 3 and A 2 , A 4 both trivially satisfy the strong substitutivity problem and the partial strong substitutivity problems. However, when considering the pair A 1 .A 2 , A 3 .A 4 , one has {((p 1 , p 2 ), (q 1 , q 2 )), ((p 1 , p 2 ), q 2 ), (p 2 , q 2 )} ⊆ A1.A2,A3.A4 .

Consequently, ((p 1 , p 2 ), a, 1, (p 1 , p 2 ))((p 1 , p 2 ), a, 4, p 2 ) ((q 1 , q 2 ), a, 3, q 2 )(q 2 , a, 3, q 2 ).

But these paths do not satisfy the weight conditions of the strong and the partial strong substitutivity problems. Intuitively, a sequential composition of automata may create new ways to perform a sequence of actions: these new ways may have costs that do not full the universal weight condition required by the strong substitutivity.

However, when the automata in the pair have disjoint alphabets, the following composition result holds.

Proposition 12. Let A 1 , A 2 , A 3 , A 4 be nite trim automata [resp. are nite trim automata such that A 1 .A 2 and A 3 .A 4 are both trim] such that A 1 and A 2 have disjoint alphabets. If

A 1 st A 3 and A 2 st A 4 [resp. A 1 st p A 3 and A 2 st p A 4 ], then the pair A 1 .A 2 st A 3 .A 4 [resp. A 1 .A 2 st p A 3 .A 4 ].
Proof. Assume that A 1 st A 3 and A 2 st A 4 . Let π be a successful path of A 1 .A 2 . By Proposition 11, there exists a successful path of A 3 .A 4 similar to π with a lower cost. First we claim that the relation R dened in Lemma 10 is the largest simulation relation. Remark that since transitions that can be red from non composed states of A 1 .A 2 are exactly the transitions of A 2 and since A 2 and A 1 .A 2 have the same set of nal states, if p 2 A1.A2,A3.A4 p 4 , then p 2 A2,A4 p 4 . Now if (p 1 , p 2 ) A1.A2,A3.A4 (p 3 , p 4 ), then p 1 A1,A3 p 3 and p 2 A2,A4 p 4 . For every transition (p 2 , a 3 , c 3 , r 2 ) of A 2 , there exists a state transition in A 3 4 from (p 3 , p 4 ) labelled by a 3 to a state related to r 2 by A1.A2,A3.A4 . According to the assumption on the alphabet, this state, denoted r 4 , is not a composed state. Therefore (using the above remark) r 2 A2,A4 r 4 , proving the claim.

One can now prove the proposition.

Consider a path π of A 3 .A 4 such that π π . The path π can be decomposed into π = π 3 , ((p 3 , p 4 ), a, c, q 4 ), π 4 such that π 3 is a successful path of A 3 and ((p 3 , p 4 ), a, c, q 4 ), π 4 is a successfully path of A 4 . Similarly π can be decomposed into π = π 1 , ((p 1 , p 2 ), b, d, q 2 ), π 2 such that π 1 is a success-full path of A 1 and ((p 1 , p 2 ), b, d, q 2 ), π 2 is a success-full path of A 2 . Since π π and by alphabet conditions, π 1 and π 3 have the same length, a = b and, π 2 and π 4 have the same length. Now inductively using the claim (resp. the remark) on states of π 1 and π 3 (resp. of ((p 1 , p 2 ), b, d, q 2 )π 2 and ((p 3 , p 4 ), a, c, q 4 ), π 4 ), one has π 1 A1,A3 π 3 (resp. ((p 1 , p 2 ), b, d, q 2 ), π 2 A2,A4 ((p 3 , p 4 ), a, c, q 4 ), π 4 ). Since A 1 st A 3 and A 2 st A 4 , one has cost(π 3 ) ≤ cost(π 1 ) and cost(((p 3 , p 4 ), a, c, q 4 ), π 4 ) ≤ cost(((p 1 , p 2 ), b, d, q 2 ), π 2 ). Therefore, cost(π ) ≤ cost(π), which concludes the proof.

The proof for the strong substitutivity problem is very close to the above proof.

2

Let us consider a variant of the sequential composition of automata, called the strict sequential product, where additional transitions with a special label are introduced. This label allows one to identify parts of a path w.r.t. composed automata.

Denition 13. Let

A 1 = (Q 1 , A 1 , E 1 , I 1 , F 1 ) and A 2 = (Q 2 , A 2 , E 2 , I 2 , F 2 ) be two integer weighted automata. The strict sequential composition of A 1 and A 2 , denoted A 1 → A 2 , is the automaton A 12 = (Q 1 ∪ Q 2 , A 1 ∪ A 2 ∪ {δ}, E 1 ∪ E 2 ∪ E 12 , I 1 , F 2 ) where δ / ∈ A 1 ∪ A 2 and E 12 = {(p, δ, 0, q) | p ∈ F 1 , q ∈ I 2 }.
For our running automata A exe1 and A exe2 in Fig. 3, their strict sequential product A exe1 → A exe2 is depicted in Fig. 8.

Proposition 14. Let A 1 , A 2 , A 3 , A 4 be nite trim automata. If A 1 A 3 and A 2 A 4 [resp. A 1 p A 3 and A 2 A 4 ] [resp. A 1 st A 3 and A 2 st A 4 ] [resp. A 1 st p A 3 and A 2 st A 4 ] , then A 1 → A 2 A 3 → A 4 [resp.A 1 → A 2 p A 3 → A 4 ] [resp. A 1 → A 2 st A 3 → A 4 ] [resp. A 1 → A 2 st p A 3 → A 4 ] .
Proof.

The relation R between states of A 1 → A 2 and states of A 3 → A 4 is dened as follows: pRq if and only if either p is a state of A 1 and q a state of A 3 and p A1,A3 q, or p is a state of A 2 and q a state of A 4 and p A2,A4 q. One can easily check (as for Lemma 10) that R is a simulation relation.

The proof is structured as follows: rstly, (part 1), we prove the proposition for the substitutivity problem. Secondly, (part 2), we show that R is the largest simulation relation

1 start 2 b, 1 a, 2 a, 0 3 5 4 a, 3 b, 3 b, 4 a, 1 a, 1 δ, 0 δ, 0 a, 1 Figure 8: Automaton A exe1 → A exe2
between A 1 → A 2 and A 3 → A 4 . This leads to the nal third step (part 3), where we prove the proposition for the strong substitutivity problem. Proofs for partial (strong) substitutivity problems are very similar and left to the reader. Notice that since A 1 , A 2 , A 3 , A 4 are nite trim automata, so are A 1 → A 2 and A 3 → A 4 .

(Part 1):

Let π be a successful path in A 1 → A 2 . By construction of A 1 → A 2 , π can be decomposed into π 1 , (p 1 , δ, p 2 ), π 2 , where π 1 is a successful path of A 1 , π 2 is a successful path of A 2 , p 1 is a nal state of A 1 and p 2 an initial state of A 2 .
Assume that A 1 A 3 and A 2 A 4 , then there exist successful paths π 3 of A 3 and π 4 of A 4 such that π 1 A1,A3 π 2 , π 3 A3,A4 π 4 , cost(π 3 ) ≤ cost(π 1 ) and cost(π 4 ) ≤ cost(π 2 ). Let p 3 be the ending state of π 3 , and p 4 the starting state of p 4 . Since π 3 is a successful path in A 3 , p 3 is a nal state of A 3 . Similarly, p 4 is an initial state of A 4 . Consequently, π 3 , (p 3 , δ, 0, p 4 ), π 4 is a successful path of A 3 → A 4 . Moreover, by construction, πR(π 3 , (p 3 , δ, 0, p 4 ), π 4 ). Thus π π 3 , (p 3 , δ, 0, p 4 ), π 4 . Furthermore, cost(π 2 ) ≤ cost(π 1 ) and cost(π 4 ) ≤ cost(π 3 ) ensure that cost(π 3 , (p 3 , δ, 0, p 4 ), π 4 ) ≤ cost(π), proving the proposition for the substitutivity problem.

(Part 2):

We claim that R = , i.e. that R is the largest simulation relation between A 1 → A 2 and A 3 → A 4 . Indeed, let p be a state of A 1 → A 2 , and q be a state of A 3 → A 4 such that p A1→A2,A3→A4 q. Following cases arise:

(1) Assume that p is a state of A 2 . Since A 2 is trim, there exists a path in A 2 from p to a nal state of A 2 . Now, the assumption p A1→A2,A3→A4 q implies that there is a similar path in A 4 . Since δ doesn't occur in the label of this path, q is a state of A 4 .

Since the restriction of A1→A2,A3→A4 to states of A 2 and states of A 4 is a simulation relation, one has p A2,A4 q. Therefore pRq.

(2) Assume that p is a state of A 1 . We will show by contradiction that q is a state of A 3 . Assume that q is a state of A 4 . Since A 1 and A 3 are trim, there is a path in A 1 → A 2 from p to a nal state. By construction, δ occurs in the label of this path. Since p A1→A2,A3→A4 q, there is a similar path in A 3 → A 4 . But q is a state of A 4 , thus there is no path from q whose label contains δ, a contradiction. Therefore, q ∈ A 3 . As for case (1), this ensures that pRq, proving the claim.

(Part 3):

Assume that A 1 st A 3 and A 2 st A 4 . According to above proof, it remains to show that for every successful path π of A 1 → A 2 and every successful path

π of A 3 → A 4 , if π π , then cost(π ) ≤ cost(π). Assuming that π is a successful path of A 1 → A 2
and that π is a successful path of A 3 → A 4 , the path π can be decomposed into π = π 1 , (p 1 , δ, p 2 ), π 2 and the path π into π = π 3 , (p 3 , δ, p 4 ), π 4 . Symbol δ occurs only once in the label of π and in the label of π . Thus, by length argument, if π π , using the claim (point 2), one has π 1 A1,A3 π 3 and π 2 A2,A4 π 4 . It follows that cost(π 3 ) ≤ cost(π 1 ) and cost(π 4 ) ≤ cost(π 2 ). Consequently, cost(π ) ≤ cost(π), proving the proposition for the strong substitutivity problem. 2

Substitutivity and Parallel Composition

We now dene a parallel composition operator and oer the positive and negative results on the compatibility of the substitutivity with relation to the parallel composition.

Denition 15. Let

A 1 = (Q 1 , A 1 , E 1 , I 1 , F 1 ) and A 2 = (Q 2 , A 2 , E 2 , I 2 , F
2 ) be two integer weighted automata. The parallel product of A 1 and A 2 , denoted A 1 ⊗ A 2 , is the automaton

A 12 = (Q 12 , A 12 , E 12 , I 12 , F 12 )
where

• Q 12 = {(p 1 , p 2 ) | p 1 ∈ Q 1 , p 2 ∈ Q 2 }, • A 12 = A 1 ∪ A 2 , • I 12 = I 1 × I 2 , • F 12 = F 1 × F 2 ,
and where the transition relation E 12 obeys the following rules:

[SYNC] p 1 a1,c1 -→ A1 q 1 , p 2 a2,c2 -→ A2 q 2 (p 1 , p 2 ) a,c1+c2 -→ A1⊗A2 (q 1 , q 2 ) a ∈ A 1 ∩ A 2 [PAR1] p 1 a1,c1 -→ A1 q 1 (p 1 , p 2 ) a1,c1 -→ A1⊗A2 (q 1 , p 2 ) a 1 ∈ A 1 \ A 2 [PAR2] p 2 a2,c2 -→ A2 q 2 (p 1 , p 2 ) a2,c2 -→ A1⊗A2 (p 1 , q 2 ) a 2 ∈ A 2 \ A 1
The parallel composition of A 1 and A 2 , denoted A 1 A 2 , is the automaton obtained by deleting in A 1 ⊗ A 2 states (and related transitions) that are not co-accessible.

Consider, for instance, the two automata A exe3 and A exe4 depicted in Fig. 9. The automata A exe3 ⊗ A exe4 and A exe3 A exe4 are respectively displayed in Fig. 10 and Fig. 11.

Proposition 16. Let A 1 , A 2 , A 3 , A 4 be nite trim automata [resp. are nite trim automata such that A 1 A 2 and A 3 A 4 are both trim]. If A 1 A 3 and A 2 A 4 [resp. A 1 p A 3 and A 2 p A 4 ], then A 1 A 2 A 3 A 4 satises the substitutivity problem [resp. A 1 A 2 p A 3 A 4 ]. Proof.
In this proof A 1 is the common alphabet of A 1 and A 3 and A 2 is the common alphabet of A 2 and A 4

The relation R between states of A 1 A 2 and states of A 3 A 4 is dened as follows: (p 1 , p 2 )R(p 3 , p 4 ) if and only if p 1 A1,A3 p 3 and p 2 A2,A4 p 4 . The proof is divided into two -If the i-th transition of π is labelled by a letter a in A 1 ∩ A 2 , then the i-th transition of π is ((p 3 , p 4 ), a, c 3 + c 4 , (q 3 , q 4 )) where (p 3 , a, c 3 , q 3 ) is the α i -th transition of π 3 and (p 4 , a, c 4 , q 4 ) is the β i -th transition of π 4 .

p 3 start p 4 a, 1 a, 1 a, 1 q 1 start q 3 q 2 a, 1 a, 1 a, 6 a, 0 q 4 start a, 0
-If the i-th transition of π is labelled by a letter a in A 1 \ A 2 , then the i-th transition of π is ((p 3 , p 4 ), a, c 3 , (q 3 , p 4 )) where (p 3 , a, c 3 , q 3 ) is the α i -th transition of π 3 .

-If the i-th transition of π is labelled by a letter a in A 2 \ A 1 , then the i-th transition of π is ((p 3 , p 4 ), a, c 4 , (p 3 , q 4 )) where (p 4 , a, c 4 , q 4 ) is the β i -th transition of π 4 .

One can easily check that α i is less or equal to the length of π 1 (equivalently the length of π 3 ) and that β i is less or equal to the length of π 2 (equivalently the length of π 4 ). Thus, following rules [P AR1], [P AR2] and [SY N C], π is well-dened. By a direct induction, one can prove that π is a successful path of A 3 A 4 satisfying πRπ and cost(π ) ≤ cost(π).

Since R is, by denition, included in A1 A2,A3 A4 , the proof for the substitutivity problem is complete.

2

Unfortunately, Proposition 16 does not hold for (partial) strong substitutivity problems.

Consider, for instance, the following automata (depicted in Fig. 12):

A 1 = ({p 1 , p 2 }, {a}, {(p 1 , a, 1, p 1 ), (p 1 , a, 1, p 2 ), (p 2 , a, 1, p 2 )}, {p 1 }, {p 2 }), A 3 = ({q 1 , q 2 , q 3 }, {a}, {(q 1 , a, 1, q 3 ), (q 3 , a, 6, q 1 ), (q 1 , a, 0, q 2 ), (q 2 , a, 1, q 2 )}, {q 1 }, {q 2 }), A 2 = ({p 3 , p 4 }, {a}, {(p 3 , a, 1, p 3 ), (p 3 , a, 1, p 4 ), (p 4 , a, 1, p 4 )}, {p 3 }, {p 4 }), A 4 = ({q 4 }, {a}, {(q 4 , a, 0, q 4 )}, {q 4 }, {q 4 }). Both pairs of automata A 1 , A 3 and A 2 , A 4 satisfy the strong substitutivity problem. But (p 1 , p 3 ) A1 A2,A3 A4 (q 1 , q 4 ), (p 1 , p 3 ) A1 A2,A3 A4 (q 3 , q 4 ) and (p 2 , p 4 ) A1 A2,A3 A4 (q 2 , q 4 ). Therefore the successful paths π 12 = ((p 1 , p 3 ), a, 2, (p 1 , p 3 ))((p 1 , p 3 ), a, 2, (p 1 , p 3 ))((p 1 , p 3 ), a, 2, (p 2 , p 4 )) and π 34 = ((q 1 , q 4 ), a, 1, (q 3 , q 4 ))((q 3 , q 4 ), a, 6, (q 1 , q 4 ))((q 1 , q 4 ), a, 0, (q 2 , q 4 )) satisfy π 12 A1 A2,A3 A4 π 34 . But cost(π 12 ) = 6 and cost(π 34 ) = 7.

However, as for the sequential composition, one has the following result for pairs of automata with disjoint alphabets. Proposition 17. Let A 1 , A 2 , A 3 , A 4 be nite trim automata such that A 1 and A 2 have disjoint alphabets and, A 3 and A 4 have disjoint alphabets. If A 1 st A 3 and A 2 st A 4 [resp.

A 1 st p A 3 and A 2 , st p A 4 ], then the pair

A 1 A 2 st A 3 A 4 [resp. A 1 A 2 st p A 3 A 4 ].
Proof. Assume that both couples A 1 st A 3 and A 2 st A 4 . Let π be a successful path of A 1 A 2 . By Proposition 16, there exists a successful path of A 3 A 4 similar to π with a smaller cost.

We claim that if (p 1 , p 2 ) A1 A2,A3 A4 (p 3 , p 4 ), then p 1 A1 A2 p 3 and p 2 A3 A4 p 4 . It suces to prove that p 1 A1 A2 p 3 because of the case symmetry. Assume that p 1 A1 A2 p 3 . Then the following cases may arise:

(1) p 1 is a nal state of A 1 whereas p 3 is not. Since A 2 is trim, there exists a path in A 2 from p 2 to a nal state q 2 of A 2 . This path is labelled by letters in the A 2 alphabet. Therefore there is a path in A 1 A 2 from (p 1 , p 2 ) to (p 1 , q 2 ). Since (p 1 , p 2 ) A1 A2,A3 A4 (p 3 , p 4 ), there is a similar path in A 3 A 4 to a state of the form (p 3 , q 4 ). Now since q 2 is a nal state in A 2 , so is (p 1 , q 2 ) in A 1 A 2 . But (p 1 , q 2 ) A1 A2,A3 A4 (p 3 , q 4 ), so, (p 3 , q 4 ) is nal in A 3 A 4 . Consequently, p 3 isnal, a contradiction.

(2) There is a transition in A 1 starting from p 1 labelled by a, but no transition labelled by a starts from p 3 in A 3 . Therefore there is a transition in A 1 A 2 starting from (p 1 , p 2 ) labelled by a. Since a is not a letter from the alphabet of A 3 , no transition labelled by a in A 3 A 4 can be red from (p 3 , p 4 ), a contradiction.

(3) There is a transition (p 1 , a 1 , c 1 , q 1 ) of A 1 such that for every transition of the form (p 3 , a 1 , c 3 , q 3 ) of A 2 , q 1 A1,A3 q 3 . Iterating this construction, one can reach states (p 1 , p2) and (p 3 , p 3 ) satisfying conditions of case (1), proving the claim. Now let π be a path in A 3 A 4 such that π A1 A2,A3 A4 π . Let π 3 be the sequence of transitions obtained by deleting in π all the transitions labelled by a letter in the A 4 alphabet. Let also π 4 be the sequence of transitions obtained by deleting in π all the transitions labelled by a letter in the alphabet of A 3 . Using the hypotheses on the alphabets, one can easily check that the projection π 3 of π on A 3 is a successful path of A 3 . Similarly, the projection π 4 of π on A 4 is a successful path of A 4 . Following the same way, π can be projected to produce a successful path π 1 of A 1 and a successful path π 2 of A 2 . The claim ensures that π 1 A1,A3 π 3 and that π 2 A1,A3 π 4 . Now remind that both couples A 1 st A 3 and A 2 st A 4 satisfy the strong substitutivity problem. Thus cost(π 3 ) ≤ cost(π 1 ) and cost(π 4 ) ≤ cost(π 2 ). Since cost(π) = cost(π 1 ) + cost(π 2 ) and since cost(π ) = cost(π 3 ) + cost(π 4 ), one has cost(π ) ≤ cost(π), proving the proposition.

The proof for the partial strong substitutivity problem is similar and left to the reader.

2

Practical Issues

As explained in Section 1, this paper is dedicated to component and service substitutivity with a special emphasis on their assembly. The challenge is to build trustworthy systems which satisfy both functional and non functional requirements.

The obtained theoretical results have practical applications. Indeed, the methodological and practical approaches we have been developing through various project collaborations rest on them. These approaches can be summarised by:

1. The construction of trustworthy software systems from existing components.

2. An incremental approach to specify and verify component assembling.

3. The elicitation of non-functional requirements and their integration in the specication.

Application to Web Services with QoS

There are numerous works on automata-based analyses of service composition (see [START_REF] Beek | Formal methods for service composition[END_REF] for a survey). In the setting of the present paper, i.e. without silent τ -transitions, thesimulation relation is compatible with a sequential composition operator modelling e.g. the sequence BPEL structured activities, and with an asynchronous parallel composition operator implementing e.g. the ow BPEL structured activities. Notice that for the ow activities, the encoding would work without the source/target links that would somehow be encoded through a synchronisation. Both BPEL operators are important in practice since they allow building complex services by a composition of services.

An algorithm for the trace-based substitutivity problem has been implemented. The tests have been performed on dierent versions of a movie store example, a book store example provided by Oracle [START_REF] Juric | A Hands-on Introduction to BPEL, Part 2: Advanced BPEL[END_REF], and the classical loan approval example. We intend to continue the implementation and extend that work to simulation-based substitutivity problems presented in this paper.

Application to Embedded Components

Thousands of systems in very various domains such as telecommunications, transportation, home automation (also called smart homes or domotics), system-on-chip, etc. are equipped with smart devices or "intelligent" components. They embed a growing software part which is often critical for the safety of the global system. Embedded systems whose resources are in general limited must satisfy both functional and non functional properties to optimise the use of their resources (memory, energy, etc.).

Within the application domain of land transportation systems, dierent models of a localisation system are proposed 4 . A localisation composite component, which is a critical part of land transportation systems, is made up of dierent positioning systems, like GPS, Wi or GPS+Wi. The use of more than one localisation system is required in a driverless vehicle like Cristal or Cycab, because no system is ecient enough to be used alone. Indeed, a localisation based on the GPS data cannot be used in certain contexts, and the localisation component must respond even if no satellite data can be captured. These requirements allow the vehicle to set a real trustworthy level and to improve the condence in the reliability.

The composite localisation component includes several positioning systems, a controller, and a merger. Figure 13 In addition, the proposed framework seems to be well-adapted to handle energy dispersion associated with actions, that is particularly relevant for sensor networks (see for instance [START_REF] Wu | Energyaware routing for wireless sensor networks by AHP[END_REF]).

a 1 , 1 d, 1 c 1 , 3 a 1 , 1 d, 1 c 1 , 3 a, 1 b 1 , 2 b 2 , 2 c, 3 c, 3 b 2 , 4 a, 1 b 1 , 1 c, 3

Conclusion

In this paper we proposed to manage both functional and non functional aspects of components. To sum up, this paper exposes how integer weighted automata can be used to address substitutivity issues in the context of component-based applications. We dened four kinds of substitutivity managing QoS aspects. Several complexity results for these substitutivity problems were provided. They are summed up in the following table. Provided proofs being constructive, above complexity results are tractable in practice. 5 In this paper, there is no distinction between inputs, outputs and internal actions because we want the substitutivity to deal with all kinds of actions. In our approach, distinguishing actions will just lead to divide the alphabet into three parts: results will be exactly the same.

Distinguishing actions would be useful either for composition purposes or for simulation denitions. On the one hand, the parallel composition dened in Section 6 can manage dierent kinds of actions that can be synchronised or not. In this context, it is possible to manage synchronisation on external actions. On the other hand, using internal actions may lead to several simulation relation denitions. At this step, our work does not handle taubased simulation. We plan to investigate this direction in a future work. Several information on that was pointed out at the beginning of Section 7.1. Notice that synchronisations for the parallel composition operator we consider can manage tau-actions as another action.

In the paper, we consider that automata represent compositions already built up from components/services. This approach seems to be not contradictory with works in [START_REF] Lohmann | Operating guidelines for nite-state services[END_REF][START_REF] Ch | Deciding service composition and substitutability using extended operating guidelines[END_REF] where the behaviour semantics of a set of open nets (uncoloured Petri nets with interfaces modelling services) is given by automata whose states are annotated by boolean formula over states. In those automata, interactions/communications are already performed. Once the interactions/synchronisations are hidden in composition automata, the only remained piece of information we are interested in concerns action costs.

Note that the answer to the substitutivity problem proposed in this paper depends on the chosen abstraction. In fact, the results obtained in our framework, as well as for all abstraction-based approaches, depend on the expressive power of the formalism and on the quality of the model. It would be interesting to address the same problem with ner abstractions. In the future, following works on automata-based analyses of services [START_REF] Beek | Formal methods for service composition[END_REF] and components [BABC + 09], we plan to extend the model to include messages among components. To go further, more expressive formalisms like Mealy machines, process algebra or Petri nets would provide more precise component abstractions. In this context, extending substitutivity denitions to these formalisms is easy, but algorithmic studies have to be performed again: however substitutivity problems may be undecidable or have an intractable complexity for these formalisms. In other respects, the matter of whether the substitutivity problem is decidable in the general case, remains open. In the context of the trace-based substitutivity, this problem is undecidable. We conjecture the same result holds for the simulation-based substitutivity.

Polynomial time decidability shows the substitution notion presented in the paper is reasonable and practical. For example, it would be possible to take into consideration the fact that performance/reliability metrics of a component service are not only a function on the service or the service trace, but also on parameters such as the execution environment, the performance/reliability of externally called services, and the usage prole. In fact, the decidability being polynomial time, it could be possible to apply the algorithms for each of these parameters.

In a more general context, modelling quantitative aspects is of great interest for modelling and verifying component-based applications. Work continues on modelling and verifying properties simpler than substitutivity, and on considering other applications, e.g. business protocols.

We would like to thank the anonymous referees and FACS'08 participants for their interesting and helpful comments and suggestions to improve and to develop the preliminary results in [START_REF] Héam | Component simulation-based substitutivity managing QoS aspects[END_REF]. We are grateful to the anonymous SCP referees for their corrections, interesting comments and helpful advice to improve the preliminary version of this paper.

Figure 1 :

 1 Figure 1: Components C 1 and C 2

Fig. 1 .Figure 2 :

 12 Figure 2: Components C 3 and C 4 with costs

Figure 3 :

 3 Figure 3: Automata A exe1 and A exe2

Figure 4 :

 4 Figure 4: Automaton A exe1 .A exe2

Figure 6 :

 6 Figure 6: Proof of Lemma 11.

Figure 7 :

 7 Figure 7: Proof of Proposition 11.

Figure 9 :Figure 10 :Figure 11 :

 91011 Figure 9: Automata A exe3 and A exe4

Figure 12 :

 12 Figure 12: Automata for a counter-example on Proposition 16

Figure 13 :

 13 Figure 13: Sequential and parallel composition

  http://think.ow2.org/ In addition, the substitutivity notions were considered in the composition context. Three natural composition operators sequential, strict-sequential and parallel compositions were dened. For these composition operators, new positive and negative results on the substitutivity vs. composition compatibility were provided. We demonstrated that considering path costs when verifying simulation relations in a composition manner, has a cost. To sum up, the composition results are given in the chart below.We are well aware that there are other possibilities for dening compositions. Nevertheless, our denitions are general enough, so the present paper can be seen as a step towards more sophisticated settings to be of use in real-life applications (see, e.g.,[START_REF] Mateescu | Formal modeling and discrete-time analysis of BPEL Web services[END_REF][START_REF] Evans | Interactive tool support for csp || b consistency checking[END_REF]

		deterministic		nitely ambiguous	non-deterministic
		automata		automata	automata
	substitutivity	Polynomial time	Polynomial time	open
	partial	Polynomial time	Polynomial time	Polynomial time
	substitutivity
	strong	Polynomial time	Polynomial time	P-complete
	substitutivity
	partial strong	Polynomial time	Polynomial time	P-complete
	substitutivity
		sequential	sequential	strict	parallel	parallel
		disj. alphabets		disj. alphabets
	substitutivity	yes		yes	yes	yes	yes
	partial	yes		yes	yes	yes	yes
	substitutivity
	strong	no		yes	yes	no	yes
	substitutivity
	partial strong	no		yes	yes	no	yes
	substitutivity

BABC

+ 09]).

The French National Research Agency TACOS project, ANR-06-SETI-017 (http://tacos.loria.fr).

parts: Firstly, in (Part 1), we prove that R is a simulation relation. Secondly, in (Part 2), we prove the proposition for the substitutivity problem.

(Part 1):

We rst prove that relation R is a simulation relation. Indeed, if (p 1 , p 2 ) is nal then, by denition of A 1 ⊗ A 2 , p 1 and p 2 are respectively nal states of A 1 and A 2 . Then, if p 1 A1,A3 p 3 , p 3 is nal, and if p 2 A2,A4 p 4 , p 4 is nal, proving R satises condition ii) of Denition 2. Now it remains to prove condition i). Assume that (p 1 , p 2 )R(p 3 , p 4 ). The following three cases arise:

(1) If there exists a transition ((

obtained by applying [P AR1]. So, there exist a transition (p 1 , a 1 , c 1 , q 1 ) in A 1 and a state q 3 of A 3 such that p 1 A1,A3 q 3 . Since (q 1 , p 2 ) is accessible and co-accessible in

(2) If a transition from (p 1 , p 2 ) is red by applying [P AR2], one can prove, as for case (1), that condition i) of Denition 2 is satised.

(3) If a transition from (p 1 , p 2 ) is red by applying [SY N C], then there exist a transition (p 1 , a, c 1 , q 1 ) in A 1 and a transition (p 2 , a, c 2 , q 2 ) such that a ∈ A 1 ∩ A 2 . Since (p 1 , p 2 )R(p 3 , p 4 ), there are q 3 in A 3 and q 4 in A 4 and transitions (p 3 , a, c 3 , q 3 ) and (p 4 , a, c 4 , q 4 ) in respectively A 3 and A 4 such that q 1 A1,A3 q 3 and q 2 A2,A4 q 4 . Since (q 3 , q 4 ) is both an accessible and co-accessible state of A 1 ⊗ A 2 , (q 1 , q 2 )R(q 3 , q 4 ), proving that R is a simulation relation.

(Part 2):

Now we will prove the proposition for the substitutivity problem. Assume that A 1 A 3 and A 2 A 4 . Let π be a successful path in A 1 A 2 . We denote by ϕ i (i ∈ {1, 2}), the partial function that maps transitions of A 1 A 2 to transitions of A i as follows: a transition ((p 1 , p 2 ), a, c, (q 1 , q 2 )) of A 1 A 2 is mapped to (p i , a, c, q i ) if a ∈ A i . Partial functions ϕ i (i ∈ {1, 2}) are extended to sequences of transitions: ϕ i (t 1 , . . . , t k ) = ϕ i (t 1 ), . . . , ϕ i (t k ) with the convention that if ϕ i (t) is not dened, then ϕ i (t) is mapped to the empty path. For instance, if t 1 , t 2 , t 3 are three transition respectively labelled by letter of

Let π be a successful path in A 1 A 2 . One can easily check that ϕ i (π) is a successful path of A i . Therefore there are successful paths π 3 and π 4 of respectively A 3 and A 4 such that ϕ 1 (π) A1,A3 π 3 , ϕ 2 (π) A1,A3 π 4 , cost(π 3 ) ≤ cost(ϕ 1 (π)) and cost(π 4 ) ≤ cost(ϕ 2 (π)). We inductively dene the nite sequences of integers α i and β i by

-if the i-th transition of π is labelled by a letter in A 2 \ A 1 , then α i+1 = α 1 and β i+1 = 1 + β i .

Informally, when running the path π, each time a transition labelled by a letter in A i is met, the corresponding counter (α for A 1 and β for A 2 ) increases. Now we dene the sequence of transitions π of A 3 ⊗ A 4 by: