部分可观离散事件系统观测性质验证的统一框架
系统与控制
2022-12-20 v4 系统与控制
摘要
本文研究部分可观离散事件系统（DES）中的性质验证问题。特别地，我们关注与系统信息流相关的观测性质验证。这里考虑的观测性质包括可诊断性、可预测性、可检测性与不透明性，它们在文献中已引起相当关注。然而，与现有针对不同性质逐例开发不同验证流程的结果相反，本工作通过将每种性质归约为 HyperLTL 模型检验的实例，提供了验证所有这些性质的统一框架。我们的方法基于构建一个 Kripke 结构，其有效捕捉部分可观 DES 中的不可观性问题与有限字符串语义，从而可恰当应用 HyperLTL 模型检验技术。随后对每种考虑的观测性质，我们显式给出需在 Kripke 结构上检验的 HyperLTL 公式以完成验证。我们的方法具有一致性，即所有不同性质均可用同一模型检验引擎验证。此外，我们的统一框架也为依据验证复杂度对部分可观 DES 的观测性质进行分类提供了新见解。
引用
@article{arxiv.2205.01392,
title = {A Unified Framework for Verification of Observational Properties for Partially-Observed Discrete-Event Systems},
author = {Jianing Zhao and Xiang Yin and Shaoyuan Li},
journal= {arXiv preprint arXiv:2205.01392},
year = {2022}
}