Towards a Proof System for Probabilistic Dynamic Logic

TL;DR

This paper explores developing a formal proof system for probabilistic dynamic logic (pDL), aiming to verify properties of probabilistic programs by extending dynamic logic with probabilistic reasoning.

Contribution

It introduces a work-in-progress deductive proof system for pDL, enabling formal verification of probabilistic program properties through symbolic execution.

Findings

Conceptual framework for a proof system for pDL

Extension of dynamic logic with probabilistic reasoning

Work in progress towards a formal verification tool

Abstract

Whereas the semantics of probabilistic languages has been extensively studied, specification languages for their properties have received less attention -- with the notable exception of recent and on-going efforts by Joost-Pieter Katoen and collaborators. In this paper, we revisit probabilistic dynamic logic (pDL), a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. Building on dynamic logic, pDL can express both first-order state properties and probabilistic reachability properties. In this paper, we report on work in progress towards a deductive proof system for pDL. This proof system, in line with verification systems for dynamic logic such as KeY, is based on forward reasoning by means of symbolic execution.