A Z-Based Formalism to Specify Markov Chains

Probabilistic techniques in computer programs are becoming more and more widely used. Therefore, there is a big interest in methods for formal specification, verification, and development of probabilistic programs. In this paper, we introduce a Z-based formalism that assists us to specify probabilistic programs simply. This formalism is mainly based on a new notion of Z operation schemas, called probabilistic schemas, and a new set of schema calculus operations that can be applied on probabilistic schemas as well as ordinary operation schemas. To demonstrate the applicability of this formalism, we show that any probabilistic system modelled with Markov chains can be formally specified using the new formalism. More precisely, we show the resulting formalism can be used to specify any discrete-time and continues-time Markov chain. Since our formalism is obtained from enriching Z with probabilistic notions, unlike notations such as Markov chains, it is appropriate for modelling both probabilistic and functional requirements simultaneously. In addition, since we provide an interpretation of our formalism in the Z notation itself, we can still use Z tools, such as Z-eves to check the type and consistency of the written specifications formally. For the same reason, we can still use various methods and tools which are targeted for formal validation, verification and program development based on the Z specification language.