Benoit Caillaud
email: benoit.caillaud@irisa.fr

Benoît Delahaye
email: benoit.delahaye@irisa.fr

Kim Guldstrand Larsen

Axel Legay
email: axel.legay@irisa.fr

Mikkel L Pedersen
email: mikkelp@cs.aau.dk

Andrzej Wasowski
email: wasowski@itu.dk

Benoît Caillaud

Andrzej W Ąsowski

Compositional design methodology with constraint Markov chains

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

I. INTRODUCTION

Modern systems are big and complex, resulting from assembling multiple components. The components are designed by teams, working independently but with a common agreement on what the interface of each component should be. As a consequence, mathematical foundations that allow to reason at the abstract level of interfaces in order to infer global properties are an active research area known as compositional design [START_REF] Henzinger | The embedded systems design challenge[END_REF]. Within this area specification theories provide a modeling language that allows designing, evolving and advisedly reusing components with formal guarantees. In a logical interpretation, interfaces are specifications and systems/components that implement a specification are models/implementations. There is an agreement that a good theory should support the following requirements:

1) Consistency and Satisfaction. It should be decidable whether a specification admits at least one implementation, and whether a system implements a specification. 2) Refinement. Refinement of specification expresses inclusion of sets of implementations, and therefore allows to compare richness and precision of specifications. 3) Structural composition. A theory should provide a combination operator on specifications, reflecting the standard composition of systems by, e.g. parallel product. 4) Logical composition/conjunction. Different aspects of systems are often specified by different teams. The issue of dealing with multiple aspects of multiple viewpoints is thus essential. It should be possible to represent several specfications (viewpoints) for the same system, and to combine them in a logical/conjunctive fashion. 5) Incremental Design. A theory should allow incremental design (composing/conjoining specifications in any order) and independent implementability (composable specifications can always be refined separately) [START_REF] Alfaro | Interface-based design[END_REF]. For functional analysis of discrete-time non-probabilistic systems, the theory of Modal Transition Systems (MTS) [START_REF] Larsen | Modal specifications[END_REF] provides a specification formalism supporting refinement as well as conjunction and parallel composition. It has been recently applied to construct interface theories [START_REF] Raclet | Modal interfaces: Unifying interface automata and modal cifications[END_REF], [START_REF] Larsen | Modal I/O automata for interface and product line theories[END_REF], which are extensions of classical interface automata proposed by de Alfaro et al. [START_REF] Alfaro | Interface automata[END_REF], [START_REF] Doyen | Interface theories with component reuse[END_REF], [START_REF] Chakrabarti | Synchronous and bidirectional component interfaces[END_REF].

As soon as systems include randomized algorithms, probabilistic protocols, or interact with physical environment, probabilistic models are required to reason about them. This is exacerbated by requirements for fault tolerance, when systems need to be analyzed quantitatively for the amount of failure they can tolerate, or for the delays that may appear. As Henzinger and Sifakis [START_REF] Henzinger | The embedded systems design challenge[END_REF] point out, introducing probabilities into design theories allows assessing dependability of IT systems in the same manner as commonly practiced in other engineering disciplines.

Generalizing the notion of MTSs to the non-functional analysis of probabilistic systems, the formalism of Interval Markov Chains (IMCs) was introduced [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF]; with notions of satisfaction and refinement generalizing probabilistic bisimulation. Informally, IMCs extend Markov Chains by labeling transitions with intervals of allowed probabilities rather than concrete probability values. Implementations of IMCs are Markov Chains (MCs) whose probability distributions match the constraints induced by the intervals. IMCs is known to be an efficient model on which refinement and composition can be performed with efficient algorithms from linear algebra. Unfortunately, as we shall now see, the expressive power of IMCs is inadequate to support both logical and structural composition.

Consider two IMCs, S 1 and S 2 , in Figure 1 specifying different probability constraints related to the height H and weight W of a given person. Attempting to express the conjunction S 1 ∧ S 2 as an IMC by a simple intersection of bounds gives z 1 ≤ 1 2 , 1 6 ≤ z 2 ≤ 1 2 , 1 8 ≤ z 3 and 1 6 ≤ z 4 . However, this naive construction is too coarse: whereas (z 1 , z 2 , z 3 , z 4 ) = W ≥ 60 [ 1 6 , 1]

[0, 1]

[ 1 8 , 1]

[0, 1 2 ]

S 1 S 2 1, 1 3, 3 2, 3 2, 2 3, 2 H ≥ 160 W ≥ 60 W ≥ 60 W ≤ 90 H ≥ 160 H ≤ 190 z 2 z 1 z 4 z 3 W ≤ 90 H ≤ 190 S 1 ∧ S 2
Fig. 1: IMCs showing non-closure under conjunction

( 1 2 , 1 6 , 1 8 , 5 24
) satisfies the constraints the resulting overall probability of reaching a state satisfying H ≥ 160, i.e. z 1 +z 2 = 2 3 , violates the upper bound 1 2 specified in S 1 . What is needed is the ability to express dependencies between the probabilities z 1 , z 2 , z 3 , z 4 besides that of being a probability distribution (z 1 + z 2 + z 3 + z 4 = 1). The correct conjunctive combination is expressed by three following constraints, exceeding the expressive power of IMCs:

z 1 +z 2 ≤ 1 2 , 1 8 ≤ z 3 +z 4 , 1 6 ≤ z 2 +z 4 .
A similar example shows that IMCs are also not closed under parallel composition, either.

One way to approach this problem could be to work with two types of specifications: IMCs for refinement and structural composition, and a probabilistic logic such as PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] on which a logical conjunction is naturally defined. Such a solution is clearly not satisfactory. Indeed, it is not clear how one can synthesize a MC (an implementation) that satisfies two PCTL formulas. It is also not possible to structurally compose two logical PCTL formulas.

The solution promoted in this paper is to enrich the model of IMCs. More precisely, we introduce Constraint Markov Chains (CMCs) as a foundation for component-based design of probabilistic systems. CMCs are a further extension of IMCs allowing rich constraints on the next-state probabilities from any state. Whereas linear constraints suffice for closure under conjunction, polynomial constraints are necessary for closure under parallel composition. We provide constructs for refinement, consistency checking, logical and structural composition of CMC specifications -all indispensable ingredients of a compositional design methodology.

In CMCs, each state is also labelled with a set of subsets of atomic propositions. Those propositions represent properties that should be satisfied by the implementation. The idea being that the satisfaction relation ensures that an implementation matches at least one of the subsets. This allows the specification to make additional assumptions on the behaviors of the implementation. Hence, at the level of specification, our model thus presents choices on subsets of actions. However these choices are independent from the probabilistic ones in the sense that any CMC whose states are labelled with a set of subsets of atomic propositions can be turned to an equivalent (in terms of set of implementations) CMC whose states are labeled with a single subset of atomic propositions. There, choices between the subsets of actions disappear. It is thus not surprising that our notion of parallel composition is following the widely accepted principle of separation of concerns. The idea is to separate parallel composition of probability distributions from synchronization on sets of actions. This separation can be found in probabilistic specification theories that have probabilistic automata as an underlying semantic model [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], [START_REF] Hansson | A calculus for communicating systems with time and probabitilies[END_REF], [START_REF] Jonsson | Probabilistic extensions of process algebras[END_REF], [START_REF] Hermans | Interactive Markov Chains[END_REF]. In fact, we show how probabilistic automata can be represented as CMCs, and how the traditional notions of parallel composition on such model can be derived in our framework with precongruence properties obtained for free. This latter result shows that CMCs capture computational structure of known models and operators, laying down a basis for studying shared properties of many probabilistic automata based languages. As already mentioned, we exemplify this by showing how precongruence properties for composition of probabilistic automata and known refinements can be obtained by reductions to CMCs.

The notions of satisfaction and strong/weak refinements for CMCs conservatively extend similar notions for IMCs [START_REF] Fecher | Don't Know in probabilistic systems[END_REF], [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF]. We characterize these relations in terms of implementation set inclusion. In particular, in the main theorem, we prove that for deterministic CMCs weak and strong refinements are complete with respect to implementation set inclusion. In addition, we provide a construction, which for any CMC S returns a deterministic CMC (S) containing the models of S. Refinement relations are not complete for non-deterministic CMCs, but one can show that the weak refinement is more likely to coincide with implementation set inclusion in such a context. We show that refinement between CMCs with polynomial constraints can be decided in essentially single exponential time.

Structure of the paper. In Section II, we introduce the concept of CMCs and a satisfaction relation with respect to Markov Chains. Consistency, refinement and conjunction are discussed in Section III. Structural composition is introduced in Section IV. In Section V, we introduce deterministic CMCs and show that, for this class of CMCs, strong and weak refinements coincide with inclusion of implementation sets. Section VI discusses the class of polynomial CMCs, which is the smallest class of CMCs closed under all the compositional design operations. Section VIII concludes the paper with related and future work. Due to space constraints, some algorithms and proofs are given in a long version of this paper [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF].

II. CONSTRAINT MARKOV CHAINS

Let A, B be sets of propositions with A ⊆ B. The

restriction of W ⊆ B to A is given by W↓ A ≡ W ∩ A. If T ⊆ 2 B , then T↓ A ≡ {W↓ A | W ∈ T }. For W ⊆ A define the extension of W to B as W ↑ B ≡ {V ⊆ B | V ↓ A = W },
so the set of sets whose restriction to A is W . Lift it to sets of sets as follows: if

T ⊆ 2 A then T↑ B ≡ {W ⊆ B | W↓ A ∈ T }.
Let M, ∆ ∈ [0, 1] n×k be two matrices and x ∈ [0, 1] 1×k be a vector. We write M ij for the cell in ith row and jth column of M , M p for the pth row of M , and x i for the ith element of x.

Finally, ∆ is a correspondence matrix iff 0 ≤ ∑ k j=1 ∆ ij ≤ 1 for all 1 ≤ i ≤ n.
, . . . , k} → [0, 1] k → {0, 1} is a constraint function such that if ϕ(j)(x) = 1 then the x vector is a probability distribution: x ∈ [0, 1] k and ∑ k i=1 x i = 1.
An Interval Markov Chain (IMC for short) [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] is a CMC whose constraint functions are represented by intervals, so for all

