一句话：针对时间常数不确定与受扰动的计时自动机，提出若干概念与技术，用模型检测分析其鲁棒性并辅助设计阶段的常数额定。
计时自动机（TA）是建模时间关键系统的常用形式化工具，现有模型检测工具可以判定 TA 是否满足系统规约。然而设计阶段精确的时间常数往往未知：设计者通常只能构造出结构正确、常数待调的模型；而且即便当前模型满足规约，实现过程中时间常数的微小扰动也可能导致规约违例，而模型检测工具一般无法给出如何修正模型的有效指导。本文针对可达性与安全性规约，提出若干概念与技术来应对上述设计阶段的问题，使设计者能够刻画和推理时间常数的不确定性及其对规约满足性的影响，从而为模型的时间常数调整与鲁棒性判定提供依据。摘要未给出具体的实验设置与量化结果。
Timed automata (TA) have been widely adopted as a suitable formalism to model time-critical systems. Furthermore, contemporary model-checking tools allow the designer to check whether a TA complies with a system specification. However, the exact timing constants are often uncertain during the design phase. Consequently, the designer is often able to build a TA with a correct structure, however, the timing constants need to be tuned to satisfy the specification. Moreover, even if the TA initially satisfies the specification, it can be the case that just a slight perturbation during the implementation causes a violation of the specification. Unfortunately, model-checking tools are usually not able to provide any reasonable guidance on how to fix the model in such situations. In this paper, we propose several concepts and techniques to cope with the above mentioned design phase issues when dealing with reachability and safety specifications.
@article{paperbot1679,
title = {Timed Automata Robustness Analysis via Model Checking},
author = {Jaroslav Bendík and Ahmet Sencan and Ebru Aydin Gol and Ivana Černá},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:12)2022}
}