Quantitative Programming and Markov Decision Processes

Quantitative programming (or performance evaluation programming) is a programming paradigm, which supports the formal verification of (bounded versions of) concurrent programs by using model checking techniques. By partitioning the state space of programs into bisimulation equivalence classes, this approach enables the formal verification of programs with large state spaces. The paradigm was introduced by us in previous works by developing an experimental concurrent language designed to facilitate the construction of probabilistic models that capture the behavior of programs and that can be verified by using probabilistic model checking techniques. The experimental language introduced in previous works is extended in this paper with constructions which enable the specification of behavioral equivalence classes. Concurrent programs are translated into corresponding probabilistic models, which are analyzed by using the PRISM probabilistic model checker. The programmer identifies bisimulation equivalence classes to enable the formal verification of programs with large state spaces. For formal verification, we employ Markov Decision Processes.