1 ≤ i ≤ k there exist constants α i , β i such that ϕ(j)(x) = 1 iff ∀1 ≤ i ≤ k, x i ∈ [α i , β i ].
Example. Two parties, a customer and a vendor, are discussing a design of a relay for an optical telecommunication network. The relay is designed to amplify an optic signal transmitted over a long distance over an optic fiber. The relay should have several modes of operation, modelled by four dynamically changing properties and specified by atomic propositions a, b, c, and e: The customer presents CMC S 1 (Figure 2a) specifying the admissible behaviour of the relay from their point of view. States are labelled with formulas characterizing sets of valuations. For instance, "(a + b + c ≥ 2) ∧ (e = 0)" at state 2 of S 1 represents V 1 (2) = {{a, b}, {b, c}, {a, c}, {a, b, c}}, where a, b, c, and e range over Booleans. State 1 specifies a standby mode, where no signal is emitted and only marginal power is consumed. State 2 is the high power mode, offering a high signal/noise ratio, and hence a high bit-rate and low error rate, at the expense of a high power consumption. State 3 is the low power mode, with a low power consumption, low bit-rate and high error rate. The customer prescribes that the probability of the high power mode (state 2) is higher than 0.7. The vendor replies with CMC S 2 (Figure 2b), which represents possible relays that they can build. Because of thermal limitations, the low power mode has a probability higher than 0.2.

A state u of S is (directly) reachable from a state i if there exists a probability distribution x ∈ [0, 1] k with a nonzero probability x u , which satisfies ϕ(i)(x).

We relate CMC specifications to MCs implementing them, by extending the definition of satisfaction presented in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] to observe the valuation constraints and the full-fledged constraint functions. Crucially, like [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], we abstract from syntactic structure of transitions-a single transition in the implementation MC can contribute to satisfaction of more than one transition in the specification, by distributing its probability mass against several transitions. Similarly many MC transitions can contribute to satisfaction of just one specification transition.

Definition 3 (Satisfaction Relation). Let P = {1, . . . , n}, o P , M, A P , V P be a MC and S = {1, . . . , k}, o S , ϕ, A S , V S be a CMC with A S ⊆ A P . Then R ⊆ {1, . . . , n} × {1, . . . , k} is a satisfaction relation between states of P and S iff whenever p R u then 1)

V P (p)↓ AS ∈ V S (u), and
2) there exists a correspondence matrix ∆ ∈ [0, 1] n×k such that • for all 1 ≤ p ≤ n with M pp = 0, ∑ k j=1 ∆ p j = 1; • ϕ(u)(M p × ∆) holds and • if ∆ p u = 0 then p R u .
We write P |= S iff there exists a satisfaction relation relating o P and o S , and call P an implementation of S. The set of all implementations of S is given by [[S]] ≡ {P | P |= S}. Rows of ∆ that correspond to reachable states of P always sum up to 1. This is to guarantee that the entire probability mass of implementation transitions is allocated. For unreachable states, we leave the corresponding rows in ∆ unconstrained. P may have a richer alphabet than S, in order to facilitate abstract modelling: this way an implementation can maintain local information using internal variables. Algorithms to decide satisfaction are particular cases of algorithms to decide refinement between CMCs. See the next section.

Example. We illustrate the concept of correspondence matrix between Specification S 1 (given in Figure 2a) and Implementation P 2 (given in Figure 2d). The CMC S 1 has three outgoing transitions from state 1 but, due to constraint function in 1, the transition labelled with x 1 cannot be taken (the constraint implies x 1 = 0). The probability mass going from state 1 to states 2 and 3 in P 2 corresponds to the probability allowed by S 1 from its state 1 to its state 2; The redistribution is done with the help of the matrix ∆ given in Figure 3c. The ith column in ∆ describes how big fraction of each transition probability (for transitions leaving 1) is associated with probability x i in S 1 . Observe that the constraint function ϕ 1 (1)(0, 0.8, 0.2) = ϕ 1 (1)((0, 0.7, 0.1, 0.2) × ∆) is satisfied.

1 (e = 1) ∧ (a = b = c = 0) x 1 2 3 (a + b + c ≤ 1) ∧ (e = 0) (a + b + c ≥ 2) ∧ (e = 0) x 3 1 1 x 2 ϕ 1 (1)(x) ≡ (x 2 ≥ 0.7) ∧(x 2 + x 3 = 1)
(a) CMC S 1 , the customer specification of the optical relay

2 3 1 y 3 1 1 y 2 (a = 1) ∧ (e = 0) (a = 0) ∧ (e = 0) y 1 (e = 1) ∧ (a = b = c = 0) ϕ 2 (1)(y) ≡ (y 3 ≥ 0.2) ∧(y2 + y3 = 1) (b) CMC S 2 ,
(a + b + c ≥ 2) ∧ (e = 0) [ (a + b + c ≤ 1) ∨ ((a = 0) ∧ (b = c = 1)) ]
∧ (e = 0)

x 3 1 1 x 2 x 1 1 3 2 (e = 1) ∧ (a = b = c = 0) ϕ 4 (1)(x) ≡ (x 1 = 0) ∧ (x 2 ≥ 0.7) ∧ (x3 ≥ 0.2) ∧ (x2 + x3 = 1) (a) CMC S 4 generalizing S 3 , so S 3 S 4 1 1 1 1 2, 2 2, 3 3, 3 3, 2 1, 1 z 2,2 z 3,2 z 1,1 z 2,3 z 3,3 ϕ 3 (1, 1)(Z) ≡ (∀j. z 1,j = 0) ∧ (z2,2 + z2,3 ≥ 0.7) ∧ (z 2,2 +z 2,3 +z 3,2 +z 3,3 = 1) ∧ (∀i. zi,1 = 0) ∧ (z2,3 + z3,3 ≥ 0.2) (b) S 3 = S 1 ∧ S 2 .
Constraints on propositions, pairwise conjunctions of constraints of S 1 and S 2 , are left out to avoid clutter Fig. 3: Examples of refinement, conjunction and satisfaction for CMCs CMC semantics follows the Markov Decision Process (MDP) tradition [START_REF] Sen | Model-checking Markov chains in the presence of uncertainties[END_REF], [START_REF] Chatterjee | Model-checking omegaregular properties of interval Markov chains[END_REF]. The MDP semantics is typically opposed to the Uncertain Markov Chain semantics, where the probability distribution from each state is fixed a priori.

States of CMCs are labeled with set of subsets of atomic propositions. A single set of propositions represents properties that should be satisfied by the implementation. A set of sets models a choice of properties, with the idea being that the satisfaction relation ensures that an implementation matches at least one of the subsets. This allows the specification to make additional assumptions on the behaviors of the implementation. For an implementation, in each state the discrete choice of proposition set and the probabilistic choice of successor are independent.

It turns out that any CMC whose states are labelled with a set of subsets of atomic propositions can be turned into an equivalent (in terms of sets of implementations) CMC whose states are labeled with sets that contains a single subset of atomic propositions. Hence working with sets of subsets of valutations is a kind of modeling sugar that can be removed with a transformation to the single valuation normal form. Definition 4. We say that a CMC is in a Single Valuation Normal Form if all its admissible valuation sets are singletons (

|V (i)| = 1 for each 1 ≤ i ≤ k).
More precisely every consistent CMC with at most one admissible valuation in the initial state can be transformed into the normal form preserving its implementation set. A polynomial time normalization algorithm can be found in [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF].

III. CONSISTENCY, REFINEMENT AND CONJUNCTION

Consistency. A CMC S is consistent if it admits at least one implementation. We now discuss how to decide consistency. A state u of S is valuation consistent iff V (u) = ∅; it is constraint consistent iff there exists a probability distribution vector x ∈ [0, 1] 1×k such that ϕ(u)(x) = 1. It is easy to see that if each state of S is both valuation and constraint consistent then S is also consistent. However, inconsistency of a state does not imply inconsistency of the specification. Indeed, an inconsistent state could be made unreachable by forcing the probabilities to reach it to zero. The operations presented later in this paper may introduce inconsistent states, leaving a question if a resulting CMC is consistent. In order to decide whether S is inconsistent, state inconsistencies are propagated throughout the entire state-space using a pruning operator β that removes inconsistent states from S. The result β(S) is a new CMC, which may still contain some inconsistent states. The operator is applied iteratively, until a fixpoint is reached. S is consistent if the resulting CMC β * (S) contains at least one state. The formal definition is given in [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF]. It can be shown (see [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF]) that pruning preserves the set of implementations.

Proposition 5. Let S be a CMC. We have that [[S]] = [[β(S)]].

The fixpoint of β, and thus the entire consistency check, can be computed using a quadratic number of state consistency checks. The complexity of each check depends on the constraint language chosen.

Refinement. Comparing specifications is central to stepwise design methodologies. Systematic comparison enables simplification of specifications (abstraction) and adding details to specifications (elaboration). Usually specifications are compared using a refinement relation. Roughly, if S 1 refines S 2 , then any model of S 1 is also a model of S 2 .

We will now introduce two notions of refinement for CMCs that extend two well known refinements for IMCs [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], [START_REF] Fecher | Don't Know in probabilistic systems[END_REF]. We not only generalize these refinements, but, unlike [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], [START_REF] Fecher | Don't Know in probabilistic systems[END_REF], we also characterize them in terms of implementation set inclusion -also called thorough refinement -and computational complexity.

The strong refinement between IMCs, by Jonsson and Larsen [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], extends to CMCs in the following way:

Definition 6 (Strong Refinement). Let S 1 = {1, . . . , k 1 }, o 1 , ϕ 1 , A 1 , V 1 and S 2 = {1, . . . , k 2 }, o 2 , ϕ 2 , A 2 , V 2 be CMCs with A 2 ⊆ A 1 . A relation R ⊆ {1, . . . , k 1 }×{1, . . . , k 2 } is a strong refinement relation between states of S 1 and S 2 iff whenever v R u then 1) V 1 (v)↓ A2 ⊆ V 2 (u), and
2) there exists a correspondence matrix ∆ ∈ [0, 1] k1×k2 such that for all probability distribution vectors x ∈

