Probabilistic model checking can provide formal guarantees on the behavior of stochastic models relating to a wide range of quantitative properties, such as runtime, energy consumption or cost. But decision making is typically with respect to the expected value of these quantities, which can mask important aspects of the full probability distribution such as the possibility of high-risk, low-probability events or multimodalities. We propose a distributional extension of probabilistic model checking, applicable to discrete-time Markov chains (DTMCs) and Markov decision processes (MDPs). We formulate distributional queries, which can reason about a variety of distributional measures, such as variance, value-at-risk or conditional value-at-risk, for the accumulation of reward until a co-safe linear temporal logic formula is satisfied. For DTMCs, we propose a method to compute the full distribution to an arbitrary level of precision, based on a graph analysis and forward analysis of the model. For MDPs, we approximate the optimal policy with respect to expected value or conditional value-at-risk using distributional value iteration. We implement our techniques and investigate their performance and scalability across a range of benchmark models. Experimental results demonstrate that our techniques can be successfully applied to check various distributional properties of large probabilistic models.

翻译：概率模型检验能够对随机模型的行为提供形式化保证，涵盖运行时间、能量消耗或成本等广泛的定量属性。然而，决策通常基于这些量的期望值，这可能掩盖全概率分布中的重要特征，例如高风险低概率事件或多峰分布的可能性。我们提出概率模型检验的分布式扩展，适用于离散时间马尔可夫链（DTMCs）和马尔可夫决策过程（MDPs）。我们制定了分布式查询，能够针对多种分布度量进行推理，例如方差、风险价值或条件风险价值，用于在满足共安全线性时序逻辑公式之前的奖励累积。对于DTMCs，我们提出了一种基于图分析与模型前向分析的方法，以任意精度计算完整分布。对于MDPs，我们使用分布式价值迭代近似最优策略，该策略分别针对期望值或条件风险价值进行优化。我们实现了所提出的技术，并在多个基准模型上研究了其性能与可扩展性。实验结果表明，我们的技术能够成功应用于检查大规模概率模型的各种分布属性。