Mohamed Amine Aouadhi
email: mohamed-amine.aouadhi@univ-nantes.fr

Benoit Delahaye
email: benoit.delahaye@univ-nantes.fr

Arnaud Lanoix
email: arnaud.lanoix@univ-nantes.fr

Benoit Delahaye

Benoît Delahaye

About Probabilistic Event-B

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

Introduction

We present in this document our investigation of the probabilistic version of Event-B. We will present the reasons for expressing a such formalism and the modifications of the standard proof obligations or the new proof obligations that can be generated for this Event-B version. We will then study the case of refinement of a probabilistic Event-B model by another probabilistic Event-B model and express the related proof obligations.

Related Work

Many formal methods were developed for the design of complex software-intensive systems including the Event-B [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF] method that was proposed as an extension of the B method [START_REF] Abrial | The B-Book: Assigning programs to meanings[END_REF] to model parallel, distributed and reactive systems. However, the latter systems exhibit sometimes a probabilistic behaviour and are more appropriately modeled in a probabilistic way. Then, many works have discussed the extension of the semantics of Event-B to ensure the expression of probabilistic information in the systems models. Earlier works have also focused in the same extension on the ancestor of the Event-B method: the B method. A first step allowing probabilistic programs to be written and reasoned within B was treated by Thai Son Hoang and al is described in [START_REF] Thai | Probabilistic invariants for probabilistic machines[END_REF]. A study about the refinement of probabilistic programs in B was conducted by the same author, the work is described in [START_REF] Thai | The development of a probabilistic B-method and a supporting toolkit[END_REF]. The overall works about extending B with probabilistic meaning are presented in [START_REF] Thai | The development of a probabilistic B-method and a supporting toolkit[END_REF]. All the research works undertaken to extend Event-B with probabilistic semantics follows the earlier work in B, by transporting ideas from B to Event-B. The purpose of these works is to describe probabilistic systems in Event-B. For probabilistic systems, some problems can only be described in terms of numerical measures such reliability problems, performance problems or dependability problems. In the other side, there are many probabilistic models where the exact numerical measures are not of importance when it comes to problems like modelling communication protocols or human behaviours. The most important for these problems is to guarantee the termination of these systems. This arises two kind of propositions for the probabilistic Event-B semantics: the qualitative probabilistic operator [START_REF] Hallerstede | Qualitative probabilistic modelling in event-b[END_REF] and the quantitative probabilistic operator [START_REF] Tarasyuk | Reliability assessment in event-b development[END_REF][START_REF] Tarasyuk | Integrating stochastic reasoning into eventb development[END_REF][START_REF] Tarasyuk | Towards probabilistic modelling in event-b[END_REF] , we describe each one below. We state that the two propositions for the probabilistic extension does not depart from the original structure of Event-B machines but they introduce the probabilistic choice as a replacement of non-deterministic choices( for these works, the probabilistic choice is introduced only in the place of non-deterministic assignments). A non-deterministic choice in Event-B can occurs in three places:

• choice between different events,

• choice of local variables of events,

• non-deterministic assignments.

The propositions of a probabilistic Event-B reclaims also some requirements:

• the probabilistic Event-B must be simple, i.e easy to understand,

• it should be useful, i.e solve a commonly encountered class of problems,

• it should permit efficient tool support.

We present in what follows the two propositions of a probabilistic Event-B.

Qualitative probabilistic Event-B

Hallerstede and al propose a variant of expressing probabilistic properties in Event-B [START_REF] Hallerstede | Qualitative probabilistic modelling in event-b[END_REF]. In fact, the standard Event-B is based on demonic non-determinism which is not sufficient for modeling some systems that their behaviours are more appropriately modeled in a probabilistic way. In this work, authors restrict their attention on a qualitative aspect of probability, they do not specify the exact numerical measures of probability, but they specify that a non-deterministic choice in the standard Event-B is replaced by a probabilistic choice according to some unknown positive probability. Specifically, they specify that a non-determinism assignment in an action of an event can be replaced by a probabilistic assignment. The purpose of this kind of reasoning is to provide the concept of almost-certain convergence in Event-B like the same reasoning introduced in B. The qualitative probabilistic reasoning is introduced into Event-B by means of the qualitative probabilistic operator choice introduced in B described by: S ⊕ T S or T are chosen according to some unknown positive probability. In the case of assignment, this choice is presented as follows:

x:= a ⊕ b A variable x take as a value a or b according to some positive unknown probability. The authors have made some modifications to the standard proof obligations related to termination, more precisely for the VAR (see section 3.3) proof obligation mentioning that the variant is decreased by each new event introduced during refinement. In fact, when introducing a new event, and when the action of this event is non-probabilistic, this action must decrease the variant. Suppose we have two events ea and ec, where ea is the abstract event and ec is an event introduced during the refinement of the abstract machine, the invariant of the abstract machine is denoted I(v) where the invariant of the concrete machine (gluing invariant) is denoted J(v, w): ea = any t where G(t, v) then S(t, v) end ec = any u where H(u, w) then T (u, w) end

The progress proof obligation (VAR) is as follows:

I(v) J(v, w) H(u, w) ( ∀ w . T (u, v, w ) =⇒ V (w )<V (w))
The authors specifies that a probabilistic action behaves identically to a non-deterministic action, i.e demonically and it behaves angelically when it comes to the progress constraint. A probabilistic action follows the angelical interpretation of a non-deterministic action and it may decrease the variant, so the proof obligation is modified as presented bellow:

1. ea = any t where G(t, v) then S(t, v) end : t represents a parameter of the event, G(t, v) the guard and S(t, v) the action. This is the general form of an event in Event-B. An event is enabled only if the guard G(t, v) is fulfilled.

2. ea = when G(v) then S(v) end : when an event does not have a parameter t. The guard G(v) and the action S(v) are independent from the parameter.

3. ea = begin S(v) end : when the event does not contain any parameter or guard. This is the simplest form of an event, the initialization event is expressed in this form.

The action of an event may contain different assignments that are executed in parallel. An assignment can be expressed in one of the following form:

1. x:= E(t, v): a deterministic assignment, x represents some variables of our system, E(t, v) some expressions.

2. x:∈ E(t, v) : a non-deterministic assignment, x represents a variable of our system, E(t, v) some expressions, x take a value non-deterministically from the set of expressions E(t, v).

3.

x:| Q(t, v, x ) : a non-deterministic assignment, x represents a variable or our system, Q(t, v, x ) represent a predicate. In this case, x take a new value x such that the predicate Q(t, v, x ) must be satisfied.

When the action of an event contain some assignments of the form 2 or 3 presented above, the action of the corresponding event is denoted by S nd (t, v). If all the assignments of an action are in the form 1 presented above, then the action is denoted by S d (t, v).

The effect of each assignment can be described by means of a before-after predicate (BA) that describe the relationship between the values of the variables of the system just before an assignment has occurred (represented by the variable name x) and the values of the variables of our system just after the occurrence of the assignment (represented by the variable name x ). A before-after predicate can be represented by:

• If the assignment is in the form 1 presented previously, then BA(x

:= E(t, v)) ∼ = x = E(t, v).
• If the assignment is in the form 2 presented previously, then BA(x

:∈ E(t, v)) ∼ = x ∈ E(t, v).
• If the assignment is in the form 3 presented previously, then BA(x

:| Q(t, v, x )) = Q(t, v, x ).

Proof Obligations specific to Event-B abstract machines

In Event-B modelling, proof obligations, [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF]Ch5] serve to verify certain properties of a model. Let evt be an abstract event with an invariant inv(c, v) (c represent the constants of our model and v the variables). The guard of this event is G(t, v) while the action is expressed by means of the before-after predicate (v :| BA(c, v, t, v )):

evt any t where G(c, v, t) then v :| BA(c, v, t, v ) end
Invariant preservation proof obligation rule. This proof ensures that each event in the machine preserves the different invariants. For an event evt, this proof obligation is named: "evt/inv/IN V ". Consider the abstract event evt, the standard form of the invariant preservation proof obligation rule is presented below:

Axioms and theorems Invariants and theorems Guards of the event Before-after predicate of the event Modified specific invariant

A(c) I(c, v) G(c, v, t) BA(c, v, t, v ) inv(c, v )
Feasibility proof obligation rule: FIS. This proof aims to ensure that a non-deterministic action is feasible. Suppose that the action of the event evt presented above is non-deterministic. If the action name is act then the name of this proof obligation is "evt/act/F IS". This proof obligation is presented below:

Axioms and theorems Invariants and theorems Guards of the event ∃ v'. before-after predicate

A(c) I(c, v) G(c, v, t) ∃ v . BA(c, v, t, v )
Deadlock freedom rule. This rule ensures that an Event-B model is deadlock free. Given a model with constants c, set of axioms A(c), variables v and set of invariants inv(c, v), this proof obligation consists in proving that one of the guards G 1 (c, v), ..., G n (c, v) of the different events is always true. We present below the form of this proof:

