Probabilistic Model Checking and Autonomy
Probabilistic Model Checking and Autonomy
复制标题
概率模型检查和自治
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
D. Parker
中科院分区：
文献类型：
--
作者：
M. Kwiatkowska;G. Norman;D. Parker
通过形式化的建模和分析，可以方便地设计和控制在不确定或对抗性环境中运行的自治系统。概率模型检测是一种针对给定的时态逻辑规范自动验证系统模型是否满足规范，并为其控制综合最优策略的技术。这种方法最近被扩展到通过随机博弈和均衡策略的合成来建模的竞争或合作行为的多智能体系统。在本文中，我们提供了概率模型检查的概述，重点是PRISM和PRISM-GAMES模型检查器支持的模型。该综述包括完全可观测和部分可观测的马尔可夫决策过程，以及基于回合和并发的随机博弈，以及相关的概率时态逻辑。通过自治系统的实例说明了该框架的适用性。最后，我们强调了研究面临的挑战，并为该领域未来的工作提出了方向。《控制、机器人和自主系统年度回顾》第5卷预计最终在线出版日期为2022年5月。有关修订后的估计数字，请参阅http://www.annualreviews.org/page/journal/pubdates。
The design and control of autonomous systems that operate in uncertain or adversarial environments can be facilitated by formal modeling and analysis. Probabilistic model checking is a technique to automatically verify, for a given temporal logic specification, that a system model satisfies the specification, as well as to synthesize an optimal strategy for its control. This method has recently been extended to multiagent systems that exhibit competitive or cooperative behavior modeled via stochastic games and synthesis of equilibria strategies. In this article, we provide an overview of probabilistic model checking, focusing on models supported by the PRISM and PRISM-games model checkers. This overview includes fully observable and partially observable Markov decision processes, as well as turn-based and concurrent stochastic games, together with associated probabilistic temporal logics. We demonstrate the applicability of the framework through illustrative examples from autonomous systems. Finally, we highlight research challenges and suggest directions for future work in this area. Expected final online publication date for the Annual Review of Control, Robotics, and Autonomous Systems, Volume 5 is May 2022. Please see http://www.annualreviews.org/page/journal/pubdates for revised estimates.
预期可达时间游戏
DOI：
10.48550/arxiv.1604.04435
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Forejt V
通讯作者：
Forejt V