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

Producción científica: Capítulo del libro/informe/acta de congresoContribución a la conferenciarevisión exhaustiva

7 Citas (Scopus)

Resumen

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.

Idioma originalInglés
Título de la publicación alojadaESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering
EditoresAlessandro Garci, Corina S. Pasareanu, Gary T. Leavens
EditorialAssociation for Computing Machinery, Inc
Páginas587-597
Número de páginas11
ISBN (versión digital)9781450355735
DOI
EstadoPublicada - 26 oct. 2018
Evento26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018 - Lake Buena Vista, Estados Unidos
Duración: 4 nov. 20189 nov. 2018

Serie de la publicación

NombreESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Conferencia

Conferencia26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018
País/TerritorioEstados Unidos
CiudadLake Buena Vista
Período4/11/189/11/18

Huella

Profundice en los temas de investigación de 'Verifying the long-run behavior of probabilistic system models in the presence of uncertainty'. En conjunto forman una huella única.

Citar esto