Axioms Invariants

Disjunction of the guards

A(c) I(c, v) G 1 (c, v) ∨ ... ∨ G n (c, v)

Termination in Event-B

Termination is a crucial aspect in Event-B development, it means that a chosen set of new events introduced during refinement are enabled only a finite number of time before an event that is not marked as terminating occurs. In Event-B, the type of an event fixes its type and the proof obligations derived for it. These proof obligations are related to the concept of termination. To support proof for termination, a variant is proposed and all the proof obligations specific to termination act over this variant. There are three types of events in the standard Event-B:

• Ordinary: an event is ordinary if it occurs arbitrary often and does not put any restriction upon the variant.

• Convergent: Convergent events are considered internal and must not be executed forever, an event is said to be convergent if it must decrease the variant every time it occurs.

• Anticipated: Anticipated events are those which will take on their roles in later refinement steps and they might be convergent in these steps. An event is said to be anticipated if it must not decrease the variant.

Each new event introduced during refinement must be either convergent or anticipated. To prove termination in the standard Event-B, we must prove that each convergent event must decrease the variant and this latter has a lower bound. If the model contains only anticipated events, we create simply a default constant variant that must not be increased by each event. Each anticipated event is refined by only an anticipated or a convergent event, the proof of termination is delayed for the stage when all the anticipated events are refined by convergent events. We present in the following the proof obligations related to termination: Let m be an Event-B machine containing two events: evt 1 a convergent event and evt

then v :| BA(c, v, x, v ) end
The numeric variant proof obligation rule: NAT. This rule ensures that under the guards of each convergent or anticipated event, a proposed numeric variant is indeed a natural number. For a convergent (or anticipated) event evt, the name of this rule is "evt/N AT ".

The NAT proof obligation is as follows:

Axioms and theorems Invariant and theorems Event guards

A numeric variant is a natural number

A(c) I(c, v) G(c, v, x) n(c, v) ∈ N
The finite set variant proof obligation rule: FIN. This rule ensures that under the guards of each convergent or anticipated event, a proposed set variant must be a finite set. For a convergent (or anticipated) event evt, the name of this rule is "evt/F IN ". The FIN proof obligation is as follows:

Axioms and theorems Invariants and theorems Event guards

Finiteness of set variant

A(c) I(c, v) G(c, v, t) finite(t(s, c, v))
The variant proof obligation rule: VAR. This rule ensures that each convergent event must decrease the variant, it ensures also that each anticipated event does not increase the variant. Let evt be an event, the name of the rule is "evt/V AR". Given the convergent event evt 1 presented above, if the variant n(c, v) is numeric, then the proof obligation is as follows:

Axioms and theorems Invariants and theorems Guards of the event Before-after predicate of the event Modified variant smaller than variant

A(c) I(c, v) G(c, v, x) BA(c, v, x, v ) n(c, v ) < n(c, v)
If the variant t(c, v) is a finite set, then the proof obligation rule is as follows:

Axioms and theorems Invariants and theorems Guards of the event Before-after predicate of the event Modified variant strictly included in variant

A(c) I(c, v) G(c, v, x) BA(c, v, t, v ) t(c, v ) ⊂ t(c, v)
Given the anticipated event evt 2 , if the variant n(c, v) is numeric, then the proof obligation rule is as follows:

Axioms and theorems Invariants and theorems Guards of the event Before-after predicate of the event Modified variant not greater than variant

A(c) I(c, v) G(c, v, x) BA(c, v, x, v ) n(c, v ) ≤ n(c, v)
If the variant t(c, v) is a finite set, then the proof obligation is as follows:

Axioms and theorems Invariants and theorems Guards of the event Before-after predicate of the event Modified variant in or equal to variant

A(c) I(c, v) G(c, v, x) BA(c, v, x, v ) t(c, v ) ⊆ t(c, v)

Refinement in Event-B

Many research works have focused in the development of the theory of refinement inducing a growing body of experience and literature around this thematic [START_REF] Ralph | Refinement calculus, part i: Sequential nondeterministic programs[END_REF][START_REF] Back | Refinement calculus, part ii: Parallel and reactive programs[END_REF][START_REF] Mciver | Abstraction, refinement and proof for probabilistic systems[END_REF][START_REF] Wirth | Program development by stepwise refinement[END_REF][START_REF] He | Data refinement refined resume[END_REF][START_REF] De Roever | Data refinement: model-oriented proof methods and their comparison[END_REF][START_REF] Boiten | Relational concurrent refinement part ii: Internal operations and outputs[END_REF]]. It appears from the literature that refinement is used in two related concepts in computer science, the first one considers refinement as a top-down program development methodology when the system is firstly described by an abstract specification and progressively refined by other specifications. Each abstract specification will be more detailed and new specifications can be introduced during refinement. The second concept concerns the preservation of correctness between abstract and refined specifications. The process of modelling systems in Event-B is based in the theory of refinement. Event-B is a state based methodology like Z [START_REF] Woodcock | Using Z: Specification, Refinement, and Proof[END_REF], ASM [START_REF] Schellhorn | Asm refinement and generalizations of forward simulation in data refinement: a comparison[END_REF], LOTOS [START_REF] Ferreira | Step-wise refinement design example using lotos[END_REF] and Action Systems [START_REF] Back | Stepwise refinement of action systems[END_REF] where the system is described by a set of "states plus events", the state space describes the variables of the system while the events describes the dynamic part of a system (the actions performed on those variables). Then, refinement permit either a fine description of the state space and the events or the introduction of extra details to the state space (data refinement [START_REF] He | Data refinement refined resume[END_REF][START_REF] De Roever | Data refinement: model-oriented proof methods and their comparison[END_REF]) or the introduction of new events. For the refinement of events in Event-B, three properties must be satisfied:

• Consistency: The effect of the concrete event corresponds to an effect that is allowed by the abstract event in a corresponding state.

• Restricted Consistency: In states where the abstract event is enabled in a corresponding state, the effect of the concrete event corresponds to an effect that is allowed by the abstract event in such a state.

• Enabledness: When events can be invoked in the abstract state, they can be invoked in the corresponding concrete state as well.

Then, starting from a system described by an abstract model, Event-B refinement allows the building of complex systems by the introduction of more details in every step. The three properties mentioned above involve that a crucial aspect in the Event-B refinement is the maintain of correctness between the abstract and the concrete model, i.e, the behaviour of the concrete model must be compatible with the behaviour of the abstract one. This constraint is verified and maintained by some proofs obligations dedicated to refinement.

Proof obligations specific to refinement

We present below the proof obligations specific to refinement:

The guard merging proof obligation rule: MRG. This proof obligation ensures that the guard of a concrete event merging two abstract events is stronger than the disjunction of the guards of the abstract events. For a merging event evt, the name of the rule is "evt/M RG". Let evt 01 and evt 02 be two abstract events with the same parameters and the same action and let evt be the concrete merging event:

evt
A(c) I(c, v) H(c, v, y) G1(c,v,t) ∨ G2(c,v,t)
Guard strengthening proof obligation rule: GRD. The purpose of this rule is to ensure that the concrete guards in a concrete event are stronger than the abstract ones in the abstract event. This ensures that when a concrete event is enabled, so its corresponding abstract one is enabled too. Let an abstract event evt 0 , the name of this proof obligation is: "evt 0 /grd/GRD". Let evt be the refinement of evt 0 , we present below the two events:

evt
A(c) I(c, v) J(c, v, w) H(y, c, w) W (t, c, w, y) g(c, v, t)
Simulation proof obligation. The purpose of this proof is to ensure that each action in an abstract event is correctly simulated in the corresponding refinement. This ensure that when a concrete event is "executed", what it does is not contradictory with what the corresponding abstract event does. For a concrete event evt, the name of this proof obligation is "evt/act/SIM ". Let evt 0 be an event and evt be its refinement:

evt 0 any x where G(c, v, x) then v :| BA1(c, v, x, v ) end evt refines evt 0 any y where H(y, c, w) with x : W 1(x, c, w, y, w ) v : W 2(v , c, w, y, w ) then w:| BA2(c, w, y, w ) end
The proof obligation is as follows:

Axioms and theorems Abstract invariants and theorems Concrete invariants and theorems Concrete event guards witness predicates for parameters witness predicates for variables Concrete before-after predicate Abstract before-after predicate

A(c) I(c, v) J(c, v, w) H(y, c, w) W 1(x, c, w, y, w ) W 2(v , c, w, y, w ) BA2(c, w, y, w ) BA1(c, v, x, v )

Probabilistic Event-B: Syntax

We propose a new version of the standard Event-B entitled "Probabilistic Event-B". In this version, all the non-deterministic choices in an Event-B model are replaced by probabilistic choices. In the standard Event-B, a non-deterministic choice can appear in:

