Raúl Pardo will give a talk about his work on A Specification Logic for Programs in the Probabilistic Guarded Command Language. Details below.
SPEAKER
Raúl Pardo, Prof., ITU.
TITLE
A Specification Logic for Programs in the Probabilistic Guarded Command Language
ABSTRACT
The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention. In this talk, I present 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.
This work has been accepted for publication at ICTAC’22. Pre-print available at https://arxiv.org/abs/2205.04822