[0, 1] 1×k1 if ϕ 1 (v)(x) holds then • For all 1 ≤ i ≤ k 1 , x i = 0 =⇒ ∑ k2 j=1 ∆ ij = 1; • ϕ 2 (u)(x × ∆) holds and • if ∆ v u = 0 then v R u . We say that S 1 strongly refines S 2 iff o 1 R o 2 .
Strong refinement imposes a "fixed-in-advance" correspondence matrix regardless of the probability distribution satisfying the constraint function. In contrast, the weak refinement, which generalizes the one proposed in [START_REF] Fecher | Don't Know in probabilistic systems[END_REF] for IMCs, allows choosing a different correspondence matrix for each probability distribution satisfying the constraint:

Definition 7 (Weak Refinement). Let S 1 = {1, . . . , k 1 }, o 1 , ϕ 1 , A 1 , V 1 and S 2 = {1, . . . , k 2 }, o 2 , ϕ 2 , A 2 , V 2 be CMCs with A ⊆ A 1 . The relation R ⊆ {1, . . . , k 1 } × {1, . . . , k 2 } is a weak refinement relation iff whenever v R u then: 1) V 1 (v)↓ A2 ⊆ V 2 (u) and 2) for any distribution x ∈ [0, 1] 1×k1 satisfying ϕ 1 (v)(x), there exists a matrix ∆ ∈ [0, 1] k1×k2 such that • For all 1 ≤ i ≤ k 1 , x i = 0 =⇒ ∑ k2 j=1 ∆ ij = 1; • ϕ 2 (u)(x × ∆) holds and • if ∆ v u = 0 then v R u . CMC S 1 (weakly) refines S 2 , written S 1 S 2 , iff o 1 R o 2 .
Example. Figure 3d illustrates a family of correspondence matrices parametrized by γ, witnessing the weak refinement between initial states of S 3 and S 4 (defined in Figures 3a-3b). The actual matrix used in proving the weak refinement depends on the probability distribution vector z that satisfies the constraint function ϕ 3 of state [START_REF] Henzinger | The embedded systems design challenge[END_REF][START_REF] Henzinger | The embedded systems design challenge[END_REF]. Take γ = 0.7-z22 z23 if z 22 ≤ 0.7 and γ = 0.8-z22 z23 otherwise (z 22 ≤ 0.8 by definition). It is easy to see that ϕ 3 ((1, 1))(z) implies ϕ 4 (1)(z×∆).

Both weak and strong refinements imply implementation set inclusion (see [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF]). In Section V, we shall see that the converse holds for a particular class of CMCs. However, this is not the case in general: strong refinement is strictly stronger than weak refinement, which is strictly stronger than implementation set inclusion. Formally, we have the following proposition. So our refinement relations for CMCs can be ordered from finest to coarsest: the strong refinement, the weak refinement, and the implementation set inclusion. As the implementation set inclusion is the ultimate refinement, checking finer refinements is used as a pragmatic syntax-driven, but sound, way of deciding it. Algorithms for checking strong and weak refinements are discussed in [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF]. Those algorithms are polynomial in the number of state, but the treatment of each state depends on the complexity of the constraints. Finally, let us mention that lower-bounds for the strong and weak refinement checking remain open problems.

Conjunction. Conjunction, also called logical composition, combines requirements of several specifications.

Definition 9 (Conjunction). Let S 1 = {1, . . . , k 1 }, o 1 , ϕ 1 , A 1 , V 1 and S 2 = {1, . . . , k 2 }, o 2 , ϕ 2 , A 2 , V 2 be two CMCs. The conjunction of S 1 and S 2 , written S 1 ∧ S 2 , is the CMC S = {1, . . . , k 1 } × {1, . . . , k 2 }, (o 1 , o 2 ), ϕ, A, V with A = A 1 ∪ A 2 , V ((u, v)) = V 1 (u)↑ A ∩V 2 (v)↑ A , and ϕ((u, v))(x1,1, x1,2, . . . , x2,1, . . . , x k 1 ,k 2 ) ≡ ϕ1(u)( P k 2 j=1 x1,j, . . . , P k 2 j=1 x k 1 ,j )∧ ϕ2(v)( P k 1 i=1 xi,1, . . . , P k 1 i=1 x i,k 2 ).
Conjunction may introduce inconsistent states and thus its use should normally be followed by applying the pruning operator β * . As already stated in the introduction, the result of conjoining two IMCs is not an IMC in general, but a CMC whose constraint functions are systems of linear inequalities. Figure 3b depicts a CMC S 3 expressing the conjunction of IMCs S 1 and S 2 (see Figures 2a-2b). The constraint z 2,3 + z 3,3 ≥0.2 in state (1, 1) cannot be expressed as an interval.

As expected, conjunction of two specifications coincides with their greatest lower bound with respect to the weak refinement (also called shared refinement).

Theorem 10. Let S 1 , S 2 and S 3 be three CMCs. We have (a) ((S 1 ∧ S 2 ) S 1 ) and ((S 1 ∧ S 2 ) S 2 ) and (b) if (S 3 S 1 ) and (S 3 S 2 ), then S 3 (S 1 ∧ S 2 ).

In fact, as follows from the later results of Section V, the set of implementations of a conjunction of two deterministic specifications S 1 and S 2 coincides with the intersection of implementation sets of S 1 and S 2 (the greatest lower bound in the lattice of implementation sets).

IV. COMPOSITIONAL REASONING USING THE PRINCIPLE

OF SEPARATION OF CONCERNS Let us now turn to structural composition. In our theory, as we already said in the introduction and after presenting CMCs, choices regarding the set of valuations and stochastic choices are independent from each others. This property of the model naturally leads to a definition of the parallel composition operator based on the principle of separation of concerns. The idea is that probabilistic behaviours are composed separately from the synchronization of the sets of state valuations. This allows realizing probabilistic composition as a simple product of independent distributions.

Remark 1. The principle of separation of concerns is intensively used in the definition of parallel composition for many systems that mix stochastic and non-deterministic choices.

Among them, one can cite many theories for probabilistic process algebra [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], [START_REF] Jonsson | Probabilistic extensions of process algebras[END_REF]. Similar principles are also applied for continuous time stochastic models, in a slightly different setting based on CTMCs [START_REF] Hermans | Interactive Markov Chains[END_REF]. In Section VII, we shall see that our structural composition covers the one of probabilistic automata.

Following the separation of concerns principle, components are composed first into a product (or effectively just a vector of independent entities), and then synchronized by constraining their behaviour. This design is both simple and expressive: it allows applying diverse synchronization mechanisms, beyond just matching inputs to outputs. Moreover it elegantly exploits the prior knowledge on logical composition, as the synchronization operator turns out to be realizable using conjunction.

We start by discussing how systems and specifications can be composed in a non-synchronizing way, then we introduce a notion of synchronization. The non-synchronizing independent composition is largely just a product of two MCs (or CMCs).

Definition 11 (Parallel Composition of MCs). Let

P 1 = {1, . . . , n 1 }, o 1 , M , A 1 , V 1 and P 2 = {1, . . . , n 2 }, o 2 , M , A 2 , V 2 be two MCs with A 1 ∩ A 2 = ∅.
The parallel composition of P 1 and P 2 is the MC

P 1 P 2 = {1, . . . , n 1 } × {1, . . . , n 2 }, (o 1 , o 2 ), M, A 1 ∪ A 2 , V where: M ∈ [0, 1] (n1×n2)×(n1×n2) is such that M (p,q)(r,s) = M pr • M qs ; and V ((p, q)) = V 1 (p) ∪ V 2 (q).
For CMCs, we have the following definition.

Definition 12 (Parallel Composition of CMCs

). Let S 1 = {1, . . . , k 1 }, o 1 , ϕ 1 , A 1 , V 1 and S 2 = {1, . . . , k 2 }, o 2 , ϕ 2 , A 2 , V 2 be CMCs with A 1 ∩ A 2 = ∅. The parallel composition of S 1 and S 2 is the CMC S 1 S 2 = {1, . . . , k 1 } × {1, . . . , k 2 }, (o 1 , o 2 ), ϕ, A 1 ∪ A 2 , V , where ϕ((u, v))(z 1,1 , z 1,2 , . . . z 2,1 , . . . , z k1,k2 ) = ∃x 1 , . . . , x k1 , y 1 , . . . , y k2 ∈ [0, 1] such that ∀(i, j) ∈ {1, . . . , k 1 } × {1, . . . , k 2 } we have z i,j = x i • y j and ϕ 1 (u)(x 1 , . . . , x k1 ) = ϕ 2 (v)(y 1 , . . . , y k2 ) = 1. Finally, V ((u, v)) = {Q 1 ∪ Q 2 | Q 1 ∈ V 1 (u), Q 2 ∈ V 2 (v)}.
It is worth mentioning that IMCs are not closed under composition. Consider IMCs S and S given in Figure 4a and their composition S S given in Figure 4b. Assume first that S S is an IMC. As a variable z ij is the product of two variables x i and y j , if S S is an IMC, then one can show that the interval for z ij is obtained by computing the products of the bounds of the intervals over which x i and y j range. Hence, we can show that

z 11 ∈ [0, 1/2], z 12 ∈ [0, 1/3], z 21 ∈ [1/6, 1], z 22 ∈ [0, 2/3]. Let [a, b
] be the interval for the constraint z ij , it is easy to see that there exist implementations I 1 of S 1 and I 2 of S 2 such that I 1 I 2 satisfies the constraint z ij = a (resp. z ij = b). However, while each bound of each interval can be satisfied independently, some points in the polytope defined by the intervals and the constraint ∑ z ij = 1 cannot be reached. As an example, consider z 11 = 0, z 12 = 1/3, z 21 = 1/3, z 22 = 1/3. It is clearly inside the polytope, but one cannot find an implementation I of S S satisfying the constraints given by the parallel composition. Indeed, having z 11 = 0 implies that x 1 = 0 and thus that z 12 = 0. Theorem 13. If S 1 , S 2 , S 1 , S 2 are CMCs then S 1 S 1 and S 2 S 2 implies S 1 S 2 S 1 S 2 , so the weak refinement is a precongruence with respect to parallel composition. Consequently, for any MCs P 1 and P 2 we have that

