Towards a Proof System for Probabilistic Dynamic Logic
Einar Broch Johnsen, Eduard Kamburjan, Raúl Pardo, Erik Voogd, Andrzej Wąsowski
TL;DR
The paper addresses the lack of a deductive specification framework for probabilistic programs by advancing probabilistic dynamic logic ($pDL$) as a expressive, forward-reasoning-based specification language grounded in dynamic logic. It develops a forward symbolic-execution proof system for $pDL$ applied to pGCL programs, generating probabilistic constraints that are discharged by an SMT solver, and demonstrates a Crowbar/Z3 prototype implementation. A Monty Hall example and formal definitions of MDP semantics for pGCL illustrate how $[s]_{\boldsymbol{p}}\varphi$ specs capture probabilistic reachability under nondeterminism. The work contributes a practical, forward-deductive verification approach and a foundation for reasoning about probabilistic loops, with promising directions for integration with existing weakest-preexpectation methods and extended language features to broaden applicability in probabilistic programming verification.
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.