Probabilistic Model Checking Under Partial Observability With Multiple Objectives

概率模型检验（PMC）是计算机辅助验证的一个分支，侧重于概率模型的自动验证。马尔可夫决策过程（mdp）就是这样一个突出的概率模型。它们起源于运筹学和随机控制理论，经常用于优化问题。PMC检查给定的MDP M和属性规范M是否满足f。在底层，它使用了图算法、值或策略迭代、紧凑的数据结构等，从而实现了一个完全自动化的过程。有效的抽象、简化和符号技术抑制了“维度的诅咒”问题。像PRISM和Storm这样的模型检查器可以在几分钟内解决数十亿状态的（许多）mdp。一个重要的优点是PMC自动获得f的最优策略，作为验证过程的副产品。然而，mdp的一个主要假设是状态是完全可观察的。也就是说，考虑到到目前为止所采取的状态和行动的有限序列（“历史”），民主党的当前状态是唯一确定的。在许多现实场景中——例如，一个机器人的传感器无法覆盖整个环境，或者一个攻击者的系统是一个灰色盒子——这种完美的信息假设太严重了。本课题的目的是研究部分可观测条件下概率模型的自动验证。我们通过逐渐考虑难度越来越大的模型来做到这一点：我们首先考虑部分状态可观察而部分状态不可观察的MDPs，即所谓的混合可观察MDPs （MOMDPs）。然后我们考虑部分可观察的MDP (pomdp)，其中每个状态都是部分可观察的。pomdp是人工智能规划中的一个重要模型。最后，我们考虑部分可观察随机博弈（posg），这是带有额外参与者的pomdp的推广。我们的主要焦点是考虑由多个目标组成的规范，例如，应该以高概率达到目标状态，同时当然避免专用的“坏”状态。作为预备性调查，我们将首先审议一些关于多边发展方案多重目标的开放性问题。根据手头的模型，我们将考虑各种类型的多目标：随机和非随机（例如总是/存在）目标的混合，字典顺序下的多个目标，多个总奖励目标，完全可观察状态和部分可观察状态的目标，等等。我们的调查将集中在可决定性和复杂性，以及开发（近似）算法，在Storm模型检查器之上实现这些算法，并进行一些实验评估。

Probabilistic model checking (PMC) is a branch of computer-aided verification focusing on the automated verification of probabilistic models. Markov decision processes (MDPs) are such a prominent probabilistic model. They have their roots in operations research and stochastic control theory and are frequently used for optimisation problems. PMC checks for a given MDP M and a property specification f whether M satisfies f. Under the hood, it uses graph algorithms, value or policy iteration, compact data structures, etc. so as to achieve a fully automated procedure. Effective abstraction, reduction, and symbolic techniques curb the ``curse of dimensionality'' problem. Model checkers such as PRISM and Storm can solve (many) MDPs with billions of states in a few minutes. An important advantage is that PMC automatically obtains an optimal policy for f as a by-product of the verification process. A major assumption in MDPs though is that states are fully observable. That is to say, given a finite sequence of states and actions taken so far (the ``history''), the current state of the MDP is uniquely determined. In many realistic scenarios --- e.g., a robot with sensors that cannot cover the entire environment or an attacker for which the system is a gray box --- this perfect information assumption is too severe. The aim of this project is to investigate the automated verification of probabilistic models under partial observability. We do so by gradually considering models of increasing difficulty: we first consider MDPs in which part of the states is observable and part is not, so-called mixed observable MDPs (MOMDPs). We then consider partially observable MDP (POMDPs) in which each state is partially observable. POMDPs are a prominent model in planning in AI. Finally, we consider partially observable stochastic games (POSGs), a generalisation of POMDPs with an extra player. Our primary focus is to consider specifications that consist of multiple objectives, e.g., target states should be reached with high probability while certainly avoiding dedicated ``bad'' states. As preparatory investigations, we will start off by considering some open questions concerning multiple objectives on just MDPs. Depending on the model at hand, we will consider various types of multiple objectives: mixtures of stochastic and non-stochastic (e.g. always/exist) objectives, multiple objectives under a lexicographic ordering, multiple total reward objectives, objectives on fully as well as partially observable states, and the like. Our investigations will focus on decidability and complexity as well as developing (approximate) algorithms, implementing those algorithms on top of the Storm model checker, and conducting some experimental evaluations.