1. When many events are enabled in the same time, only one of these events is chosen non-deterministically to be executed.

2. When an event contains a parameter, the value taken by this parameter is chosen non-deterministically from the set of values such that for each value in this set, the guard of the event is fulfilled.

3. The last case is when the action of an event contains non-deterministic assignments.

Replacing non-deterministic choice with probabilities

In the proposed version of Event-B, we resolve the non-deterministic choice of the event to be executed in the case when many events are enabled in the same time by modifying the structure of an event in the standard Event-B such that each event will occur with a precise positive weight. In the case also when the event has a parameter t, we replace the non-deterministic choice of the value taken by the parameter by an uniform choice of this value from the subset of values in such a way that the guard of the parameter will be satisfied. Lastly, when the action of the event contains some non-deterministic assignments, we propose also a new probabilistic assignment to resolve the non-deterministic choice of the assignment to be executed. We present in what follows the different cases of non-deterministic choices and its corresponding probabilistic version.

Case 1: Annotating events with weights.

To resolve the non-deterministic choice between some enabled events, we annotate all the events by a positive weight. In the standard Event-B, the general form of an event is:

e a = any t where G(t, v) then S d (t, v) end
We suppose that the action of the event is deterministic, it is noted by S d . The corresponding form of this event in our new probabilistic version of Event-B will be:

e a = weight w any t where G(t, v) then S d (t, v) end
The weight of a probabilistic event must be strictly greater than 0. For each probabilistic event e a , we denote by W (e a ) the weight of occurrence of e a .

Case 2: Some events contain a probabilistic choice of the value of the parameter.

We suppose that the parameter of an event take this value from a finite set T , the form of the event in the standard Event-B is:

e a = begin any t where t ∈ T ∧ G(t, v) then S d (t, v) end.
The parameter t take its value non-deterministically from the set T in such a way the guard G(t, v) must be fulfilled. In our new version of Event-B, the value taken by the parameter t of the event is chosen in an uniform manner from the set T . This latter must be a finite set ( {t 1 , t 2 ..., t n }). Specifically, this value is chosen from a subset T v = {t m ..., t k } 1≤m≤n,1≤k≤n such that for each value t of the parameter in T v , we have G(t = t , v) |= true. Then we note this subset of value of parameters by

T v = {t ∈ T \G(t, v)
|= true}, the different values of the parameter in T v depends also in the valuation of the different variables of our model when the guard is evaluated. We associate a probability function P T such that for each value

t z ∈ T , P T (t = t z ) = P T (t z ) = 1 card(T ) . It is also the case for the subset T v where P T v (t = t z ) = P T v (t z ) = 1 card(T v ) .

Case 3: The action of the event is non-deterministic.

In the case where the action of the event is non-deterministic like presented below:

e a = any t where t ∈ T ∧ G(t, v) then S nd (t, v) end
We denote a non-deterministic action by S nd (t, v), its full syntax is presented below:

x 1 :∈ {E 11 (t, v), E 12 (t, v), ..., E 1m1 (t, v)} (S 1 (t, v)) || x 2 :∈ {E 21 (t, v), E 22 (t, v), ..., E 2m2 (t, v)} (S 2 (t, v)) ... || x k :∈ {E k1 (t, v), E k2 (t, v), ..., E km k (t, v)} (S n (t, v))
The action of the event e a assigns to each variable x i of our model an expression

E ij (1 ≤ j ≤ m i ) that is chosen non-deterministically from a finite set of expressions {E i1 (t, v), E i2 (t, v), ..., E im1 (t, v)}.
m i represents the number of expressions that can be assigned to the variable x i . We propose a new probabilistic action S p (t, v). The syntax of this action is presented below:

x 1 := E 11 (t, v) ⊕ @ p11 ...E 1m1 (t, v) ⊕ @ p1m 1 (S 1 (t, v)) || x 2 := E 21 (t, v) ⊕ @ p21 ...E 2m2 (t, v) ⊕ @ p2m 2 (S 2 (t, v)) ... || x k := E k1 (t, v) ⊕ @ pk1 ...E km k (t, v) ⊕ @p km k (S n (t, v)) For each variable x i of our model (1 ≤ i ≤ k), there is a positive number (m i ) of expressions E i,j (1 ≤ j ≤ m i ) that can be assigned to x i each one with probability p ij (1 ≤ j ≤ m i ∧ 0 ≤ p ij ≤ 1). For each x i , we have mi j=0 p ij = 1.
The syntax of the new probabilistic event then will be:

e a = begin weight w any t where t ∈ T ∧ G(t, v) then S p (t, v) end.

Proof obligations related to the new proposition

We investigate in this part the modifications that can be done in the standard proof obligations, we express also some new proof obligations related to the new kind of events presented above.

In the following, we use the following notations. If the action of an event e a is probabilistic, then we denote by < e a /E ij > the fact that the action of the event e a will assign the expression E ij to the variable x i , we denote also by P xi (< ea/E ij >) the probability that the expression E ij will be assigned to the variable x i . If the action of the event is deterministic, then P xi (< ea/E ij >) is equal to 1. We denote also by < e a /E 1j1 ; E 2j2 ; ...; E kj k > the fact that the action of the event e a will assign to each of the variables of our model (x 1 , ..., x k ) respectively the expressions (E 1j1 ; E 2j2 ; ...; E kj k ). We denote by γ = {j 1 , j 2 , ..., j k } the combination of expressions that will be assigned to the variables (x 1 , ..., x k ) such that γ(i)= j i ∀ 1 ≤ i ≤ k. The probability of this assignment is:

P (e a /γ) = k i=1 P xi (< ea/E iji >)
If the action of the event e a is deterministic (S d instead of S p ), then:

P (e a /γ) = k i=1 P xi (< ea/E iji >) = 1
For the new kind of events presented in Section 4.1, the standard proof obligations have the same form except that for the proof obligations related to termination, we add three new types of events:

• Ordinary probabilistic: this kind of event is like an ordinary event but it occurs with a positive weight, it does not put any restriction upon the variant.

• Convergent probabilistic: this kind of event is like a convergent event but likewise. It occurs with a positive weight and it must decrease the variant each time it is executed.

• Anticipated probabilistic: this kind of event is like an anticipated event except that it occurs with a positive weight. Each time it is executed, it must not increase the variant.

The proof obligations related to termination keep the same form as standard events. We now introduce our new proof obligations.

The weight of a probabilistic event must be greater than 0. This proof aims to ensure that the weight of a probabilistic event must be strictly greater than 0. Let evt be a probabilistic event like presented below:

evt weight w any t ∈ T where G(c, v, t) then S p (c, v, t) end
The new proof obligation for this event is:

The weight of occurrence of the event is strictly greater than 0. w>0 Finiteness of the set of values of the parameter of an event. Another proof obligation that is derived for our probabilistic event mention that the set T of values that can be taken by the parameter must be finite:

The set of values taken by the parameter must be finite.

finite(T )

Finiteness of the set of expressions that can be assigned to a variable. The last new proof obligation concerns the probabilistic action (S p (t, v)) of the probabilistic event:

