Distributional probabilistic model checking
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 p...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer
2024
|
| _version_ | 1826313287442104320 |
|---|---|
| author | Elsayed-Aly, I Parker, D Feng, L |
| author_facet | Elsayed-Aly, I Parker, D Feng, L |
| author_sort | Elsayed-Aly, I |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-04-09T03:56:07Z |
| format | Conference item |
| id | oxford-uuid:84fccc86-9169-4755-91bd-73f2057d0528 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-09-25T04:10:41Z |
| publishDate | 2024 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:84fccc86-9169-4755-91bd-73f2057d05282024-06-20T10:58:39ZDistributional probabilistic model checkingConference itemhttp://purl.org/coar/resource_type/c_5794uuid:84fccc86-9169-4755-91bd-73f2057d0528EnglishSymplectic ElementsSpringer2024Elsayed-Aly, IParker, DFeng, LProbabilistic 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. |
| spellingShingle | Elsayed-Aly, I Parker, D Feng, L Distributional probabilistic model checking |
| title | Distributional probabilistic model checking |
| title_full | Distributional probabilistic model checking |
| title_fullStr | Distributional probabilistic model checking |
| title_full_unstemmed | Distributional probabilistic model checking |
| title_short | Distributional probabilistic model checking |
| title_sort | distributional probabilistic model checking |
| work_keys_str_mv | AT elsayedalyi distributionalprobabilisticmodelchecking AT parkerd distributionalprobabilisticmodelchecking AT fengl distributionalprobabilisticmodelchecking |