P 1 |= S 1 ∧ P 2 |= S 2 implies P 1 P 2 |= S 1 S 2 .
As alphabets of composed CMCs have to be disjoint, the composition does not synchronize the components on state valuations like it is typically done for other (non-probabilistic) models. However, synchronization can be introduced by conjoining the composition with a synchronizer-a single-state CMC whose valuation function relates the atomic propositions of the composed CMCs.

Example. CMC S

S of Figure 4b is synchronized with the synchronizer Sync given in Figure 4c. Sync removes from S S all the valuations that do not satisfy (a = d)∧(b = ¬c). The result is given in Figure 4d. Observe that an inconsistency appears in State [START_REF] Henzinger | The embedded systems design challenge[END_REF][START_REF] Henzinger | The embedded systems design challenge[END_REF]. Indeed, there is no implementation of the two CMCs that can synchronize in the prescribed way. Synchronization is associative with respect to composition, which means that the order of synchronization and composition is inessential for final functionality of the system.

In general inconsistencies like this one can be uncovered by applying the pruning operator, which would return an empty specification. So synchronizers enable discovery of incompatibilities between component specifications in the same way as it is known for non-probabilistic specification models.

x 2 ∈ [1/3, 1] y 2 ∈ [0, 2/3] {{c}} {{a}{a, b}} y 1 ∈ [1/2, 1] x 1 ∈ [0, 1/2]
]] = [[(S 1 S 2 S 3 ) ∧ Sync 123 ]].
Finally, synchronized composition also supports component-based refinement in the style of Theorem 13:

Theorem 15. If S 1 , S 2 , S 1 , S 2 are CMCs, Sync is a synchro- nizer and S 1 S 1 ∧ S 2 S 2 then (S 1 S 2 ) ∧ Sync (S 1 S 2 ) ∧ Sync.
Consequently, a modeller can continue independent refinement of specifications under synchronization, knowing that the original synchronized specification will not be violated.

V. DETERMINISTIC CMCS

Clearly, if all implementations of a specification S 1 also implement a specification S 2 , then the former is a proper strengthening of the latter. Indeed, S 1 specifies implementations that break no assumptions that can be made about implementations of S 2 . Thus implementation set inclusion is a desirable refinement for specifications. Unfortunately, this problem is still open, and, as we have said, the weak and the strong refinement soundly approximate it. Had that approximation been complete, we would have had an effective decision procedure for implementation set inclusion. In this section, we argue that this indeed is the case for an important subclass of specifications: deterministic CMCs. A CMC S is deterministic iff for every state i, states reachable from i have pairwise disjoint admissible valuations:

Definition 16. Let S = {1, . . . , k}, o, ϕ, A, V be a CMC. S is deterministic iff for all states i, u, v ∈ {1, . . . , k}, if there exists x ∈ [0, 1] k such that (ϕ(i)(x) ∧ (x u = 0)) and y ∈ [0, 1] k such that (ϕ(i)(y) ∧ (y v = 0)), then we have that V (u) ∩ V (v) = ∅.
In Figures 2a and2b, both S 1 and S 2 are deterministic specifications. In particular states 2 and 3, reachable from 1 in both CMCs, have disjoint constraints on valuations. On the

1 2 3 4 x2 1 1 1 {{a, b}} {{a, c}{b, c}} {{a, b, c}{a, c}} {{a}} ϕ T (1)(x 1 , x 2 , x 3 , x 4 ) = ((x 2 = 1 ∧ x 3 = 0) ∨(x 2 = 0 ∧ x 3 = 1)) x3
Fig. 5: A CMC T whose set of implementations cannot be represented with a deterministic CMC other hand, the CMC T given in Figure 5 is non-deterministic. Indeed, for States 2 and 3, which can both be reached from State 1, we have that

V T (2) ∩ V T (3) = {{a, c}} = ∅.
Deterministic CMCs are less expressive than nondeterministic ones, in the sense that the same implementation sets cannot sometimes be expressed. Consider again the CMC T given in Figure 5. It is such that its set of implementations cannot be represented by a deterministic CMC. Indeed, any merging of States 2 and 3 in T would result in a CMC that accepts models where one can loop on valuation {a, c} and then accept valuation {a} with probability 1. Such a model cannot be accepted by T .

Proposition 17. Conjunction and composition preserve determinism.

In [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF], we present a determinization algorithm that can be applied to any CMC S whose initial state is a single valuation set. The result of the algorithm is a new CMC weakly refined by S. Consequently the implementation set of the result includes the one of S (see [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF]). This character of determinization resembles the known determinization algorithms for modal transition systems [START_REF] Benes | On determinism in modal transition systems[END_REF].

We now state one of the main theorems of the paper: the weak refinement is complete with respect to implementation set inclusion for deterministic CMCs:

Theorem 18. Let S 1 = {1, . . . , k 1 }, o 1 , ϕ 1 , A 1 , V 1 and S 2 = {1, . . . , k 2 }, o 2 , ϕ 2 , A 2 , V 2 be two consistent single valuation normal form deterministic CMCs with A 2 ⊆ A 1 . We have [[S 1 ]] ⊆ [[S 2 ]] ⇒ S 1 S 2 .
Proof: We present a sketch of the proof and refer to [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF] for details. We construct the refinement relation by relating all pairs of states of S 1 and S 2 for which implementation inclusion holds. Let R ⊆ {1, . . . , k 1 }×{1, . . . , k 2 } such that v R u iff for all MC I and state p of I we have p |= v ⇒ p |= u.

As we consider pruned CMCs, there exist implementations for all states. Then the usual, albeit complex and long in this case, coinductive proof technique is applied, showing that this relation is indeed a weak refinement relation. The crucial point of the argument lies in proving the closure propertyi.e. that if a S 1 state u advances possibly to u , then indeed the corresponding state v of S 2 can also advance to v and the (u , v ) pair is in R. In other words that implementation inclusion of predecessors implies the implementation inclusion of successors. This is proven in an ad absurdum argument. Roughly, assume that there would exist an implementation I of u which is not an implementation of v . Then one can construct an implementation I of u which evolves as I . This implementation would not implement v but could implement some other state of S 2 . This case is ruled out by requiring determinism and a normal form of S 2 . Then the only way for I to evolve is to satisfy v which contradicts the assumption that I is not an implementation of v . Since any consistent CMC with a single valuation in initial state can be normalized, Theorem 18 holds even if S 1 and S 2 are not in single valuation normal form. Thus, weak refinement and the implementation set inclusion coincide on the class of deterministic CMCs with at most single valuation in the initial state. Finally, Theorem 18 also holds for strong refinement. Indeed, the following theorem states that weak and strong refinements coincide on the class of deterministic CMCs.

Theorem 19. Let S 1 = {1, . . . , k 1 }, o 1 , ϕ 1 , A, V 1 and S 2 = {1, . . . , k 2 }, o 2 , ϕ 2 ,
A, V 2 be two deterministic CMCs in normal form. If there exists a weak refinement relation R such that S 1 R S 2 , then R is also a strong refinement relation.

Finally, the above results on completeness for deterministic specifications carry over to refinements of [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] and [START_REF] Fecher | Don't Know in probabilistic systems[END_REF], which are special cases of our refinements. Completeness properties for these refinements were open problems until now.

Discussion: A weaker Definition of Determinism. Our notion of determinism may look too strong. Indeed, it assumes that, from a given state i, one cannot reach two states u and v that share common sets of valuations. The assumption is made independently of the distributions used to reach the two states, i.e., it may be the case that there exists no distribution in where both u and v can be reached simultaneously. A natural way to solve the problem would be to consider a weaker version of determinism. More precisely, we say that a CMC S = {1, . . . , k}, o, ϕ, A, V } is weakly deterministic if whenever there exists x ∈ [0, 1] k and states i, u, v such that ϕ(i)(x) and x u > 0 and x v > 0, we have

V (u) ∩ V (v) = ∅.
This version of determinism is weaker than the one given in Definition 16. Indeed, only states that can be reached by the same distribution should have disjoint sets of valuations. Though this notion seems reasonable, one can show (see [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF] for a proof) that there exist two weakly deterministic CMCs S c and S d such that S c thoroughly but not weakly refines S d . Hence working with this weaker, but natural, version of determinism does not close the gap between weak and thorough refinements.

VI. POLYNOMIAL CMCS

It is not surprising that CMCs are closed under both logical and structural compositions. Indeed, CMCs do not make any assumptions on constraint functions. There are however many classes of constraints that are practically intractable. While this paper is mainly concerned with the development of the theoretical foundations for CMCs, we now briefly study classes of CMCs for which operations on constraints required by our algorithms can be managed quite efficiently.

A first candidate could be linear constraints, which is the obvious generalization of interval constraints. Unfortunately, linear constraints CMCs are not closed under structural composition. Indeed, as we have seen in Section IV the composition of two linear constraints leads to a polynomial constraint. However, what is more interesting is that polynomial constraints are closed under both logical and structural composition and that these operations do not increase the quantifier alternations since they only introduce existential quantifiers. Hence, one can claim that CMCs with polynomial constraints and only existential quantifiers are certainly the smallest extension of IMCs closed under all operations.

From the algorithmic point of view, working with polynomial constraints should not be seen as an obstacle. First, we observe that algorithms for logical and structural composition do not require any complex operations on polynomials. The refinements algorithms (presented in [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF]) are polynomial in the number of states, and each iteration requires a quantifier elimination. This procedure is known to be double exponential in general, but there exist efficient single exponential algorithms [START_REF] Brown | Simple CAD construction and its applications[END_REF], [START_REF] Brown | The complexity of quantifier elimination and cylindrical algeraic decomposition[END_REF] when quantifier alternations are fixed. Those algorithms are implemented in Maple [START_REF] Yanami | SyNRAC: a Maple toolbox for solving real algebraic constraints[END_REF]. The pruning operation is polynomial in the number of states, but each iteration also requires an exponential treatment as one has to decide whether the constraints have at least a solution. Again, such problem can be solved with efficient algorithms. Finally, determinizing a CMC can be performed with a procedure that is similar to the determinization procedure for finite-state automata. Such a procedure is naturally exponential in the number of states.

