Probabilistic Epistemic Dynamic Agentive Logic
Logic in Computer Science
2026-04-27 v1
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.
Cite
@article{arxiv.2604.22042,
title = {Probabilistic Epistemic Dynamic Agentive Logic},
author = {Shay Allen Logan},
journal= {arXiv preprint arXiv:2604.22042},
year = {2026}
}
Comments
15 pages