一句话：提出面向信息物理系统的广义无作弊性概念及 HyperSTL* 超属性时序逻辑，用于时空域符合性监测与作弊检测。
针对信息物理系统作弊检测，论文提出一种泛化的 doping cleanness 概念，允许在时间和值域上同时扰动输入并观察受扰输出，并利用现有 CPS 符合关系对该定义进行实例化。为监测基于符合关系的洁净性，作者发展了 HyperSTL*，即在 Signal Temporal Logic 上增加轨迹量词与 freeze 算子的时序逻辑，为超属性监测提供形式基础。论文论证泛化定义在数据驱动作弊检测中必不可少，并将其应用于柴油排放测试案例，展示其在时空域检测作弊行为的能力。
We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.
@article{paperbot1741,
title = {Conformance Relations and Hyperproperties for Doping Detection in Time and Space},
author = {Sebastian Biewer and Rayna Dimitrova and Michael Fries and Maciej Gazda and Thomas Heinze and Holger Hermanns and Mohammad Reza Mousavi},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:14)2022}
}