Thu 8 Nov 2018 14:14 - 14:36 at Horizons 5 - Probabilistic Reasoning Chair(s): Antonio Filieri

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 \emph{abort}-command 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 \emph{abort}-command with an insufficient probability.

In this paper, we introduce the first probabilistic verification technique that accounts for uncertainty on the verification of long-run 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 \emph{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.

Thu 8 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

13:30 - 15:00
Probabilistic ReasoningResearch Papers at Horizons 5
Chair(s): Antonio Filieri Imperial College London
13:30
22m
Talk
Phys: Probabilistic Physical Unit Assignment and Inconsistency Detection
Research Papers
Sayali Kate Purdue University, USA, John-Paul Ore University of Nebraska-Lincoln, USA, Xiangyu Zhang Purdue University, Sebastian Elbaum University of Nebraska-Lincoln, USA, Zhaogui Xu Nanjing University, China
Pre-print
13:52
22m
Talk
Testing Probabilistic Programming Systems
Research Papers
Saikat Dutta University of Illinois at Urbana-Champaign, USA, Owolabi Legunsen University of Illinois at Urbana-Champaign, Zixin Huang University of Illinois at Urbana-Champaign, USA, Sasa Misailovic University of Illinois at Urbana-Champaign
14:14
22m
Talk
Verifying the Long-Run Behavior of Probabilistic System Models in the Presence of Uncertainty
Research Papers
Yamilet R. Serrano Llerena National University of Singapore, Singapore, Marcel Böhme Monash University, Marc Brünink nil, Singapore, Guoxin Su University of Wollongong, Australia, David Rosenblum National University of Singapore