Probabilistic process algebra

Every day we witness the fast development of the hardware and software technology. This, of course, is the reason that new and more complex systems controlled by some kind of computational-based devices become an unseparated part of our daily life. As more as the system complexity increases, as more the reasoning about its correct behaviour becomes dif??cult. A variety of consequences may occur as a result of a failure, ranging from simple annoying to life threatening ones. Thus for some systems it is crucial that they exhibit a correct functioning. However, for systems with an extremely complex construction it is almost impossible to give an absolute guarantee for their correctness. In this case, it is still satisfactory to know that the possibility for a system to fail is low enough. Formal methods have been developed for establishing correctness of computer systems. They provide rigorous methods with which one can formally specify properties of a systems's intended behaviour, and also can check if the system conforms to that speci??cation. In case of complex systems we need a formal method that allows us to reason in compositional way, it provides us with techniques that can be used to build larger systems from the composition of smaller ones. Process algebra carries exactly this idea; it provides operators that allow to compose processes in order to obtain a more complex process. Besides, every process algebra contains a set of axioms. Every axiom is an algebraic equation that carries our intuition and insight in process behaviour, it expresses which two processes behaviour we consider equal. In such a way, manipulation with processes becomes manipulation with equations in the algebraic sense. But, equations and operators do not have any meaning unless we place them in a certain real ¿world¿ and match the terms of the process algebra with the entities of the real world. This step is traditionally called ¿giving a semantic of the syntax¿. The structure constructed in this way is called a model of the considered process algebra. For every given process algebra we can construct an in??nite number of models, but only several of them are interesting for the purpose process algebra was developed as a formal method. However, there is a tendency always to use so-called a bisimulation model. In this thesis we propose several process algebras and construct their models based on the notion of bisimulation.