A Specification Logic for Programs in the Probabilistic Guarded Command Language (Extended Version)

TL;DR

This paper introduces pDL, a formal specification logic for probabilistic programs in pGCL, enabling precise reasoning about both state and probabilistic reachability properties using a formal MDP semantics.

Contribution

It develops pDL, a novel logic that combines first-order and probabilistic reasoning for pGCL programs, extending existing probabilistic logics with a formal semantics and reasoning support.

Findings

pDL can express complex probabilistic properties of pGCL programs.

The logic supports reasoning about program behavior and properties.

Formal properties like weakening and distribution are established for pDL.

Abstract

The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language (pGCL) of McIver and Morgan. The proposed logic pDL can express both first-order state properties and probabilistic reachability properties, addressing both the non-deterministic and probabilistic choice operators of pGCL. In order to precisely explain the meaning of specifications, we formally define the satisfaction relation for pDL. Since pDL embeds pGCL programs in its box-modality operator, pDL satisfiability builds on a formal MDP semantics for pGCL programs. The satisfaction relation is modeled after PCTL, but extended from propositional to first-order setting of dynamic logic, and also embedding program fragments. We study basic properties of pDL, such as weakening and distribution, that can support reasoning systems. Finally, we demonstrate the use of pDL to reason about program behavior.