EvTL:一种用于信息物理系统瞬态分析的时间逻辑
计算机科学中的逻辑
2022-04-29 v1
摘要
由软件组件与环境封闭交互所表征的系统行为不可避免地受到扰动与不确定性的影响。在本文中,我们提出一个用于规约与验证这些系统行为需求的通用框架。我们引入了演化时间逻辑(EvTL),它是 STL 的随机扩展,允许我们规约描述系统瞬态行为的概率分布的性质,并在规约中纳入不确定性的存在。我们为 EvTL 配备了鲁棒性语义,并证明其相对于由演化度量(即表达一个系统相对于另一个系统完成其任务优劣程度的半度量)诱导的语义是可靠且完备的。最后,我们开发了针对 EvTL 规约的统计模型检测算法。作为我们框架应用的一个示例,我们考虑了一个三水箱实验室实验。
引用
@article{arxiv.2204.13357,
title = {EvTL: A Temporal Logic for the Transient Analysis of Cyber-Physical Systems},
author = {Valentina Castiglioni and Michele Loreti and Simone Tini},
journal= {arXiv preprint arXiv:2204.13357},
year = {2022}
}
备注
arXiv admin note: text overlap with arXiv:2111.15319