x 1 := E 11 (t, v) ⊕ p11 ... ⊕ p1m 1 E 1m1 (t, v) (S 1 (t, v)) x 2 := E 21 (t, v) ⊕ p21 ... ⊕ p2m 2 E 2m2 (t, v) (S 2 (t, v)) ... x k := E k1 (t, v) ⊕ pk1 ... ⊕ p km k E km k (t, v) (S n (t, v))
Like mentioned in the previous section, each variable x i of our model (1 ≤ i ≤ k) can take one of the expressions E ij ((1 ≤ j ≤ m i ) each one with a probability p ij . This proof ensure that the sum of the probabilities of the expressions that can be assigned to each variable x i must be equal to one:

∀x i , 1 ≤ i ≤ k, mi j=0 p ij = 1
Then for the event presented above, we have:

∀x i , mi j=0 P xi (< evt/E ij >) = 1

Probabilistic Event-B: Operational Semantics

We present in this section the operational semantics of a probabilistic Event-B model in the form of a discrete-time Markov chain. We start by giving the definitions of a probabilistic Event-B model and a discrete-time Markov chain. Afterwards, we provide the operational semantics of a probabilistic Event-B model.

Background

We first introduce probabilistic Event-B model which is the main proposition of this document and discrete-time Markov chain which is a well-known mathematical model for stochastic systems.

Definition 1 (Probabilistic Event-B model)

A probabilistic Event-B model is a tuple M =(X, Init, Inv, Evts) where

• X = (x 1 , x 2 , ..

., x k ) represents the variables of our model,

• Init is the initialization event,

• Inv is the invariant of our model,

• Evts are the events of our model,

The variables (x 1 , x 2 , ..., x k ) take their values from a set D = D 1 × D 2 × .... × D k .
The different valuations of the variables of our model must satisfy the invariant Inv. Moreover, each event of our model occurs with a positive weight and if its guard is enabled. We denote the guard of each event e a by grd(e a ) and its weight by w(e a ). We denote by α(M ) the set of event names in M ( suppose M contains two events named respectively e a1 and e a2 , then α(M )={e a1 , e a2 }). The general form of an event in Evts is: e a = weight w any t where t ∈ T ∧ G(t, v) then S p (t, v) end An event can be also written in one of the following forms:

1. the initialization event: e a1 = weight w S d (v) end 2. when the event does not have a parameter and its action is deterministic:

e a2 = weight w when G(v) then S d (v) end
3. when the event does not have a parameter and its action is probabilistic:

e a3 = weight w when G(v) then S p (v) end 4.
when the event has a parameter and its action is deterministic:

e a4 = weight w any t where t ∈ T ∧ G(t, v) then S d (t, v) end
We now define a discrete-time Markov chain

Definition 2 (discrete-time Markov chain)

We define (discrete-time) Markov chain as a tuple M=(S, P , s 0 , AP , L, Acts) where:

• S is a countable, nonempty set of states,

• Acts is a set of actions ,

• P: S × Acts × S → [0,1] is the transition probability function such that for all states s: s ∈S,a∈Acts P (s, a, s ) = 1

• s 0 : the initial state,

• AP is a set of atomic propositions and L: S → 2 AP a labeling function.

Operational Semantics

After providing the definitions of a probabilistic Event-B model and a discrete-time Markov chain, we provide in this section the operational semantics of a probabilistic Event-B model. The operational semantics of a probabilistic Event-B model M =(X, Init, Inv, Evts) is a discrete-time Markov chain. A transition in this Markov chain corresponds to an occurrence of an event in the Event-B model M . The states of this Markov chain corresponds to the different valuations of the variables of M . Given a state s of M , we denote the set of actions (events) enabled in this state by:

Acts(s) = {E j /[L(s)]grd(E j ) |= true}
The state destination of a transition (s, e a , s ) performed by an event e a is labelled by:

Ł(s ) = {x j → v j |[L(s)](< e a (x j = v j ) >)}∀j ∈ 1..k
If the action of the event e a is probabilistic:

S p (t, v) x 1 := E 11 (t, v) ⊕ @ p11 ...E 1m1 (t, v) ⊕@ p1m 1 (S 1 (t, v)) x 2 := E 21 (t, v) ⊕ @ p21 ...E 2m2 (t, v) ⊕@ p2m 2 (S 2 (t, v)) ... x k := E k1 (t, v)⊕@ pk1 ...E km k (t, v) ⊕@ p km k (S n (t, v))
then we denote a combination of expressions that can be assigned to the variables x i (1 ≤ i ≤ k) by the action of e a taking the system to a state s by:

γ s ea (s ) = {γ = (j 1 , ..., j k )|L(s ) = {x i → E iγ(i) |[L(s)](e a (x i = E iγ(i) ))}}∀i ∈ 1..k
From the state s, if there are many combinations of expressions that can be assigned to the variables x i (1 ≤ i ≤ k) taking the system to the same state s , then we denote these combinations by:

β s ea (s ) = {β = (γ 1 , ..., γ t )|∀γ z ∈ β, L(s ) = {x i → E iγz(i) |[L(s)](e a (x i = E iγz(i) ))}}∀i ∈ 1..k
We present below the formal definition of the semantics of a probabilistic Event-B model: • S the set of states of the Markov chain, they are formed accordingly to the different valuations of the variables of the model M . The semantic interpretation of a state over X is defined by the labeling function L that associate for a given state s, for each variable

Definition
x i ∈ X, a value v i ∈ D i .
We denote by L(s i , x j ) the current value of the variable x j in the state s i .

• l init is the initial distribution such that s∈S l init (s) = 1 . The initial state of the Markov chain is obtained after the execution of the Init event, and

L(s 0 ) ={ x j → v j |< Init > (x j = v j )} ∀j ∈ 1..k.
• AP represents the different assignments to the different variables of our model, these assignments must satisfy the invariant Inv of the Event-B model.

AP = {x i → d j |(x i → d j ) |= Inv} ∀x i ∈ X ∧ d j ∈ D i .
• Acts is the alphabet of events of the Event-B model M .

• P : S × Acts × S → [0,1] is the transition probability function such that the probability of occurrence of the event e a in the state s taking the system to the state s is:

P (s, e a , s ) = W (e a ) Ej ∈Acts(s) W (E j ) × tz∈T v P T v (t z ) × γ∈β s ea (s ) k i=1 P xi (e a /E iγ(i) (t z , v))
Many cases can be derived from this formula:

1. If the event e a does not have a parameter t and its action is probabilistic, then the probability of the transition from s to s is:

P (s, e a , s ) = W (e a ) Ej ∈Acts(s) W (E j ) × β∈β s ea (s ) k i=1 P xi (e a /E iβ(i) (v))
2. If the event e a does not have a parameter t and its action is deterministic, then the probability of the transition from s to s is:

P (s, e a , s ) = W (e a )
Ej ∈Acts(s) W (E j )

3. If the event e a have a parameter t and its action is deterministic, then the probability of the transition from s to s is:

P (s, e a , s ) = W (e a ) Ej ∈Acts(s) W (E j ) × tz∈T v P T v (t z ) Lemma 1 Given a probabilistic Event-B model M , the operational semantics [[M ]] of M is a discrete- time Markov chain.

Proof.

We must prove then that for each state s in [[M ]], the sum of probabilities of transitions enabled in s is equal to 1:

s ∈S,e∈Acts(s)

P (s, e, s ) = 1
Let s be a state of [[M ]] and let e a an event enabled in s, the action of e a is presented below:

x 1 := E 11 (t, v) ⊕ @ p11 ...E 1m1 (t, v) ⊕@ p1m 1 x 2 := E 21 (t, v) ⊕ @ p21 ...E 2m2 (t, v) ⊕@ p2m 2 ... x k := E k1 (t, v) ⊕ @ pk1 ...E km k (t, v) ⊕@ p km k
There are c = k i=1 m i combinations of expressions that can be assigned to the variables x i (1 ≤ i ≤ k). Each combination take the system to a state s , many combinations can take the system to the same state s .

The probability of a transition (s, e a , s ) is:

P (s, e a , s ) = W (e a ) Ej ∈Acts(s) W (E j ) × tz∈T v P T v (t z ) × γ∈β s ea (s ) k i=1 P xi (e a /E iγ(i) (t z , v))
The sum of probabilities of transitions performed by the event(action) e a is:

s ∈S P (s, e a , s ) = s ∈S W (e a ) Ej ∈Acts(s) W (E j ) × tz∈T v P T v (t z ) × γ∈β s ea (s ) k i=1 P xi (e a /E iγ(i) (t z , v)) = W (e a ) Ej ∈Acts(s) W (E j ) × tz∈T v P T v (t z ) s ∈S γ∈β s ea (s ) k i=1 P xi (e a /E iγ(i) (t z , v)) = W (ea) E j ∈Acts(s) W (Ej ) × tz∈T v P T v (t z ) × k i=1 mi j=1 P xi (e a /E ij ) or ∀x i , mi j=1 P xi (e a /E ij ) = 1, then k i=1 mi j=1 P xi (e a /E ij ) = 1 and we have tz∈T v P T v (tz) = 1 then: s ∈S P (s, e a , s ) = W (e a ) Ej ∈Acts(s) W (E j ) × tz∈T v P T v (t z ) × k i=1 mi j=1 P xi (e a /E ij ) = W (e a )
Ej ∈Acts(s) W (E j ) Then, the sum of probabilities of transitions enabled in the state s is: After defining the operational semantics of a probabilistic Event-B model and proving that it corresponds to a discrete-time Markov chain, we present below some examples of probabilistic Event-B models and their corresponding operational semantics.

Examples

We present below the first probabilistic Event-B model and its corresponding discrete-time Markov chain.

Example 1: Markov chains semantics of a probabilistic Event-B model where the guards of the events are independent from the parameters

We present below an example of a probabilistic Event-B model and its operational semantics. We begin firstly by presenting the probabilistic Event-B model, after that we present the corresponding discretetime Markov chain.

Probabilistic Event-B model.

We present below the probabilistic Event-B model, we note that the guards of the first event are independent from the parameter.

Model example 1

Variables x, y Invariant x, y ∈ N Events evt1 ∼ = weight 4 any t where (t = 0 @ 1 2 , t = 1 @ 1 2 ) ∧ (x < 1 ∧ y < 1) then x := x + t 1/3 ⊕ x + 2t (S 11 ) y := y + t 1/4 ⊕ y + 2t (S 22 ) end evt2 ∼ = weight 3 when (x < 1 ∧ y < 1) then We present in the next section the second probabilistic Event-B model and its corresponding Markov chain semantics.

x := x 2/5 ⊕ x

Example 2: Markov chains semantics of a probabilistic Event-B model where the guards depends on the parameters

We now present a second example of a probabilistic Event-B model and its operational semantics. We begin firstly by presenting the probabilistic Event-B model after that we present the corresponding discrete-time Markov chain.

Probabilistic Event-B model.

We present below the probabilistic Event-B model, the only difference with the previous example is that the guards of the first event of this example depends on the value taken by the parameter of the event:

Model example2

Variables x,y Invariant x,y ∈ N Events evt1 ∼ = weight 4 any t where (t = 0 @ 1 2 , t = 1 @ 1 2 ) ∧ (x + t < 2 ∧ y + t < 2) then x := x + t 1/3 ⊕ x + 2t (S 11 ) y := y + t 1/4 ⊕ y + 2t (S 22 ) end evt2 ∼ = weight 3 when (x < 1 ∧ y < 2) then

x := x 2/5 ⊕ x + 1 (S 21 ) y := y 1/7 ⊕ y + 1 (S 22
) end Operational semantics.

We present below the corresponding discrete-time Markov chain of the Event-B model presented above, the only difference from the Markov chain derived from the Event-B model presented above is the fact that in the state (0, 1), the event evt1 is enabled (guard fulfilled) only if the parameter t take the value 0, so that, the subset of values for the parameter t in this state is the singleton {0} and the parameter take this value with probability 1. 0,0 0,1 0,2

Probabilistic Simulation

Based on the theory of probabilistic simulation and bisimulation, we propose a new theorem for the refinement between discrete-time Markov chains. We begin firstly by presenting some basic definitions about Probabilistic systems. After that, we present our new theorem.

Probabilistic Systems

In this section, we introduce some related concepts and definitions of probabilistic systems, these definitions will be used through the rest of this document. We begin by presenting the definition of a probability space:

Definition 4 (Probability Space)

A probability space is a triplet (Ω, F, P) where Ω is a set, F is a collection of subsets of Ω that is closed under complement and countable union and P is a function from F to [0, 1] such that P [Ω] = 1 and for any collection {C i } of at most countably many stepwise disjoint elements of

F, P [∪ i C i ] = i P[C i ]. A probability space (Ω, F, P) is discrete if F= 2 Ω and for each C ⊆ Ω , P[C] = x∈C P[x].
We give now the definition of an automata:

Definition 5 (Automata)

Formally, an automata A is composed of:

• a set S of states,

• a subset S 0 of initial states,

• a set of actions Acts= {ext(A), int(A)} where ext(A) denotes the set of external actions and int(A) denotes the set of internal actions,

• a set of transitions trans(A) ⊆ S × Acts × S that describes the different behaviours of the system describes by this automata.

After presenting the definition of a probability space and an automata, we introduce now the concept of Probabilistic Automata [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF].

Definition 6 (Probabilistic Automata )

A Probabilistic Automata M is an automata where the transition relations trans(A) is a subset of S(a) × P robs(acts(A) × S(A) ∪ δ) where P robs(X) is the set of discrete probability space (Ω, F, P) where Ω ⊆ X.

A Probabilistic Automata M is simple if for each transition trans(s, (Ω, F, P ) ) ∈ trans(M ), there is an action a ∈ acts(M ) such that Ω ⊆ a ×S(A). In this case, a transition can be represented as (s, a, (Ω, F, P)) where P robs(A) ∈ P robs(S(A)) and is called a simple transition with action a and then the action is the same but it take the system to different states when the choice between these states is done in a probabilistic way. A Probabilistic automata is fully probabilistic if it has a unique start state and from each state, there is at most one step enabled. Thus a probabilistic automata differs from an automata in that the action and the next state of a given transition are chosen probabilistically. The symbol δ represents the situation when the system deadlocks. It is then possible that from a state s , a probabilistic automata performs some action with probability p and deadlock with probability 1 -p. For expressing the equivalence between states of probabilistic automata, we present below a formal definition of an equivalence relation:

Definition 7 (Equivalence Relation [35])

Let R be an equivalence relation over a set X. Two probability spaces (Ω 1 , F 1 , P 1 ) and (Ω 2 , F 2 , P 2 ) of P robs(X) are R_equivalent written

(Ω 1 , F 1 , P 1 ) ≡ R (Ω 2 , F 2 , P 2 ) if for each [x 1 ] R ∈ Ω 1 /R there exists an [x 2 ] R ∈ Ω 2 /R such that x 1 R x 2 , for each [x 2 ] R ∈ Ω 2 /R there exists an [x 1 ] R ∈ Ω 1 /R such that x 2 R x 1 , and for each [x 1 ] R ∈ Ω 1 /R[x 2 ] R ∈ Ω 2 /R such that x 1 Rx 2 , x∈Ω1∩[x1] R P [x]= x∈Ω2∩[x2] R P [x].
In other worlds (Ω 1 , F 1 , P 1 ) and (Ω 2 , F 2 , P 2 ) are R_equivalent if they assign the same probability measure to each equivalence class of R.

Simulation and Bisimulation between probabilistic automata.

Simulation ( ) and bisimulation relations (∼) have been widely used for the comparison of the stepwise behaviour of states in labeled transition systems [START_REF] Baier | Principles of model checking[END_REF]Ch2]. Bisimulation relation [START_REF] Milner | A calculus of communicating systems[END_REF][START_REF] Milner | Communication and concurrency[END_REF][START_REF] Park | Concurrency and automata on infinite sequences[END_REF] requires that two bisimilar states exhibit an identical stepwise behaviour whereas Simulation relations [START_REF] Abadi | The existence of refinement mappings[END_REF][START_REF] Rauch Henzinger | Computing simulations on finite and infinite graphs[END_REF][START_REF] Jonsson | Simulations between specifications of distributed systems[END_REF][START_REF] Lynch | Forward and backward simulations[END_REF][START_REF] Park | Concurrency and automata on infinite sequences[END_REF] are preorders over the state space requiring that whenever s s (s simulate s), state s can emerge all the stepwise behaviour of s, the converse s s is not guaranteed and then state s can perform some steps that cannot be matched by s. Simulation and bisimulation relations was also extended to the case of probabilistic systems and several studies has been also carried out to define probabilistic simulation and Bisimulation relations. For a more details about these works, see the research papers [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF][START_REF] Kim | Bisimulation through probabilistic testing (preliminary report)[END_REF][START_REF] Andova | Abstraction in probabilistic process algebra[END_REF][START_REF] Jou | Equivalences, congruences, and complete axiomatizations for probabilistic processes[END_REF][START_REF] Baier | Weak bisimulation for fully probabilistic processes[END_REF][START_REF] Philippou | Weak bisimulation for probabilistic systems[END_REF][START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. We present now a restatement of the strong probabilistic simulation defined by Segala in [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]:

Definition 8 (Strong probabilistic simulation)

Given two probabilistic automata M 1 and M 2 , we define two probability spaces (Ω 1 , F We say that M c refine M a if there exits a refinement relation R r such that t 0 R r s 0 .

We show now the equivalence between the notions of refinement and the strong probabilistic simulation.

Theorem 1 (Equivalence between the notions of refinement and strong probabilistic simulation)

Given two discrete-time Markov chains M a and M c . M c refines M a iff M a strongly simulate M c (M c R r M a ⇐⇒ M a R s M c ).
Proof. ⇒ : we begin by proving that the notion of refinement between discrete-time Markov chains implies the notion of strong probabilistic simulation. Suppose that we have two discrete-time Markov chains M a and M c such that M c refines M a (M c R r M a ). We want to prove that M a simulate M c (M c R s M a ) like defined in Section 8, we prove then the different items of R s :

1. each start state of M a is related to at least one start state of M c :

We have M c refine M a , then there exist a refinement relation between the initial states of M c and M a (given an initial state t 0 of M c and an initial state s 0 of M a , then t 0 R r s 0 ) then each start state of M a is related to at least one start state of M c .

2. for each two states t and s of M c and M a respectively such that t R s s, for each step t → (Ω 1 , F 1 , P 1 ) of M c , there exists a step s → (Ω 2 , F 2 , P 2 ) of M a such that there exist a weight function w:

Ω 1 × Ω 2 → [0, 1] such that: a. for each x ∈ Ω 1 y∈Ω2 w(x, y)=P 1 [x] (x = (e c , t
) represents an action e c enabled in the state t and take the system to a state t where y = (e a , s ) represents an action e a enabled in the state s and take the system to a state s )

Let w(x, y) = P 1 [x].δ(x)(y), y∈Ω2 w(x, y) = y∈Ω2 P 1 [x].δ(x)(y) = P 1 [x]. y∈Ω2 δ(x)(y)
Or from 2.a in Section 10, we have δ(e c , t ) is a distribution on Acts a × S a , i.e:

e∈Actsa,sa∈Sa δ(e c , t )(e, s a ) = y∈Ω2 δ(x)(y) = 1 then: y∈Ω2 P 1 [x].δ(x)(y) = P 1 [x]. y∈Ω2 δ(x)(y) = P 1 [x].1 = P 1 [x] b. for each y ∈ Ω 2 x∈Ω1 w(x, y)=P 2 [y]: Let w(x, y) = P 1 [x].δ(x)(y),
x∈Ω1 w(x, y) = P 2 [y] c. ∀x, y ∈ Ω 1 × Ω 2 if w(x, y) > 0 where x = (e c , s c ) and y = (e a , s a ), then s c R s s a If w(x, y) > 0, then P 1 [x].δ(x)(y) > 0 or P 1 [x]
is strictly greater than 0, then δ(x)(y) > 0 ,i.e, x R r y =⇒ x R s y.

⇐ : we prove now that the notion of strong probabilistic simulation implies the notion of refinement. Suppose that we have two discrete-time Markov chains M a and M c such that

M a simulate M c (M c R s M a )
, suppose that we have two states t and s of M c and M a respectively such that t R s s, we want to prove that t R r s, we must then prove the different items of R r :

1. (t, s) ∈ L eq we have t R s s =⇒ t R r s and then (t, s) ∈ L eq .

2. there exits a function δ:

(Acts c × S c ) → ((Acts a × S a ) → [0, 1]) such that: a. ∀ e c , t ∈ Acts c × S c such that P c (t, e c , t ) > 0, δ(e c , t
) is a distribution on (Acts a × S a ), i.e, ea∈Actsa,s ∈Sa δ(e c , t )(e a , s ) = 1 we denote by x = (e c , t ) an action e c enabled in the state t that take the system to a state t and by y = (e a , s ) an action e a enabled in s that take the system to a state s , we want to prove then that y∈Ω2 δ(x)(y) = 1. By analogy with R s , this sum can be rewritten as:

Let δ(x)(y) = w(x,y) P1[x] if P 1 [x] = 0 0 if P 1 [x] = 0 y∈Ω2 δ(x)(y) = y∈Ω2 w(x, y) P 1 [x] = 1 P 1 [x] × y∈Ω2 w(x, y) or from 2.a in 8, ∀x ∈ Ω 1 , y∈Ω2 w(x, y) = P 1 [x], then: y∈Ω2 δ(x)(y) = 1 Then, δ(x) is a distribution on Acts a × S a , i
x∈Ω1 P 1 [x].δ(x)(y) = x∈Ω1 P 1 [x]. w(x, y) P 1 [x] = x∈Ω1 w(x, y) = P 2 [y]
Then we obtain: We denote (e c , t ) by x and (e a , s ) by y. we have taken previously δ(x, y) = w(x,y) P1[x] , we have δ(x, y) > 0, then w(x,y) P1[x] > 0 or P 1 [x] > 0, then w(x, y) > 0 and then t R s s , then t R r s .

Refinement of a Probabilistic Event-B model

After defining the syntax and the operational semantics of a probabilistic Event-B model, we present in this section our proposition of refinement of a probabilistic Event-B model. We begin by presenting our notion of refinement of a probabilistic Event-B model and the related new proof obligations. Afterwards, we show that the notion of refinement between two probabilistic Event-B models implies the notion of refinement between their corresponding discrete-time Markov chains. We conjuncture that the notion of refinement between two probabilistic Event-B models is equivalent to the notion of refinement between their corresponding discrete-time Markov chains. In future work, we will prove that the notion of refinement between discrete-time Markov chains implies the notion of refinement between their corresponding probabilistic Event-B models.

Refinement in Probabilistic Event-B

We introduce a new notion of refinement for probabilistic Event-B models. We begin by presenting the abstract and the concrete models and explaining our notion of refinement. After that, we present the new proof obligations specific to refinement.

Abstract and Concrete Event-B models

Let M a and M c two probabilistic Event-B models such that M c refine M a :

Abstract Probabilistic Event-B model. M a =(X a , Init a , Inv a , Evts a ) is an abstract probabilistic Event-B model where:

• X a = (x 1 , x 2 , ..., x k ) : the variables of M a , these variables take their values from the set D = D 1 × D 2 × .... × D k and must satisfy the invariant Inv a .

• Init a : the abstract initialization event,

• Inv a : the invariant of our model that must be satisfied by the different valuations of the variables of M a .

• Evts a : the abstract events of M a , each event occurs with a positive weight w a , we denote by α a (M a ) the set of events names in M a . • Init c : the abstract initialization event,

Concrete

• Inv c : the gluing invariant that relate the variables of M a to the variables of M c .

• Evts c : the concrete events of M c , we do not allow the introduction of new events in Evts c (α c (M c )= αM a ). Each probabilistic event in the abstract model M a is refined by only one probabilistic event in M c .

We do not allow the introduction of new events during refinement, only the introduction of new variables in the concrete model and the modification of events actions are permitted. The classical proof obligations remain applicable and unchanged for the refinement of probabilistic events. In addition, we propose some new proof obligations dedicated to this refinement. We note that the syntax of our proposition for probabilistic Event-B models is not yet complete and we have not yet define an operator for expressing the probability of an event in Event-B, so we express at the moment the new proofs using their corresponding Markov chains semantics.

New proof obligations related to refinement

We present in this section the new proof obligations that must be verified in the case of the refinement of a probabilistic Event-B model by another probabilistic Event-B model. These proofs are expressed on the Markov chain semantics of both the concrete and the abstract models. Given two states s a of s c and s c of [[M a ]] and [[M c ]] respectively, we say that s a is equivalent to s c only if the valuations of s a and s c satisfies the gluing variant Inv c of the concrete Event-B model. We use the relation L eq defined in definition 10 to express that two states are equivalent.

Proof 1: Relation between the probability of occurrence of an abstract event and that of its refined event.

This proof express the relation between the probability of occurrence of an abstract event and the probability of occurrence of its refined concrete event. Given an abstract probabilistic event e a that is refined by a concrete probabilistic event e c like presented below: In the corresponding Markov chain semantics of M a and M c , suppose that the abstract event e a1 is enabled in an abstract state s a1 and the abstract event e a2 is enabled in an abstract state s a2 while the concrete event e c is enabled in a concrete state s c . We have three possibilities in this kind of refinement:

e
• If the state s c is equivalent only to the state s a1 but not to the state s a2 , then the probability of occurrence of the concrete event e c in the state s c taking the system to the state s c is equal to the probability of occurrence of the abstract event e a1 in the state s a1 taking the system s a1 :

The state s c is equivalent to the state s a1

The state s c is not equivalent to the state s a2

The probability of occurrence of the event e c in the state s c taking the system to the state s c is equal to the probability of occurrence of the abstract event e a1 in the state s a1 to the state s a1

(s c , s a1 ) ∈ L eq (s c , s a2 ) ∈ L eq P c (s c , e c , s c ) = P a (s a1 , e a1 , s a1 )

• If the state s c is equivalent only to the state s a2 but not to the state s a1 , then the probability of occurrence of the concrete event e c in the state s c taking the system to the state s c is equal to the probability of occurrence of the abstract event e a2 in the state s a2 taking the system s a2 :

The state s c is equivalent to the state s a2

The state s c is not equivalent to the state s a1

The probability of occurrence of the event e c in the state s c taking the system to the state s c is equal to the probability of occurrence of the occurrence of the abstract event e a2 in the state s a2 to the state s a2

(s c , s a2 ) ∈ L eq (s c , s a1 ) ∈ L eq P c (s c , e c , s c ) = P a (s a2 , e a2 , s a2 )

• If the state s c is equivalent to both the states s a1 and s a2 , then the probability of occurrence of the concrete event e c in the state s c taking the system to the state s c is equal to the sum of probabilities of occurrence of the abstract events e a1 in the state s a1 taking the system to the state s a1 and e a2 in the state s a2 taking the system s a2 :

The state s c is equivalent to the state s a1

The state s c is equivalent to the state s a2

The probability of occurrence of the event e c in the state s c taking the system to the state s c is equal to the sum of probabilities of occurrence of the abstract events e a1 in the state s a1 and M c , suppose that the abstract event e a is enabled in an abstract state s a and the concrete event e c1 is enabled in a concrete state s c1 while the concrete event e c2 is enabled in a concrete state s c2 . We have three possibilities in this kind of refinement:

• If the state s a is equivalent only to the state s c1 but not to the state s c2 , then the probability of occurrence of the concrete event e c1 in the state s c1 taking the system to the state s c1 is equal to the probability of occurrence of the abstract event e a in the state s a taking the system to the state s a :

The state s a is equivalent to the state s c1

The state s a is not equivalent to the state s c2

The probability of occurrence of the event e c1 in the state s c1 taking the system to the state s c1 is equal to the probability of occurrence of the occurrence of the abstract event e a in the state s a to the state s a (s c1 , s a ) ∈ L eq (s c2 , s a ) ∈ L eq P c (s c1 , e c1 , s c1 ) = P a (s a , e a , s a )

• If the state s a is equivalent only to the state s c2 but not to the state s c1 , then the probability of occurrence of the concrete event e c2 in the state s c2 taking the system to the state s c2 is equal to the probability of occurrence of the abstract event e a in the state s a taking the system s a :

The state s a is equivalent to the state s c2

The state s a is not equivalent to the state s c1

The probability of occurrence of the event e c2 in the state s c2 taking the system to the state s c2 is equal to the probability of occurrence of the occurrence of the abstract event e a in the state s a to the state s a (s c2 , s a ) ∈ L eq (s c1 , s a ) ∈ L eq P c (s c2 , e c2 , s c2 ) = P a (s a , e a , s a )

• If the state s a is equivalent to both the states s c1 and s c2 , then the probability of occurrence of the abstract event e a in the state s a taking the system to the state s a is equal to the sum of probabilities of occurrence of the abstract events e c1 in the state s c1 taking the system to the state s c1 and and e c2 in the state s c2 taking the system s c2 :

The state s a is equivalent to the state s c1

The state s a is equivalent to the state s c2

The probability of occurrence of the abstract event e a in the state s a taking the system to the state s a is equal to the sum of probabilities of occurrence of the concrete events e c1 in the state s c1 taking the system to the state s c1 and and e c2 in the state s c2 taking the system s c2 (s c1 , s a ) ∈ L eq (s c2 , s a ) ∈ L eq P a (s a , e a , s a ) = P c (s c1 , e c1 , s c1 )+P c (s c2 , e c2 , s c2 ) In this case, the action e a is refined by the actions e c1 , e c2 ,...,e cm , i.e, the corresponding event named e a in M a is splitted into the events named e c1 , e c2 ,...,e cm in M c . The condition 2.b of R r can be rewritten as: m i=1 P c (t, e ci , t i ).δ(e ci , t i )(e a , s ) = P a (s, e a , s ) or from the condition 2.a of R r , δ(e ci , t i ) (1 ≤ i ≤ m) is a distribution on (Evts a × S a ), then ∀ i, δ(e ci , t i )(e a , s )= 1 and then: This case corresponds both to the case where some action e c1 refine many actions e a1 , e a2 , ..., e am and one of the abstract action e a1 for example refine many actions e c1 , e c2 , ..., e cm , we have then: P c (t, e ci , t i ) = P a (s, e ai , s i ) ∀ 1 ≤ i ≤ m, P c (t, e ci , t i )= P a (s, e ai , s i )=0 and we deduce then that it is impossible to obtain this case, an event cannot be splitted by many events and merged by one of these events at the same time.

Equivalence to Markov Chain refinement

P c (t, e ci , t i ) =

Conclusion and Future work

In this document, we have presented our proposition for introducing probabilities in Event-B. For now, we only propose a way to model purely probabilistic systems where all originally non-deterministic choices have been replaced with probabilistic choices in our new model. We also introduce a notion of refinement between two probabilistic Event-B models. In our proposition this notion of refinement mixes classical Event-B proof obligations with semantics-based new proof obligations. In the future, we plan on providing purely syntactical proof obligation in order to prove refinement between two Event-B models. Our last contribution is to show that this new notion of refinement between two probabilistic Event-B models coincides with refinement of their Markov Chain semantics.

In the future, we expect also to express probabilistic Event-B models containing both probabilistic and standard events, we intend to define a full syntax and semantics of these models and define a notion of refinement and the related proof obligations. It would be interesting also to annotate events by a probability range instead of an exact discrete probability and define a notion of refinement for these events. Once these perspectives have been developed, we will focus on other ideas like the development of a methodology for expressing and verifying some properties expressed in several probabilistic logics (PCTL, PLTL, PCTL*, PLTL*) on Event-B. Finally, all the work should be implemented in Rodin.

3 (

 3 Operational semantics of a Probabilistic Event-B model) The operational semantics of a probabilistic Event-B model M =(X, Init, Inv, Evts) is the discrete-time Markov chain [[M ]] = (S, M, l init , AP, L, Acts, P ) where

s

  ∈S,e∈Acts(s) P (s, e, s ) = 1

  Probabilistic Event-B model. M c =(X c , Init c , Inv c , Evts c ) is the concrete probabilistic Event-B model where: • X c = (x 1 , x 2 , ..., x k , ..., x n ) : the variables of M c , these variables take their values from the set D = D 1 × D 2 × ... × D k × D n and must satisfy the invariant Inv c .

2 2 :

 22 We propose in this section a new theorem expressing the relation between the refinement relation between probabilistic Event-B models and the refinement relation between their corresponding Markov chains semantics. We denote the refinement relation between probabilistic Event-B models by B Theorem Given two probabilistic Event-B models M c and M a , we have thatM c B M a ⇒ [[M c ]]R r [[M a ]].Proof. Let M a and M c be two probabilistic Event-B models such that M c B M a and let [[M a ]] and [[M c ]] be the corresponding discrete-time Markov chains, we prove that [[M c ]] R r [[M a ]]:The states S a and S c of the two Markov chains corresponds respectively to the different valuations of the variables of M a and M c . The equivalence relation L eq between the set of states S a and S c corresponds to the gluing invariant Inv c , two states s a and s c are equivalent if their valuations satisfies the invariant Inv c . The actions of each Markov chain corresponds to the names of the events in the corresponding Event-B model, then Acts a = α a (M a ) and Acts c = α c (M c ). The equivalence relation between actions E eq specifies if an event refines another one, if a concrete event named e c refine an abstract event named e a then we have e c E eq e a .The relationR r ⊆ S c × S a is a refinement relation between [[M c ]] and [[M a ]] ifwhenever tR r s where t ∈ S c and s ∈ S a we have: 1. (t, s) ∈ L eq 2. there exists a function δ : (Acts c × S c ) → ((Acts a × S a ) → [0, 1]) such that: a. for all e c ∈ Acts c , t ∈ S c such that P c (t, e c , t ) > 0, δ(e c , t ) is a distribution on (Evts a × S a ) b. ∀ s , e a ∈ S a × Acts a we have: t ∈Sc,ec∈Actsc P c (t, e c , t ).δ(e c , t )(e a , s ) = P a (s, e a , s ) c. ∀t , s , e c , e a ∈ S c × S a × Acts c × Acts a , if δ(e c , t )(e a , s ) > 0 then (t , s ) ∈ R r From the condition 2.b of R r we have: ∀s , e a ∈ S a × Acts a : t ∈Sc,ec∈Actsc P c (t, e c , t ).δ(e c , t )(e a , s ) = P a (s, e a , s ) this formula can be rewritten as: ∀s , e a ∈ S a × Acts a : t ∈{t1|(t1,s )∈Leq},ec∈{e|e∈Actsc∧(e,ea)∈Eeq} P c (t, e c , t ).δ(e c , t )(e a , s ) = P a (s, e a , s ) Many cases can be deduced from this condition: Case 1:card({t 1 |t 1 ∈ S c ∧ (t 1 , s ) ∈ L eq }) = 1 card({e|e ∈ Evts c ∧ (e, e a ) ∈ E eq }) = 1 card({s |s ∈ S a ∧ (s , t ) ∈ L eq }) = 1 card({e|e ∈ Evts a ∧ (e, e c ) ∈ E eq }) c , t )(e a , s )In this case, the action e a is refined by the action e c , i.e the corresponding event named e a in M a is refined by the event named e c in M c , the condition 2.b of the relation R r can be rewritten as: P c (t, e c , ).δ(e c , t )(e a , s ) = P a (s, e a , s ) or from the condition 2.a of R r , δ(e c , t ) is a distribution on (Evts a × S a ), then δ(e c , t )(e a , s )= 1, we deduce then that: P c (t, e c , t ) = P a (s, e a , s ) Case card({t 1 |t 1 ∈ S c ∧ (t 1 , s ) ∈ L eq }) = m > 1 card({e|e ∈ Evts c ∧ (e, e a ) ∈ E eq }) = m > 1 card({s |s ∈ S a ∧ (s , t ) ∈ L eq }) = 1 card({e|e ∈ Evts a ∧ (e, e c ) ∈ E eq }) = 1 c , t 1 )(e a , s ) δ(e c , t 2 )(e a , s ) δ(e c , t m )(e a , s )

