Probabilistic Epistemic Dynamic Agentive Logic
This work offers a formal framework for integrating probabilistic and epistemic reasoning in program verification, but it is primarily a theoretical/logical contribution without empirical validation.
The paper introduces PEDAL, a probabilistic epistemic logic for reasoning about an agent's knowledge while verifying program correctness, and provides a sound and complete Hilbert system with one infinitary rule.
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.