Quantitative Programming and Continuous-Time Markov Chains

In recent works we have introduced the quantitative programming paradigm which provides a framework for the formal verification of concurrent programs. By partitioning the set of program states into bisimulation equivalence classes, this paradigm enables the formal verification of concurrent programs with large state spaces. For formal verification, (as in our previous works) we employ probabilistic model checking techniques. To enable formal verification, the programmer must bound the ranges of variables, and programs are translated into corresponding finite state probabilistic models. In this paper we introduce new constructions for quantitative programming that enable the programmer to maintain the compliance between the program under verification and the corresponding probabilistic model, taking into consideration the execution rates of program statements. For formal verification we use continuous-time Markov chains and a notion of strong bisimulation specific to stochastic process algebras. We present formal verification experiments performed using PRISM probabilistic model checker.