带奖励的马尔可夫决策过程的轻量级蒙特卡洛验证

马尔可夫决策过程是并发优化问题的有用模型，但对于穷举验证方法而言通常难以处理。近期的工作引入了直接从调度器空间采样的轻量级近似技术，为标准数值模型检测算法带来了可扩展替代方案的前景。迄今为止的焦点一直在于优化某个属性的概率，但许多问题需要对奖励进行定量分析。因此，在这项工作中，我们提出了用于优化马尔可夫决策过程奖励的轻量级统计模型检测算法。我们考虑了模型检测中使用的标准奖励定义，并引入了一个辅助假设检验以适应可达性奖励。我们在多个标准案例研究上展示了我们方法的性能。