TY - GEN
T1 - A Specification Logic for Programs in the Probabilistic Guarded Command Language
AU - Pardo, Raúl
AU - Broch Johnsen, Einar
AU - Schaefer, Ina
AU - Wasowski, Andrzej
PY - 2022/10
Y1 - 2022/10
N2 - 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.
AB - 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.
KW - Probabilistic Dynamic Logic
KW - Probabilistic Guarded Command Language
KW - First-Order State Properties
KW - Probabilistic Reachability
KW - Markov Decision Processes
KW - Probabilistic Dynamic Logic
KW - Probabilistic Guarded Command Language
KW - First-Order State Properties
KW - Probabilistic Reachability
KW - Markov Decision Processes
U2 - 10.1007/978-3-031-17715-6_24
DO - 10.1007/978-3-031-17715-6_24
M3 - Article in proceedings
SN - 978-3-031-17714-9
VL - 13572
T3 - Proceedings of 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022
BT - A Specification Logic for Programs in the Probabilistic Guarded Command Language
PB - Springer, Cham
T2 - 19th International Colloquium on Theoretical Aspects of Computing - ICTAC 2022
Y2 - 27 September 2022 through 30 September 2022
ER -