实时模型检测：无处不在的参数
计算机科学中的逻辑
2017-01-11 v2
摘要
在本文中，我们研究逻辑 TCTL 在离散时间自动机上的模型检测与参数综合问题，其中模型（时间自动机）和属性（时序公式）中均允许存在参数。我们的结果如下。在负面结果方面，我们证明仅带有一个参数时钟的离散时间自动机上，带参数扩展的 TCTL 的模型检测问题是不可判定的。该不可判定性结果需要逻辑中包含等式。在正面结果方面，我们证明对于逻辑中不允许等式的一个片段，模型检测与参数综合问题变得可判定。我们的方法基于自动机理论原理，以及使用 Presburger 算术来表达时间自动机中运行持续时间的方法扩展。
引用
@article{arxiv.cs/0701138,
title = {Real-Time Model-Checking: Parameters everywhere},
author = {Veronique Bruyere and Jean-Francois Raskin},
journal= {arXiv preprint arXiv:cs/0701138},
year = {2017}
}