[EPF24] Ingy Elsayed-Aly, David Parker and Lu Feng. Distributional Probabilistic Model Checking. In Proc. 16th NASA Formal Methods Symposium (NFM'24), volume 14627 of LNCS, pages 57-75, Springer. June 2024. [pdf] [bib] [Proposes a probabilistic model checking framework for distributional queries, implemented as an extension of PRISM.]
Downloads:  pdf pdf (1.76 MB)  bib bib
Notes: The original publication is available at link.springer.com.
Links: [Google] [Google Scholar]
Abstract. Probabilistic model checking provides formal guarantees for stochastic models relating to a wide range of quantitative properties, such as runtime, energy consumption or cost. But this 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, for 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 or cost 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 using distributional value iteration. We implement our techniques and investigate their performance and scalability across a range of large benchmark models.