Bounded Model Checking for PHL

Simon Engel

In the context of formal verification, model checking is the automated process of proving or disproving that a formal model of a system satisfies a given property. This property may be specified in a specialized specification language such as a temporal logic. PHL (Probabilistic Hyper Logic) is a relatively new temporal logic for specifying probabilistic hyperproperties of Markov decision processes (MDPs). PHL was first proposed a year ago by Dimitrova, Finkbeiner, and Torfah, who also developed two model checking algorithms for a fragment of PHL. One of these algorithms involves synthesizing a so-called scheduler for an MDP, applying this scheduler to the MDP, and then checking whether the resulting system satisfies a given probabilistic constraint. This process is iterated until either an adequate scheduler is found, or all schedulers up to a certain size have been checked. This thesis presents an approach to eliminating this guess-and-check loop. The key to this approach is an improved scheduler synthesis procedure that is able to immediately find an adequate scheduler, if such a scheduler exists, and that can even synthesize an optimal scheduler that maximizes or minimizes a given probability expression. A first feasibility study shows that scheduler synthesis for a simple property and small MDPs can be performed on ordinary hardware, but suggests that further optimization will be necessary to make this approach viable for real-world use cases.

Bachelor Thesis.

(pdf)