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, we first provide 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, so also embedding program fragments. We study basic properties of this specification language, such as weakening and distribution, that can support reasoning systems. Finally, we demonstrate the use of pDL to reason about program behavior.
翻译:对概率语言的语义进行了广泛的研究,但对其属性的语义的规格语言很少引起注意。本文件介绍了概率动态逻辑 pDL,这是McIver和Morgan 的概率保护指令语言(pGCL)中程序的一种逻辑。 拟议的逻辑pDL 既能表达第一顺序状态特性,又能表达概率可达性特性,同时处理pGCL的非确定性和概率选择操作员。 为了准确解释规格的含义,我们正式定义了 pDL 的满意度关系。 由于pDL 将 pGCL 程序嵌入其框式模式操作器中, 我们首先为pGCL 程序提供一个正式的 MDP 语义。 满意度关系建模于 PCTL 之后, 但从建议性逻辑设置扩展为第一顺序, 并嵌入程序碎片。 我们研究了该规格语言的基本属性, 如变弱和分布, 从而支持推理系统。 最后, 我们展示了 PDL 用于程序行为的理由 。