VII. DISCUSSION OF REFINEMENT AND COMPOSITION

CMCs are a newcomer in a long series of probabilistic modeling languages and abstractions for them. Throughout the paper we have indicated that many of our results directly translate to simpler abstractions, like IMCs. We shall now further discuss this foundational aspect of CMCs, showing how they subsume a few established notions of refinement and composition for probabilistic automata (and for process algebra based on them).

Below we write Dist(S) for the set of all probability distributions over a finite set S. Given two sets S and T and a probability distribution α ∈ Dist(S × T ), we denote the marginal distribution over S as α s,T = ∑ t∈T α s,t , and similarly for T . We say that ϕ is a non-deterministic distribution constraint over set I if all solutions x of ϕ are point distributions; so ∃i.

x i = 1. Write [ i S ]
to denote a particular point distribution for which [ i S ] i = 1. Notice that non-deterministic distribution constraints model a nondeterministic choice of an element from S. They will be used to encode non-determinism in CMCs.

A probabilistic automaton (PA for short) [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF] is a tuple S = (S, Act, →, s 1 ), where S is a finite set of states, →⊆ S × Act × Dist(S) is a finite transition relation and s 1 ∈ S is the initial state. The derived combined transition relation of S is given by -→c ∈ S × Act × Dist(S). If π ∈ Dist(S) and ∈ Dist(T ) then π⊗ denotes the unique independent product distribution such that (π⊗ ) s,t = π s • t .

We say that t a -→c iff is a convex linear combination of vectors from = { i | t a -→ i }, so = ×λ, where λ is a distribution vector λ ∈ [0, 1] | | . We interpret as a matrix, where ith column is a distribution i .

Consider two PA S = (S, Act, → S , s 0 ) and T = (T, Act, → T , t 0 ). For a binary relation R ⊆ S × T we define a derived relation R * ⊆ Dist(S) × Dist(T ) such that πR * iff there exists a distribution α ∈ Dist(S × T ) and (1) α q,T = π q for all q ∈ S, (2) α S,r = r for all r ∈ T and (3) α s,t = 0 implies sRt. Definition 20 (Simulation [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]). A relation R ⊆ S × T is a simulation iff (s, t) ∈ R implies that whenever s a -→π for a distribution π, then t a -→ for distribution such that πR * . R is a probabilistic simulation iff (s, t) ∈ R implies that if s a -→π then t a -→c for some distribution , and πR * .

Let A ⊆ Act be the subset of actions on which S and T should synchronize. The parallel composition of S and T is a PA S T = (S × T, Act, →, (s 0 , t 0 )), where → is the largest transition relation such that (s, t) a -→π ⊗ if:

a ∈ A and s a -→ S π and t a -→ T , or a / ∈ A and s a -→ S π and = [ t T ], or a / ∈ A and π = [ s S ] and t a -→ T .

We now propose a linear encoding of PAs into CMCs, which reduces simulation and composition of PAs to refinement and composition of CMCs (see Fig. 6). Let S = ({s 1 , . . . , s k }, Act, →, s 0 ) be a PA. And let l be the number of reachable action-distribution pairs, so Ω S = {(a 1 , π 1 ), . . . , (a l , π l )} = {(a, π) | ∃s ∈ S. s a -→π}. The corresponding CMC is S = ({1, . . . , 2k+l}, 1, ϕ, Act∪⊥, V }) , where ⊥ / ∈ Act. S has three kinds of states. Type-1 states, 1 . . . k, correspond directly to states of S. Distributions leaving these states model a non-deterministic choice. Type-2 states, k + 1, . . . , 2k, model a possibility that a component remains idle in a state. Type-3 states, 2k+1, . . . , 2k+l model the actual distributions of S.

V assigns value {∅} to type-1 states and value {{⊥}} to type-2 states. For type-3:

V (2k + i ) = {{a i }} for 1 ≤ i ≤ l.
The distribution constraints are as follows:

ϕ(i)(x) if i is type-1 and x = [ k+i 1..2k+l ] or s i a i ---→πi ∧ x = [ 2k+i 1..2k+l ] for 1 ≤ i ≤ l. ϕ(k + i)(x) if k+ i is type-2 and x = [ i 1..2k+l ]. ϕ(2k + i )(x) if 2k + i is type-3 and x = π i
We can now relate simulation of PA to refinement of CMCs: Theorem 21. T simulates S iff S strongly refines T.

Another, very similar, but slightly more complicated, encoding exists, for which weak refinement coincides with probabilistic simulation. See [START_REF] Caillaud | Compositional Design Methodology with Constraint Markov Chains[END_REF] for details.

The same encoding is used to characterize parallel composition of PAs using parallel composition of CMCs. Expression S[ a 1/a 1 ; . . . ; a n/a n ] a1,...,an∈Act denotes a substitution, substituting a primed version of name a i for each occurrence in a i , for all actions in Act.

Interestingly, the precongruence property for the parallel composition of PAs is obtained for free as a corollary of the above two reduction theorems and Thm. 13. Similarly, we obtain precongruence with probabilistic simulation using a suitable encoding-a good example how CMCs can be used to study properties of simpler languages in a generic way.

VIII. RELATED WORK AND CONCLUDING REMARKS

We have presented CMCs-a new model for representing a possibly infinite family of MCs. Unlike the previous attempts [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], [START_REF] Fecher | Don't Know in probabilistic systems[END_REF], our model is closed under many design operations, including composition and conjunction. We have studied these operations as well as several classical compositional reasoning properties, showing that, among others, the CMC specification theory is equipped with a complete refinement relation (for deterministic specifications), which naturally interacts with parallel composition, synchronization and conjunction. We have also demonstrated how our framework can be used to obtain properties for less expressive languages, by using reductions.

Two recent contributions [START_REF] Fecher | Don't Know in probabilistic systems[END_REF], [START_REF] Katoen | Compositional abstraction for stochastic systems[END_REF] are related to our work. Fecher et al. [START_REF] Fecher | Don't Know in probabilistic systems[END_REF] propose a model checking procedure for PCTL [START_REF] Ciesinski | On probabilistic computation tree logic[END_REF] and Interval Markov Chains (other procedures recently appear in [START_REF] Chatterjee | Model-checking omegaregular properties of interval Markov chains[END_REF], [START_REF] Haddad | Using stochastic comparison for efficient model checking of uncertain Markov chains[END_REF]), which is based on weak refinement. However, our objective is not to use CMCs within a model checking procedure for probabilistic systems, but rather as a specification theory.

Very recently Katoen and coauthors [START_REF] Katoen | Compositional abstraction for stochastic systems[END_REF] have extended Fecher's work to Interactive Markov Chains, a model for performance evaluation [START_REF] Hermanns | Process algebra for performance evaluation[END_REF], [START_REF] Hillston | A Compositional Approach to Performance Modelling[END_REF]. Their abstraction uses the continuous time version of IMCs [START_REF] Katoen | Three-valued abstraction for continuous-time Markov chains[END_REF] augmented with may and must transitions, very much in the spirit of [START_REF] Larsen | Modal specifications[END_REF]. Parallel composition is defined and studied for this abstraction, however conjunction has been studied neither in [START_REF] Fecher | Don't Know in probabilistic systems[END_REF] nor in [START_REF] Katoen | Compositional abstraction for stochastic systems[END_REF].

Over the years process algebraic frameworks have been proposed for describing and analyzing probabilistic systems based on Markov Chains (MCs) and Markov Decision Processes [START_REF] Hermans | Interactive Markov Chains[END_REF], [START_REF] Andova | Process algebra with probabilistic choice[END_REF], [START_REF] López | An overview of probabilistic process algebras and their equivalences[END_REF]. Also a variety of probabilistic logics have been developed for expressing properties of such systems, e.g., PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF]. Both traditions support refinement between specifications using various notions of probabilistic simulation [START_REF] Fecher | Don't Know in probabilistic systems[END_REF], [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] and, respectively, logical entailment [START_REF] Hermanns | Probabilistic CEGAR[END_REF]. Whereas the process algebraic approach favors structural composition (parallel composition), the logical approach favors logical composition (conjunction). Neither of the two supports both structural and logical composition.

As a future work, it would be of interest to design, implement and evaluate efficient algorithms for procedures outlined in this paper. We will also study the decidability of the set inclusion problem. We would also like to define a quotient relation for CMCs, presumably building on results presented in [START_REF] Larsen | Compositional verification of probabilistic processes[END_REF]. The quotienting operation is of particular importance for component reuse. One could also investigate applicability of our approach in model checking procedures, in the same style as Fecher and coauthors have used IMCs for model checking PCTL [START_REF] Fecher | Don't Know in probabilistic systems[END_REF]. Finally, it would be interesting to extend our composition operation by considering products of dependent probability distributions in the spirit of [START_REF] De Alfaro | Compositional methods for probabilistic systems[END_REF].

P 2 satisfying S 1 and S 2 Fig. 2 :

 222 Fig. 2: Two specifications (CMCs) and two implementations (MCs) of an optic relay

  Correspondence for initial states of P 2 and S 1 Weak refinement for initial states of S 3 and S 4

Proposition 8 .

 8 There exist CMCs S a , S b , S c and S d such that • S a weakly refines S b , and S a does not strongly refine S b ; • [[S c ]] ⊆ [[S d ]], and S c does not weakly refine S d .

Fig. 4 :

 4 Fig. 4: Parallel composition and synchronization of CMCs

Fig. 6 :

 6 Fig. 6: Reducing a PA to CMC. There π denotes a distribution constraint, which has a unique solution π.