P

  c (t, e ci , t i ) = P a (s, e a , s ) Case 3:card({t 1 |t 1 ∈ S c ∧ (t 1 , s ) ∈ L eq }) = 1 card({e|e ∈ Evts c ∧ (e, e a ) ∈ E eq }) = 1 card({s |s ∈ S a ∧ (s , t ) ∈ L eq }) = m > 1 card({e|e ∈ Evts a ∧ (e, e c ) ∈ E eq }) = m > 1

P

  a (s, e ai , s i ) Case 4:card({t 1 |t 1 ∈ S c ∧ (t 1 , s ) ∈ L eq }) = m > 1 card({e|e ∈ Evts c ∧ (e, e a ) ∈ E eq }) = m > 1 card({s |s ∈ S a ∧ (s , t ) ∈ L eq }) = m > 1 card({e|e ∈ Evts a ∧ (e, e c ) ∈ E eq }) = m > 1

P

  a (s, e ai , s i ) and m i=1

  We notice the witness predicate W (t, c, w, y) which is due to the fact that the abstract parameter t is no more used in the concrete event and is replaced by the concrete parameter y. The proof obligation rule is the following:

		evt
		refines
	0	evt 0
	any	any
	t	y
	where	where
	g(c, v, t)	H(y, c, w)
		with
	then	...
	...	t : W (t, c, w, y)
	end	then
		...
		end
	Axioms and theorems
	Abstract invariants and theorems
	Concrete invariants and theorems
	Concrete event guards
	Witness predicates for variables
	Abstract event specific guard

  1 , P 1 ) on Acts(M 1 ) × states(M 1 ) and (Ω 2 , F 2 , P 2 ) on Acts(M 2 ) × states(M 2 ). A strong probabilistic simulation relation between M 1 , M 2 is a relation R s ⊆ states(M 1 ) × states(M 2 ) where: 1. each start state of M 1 is related to at least one start state of M 2 , 2. for each s 1 R s s 2 and each step s 1→ (Ω 1 , F 1 , P 1 ) of M 1 , there exists a step s 2 → (Ω 2 , F 2 , P 2 ) of M 2 such that (Ω 1 , F 1 , P 1 ) ⊆ R (Ω 2 , F 2 , P 2 ), i.e, there exists a weight function w:Ω 1 × Ω 2 → [0, 1] such that: a. for each x ∈ Ω 1 , y∈Ω2 w(x, y) = P 1 [x], b. for each y ∈ Ω 2 , x∈Ω1 w(x, y) = P 2 [y],c. for each (x, y) ∈ Ω 1 × Ω 2 where x = (e c , s c ) and y = (e a , s a ), if w(x, y) > 0 then s c R s s a .The strong probabilistic simulation relation presented above concerns simple probabilistic automata when the probabilistic choice concerns the choice of the next state from a set of states by executing the same action a. Based on this definition and the definition of probabilistic bisimulation for probabilistic automata, we will define a new relation for probabilistic simulation between two discrete-time Markov chains. We present now the notion of equivalence class:

	Definition 9 (Equivalence Class)

