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 S. Rosenblum · 2018
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 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.