Verifying the long-run behavior of probabilistic system models in the presence of uncertainty

Yamilet R.Serrano Llerena, Marcel Böhme, Marc Brünink, Guoxin Su, David D. Rosenblum

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

1 Citation (Scopus)

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 languageEnglish
Title of host publicationESEC/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 publicationNovember 4–9, 2018 Lake Buena Vista, FL, USA
EditorsGary T. Leavens, Alessandro Garci, Corina S. Pasareanu
Place of PublicationNew York NY USA
PublisherAssociation for Computing Machinery (ACM)
Pages587-597
Number of pages11
ISBN (Electronic)9781450355735
DOIs
Publication statusPublished - 2018
EventJoint 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 20189 Nov 2018
Conference number: 26th
https://conf.researchr.org/home/fse-2018

Conference

ConferenceJoint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering 2018
Abbreviated titleESEC/FSE 2018
CountryUnited States of America
CityLake Buena Vista
Period4/11/189/11/18
Internet address

Keywords

  • Discrete-Time Markov Chains
  • Long-Run Properties
  • Perturbation Analysis
  • Probabilistic Model Checking
  • Uncertainty

Cite this

Llerena, Y. R. S., Böhme, M., Brünink, M., Su, G., & Rosenblum, D. D. (2018). Verifying the long-run behavior of probabilistic system models in the presence of uncertainty. In G. T. Leavens, A. Garci, & C. S. Pasareanu (Eds.), ESEC/FSE'18 - Proceedings of the 2018 26th ACM Joint Meeting on European Soware Engineering Conference and Symposium on the Foundations of Soware Engineering: November 4–9, 2018 Lake Buena Vista, FL, USA (pp. 587-597). Association for Computing Machinery (ACM). https://doi.org/10.1145/3236024.3236078