Let S be a set of states and R an equivalence relation on S. For s ∈ S, [s] R denotes the equivalence class of state s under R, i.e, [s] R = {s ∈ S|(s, s ) ∈ R}. Note that for s ∈ [s] R , we have [s ] R = [s] R . The set [s] R is often referred to as the R-equivalence class of s. The quotient space of S under R, denoted by S/R= {[s] R |s ∈ S} is the set consisting of all R-equivalence classes. After providing the basic definitions related to probabilistic systems, we present now the definition of a new refinement relation between discrete-time Markov chains. Definition 10 (Discrete-time Markov chains refinement) Let M a =(S a , P a , s 0 , AP a , L a , Acts a ) and M c =(S c , P c , t 0 , AP c , L c , Acts c ) be two discrete-time Markov chains. Given a relation L eq ⊆ S a × S c between the set of states S a and S c and a relation E eq ⊆ Acts a × Acts c between the actions of the two Markov chains. We say that a relation R r ⊆ S c × S a is a refinement relation between M c and M a if whenever t R r s where t ∈ S c and s ∈ S a we have: 1. (t, s) ∈ L eq 2. there exists a function δ : (Acts c × S c ) → ((Acts a × S a ) → [0, 1]) such that: a. for all e c ∈ Acts c , t ∈ S c such that P c (t, e c , t ) > 0, δ(e c , t ) is a distribution on (Evts a × S a ) b. ∀ s , e a ∈ S a × Acts a we have: t ∈Sc,ec∈Actsc P c (t, e c , t ).δ(e c , t )(e a , s ) = P a (s, e a , s ) c. ∀ t , s , e c , e a ∈ S c × S a × Acts c × Acts a , if δ(e c , t )(e a , s ) > 0 then (t , s ) ∈ R r

  .e, a distribution on Ω 2 .

