利用位向量对线性时序逻辑进行高效离线监控
计算机科学中的逻辑
2020-05-26 v1
摘要
位图是一种旨在紧凑表示整数集的数据结构；它利用位级并行性，为此类集合的查询和操作提供了非常快的速度。本文描述了一种利用位图操作对任意线性时序逻辑表达式进行离线验证的技术。事件轨迹首先被预处理并转换为一组位图。然后通过一个操作这些位图的递归过程来评估LTL表达式。实验结果表明，对于包含近20个运算符的复杂LTL公式，事件轨迹可以以每秒数百万事件的处理速率进行评估。
引用
@article{arxiv.2005.11737,
title = {Efficient Offline Monitoring of Linear Temporal Logic with Bit Vectors},
author = {Kun Xie and Sylvain Hallé},
journal= {arXiv preprint arXiv:2005.11737},
year = {2020}
}
备注
25 pages