一句话：提出直接检查压缩执行轨迹上 LTL[F,G,X] 性质的多项式时间算法，避免先解压。
程序执行是否满足形式规范是运行时验证与测试预言等任务中的核心问题。当无法在线分析时，执行轨迹日志常被压缩存储，以便离线事后分析并降低磁盘与仓储开销。直接方法通常是先解压再检查，但会带来额外成本。本文研究如何在不解压的前提下，直接对压缩轨迹检查带 F、G、X 算子的 LTL 规范，并给出多项式时间算法。其目标是在压缩表示上保持 LTL 验证的可判定性与高效性，从而支持可扩展的离线运行时验证与测试预言。摘要未展开具体压缩模型与实现细节。
The problem of checking if a program execution meets a formal specification arises in many software engineering tasks including runtime verification and designing test oracles. When online analysis is not possible, execution trace logs are stored for offline postmortem analysis, often in a compressed format to reduce disk space and warehousing requirements. A straightforward method for checking if a compressed execution satisfies a property is to first decompress it and then analyze the resulting uncompressed execution.
DOI 原文 ·
@inproceedings{paperbot6385,
title = {Checking LTL[F,G,X] on compressed traces in polynomial time},
author = {Minjian Zhang and Umang Mathur and Mahesh Viswanathan},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3468557}
}