论文标题
与位向量的线性时间逻辑的有效离线监视
Efficient Offline Monitoring of Linear Temporal Logic with Bit Vectors
论文作者
论文摘要
位图是一种数据结构，旨在紧凑地表示整数集；它提供了非常快速的操作，用于查询和操纵此类集合，从而利用位级并行性。在本文中，我们描述了一种使用位图操纵对线性时间逻辑的任意表达式的技术验证的技术。首先将事件跟踪预处理并转换为一组位图。然后，通过操纵这些位图的递归程序来评估LTL表达。实验结果表明，对于包含近20个操作员的复杂LTL公式，可以以每秒数百万事件的吞吐量进行评估。
A bitmap is a data structure designed to compactly represent sets of integers; it provides very fast operations for querying and manipulating such sets, exploiting bit-level parallelism. In this paper, we describe a technique for the offline verification of arbitrary expressions of Linear Temporal Logic using bitmap manipulation. An event trace is first preprocessed and transformed into a set of bitmaps. The LTL expression is then evaluated through a recursive procedure manipulating these bitmaps. Experimental results show that, for complex LTL formulas containing almost 20 operators, event traces can be evaluated at a throughput of millions of events per second.
