Abstract
Verifying that a stochastic system is in a certain state when it has reached equilibrium has important applications. For instance, the probabilistic verification of the long-run behavior of a safety-critical system enables assessors to check whether it accepts a human abortcommand at any time with a probability that is sufficiently high. The stochastic system is represented as probabilistic model, a long-run property is asserted and a probabilistic verifier checks the model against the property. However, existing probabilistic verifiers do not account for the imprecision of the probabilistic parameters in the model. Due to uncertainty, the probability of any state transition may be subject to small perturbations which can have direct consequences for the veracity of the verification result. In reality, the safety-critical system may accept the abort-command with an insufficient probability. In this paper, we introduce the first probabilistic verification technique that accounts for uncertainty on the verification of longrun properties of a stochastic system. We present a mathematical framework for the asymptotic analysis of the stationary distribution of a discrete-time Markov chain, making no assumptions about the distribution of the perturbations. Concretely, our novel technique computes upper and lower bounds on the long-run probability, given a certain degree of uncertainty about the stochastic system.
Original language | English |
---|---|
Title of host publication | ESEC/FSE'18 - Proceedings of the 2018 26th ACM Joint Meeting on European Soware Engineering Conference and Symposium on the Foundations of Soware Engineering |
Subtitle of host publication | November 4–9, 2018 Lake Buena Vista, FL, USA |
Editors | Gary T. Leavens, Alessandro Garci, Corina S. Pasareanu |
Place of Publication | New York NY USA |
Publisher | Association for Computing Machinery (ACM) |
Pages | 587-597 |
Number of pages | 11 |
ISBN (Electronic) | 9781450355735 |
DOIs | |
Publication status | Published - 2018 |
Event | Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering 2018 - Lake Buena Vista, United States of America Duration: 4 Nov 2018 → 9 Nov 2018 Conference number: 26th https://conf.researchr.org/home/fse-2018 |
Conference
Conference | Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering 2018 |
---|---|
Abbreviated title | ESEC/FSE 2018 |
Country/Territory | United States of America |
City | Lake Buena Vista |
Period | 4/11/18 → 9/11/18 |
Internet address |
Keywords
- Discrete-Time Markov Chains
- Long-Run Properties
- Perturbation Analysis
- Probabilistic Model Checking
- Uncertainty