Theorem 22 .

 22 For two PAs S and T over the same set of actions Act and a set of synchronizing actions A ⊆ Act we have that S T is isomorphic to (( S T[ a /a] a∈Act ) ∧ S A ) [ a /(a,a ); a /(a,⊥ ); a /(⊥,a )] a∈Act where S A is a synchronizer over Act ⊥ × Act ⊥ defined by (∀a ∈ A. a ⇐⇒ a ) ∧ (∀a / ∈ A. (a =⇒ ⊥ ) ∧ (a =⇒ ⊥))

  Definition 1 (Markov Chain). P = {1, . . . , n}, o, M, A, V is a Markov Chain if {1, . . . , n} is a set of states containing the initial state o, A is a set of atomic propositions, V : {1, . . . , n} → 2 A is a state valuation, and M ∈ [0, 1]

	a probability transition matrix:	n×n is j=1 M ij = 1 for i = 1, . . . , n. ∑ n
	We now introduce Constraint Markov Chains (CMCs for
	short), a finite representation for a possibly infinite set of MCs.
	Roughly speaking, CMCs generalize MCs in that, instead of
	specifying a concrete transition matrix, they only constrain
	probability values in the matrix. Constraints are modelled
	using a characteristic function, which for a given source state
	and a distribution of probabilities of leaving the state evaluates
	to 1 iff the distribution is permitted by the specification.
	Similarly, instead of a concrete valuation function for each
	state, a constraint on valuations is used. Here, a valuation is
	permitted iff it is contained in the set of admissible valuations
	of the specification.
	Definition 2 (Constraint Markov Chain). A Constraint Markov
	Chain is a tuple S = {1, . . . , k}, o, ϕ, A, V , where
	{1, . . . , k} is a set of states containing the initial state o, A
	is a set of atomic propositions, V : {1, . . . , k} → 2 2 A	is a set
	of admissible state valuations and ϕ : {1

  Theorem 14. Let S 1 , S 2 and S 3 be three CMCs with pairwise disjoint sets of propositions A 1 , A 2 and A 3 . Let Sync 123 be a synchronizer over A 1 ∪ A 2 ∪ A 3 and let Sync 12 be the same synchronizer with its set of propositions restricted to A 1 ∪ A 2 . The following holds [[[((S 1 S 2 )∧Sync 12 ) S 3 ]∧Sync 123

ACKNOWLEDGEMENTS

This work was supported by the European STREP-COMBEST project no. 215543, by VKR Centre of Excellence MT-LAB, and by an "Action de Recherche Collaborative" ARC (TP)I.


Temitayo A Ewemoje
email: ta.ewemoje@mail.ui.edu.ng

Potentials and projections of freshwater resources in Sub-Saharan Africa; focus on Nigeria

Keywords: Freshwater, Resources, Sustainable development, Developing Countries

This paper discusses the abundance of freshwater availability in Nigeria which is approximately 0.51% of world freshwater resources. It further highlights the projected freshwater crises in Nigeria and Africa as a whole. Based on analyzed country data retrieved from International Organizations, Nigeria and in fact many developing countries in Sub Saharan Africa is presently termed water secure based on total Actual Renewable Water Resources, but projections into the nearest future (2025) classify Nigeria as water stress/scarce due to lack of economic, financial and skilled human resources to tap water for basic human needs, food production and maintenance of freshwater ecosystem. Causes of this projected impending danger were attributed to increase in freshwater quantity supply made available through unsustainable water resources development and inappropriate water management programmes.

INTRODUCTION

One question most projections of world resources leave open is the degree to which the level of population is resource-determined. The most basic of all resources, although often taken for granted is water. Unlike carbon reduction, there is no global water alternative to neither promote nor negotiate. Turning off your tap in Europe will not mitigate the drought in Africa. Water is local, but water issues are of importance in the world's major water basins. The poorest of the world continents in terms of annual freshwater renewal is Africa [START_REF] Falkenmark | Rapid Population Growth and Water Scarcity: The Predicament of Tomorrow's Africa[END_REF].

Globally this environmental resource -water, suffer from irreversible degradation leading to scarcity due to the fact that only 0.3% of the 1.385 billion m 3 of water on the earth are available for human activities (Water Department, 2006). Water, the "blood of the biosphere" according to [START_REF] Iwmi | Water Figures; Turning Research into Development[END_REF] is grabbing the world's attention these days. Against a backdrop of growing water scarcity, it is no wonder that the profile of global water development is rapidly rising. Water scarcity is both a national and a regional problem for many Sub Saharan countries; water resources are generally recognized as unevenly distributed. Until now, most activities have been geared towards storing water at the local level, for instance, for irrigation, urban supplies, and hydro power, with no consideration for neighbouring countries. As [START_REF] Samson | International freshwater conflict: issues and prevention strategies[END_REF] noted, the chance of finding new water sources is small in most regions of the world. Hence without new supplies, there should be increase in the efficiency of urban water use and improvement in the conservation of available water resources.

As the global population grows and the economies of countries expand, the world is going to get hungrier and thirstier. Agriculture uses up to 70% of the world's freshwater and to make basic

MATERIAL & METHODS

The conceptual framework of the analysis of potentials and projections of freshwater resources in Sub Saharan Africa (SSA) is based on the International Water Management Institute (IWMI) methodology of assessing the performance of water resources systems. This methodology is reported in various previous studies of IWMI research reports and working papers; notable of mentioning is the works of Seckler et al ( 1998) and Sakthivadivel et al (2001).

The first part of this paper focuses on the potentials of freshwater resources in Africa and narrowing it down to a focus on Nigeria; viz a viz the freshwater availability and withdrawals. The latter part highlights the projections of this availability and withdrawals in the next few years. The data used in this work are data obtained primarily from four different sources which are the Food and Agriculture Organization of the United Nations (FAO), Population Division of the Department of Economic and Social Affairs of the United Nations Secretariat, and IWMI.

The choice of these organizations stems from the fact that data on water quality at a global level are scarce; there are few sustained programs to monitor water quality worldwide. Information is usually limited to industrial countries or small, localized areas. For regions such as Europe, where some monitoring is taking place, differences in measures and approaches make the data hard to compare (World Resources, 2000). Similarly in Africa, water quantity statistics are poor on water use, water availability, and irrigated area on a global scale. Estimates are frequently based on a combination of modeled and observed data.

RESULTS AND DISCUSSION

The Potentials

Freshwater availability which is also referred to as Internal Renewable Water Resources (IRWS) is 214×10 9 m 3 per year while total IRWS is 221x10 9 m 3 per year for Nigeria. The IRWS is an indication to the fact that there is an appreciable average annual flow in the rivers within the country and also recharge of groundwater from precipitation within Nigeria's borders is quite enormous.

Freshwater Crisis and Projections

While Africa uses only about 4 per cent of its renewable freshwater resources (WRI, 2005), water is becoming one of the most critical natural resource issues. The continent is one of the two regions in the world facing serious water shortages (Johns [START_REF] Hopkins | Solutions for a Water-Short World[END_REF]. Although it has abundant freshwater resources, there are great disparities in water availability and use within and between African countries because the water resources are so unevenly distributed. Only three Sub-Saharan countries, Guinea, Democratic Republic of Congo and Angola, have untapped water resources. In all other countries, water scarcity is inevitable within the first quarter of the 21st century [START_REF] Kakonge | Water Scarcity and related Environmental Problems in Parts of Sub-Environmental health References[END_REF]. Other contributing factors are the inadequate assessment and underdevelopment of water resources, the lack of technical and institutional infrastructure as well as the lack of investment in water resource development. While the Sahelian countries have limited supplies of freshwater, most countries in the humid tropical zone have abundant water. The availability of water varies considerably, even within countries, and the situation is further complicated by frequent droughts as well as inappropriate water management programme. The demand for water is increasing rapidly in most countries due to population growth and economic development. Projected freshwater resources are shown in figure 1. In view of the increasing demand for water, [START_REF] Molden | Water for Rural Development: Background Paper on Water for Rural Development Prepared for the World Bank[END_REF] projected that municipal (urban) sector withdrawals will be greater than those for domestic sector in most developing countries, and this municipal withdrawals are projected to double over the next 30 years.

Increases in demand for freshwater are anticipated in all African countries, in all sectors (domestic, agricultural and municipal), over the next 10 years. In West Africa countries, demand is projected to double within the next 30 years (Figure 2). This projected double in withdrawals and demand arises not just from an increase in the number of people requiring water, but also from increasing consumption patterns such as the growth of water hyacinth which is adversely affecting many water bodies in Nigeria. This weed affects fishing, disrupts water-borne international trade and the movement of people, and blocked water intakes thus endangering hydroelectric installations (figure 3). The infestation of this water weed (hyacinth) has necessitated the call on neighbouring West African countries which share surface water resources to jointly tackle the eradication of this water weed which is already affecting socioeconomic activities of these neighbouring countries. Likewise, industries rarely pay the true price of water and are, therefore, not encouraged to recycle or to reduce their consumption. The lack of improved sanitation is the most important feature of slums in the African urban context. About 57 per cent of urban Africans do not have access to improved forms of sanitation.

The lack of improved water supply appears to be the second most important determining factor, affecting about one fifth of urban Africa. Lack of sufficient living space or overcrowding is the third most important factor, widely varying from one country to another (UN-HABITAT, 2004).

Pollution of these waters is a cause of many public health problems. Polluted urban surface water often leads to water-borne diseases, such as cholera, typhoid and schistosomiasis as a result of human activities in dirty water (Figure 4). A case of the urban Ogunpa river channelization project in Ibadan Nigeria shows one of the many inappropriate urban water management practices in Nigeria as a result of refuse dumping and other forms of pollution thereby degrading the ecosystem (Figure 5). Up till now, no measures have been put in place to curb this pollution menace in this locality. , 2004). With a population of about 130 million and a cultivable/habitable area of 330,000Km 2 which is about 35.7% of the total area of Nigeria, this increased population pressure puts a heavy strain on the available water resources of the country. Nigeria is termed one of the most densely populated countries in Africa (figure 6).

Only three sub-Saharan countries, Guinea, Democratic Republic of Congo and Angola, have untapped water resources. In all other countries, water scarcity is inevitable within the first quarter of the 21st century. According to [START_REF] Kakonge | Water Scarcity and related Environmental Problems in Parts of Sub-Environmental health References[END_REF], the populations of Kenya, Burundi, Rwanda and Malawi are expected to double by 2025 and by then per capita water availability will have fallen below the accepted standard (see Figures 6 and7). South Africa will have a projected population of 68 million in 2025 and a projected per capita water availability of 725m³.

For its water resources, most freshwater in Nigeria comes from abundant seasonal rainfalls and relatively low levels of withdrawals of water for its three major uses, namely, agriculture, community water supply and industry. Demand for water in West Africa has been steadily increasing as a result of population growth, commercial agricultural expansion, and industrial development. Current total withdrawal of water for domestic, industrial and agricultural consumption is 11Km 3 /yr, and demand for water from all sectors is expected to increase to some 36Km 3 /yr by 2025 (Figure 8). This figure indicated an increase in projected water withdrawal and consumption all over Africa; however this increase did not match the percentage of water withdrawal and consumption in relation to renewable water resources. Hence, this necessitates the putting in place in Nigeria appropriate water management programme through sustainable development of this vital resource.

8th

  Figure 1: Freshwater Resources in Africa. Source: AWDR (2006).

Figure 2 :

 2 Figure 2: Water Use by Sector in West Africa Source: UNEP, 2008.

Figure 3 :

 3 Figure 3: Water Hyacinth Infested Reservoir in Ibadan, Nigeria

Figure 4 :Figure 5 :

 45 Figure 4: Human Activities on Polluted Urban Water

  things for development takes volumes of water[START_REF] Iwmi | Water Figures; Turning Research into Development[END_REF]. Africa has the highest rate of population growth in the world, and is also one of the regions that are most vulnerable to climate change. Problems with freshwater availability in Africa are further complicated by highly variable levels of rainfall. As a result, large numbers of people are dependent on groundwater as their primary source of freshwater(UNEP, 2008).

	8th World Wide Workshop for Young Environmental Scientists WWW-YES 2009: Urban waters: resource
	or risks? (2-5 June 2009)
	Surface and groundwater supplies have been
	exploited, and some countries have turned to alternative sources of water such as desalinization
	of sea water and recycling of wastewater, in order to attempt to meet this increasing demand.
	Approximately 38 per cent of the population of West Africa lives in urban areas. Thirty years
	ago, only one Western African city (Lagos) had a population of more than a million. By 2000,
	cities with populations exceeding one million included Ouagadougou (Burkina Faso), Abidjan
	(Côte d'Ivoire), Accra (Ghana), Conakry (Guinea), Bamako (Mali), Ibadan (Nigeria), Lagos
	(Nigeria), and Dakar (Senegal). Lagos, the largest city in Africa and the 6th largest in the world,
	has an estimated current population of 13.4 million people and this is expected to grow to over
	23 million by 2015 (UNEP, 2008).
	2 / 9

Table 1 : Water Resources Potentials of Selected Countries

 1 ARWS) is 286.2×10 9 m 3 per year while total ARWS per inhabitant in the country is 2251m 3 per year according toFAO (2006). IRWS for Nigeria is approximately 5.61% and 0.51% of the SSA and world freshwater resources respectively. Total ARWS in Nigeria is approximately 5.23% of SSA while total ARWS per capita cubic meters per person in Nigeria is approximately 35.62%. This water abundance in some selected countries is depicted in Table1. In Nigeria, a value of 1982m 3 /capita/year was reached according to African Water Development Report[START_REF] Awdr | National Reports[END_REF], while FAO (2005) value was 2252m 3 /capita/year, depicting a water sufficient nation.

		Area,		Water Resources, Km 3 /year		Annual
	Countries	10 3 Km 2	Local Max Min	Average	Imported	Total	Runoff Layer, mm
	Gabon	268	272	133 205	15.6	221	765
	Gambia	11	5.69	1.24 3.97	6.7	10.7	361
	Niger	1267	5.4	0.28 2.33	32.1	34.4	18
	Nigeria	924	437	148 275	43.7	319	293
	Senegal	196	31.1	6.31 21.4	14.9	36.3	109
	Sudan	2505	65.3	9.74 34.6	132	167	53
	Congo
	Dem. Rep 2345	1328 786 989	313	1300 133
						Source: Shiklomanov (2002)

As a rough global indicator of water sufficiency if the annual amount of water available per capita is less than 1000m 3 /capita/yr, water scarcity occurs (United Nations Economic Commission for Africa (UNECA), 2001). The total Actual Renewable Water Resources (

/ 9

Low values of internal renewable resources in 2025 also shows that there is room for improvement in conservation of rainwater which has been attributed to the abundance of freshwater resources in Nigeria, the lack of these conservation measures accounts in part, for endemic drought in many parts of Nigeria.

Hence, efforts should be geared in Nigeria towards meeting basic human and ecosystem needs through proper government policies that will guarantee access to water. Water should be recognized as an economic good, which was one of the cornerstones of the Dublin and Rio statements [START_REF] Lundqvist | Comprehensive Assessment of the Freshwater Resources of the World; Sustaining our Waters into the 21st Century[END_REF]. Planners and users should recognise the true value of water in all its competing uses and functions. Water users must assume a larger responsibility in recovering the full cost of providing water-related services, including development, provision, maintenance and treatment costs. This will help reduce the ever increasing freshwater quantity demand and hence limit the withdrawal of unsustainable water resources in Nigeria.

The government in Nigeria should foster the principle that water planning and decision-making should involve affected parties and interests in a democratic manner thereby ensuring participatory approach which means that decisions are taken at the lowest appropriate level, with full public consultation and involvement of users.


Marcos W Medina
email: mmedina@deusto.es

The cooperativism and the management of the water in average cities in Argentina. The sample of de City of Obera

Keywords: Management, developing countries, politics, Obera, Argentina

The cooperativism and the management of the water in average cities in Argentina. The sample of de City of Obera

Marcos W. Medina

INTRODUCTION

This research outlines the cooperative management of drinking water and sanity in the city of Oberá in Misiones (Argentina). At the beginning we will refer to the public policies background, the recommendations of international organizations on drinking water and cooperativism on drinking water in Argentina.

Secondly, after considering the methodology applied in this case, we will analyse the importance of this management modality in medium-sized cities in Argentina and the particular features of Cooperativa Eléctrica Limitada Oberá (Oberá Electric Limited Cooperative -CELO). Finally, we will mention the most important aspects of this experience.

The area of water and sanity in Argentina is characterised by the diversity of service organizations methods. Some of the suppliers are public and others are private companies. This is the result of three different public policies applied in the last 30 years. The eighties was characterised by service decentralization. The nineties was marked by privatization processes. Over the last years, there has been a tendency to return to the public sector. The changing government policies in Argentina have given rise to different situations in the cities.

One of the most important reasons for this confusing situation was the double message from the international system in the nineties; on one hand, the promotion of privatization of drinking water and sanity services proposed by multilateral credit organizations and, on the other hand the recommendations from chapter 18 -Agenda 21. Argentina was one of the first governments to transfer the provision of services to the private sector. The drinking water and sanity service concession in Buenos Aires was seen as the best example of this new tendency in the international scene.

The second reason to be considered is the recommendations about drinking water from chapter 18 -Agenda 21. We highlight the following: "Community management of services, backed by measures to strengthen local institutions in implementing and sustaining water and sanitation programs". The document is even more categorical in the statement: "one realistic strategy to meet present and future needs, therefore, is to develop lower costs but adequate services that can be implemented and sustained at the community level".

The recommendations from Agenda 21 were not applied in Argentina as a public policy. However, more than 670 cooperative organizations existing in the country carry out the community management of water service and most of them existed prior to the privatization process.

The cooperative management has been proposed at a theoretical level as an alternative to privatization (Petrella,2002) as a solution facing the market failure in England (Bilchard,2002 ;Morse,2000 ;Bakker,2003 ). A few empirical studies exist about cooperativism of public services except the ones about drinking water service in Santa Cruz de la Sierra, Bolivia [START_REF] Nickson | The public-private mix in urban water supply[END_REF], the systems in Finland (Katko,2000), the cooperative experiences in the city of Córdoba, Argentina (Zilocchi,1998) or the performance analysis of water cooperatives in Misiones, Argentina [START_REF] Wysocki | Las organizaciones cooperativas de provisión de servicios de agua potable y cloaca de la Provincia de Misiones frente a las reformas del sector de saneamiento introducidas por la ley N° 3.391 'Marco Regulatorio[END_REF].

Nickson points out the dual position sustained by international credit organizations: on one hand they grant loans to governments to improve infrastructures. On the other hand, they ignore the cooperative formula when recommending important transformations for the area. In only 2002, some references to the system appeared in the documents from the World Bank (Solo,2003) and a little deeper analysis focused on the experience in Saguapac (Santa Cruz de la Sierra, Bolivia) in 2006 (Ruiz-Mier & van Ginneken,2006).

Cooperative provision of services like drinking water, urban sanity, communications, electricity, gas and other public services is not spread enough in other countries. The origin of public services cooperativism in Argentina is due to the lack of efficiency in the electricity service provision by private companies in the twenties (Cracogna,1992).

In Argentina, these cooperatives are associations integrated by partners whose main targets are management, own interests defense and promotion of the area. One of the most important characteristics of the Argentinian system is that these partners are, at the same time, producers and consumers from the drinking water service. It means that consumers become suppliers of their own services, leaving out a third party, whether it is the government or a private company.

The cooperative way ensures the active participation because all decisions -strategic, operative, financial or any other -should start and finish within associated consumers. These characteristics produce two fundamental strengths (Wysocki,2002). First, the owners experience a deep sense of belonging to the institution as they are both consumers and partners.

Second, an important characteristic of self-management is that the consumers-partners, through the Administration Council, actively participate in the decision making process about prices, staffing and other conditions for service provision.

The cooperativism and the management of the water in average cities in Argentina. The sample of de City of Obera -Marcos MEDINA

/ 8

Due to the close relationship with their associated consumers, cooperatives develop strong bonds with the community where they carry out their activities. They are important and active agents in the economic, social and cultural development of the area. Frediani (1986) points out the following advantages of cooperative management of public services:

The service is managed by the customers; consequently its quality is better than the one provided by a depersonalized public entity. The behaviour of these entities is generally based on bureaucratic and centralized guidelines.

The cooperative public services costs and tariff are relatively lower because the structural costs are lower.

The cooperative company is more socially sensitive. As a commitment, it tries to extend the provision to the outlying areas of the city and also provides other social and cultural services to its members.

There is a better income distribution considering that the surplus at the end of the financial period is shared out among the associated partners. If anyone of them decides to get retired, his initial contribution and profits are refunded.

Cooperatives are democratically managed (one member -one vote system). As a result the company is closer to the community.

In the case of public services cooperatives, the citizen is not seen as an anonymous customer but as an associated member of the supplying company.

Cooperatives, as small and medium companies, contribute to create a more socially and economically democratic structure.

In spite of all the mentioned advantages, in Argentina there is a lack of consumer participation in the cooperative system (Callejo,2002). It is limited to the possibility of voting for or being elected as a district delegate. Only the elected candidates are responsible for the company decisions without considering the mandate derived from the associated customers. Common partners do not have the chance to debate about the running of the company.

It has also been pointed out a deficiency in management like the lack of a quality management policy, a human resource policy and a task programming. In regard to the lack of a quality management policy, there are a high level of informality in the procedural norms publication, a lack of services records and a partial control of drinking water quality. The human resource policy lacks of continuing training schedule, a lack of productivity incentive programme and overstaffing (Wysosky op.cit.).

A first point of analysis is related to the cooperative model importance in medium-sized cities in Argentina because drinking water community management is usually associated to small urban areas.

Then we will refer to the experience in Oberá (Province of Misiones -Argentina).

MATERIAL & METHODS

This research was based on a case study methodology and employed both qualitative and quantitative primary data. Qualitative data covering a range of issues including the contractual framework, utilities management, and financial issues were obtained through in-depth interviews with representatives of Cooperative board, present and former managers.

An audit procedure carried out by the researcher yielded primary data on infrastructure design and operation. Secondary data were obtained from documentation provided by Instituto Nacional de Estadísticas y Censo (INDEC) , Ente Nacional de Obras Hídricas de Saneamiento (ENOHSA) and the Cooperative Annual Reports (annual reports and Balances), rules and regulatory framework.

RESULTS AND DISCUSSION

We have identified the urban areas that can be compared with Oberá city with the purpose of determining the cooperative model importance in medium-sized cities in Argentina. The selection criteria have been as following:

o Over 50.000 inhabitants cities o Under 1.000.000 inhabitants cities o Capital cities were excluded.

In the following table we can see the relation among the different institutional management models, number of cities in which they operate and number of suppliers. ). This entity also distributes electricity and gas cylinders, and provides health assistance, communication (telephones and Internet), public television system and burial services.

Until May 1979 Oberá did not have drinking water provision and until September 1993 integrated sanity services. Before that, the community used rainwater stored in private wells or water from well drillings. There were serious limitations in frequency and volume in water delivery to the neighbours by the Town Council. The sanity system was precarious, and it consisted in septic tanks flowing to cesspits (drilling holes).

In May 1979, the drinking water system concession was precariously granted to CELO for running and maintenance. In November 1982, the definitive concession contract was signed.

CELO was one of the first suppliers in the country with domiciliary water meter for an equitative water bill payment. It was also a pioneer in the addition of fluorine to water since 1983.

A very important investment was done in order to improve the service provision by modifying and extending connections and building new infrastructure. It was supported by cooperative resources.

In combination with this, the solidarity principles of cooperativism allow the access to the provision of water to new members who pay reasonable instalments to cover the net extension costs.

Concerning to sanity, building works started in 1990 supported by the Inter-American Development Bank. They included domiciliary net plumbing and a sewage treatment plant (activated sludge) prepared for 10.000 connections with the possibility to be enlarged to cover the whole community.

23 net extensions have been done by CELO since the beginning of the sewer system. This building works were carried out at the request of the interested parties and executed by the Company staff.

As a consequence of a new concession contract, CELO got the necessary resources to perform the drillings to get water from the Acuífero Guaraní. The 1300-metre borehole will allow CELO to solve supply and other sources shortage problems. CELO is made up by 23.822 partners, 15 electoral districts, 161 district delegates, a Delegates General Assembly, and an Administrative Council. The authorised partners (those with updated fees) have the right to vote and choose their district delegates once a year. These delegates choose the Administrative Council members and 2 trustees, and state the cooperative guidelines. The Council has 9 permanent members (for 3 years) and 3 substitutes (for 1 year). The Administrative Council meets once a week. It also designates a general manager for an undetermined period. The board is also constituted by an administrative manager, a technical manager, drinking water assistant manager and a sanity official.

We can state, according to the three classical evaluation variables from the customers' point of view, this Cooperative satisfactorily qualifies in two of them: water quality and adequate pressure for the distribution. However, there is a remarkable supply deficiency due to provision cuts off and water leaks in the streets what make the service irregular.

According to efficiency indicators, CELO presents following characteristics:

Bills collectability is higher than 85%. The Cooperative has a metering system for billing purposes and also a step tariff chart in accordance with the volume of consumed water. Technical losses cannot be calculated because the company does not control the volume of water produced. The company has a poor quality management as the cooperative lacks not only a function manual but also complaint forms.

The relation between number of workers and number of connections is optimum. The service scale is 3.2 workers (including operators and administrative officers) every 1000 connections. However, the company does not have a clear staffing policy.

CELO has been involved in many activities related to the Community development. Among them, the company builds the community awareness of water as a fundamental resource, environment conservation and the streams preservation, considered as a source of clean water. These activities are carried out in all the educational levels through speeches and environmental awareness campaigns promoted by schools.

Apart from providing the drinking water and sanity service, the company offers other services nowadays such as: electricity, gas cylinders, health assistance, communication (telephones and Internet), public television system and burial services.

CELO has a great sense of social responsibility. During 2001-2002 crises, it provides an emergency soup kitchen to those in need of food in the city. There is also a good relationship between the Cooperative and the Town Council. The Cooperative gives the Town Council 10.000 m3 of drinking water in exchange for municipal taxes. This water is used to cover the Town Hall's needs and to supply population in need.

The system shows some dysfunctions:

The regulatory framework for the Provincial law 3391 has introduced an external regulating entity, which modifies the partner-company relation. Since this new legal regulation, the tariff schedule is no longer freely determined by the Cooperative Administrative Council. Furthermore, this new rule made the payment demanding and service cut off systems more bureaucratic. All this promote many customers to fall into arrears.

There is a low level of participation in the voting process. As a consequence, the Administrative Council members are not renewed as they should be.

The cooperativism and the management of the water in average cities in Argentina. The sample of de City of Obera -Marcos MEDINA 7 / 8

In addition to this, the Administrative Council meddles in excess in management tasks.

This can be beneficial if we consider the management level control exercised by the associated partners but, on the other hand it hinders management technical tasks.

CONCLUSIONS

This research study shows not only the drinking water cooperative management feasibility but also its relevance both in small urban areas and medium-sized cities.

The cooperative model has a number of potential advantages over private and public utility models. All utility cooperatives are characterized by the facts that owners and customers are the same and that cooperatives do not have a profit objective. All utility cooperatives have a board; a system of oversight, and the one member-one vote election system.

The ownership model and governance structure can result in a clear objective for the utility: provide sustainable service at affordable cost. The fact that any cost reductions are translated into lower tariffs constitutes a strong incentive to pursue efficiency. Other advantages are the flexibility associated with the absence of cumbersome procedures, and a strong customer orientation derived from the alignment of objectives.

In the case of the city of Oberá, this system allows a drinking water and sanity service selffinancing extension and, the cooperative principles great validity. The cooperative is a major source of local development and shows a high level of social responsibility. However, the model lacks a members' high participation level in the voting processes. What is more, it has serious problems of management nature which threaten the company management efficiency.

The cooperative model is not an end in itself and does not guarantee success. The challenge is not so much in trying to determine whether cooperatives are an appropriate alternative for the delivery of urban WSS services, but in the careful consideration of whether and how the cooperative model can be adjusted in its design and practices to suit the particular circumstances of a given city and country.

8th

  World Wide Workshop for Young Environmental Scientists WWW-YES 2009: Urban waters: resource or risks? (2-5 June 2009) 2 / 8

Table 1 : Drinking water management in medium-sized cities

 1 The peculiar characteristics of the drinking water and sanitation provision area in Argentina originates special situations: cities with two different kinds of suppliers, cities with one supplier for drinking water provision (State Public Limited Company) and another supplier for sanity service (cooperatives), cities with two cooperatives and cities with a public entity and a few cooperatives.Next we will refer to the experience in Oberá city. Oberá is a medium-sized city situated in the Province of Misiones (Argentina), next to Brazil and Paraguay borders. In 2001, it had 54.190 inhabitants in 14.257 homes. 64.5% of them had drinking water connections and 30% of them had sewer connections. These percentages exceed the province average. The city has a sewage treatment system (activated muds with extended aeration). By 2005 /2006 drinking water provision coverage rose to 80% and sewage coverage to 51%. Drinking water and sanity services are managed by Cooperativa Eléctrica Limitada Oberá (CELO

	Sector	Kind	Number of cities Number
				of
				Suppliers
	Public	Municipal Centralized Entity	11	13
		Public Limited Company with Public Capital	8	9
		Municipal State Company	2	2
		Autocratic Emití	1	2
		Provincial State Company	1	1
	Private	Public Limited Company with Private Capital	6	7
		Cooperatives	8	18
	Public	Municipal/Cooperative Centralized Entity	2
	/Private
		Autocratic Entity/ Cooperatives	1
		Public Limited Company with Public Capital /	1
		Cooperative
	Total		41	52
	Resource: INDEC data and ENOHSA survey 2005.

Cooperatives manage the drinking water provision in 19% of medium-sized cities and cooperatives with other kind of suppliers co-manage in 10% of them. Considering the number of suppliers, cooperatives represent almost the 35%.