一句话：研究在不确定性存在时，对概率系统模型的长期行为进行概率验证，并以概率验证器检验长期性质。
论文关注随机系统达到平衡态后的状态性质验证，这类验证在安全关键系统中具有重要应用，例如检查系统是否能在任意时刻以足够高的概率接受人类中止命令。其核心流程是将随机系统表示为概率模型，形式化地断言一条长期性质，再由概率验证器检查该模型是否满足所断言的性质。标题进一步指出验证是在不确定性存在的情况下进行的，但摘要本身未说明所处理不确定性的具体类型、算法细节、案例研究或实验数值。因此，该工作可理解为面向概率模型长期行为与不确定性问题的概率验证研究。
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.
DOI 原文 ·
@inproceedings{paperbot4580,
title = {Verifying the long-run behavior of probabilistic system models in the presence of uncertainty},
author = {Yamilet R. Serrano Llerena and Marcel Böhme and Marc Brünink and Guoxin Su and David S. Rosenblum},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3236078}
}