Causal Temporal Reasoning for Markov Decision Processes
Causal Temporal Reasoning for Markov Decision Processes
复制标题
DOI：
--
复制
发表时间：
2022-12
期刊：
影响因子：
--
通讯作者：
M. Kazemi;Nicola Paoletti
中科院分区：
文献类型：
--
作者：
M. Kazemi;Nicola Paoletti
介绍了一种新的验证马尔可夫决策过程的概率时序逻辑--概率反事实时态逻辑(PCFTL)。PCFTL是第一个包括因果推理运算符的，允许我们表达干预性和反事实的查询。在给定路径公式$\Phi$的情况下，如果我们将特定的改变$i$应用于MDP(例如，切换到不同的策略)，则介入性属性与$\Phi$的满足概率有关；反事实允许我们在给定观察到的MDP路径$\tau$的情况下计算如果我们在过去应用$i$，则$\Phi$的结果会是什么。对于它对涉及MDP的不同配置的情况进行推理的能力，我们的方法代表了与只能对固定系统配置进行推理的现有概率时态逻辑的背离。从句法的角度，我们引入了一种广义的反事实算子，它包含了介入概率和反事实概率，并引入了传统的概率算子，如PCTL。从语义的角度来看，我们的逻辑是在MDP的结构因果模型翻译上解释的，这给出了一个服从反事实推理的表示。我们使用网格世界模型的基准在安全强化学习的背景下对PCFTL进行评估。
We introduce $\textit{PCFTL (Probabilistic CounterFactual Temporal Logic)}$, a new probabilistic temporal logic for the verification of Markov Decision Processes (MDP). PCFTL is the first to include operators for causal reasoning, allowing us to express interventional and counterfactual queries. Given a path formula $\phi$, an interventional property is concerned with the satisfaction probability of $\phi$ if we apply a particular change $I$ to the MDP (e.g., switching to a different policy); a counterfactual allows us to compute, given an observed MDP path $\tau$, what the outcome of $\phi$ would have been had we applied $I$ in the past. For its ability to reason about \textit{what-if} scenarios involving different configurations of the MDP, our approach represents a departure from existing probabilistic temporal logics that can only reason about a fixed system configuration. From a syntactic viewpoint, we introduce a generalized counterfactual operator that subsumes both interventional and counterfactual probabilities as well as the traditional probabilistic operator found in e.g., PCTL. From a semantics viewpoint, our logic is interpreted over a structural causal model translation of the MDP, which gives us a representation amenable to counterfactual reasoning. We evaluate PCFTL in the context of safe reinforcement learning using a benchmark of grid-world models.