The project will be divided in four sub-projects, we first detailed the scientific issues and then the participation of partners will be given.

Since in model checking formalism, models are checked to see if the considered measures are guaranteed or not, bounding techniques become useful. We propose to apply Stochastic Comparison technique for numerical stochastic model checking. The main advantage of this approach is the possibility to derive transient as well as steady-state bounding distributions. In fact, in model checking formalism, steady-state operators can be checked through steady-state distribution, path-based operators can be checked through transient analysis [2].

We have a large experience of this technique in performance evaluation issues [3, 7, 9]. Especially we have developed an algorithmic approach of this technique which lets to obtain bounding models in an automatic manner. Hence this approach can be easily implemented in model checkers.

Recently, we have applied this approach for stochastic model checking. In [14], we consider PRCTL model checking formalism, and we propose to check state formulae by using stochastic bounding techniques. In this work, state formulae with rewards for large DTMCs are checked by considering aggregated bounding Markov chains to overcome the state space explosion problem. We introduce a framework on how lumpable bounding models can be constructed, depending on the model and on the operator of interest. In fact we apply an algorithm to provide lumpable bounding models, but the state space partition and ordering of states must be compatible with the underlying formula. Obviously, it is not always possible to decide if the operator is satisfied or not through the bounding model. However in this case bounding model can be refined but with more complexity in terms of number of states.

In [4], we propose to construct bounding models having a special structure which provides closed-formsolutions to compute both transient and steady-state distributions. In this work, we present an algorithm to provide rapid model checking by means of these closed-form bounding distributions for CSL logic.

Clearly, bounding distributions may not let to decide if the underlying model meets the probability thresholds or not. However in the case where the model can be checked by the proposed method, we gain significantly in time and memory complexity.

We consider to apply this approach for other model checking formalisms. On the other hand, we intend to apply the proposed algorithms to check different real application models.

           Stochastic Model Checking and Perfect Simulation

In general numerical methods provide high accuracy but they are memory intensive which often leaves statistical solution techniques as a last resort [19, 17]. These works are based on Monte Carlo simulation and statistical hypothesis testing of samples and they consider CSL model checking formalism.

We propose to apply perfect simulation for statistical model checking. This technique has been proposed by Propp & Wilson [12] which lets to sample according to the stationary distribution. They have shown that by coupling in the past, it is possible to sample exactly the steady-state distribution of the underlying Markovian model. Thus the stopping criteria of Monte-Carlo method has been vanished, and there is no  difference with respect to direct numerical methods. In this method we must keep a trajectory per state beginning at time "-1" and a sample is obtained when they are coupled at time 0. The convergence has been theoretically established for finite state space Markov chains. However the infamous state space explosion problem will arise again because of the fact that we must consider all trajectories beginning from each state. In some cases this problem can be avoided by doing monotonous perfect simulation.

           Stochastic Monotonicity and Coupling

We consider the most known stochastic comparison relation <st. First we give the definition for two random variables X, Y : if X <st Y then Prob(X > a) <=Prob(Y > a) . In fact there are different stochastic orders associated to different families of functions. <st is associated to increasing function, obviously it is possible to consider weaker stochastic orders, for instance increasing convex order. This order is weaker then the <st order to compare random variables, but the stochastic monotonicity of such orders are in general more difficult to establish. Let us first define the stochastic monotonicity a stochastic model Xi: if X0 <st X1 then Xi < st Xi+1 and if the steady-state exists X1 the convergence will be in increasing. On the other hand if X0 <st X1 then the convergence will be decreasing. The main reason to apply the <st order is the coupling property of this order (Strassen’s theorem [18]). X <st Y if and only if there exist the realisations of  X (X) and Y ( Y ) such that  X<= Y .

All of the partners involved in this projet have a large experience of this method, coupling of trajectories. They have applied in to construct bounding models having "easier" numerical solutions and/or to study monotonicity properties. Therefore all of the partners will participate this sub-project. We consider to study this concept in order to find solutions for two aspects : First in order to provide transient perfect simulation to study transient operators in model checking. Secondly, the algorithmic stochastic comparison approach is based on the stochastic monotonicity, however it is developed for totally ordered state spaces. We extend it to partially ordered state spaces which will provide more accurate bounding models.

           Infinite Space Stochastic Model Checking

For a significant class of systems, the abstractionmodels turn out to be infinite space. In this case the classical numerical and statistical methods can not be applied. However matrix-geometric methods can be applied in some cases to numerically analyze underlying models. Stochastic model checking has been restricted to finite state spaces. Recently, an extension for infinite state spaces has been proposed by establishing crossfertilization between performance evaluation techniques and logic-based model checking algorithms for Markov chains [15].

It has been shown that in the case where the underlyingMarkov chain is monotone in the sense of the <st order, it is possible to provide lower bounds by truncating the infinite state space. Bounding models by means of the stochastic monotonicity would be useful in some cases for stochastic model checking. On the other hand, Partner 5 has a large experience on the numerical methods of Markov chains, we envisage to explore other numerical methods for infinite Markov chains to apply in stochastic model checking context.