b. ∀ s , e a ∈ S a × Acts a we have: t ∈T,ec∈Actsc P c (t, e c , t ).δ(e c , t )(e a , s ) = P a (s, e a , s )

Proof 2: Merging of two probabilistic events by a probabilistic event.

  In the corresponding Markov chain semantics of M a and M c , suppose that the corresponding action of the event e a is enabled in a state s a of [[M a ]] and take [[M a ]] to a state s a . Suppose also that the corresponding action of the event e c is enabled in a state s c of [[M c ]] and take the system to a state s c such that (s a , s c ) ∈ L eq and (s a , s c ) ∈ L eq . This proof obligation mention that the probability of occurrence of the concrete event e c in the state s c taking the system to the state s c is equal to the probability of occurrence of the abstract event e a in the state s a taking the system to the state s a :P a (s a , e a , s a ) = P c (s c , e c , s c )The state s a is equivalent to the state s c The state s a is equivalent to the state s cThe probability of occurrence of the event e a in the state s a taking the system to the state s a is equal to the probability of occurrence of the concrete event e c in the state s c to the state s c (s a , s c ) ∈ L eq (s a , s c ) ∈ L eq P a (s a , e a , s a ) = P c (s c , e c , s c ) This proof is related to the case of merging of two abstract probabilistic events by a concrete probabilistic event. Suppose we have two abstract probabilistic events e a1 and e a2 that are merged by an event e c like presented below:

	a weight w a any t where t ⊕ | T ∧ G(t, v) then S p (t, v) end	e c weight w c any u where u ⊕ | U ∧ H(u, v ) then T p (u, v ) end
	e a1
	weight
	w a1
	any t 1 where t 1 ∈ T 1 ∧ G 1 (t 1 , v) then S p1 end e a2 weight w a2 any t 2 where t 2 ∈ T 2 ∧ G 2 (t 2 , v)	e c refines e a1 e a2 weight w c1 any u where u ∈ U ∧ H(u, w) then T end
	then
	S p2
	end

