基于LTL预测语义的高效监控器构造

运行时验证中的一个重要研究内容就是从高层规约生成高效的监控器,并有效控制监控器的生成复杂度与监控器运行时开销.基于线性时序逻辑(LTL)的预测语义,通过删除与合并Büchi自动机中的大部分状态,提出一种高效的预测监控器构造技术.通过该方法,可以大大降低最终预测监控器的规模,提高监控器产生的效率;同时保证把监控器的运行时开销控制在合理的范围内.基于上述预测监控器构造技术,实现了相应工具monitor_tool,该工具比LTL3_tool工具更小,且能够为更多的LTL性质产生监控器.同时,产生的监控器能够尽可能早的识别一个持续被监控的执行轨迹是否满足指定的正确性性质.