通过传递算子视角构建具有记忆依赖性的随机系统抽象

随着安全关键自主系统在不确定环境中部署的普及，亟需数学方法对随机模型进行形式化验证。为实现对随机系统性质的形式化验证，近年来基于离散、有限马尔可夫近似——即抽象模型——的方法数量激增。这些方法的应用场景包括：要么仅获得底层连续随机过程的部分、离散观测，要么原始系统过于复杂，需将其连续状态空间划分为可处理的有限状态模型。上述情况下，抽象模型正是来自对底层连续过程离散化得到的离散随机过程的近似。由于抽象模型为马尔可夫过程，而离散过程并非如此（尽管原始过程是），这导致近似误差。为消除非马尔可夫性，本文引入具有记忆效应的随机系统抽象模型。我们的工作包含两个方面：首先，基于传递算子提供一种记忆依赖抽象模型的形式化方法；其次，通过上界估计真实连续状态分布与其离散近似之间的总变距离，量化近似误差。