Verification and control of partially observable probabilistic systems
Verification and control of partially observable probabilistic systems
复制标题
DOI：
10.1007/s11241-017-9269-4
复制
发表时间：
2017-05-01
影响因子：
1.3
通讯作者：
Zou, Xueyi
中科院分区：
文献类型：
--
作者：
Norman, Gethin;Parker, David;Zou, Xueyi
我们提出了用于验证和控制部分可观察概率系统的自动化技术，用于离散和密集的时间模型。对于离散情况，我们使用部分可观察马尔可夫决策过程对这些系统进行形式化建模；对于密集时间，我们提出了一种概率时间自动机的扩展，其中局部状态对观察者或控制器是部分可见的。我们给出了概率时间逻辑，可以表达这些模型的一系列定量属性，与事件发生的概率或奖励措施的期望值有关。然后，我们提出一些技术来验证这样的属性是否成立，或者为模型合成一个使其成立的控制器。我们的方法基于部分可观测性引起的不可数信念空间的基于网格的抽象，对于密集时间模型，实时行为的整数离散化。前者必然是近似的，因为潜在的问题是不可确定的，但是我们展示了如何生成数值结果的下界和上界。我们通过在PRISM模型检查器中实现该方法并将其应用于任务和网络调度，计算机安全和规划领域的几个案例研究来说明该方法的有效性。
We present automated techniques for the verification and control of partially observable, probabilistic systems for both discrete and dense models of time. For the discrete-time case, we formally model these systems using partially observable Markov decision processes; for dense time, we propose an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give probabilistic temporal logics that can express a range of quantitative properties of these models, relating to the probability of an event's occurrence or the expected value of a reward measure. We then propose techniques to either verify that such a property holds or synthesise a controller for the model which makes it true. Our approach is based on a grid-based abstraction of the uncountable belief space induced by partial observability and, for dense-time models, an integer discretisation of real-time behaviour. The former is necessarily approximate since the underlying problem is undecidable, however we show how both lower and upper bounds on numerical results can be generated. We illustrate the effectiveness of the approach by implementing it in the PRISM model checker and applying it to several case studies from the domains of task and network scheduling, computer security and planning.