Checking LTL[F,G,X] on compressed traces in polynomial time
Checking LTL[F,G,X] on compressed traces in polynomial time
复制标题
在多项式时间内检查压缩迹线上的 LTL[F,G,X]
DOI：
10.1145/3468264.3468557
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Viswanathan, Mahesh
中科院分区：
文献类型：
--
作者：
Zhang, Minjian;Mathur, Umang;Viswanathan, Mahesh
检查程序执行是否满足形式规范的问题出现在许多软件工程任务中，包括运行时验证和设计测试预言机。当无法进行在线分析时，执行跟踪日志将被存储用于离线事后分析，通常以压缩格式存储，以减少磁盘空间和仓储需求。检查压缩执行是否满足属性的一个简单方法是首先对其进行压缩，然后分析得到的未压缩执行。在本文中，我们考虑检查使用基于语法的无损压缩方案压缩的执行轨迹是否满足线性时序逻辑表示的规范的问题，而不显式地解压缩它。一般来说，已知该问题是难以处理的（在压缩轨迹的大小和LTL公式中是PSPACE困难的）。我们证明了对于LTL[F，G，X]，该问题可以在多项式时间内得到解决，其中LTL[F，G，X]包含LTL的除untilooperator外的所有布尔和模态算子.我们的算法用于分析SLP（基于语法的压缩方案）是有效的，在实践中-对于一套大型执行跟踪从开源项目中获得的，我们的算法显示出显着的速度相比，检查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.In this paper, we consider the problem of checking if an execution trace, compressed using a grammar-based lossless compression scheme, satisfies a specification expressed in linear temporal logic, without explicitly decompressing it. In general, this problem is known to be intractable (PSPACE-hard in the size of the compressed trace and the LTL formula). We show that the problem can be solved inpolynomial timefor the fragment LTL[F,G,X], which comprises of all Boolean and modal operators of LTL except theuntiloperator. Our algorithm for analyzing SLPs (a grammar-based compression scheme) is effective in practice — for a suite of large execution traces obtained from open source projects, our algorithm shows significant speed ups when compared with the performance of checking LTL properties over corresponding uncompressed traces.
登录
查看更多内容
关于图的简洁表示的注解
DOI：
10.1016/s0019-9958(86)80009-2
发表时间：
1986
期刊：
Inf. Control.
影响因子：
--
作者：
C. Papadimitriou;M. Yannakakis
通讯作者：
M. Yannakakis
压缩痕迹上的数据竞争检测
DOI：
10.1145/3236024.3236025
发表时间：
2018
期刊：
Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
影响因子：
--
作者：
Dileep Kini;Umang Mathur;Mahesh Viswanathan
通讯作者：
Mahesh Viswanathan
影响因子：
2.5
作者：
Kieffer, JC;Yang, EH
通讯作者：
Yang, EH
时间属性的层次结构
DOI：
10.1145/41840.41857
发表时间：
1987
期刊：
2020 IEEE/ACM 42nd International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)
影响因子：
--
作者：
Z. Manna;A. Pnueli
通讯作者：
A. Pnueli
以 OBDD 表示的图上问题的复杂性
DOI：
10.1007/bfb0028563
发表时间：
1998
期刊：
Chic. J. Theor. Comput. Sci.
影响因子：
--
作者：
J. Feigenbaum;Sampath Kannan;Moshe Y. Vardi;Mahesh Viswanathan
通讯作者：
Mahesh Viswanathan