Splitting of an abstract probabilistic event by two concrete probabilistic events.

  taking the system to the state s a1 and e a2 in the state s a2 taking the system s a2 (s c , s a1 ) ∈ L eq (s c , s a2 ) ∈ L eq P a (s a1 , e a1 , s a1 )+P a (s a2 , e a2 , s a2 ) = P c (s c , e c , s c ) This proof is related to the case of splitting of a probabilistic event e a by two others probabilistic events e c1 and e c2 like presented below:

		e c1
		weight
		w c1
		refines
		e a1
		any
		u 1
	weight w a any t 1 where t 1 ∈ T 1 ∧ G 1 (t 1 , v) then S p1 (t 1 , v) end Proof 3: e a In the corresponding Markov chain semantics of M a	where u 1 ∈ U 1 ∧ H 1 (u 1 , w) then T p1 (u 1 , w) end e c2 weight w c2 refines e a1 any u 2 where u 2 ∈ U 2 ∧ H 2 (u 2 , w) then T p2 (u 2 , w) end

  , t 1 )(e a , s 1 ) δ(e c , t 1 )(e a , s 2 ) δ(e c , t 1 )(e a , s m ) In this case, the actions e a1 , e a2 , ..., e am are refined by the action e c , i.e, the corresponding events named e a1 , e a2 , ..., e am in M a are merged by the event named e c in M c . The condition 2.b of R (t, e c , t ).δ(e c , t )(e ai , s i ) = (s, e ai , s i ) or from the condition 2.a of R r , we have δ(e c , t ) is a distribution on Evts a × S a (

	then:			s 1 P a m P m i=1 i=1 δ(e c , t )(e ai , s i ) = m i=1 i=1 δ(e c , t )(e ai , s i )=1) e a1 δ(e c m P c (t, e c , t ) =
	t	e c	t	s 2	e a2	s
					e a3
				s m

r can be rewritten as: ∀i(1 ≤ i ≤ m), P c (t, e c , t ).δ(e c , t )(e ai , s i ) = P a (s, e ai , s i ) =⇒ m i=1 P c a (s, e ai , s i ) =⇒ P c (t, e c , t ).

Jean Raymond Abrial is an independent consultant and a research visitor at many academic and research units, he is the inventor of the Z method, the B method and the Event-B method.