Some Methods for Qualifying Properties

of Probabilistic Programs

 

Jolanta Koszelew

Institute of Computer Science

Technical University of Bialystok

Wiejska 45 A 15-351 Bialystok, Poland

e-mail : jolka@ii.pb.bialystok.pl

 

Key words. probabilistic programs, Markov chain, program termination, random variable, modelling stochastic processes

In this work, some methods and tools for a quantitative analysis of iterative probabilistic programs are proposed . The need for analyse of probabilistic programs arises in two main situations. The first is when we analyse a probabilistic program whose nondeterministic constructions are realised with known probability distribution, and we wish to infer some statistical property of the program, such as its average running time, the expected value of some output state, the probability of program termination, etc. Another situation is that of a probabilistic programs where we know a set of all possible distributions for realisation of nondeterministic constructions. For that case, the method of determining average probability of program termination in a fixed state is presented.

First situation: Probabilistic Programs are understood as iterative programs with two probabilistic constructions: x:= ? , either ... or ... interpreted as follows: the first corresponds to a random generation of a value of the variable x, each part of the second one is choosen with the probability 1/2. Each possible valuation of program variables appears with known probability. Thus one can define distributions of probabilities on sets of input and output valuations and therefore programs are interpreted as mappings transforming input distributions into output distributions. In the case of probabilistic programs interpreted in a finite universe, there is an effective algebraic method (cf. [2]) for determining probabilities of transitions from an initial distribution to a to a final one.

The similarities between such programs and finite - state Markov chains enable to adopt the results for searching properties of probabilistic algorithms. On the other hand , the composiotin (decomposition) problem for the probabilistic programs can not be solved using Markov chains theory. Contrary to Markov chains, probabilistic algorithms preserve an internal structure of stochastic processes which are modelled. For example : M is a program which simulates cooperation of two alarms: x and y. Each of them can work in a „good" state (denote by 1) or „bad" state (0).

M : begin

while (x=1) and (y=1) do

{ M’:} begin x:=?; y:=?; end;

end;

If we treat such program as Markov chain we can analyse only one matrix M corresponding to whole program M. We can not determine a sub-matrix M’ which is corresponding to a sub-program M’ . The original method for composition (decomposition) of probabilistic programs is proposed.

Second situation: The exact distribution for nondeterministic construction of the form: x:=? is unknown but an information about the set Z of all admissible probability distributions is given.

Moreover, we known that each distribution r _k Î Z appears with a probability f_k . Then we can determine average case matrix , which describes an average probabilities of transition from state to state.

Let us consider the same program M. Let us assume, that the set Z is the same for both devices and is defined as follows: Z={r _k: : r _k (1)=q_k r _k(1)=1-q_k where q_k Î <0.7,1>}.

Proposed method unable us to determine an average probability of event that alarm x and alarm y will be in „bad" state simultaneously (x=0 and y=0) for a given probability distribution f_k (for all elements of a set Z). If f_k is the following: then the exact result is : 0.02504 and its practical interpretation is : An average risk, that this control system is deceptive is equal to 2,5% under condition that a probability of „ bad" state for alarm x and y (independent)

is not greater then 0.3.

A prototype of computer system for automatically analysis of statistical properties of probabilistic programs is prepared and implemented. The above problems : composition (decomposition) and „ average case" of probabilistic programs arise during a work on this system.

References

[1] Bhararucha, A., T. , Elements of the Theory of Markov Processes and Their Applications,

McGraw- Hill , New York 1960.

[2] Danko W., The set of probabilistic algorithmic formulas valid in a finite

structure is decidable with respect to its diagram, Fundamenta Informaticae,

vol. 19, 3-4, 1993, (417-431)

[3] Koszelew J., Analiza porównawcza algorytmów probabilistycznych i łancuchów

Markowa , Symulacja w badaniach i rozwoju, zbiór referatów Trzecich

Warsztatów Naukowych PTSK Wigry , 26 - 28 września 1996 r.