文件名称：基于LTL预测语义的高效监控器构造 (2013年)
文件大小：401KB
文件格式：PDF
更新时间：2024-05-29 04:34:59
自然科学 论文
运行时验证中的一个重要研究内容就是从高层规约生成高效的监控器，并有效控制监控器的生成复杂度与监控器运行时开销．基于线性时序逻辑(LTL)的预测语义，通过删除与合并Büchi自动机中的大部分状态，提出一种高效的预测监控器构造技术．通过该方法，可以大大降低最终预测监控器的规模，提高监控器产生的效率；同时保证把监控器的运行时开销控制在合理的范围内．基于上述预测监控器构造技术，实现了相应工具monitor_tool，该工具比LTL3_tool工具更小，且能够为更多的LTL性质产生监控器．同时，产生的监控器能够尽可