论文标题
概率保护命令语言中程序的规范逻辑（扩展版）
A Specification Logic for Programs in the Probabilistic Guarded Command Language (Extended Version)
论文作者
论文摘要
概率语言的语义已经进行了广泛的研究，但是其属性的规范语言很少受到关注。本文介绍了概率动态逻辑PDL，这是McIver和Morgan的概率保护命令语言（PGCL）中程序的规范逻辑。提出的逻辑PDL可以同时表达一阶状态特性和概率可及性属性，从而解决了PGCL的非确定性和概率选择算子。为了准确解释规范的含义，我们正式定义了PDL的满意关系。由于PDL将PGCL程序嵌入其盒子模式运算符中，因此PDL的满意度基于PGCL程序的正式MDP语义。满意度的关系是在PCTL之后建模的，但从命题到动态逻辑的一阶设置以及嵌入程序片段。我们研究PDL的基本特性，例如弱化和分布，可以支持推理系统。最后，我们演示了使用PDL来推理程序行为。
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.
