Probabilistic Epistemic Dynamic Agentive Logic

TL;DR

PEDAL is a probabilistic epistemic logic designed to model an agent's knowledge state during program specification verification, extending PDL with probability measures and a sound, complete proof system.

Contribution

It introduces PEDAL, a novel probabilistic epistemic logic based on PDL, with a Hilbert system and discussions on overcoming proof infinitary challenges.

Findings

PEDAL is built on PDL with probability measures on program valuations.

A Hilbert system for PEDAL is proved sound and complete.

Discussion on methods to circumvent infinitary proof difficulties.

Abstract

I introduce PEDAL -- a probabilistic epistemic logic meant to capture, in propositional dynamic terms, the epistemic state of an agent engaged in checking whether a program meets its specification. Semantically, PEDAL is built `on top of' PDL and uses probability measures defined on the set of possible program valuations of an otherwise-specified PDL-model. A Hilbert system with one infinitary rule is provided and proved to be sound and complete. Near the end, I discuss possible ways to circumvent infinitary proof difficulties.