有限迹上监控LTL规约的计数语义
计算机科学中的逻辑
2018-04-11 v1 形式语言与自动机理论
摘要
我们考虑在有限迹上监控定义在无限路径上的线性时序逻辑（LTL）规约的问题。例如，我们可能需要就系统是否满足或违反“p无限经常成立”这一性质给出判定。问题在于，总是存在满足该性质的有限迹的延续，以及违反该性质的不同延续。我们提出一种两步法来解决此问题。首先，我们引入一种计数语义，计算迹中每个位置见证公式满足或违反所需的步数。其次，我们利用该信息对不确定后缀进行预测。特别地，我们认为好的后缀是比满足的最长见证更短的后缀，坏的后缀是比违反的最长见证更短或相等的后缀。基于此假设，我们提供一个判定，评估同一系统上执行的延续大概会满足还是违反该性质。
引用
@article{arxiv.1804.03237,
title = {A Counting Semantics for Monitoring LTL Specifications over Finite Traces},
author = {Ezio Bartocci and Roderick Bloem and Dejan Nickovic and Franz Roeck},
journal= {arXiv preprint arXiv:1804.03237},
year = {2018}
}