Detecting Temporal Logic Predicates on Distributed Computations
Detecting Temporal Logic Predicates on Distributed Computations
复制标题
DOI：
10.1007/978-3-540-75142-7_32
复制
发表时间：
2007-09
期刊：
影响因子：
--
通讯作者：
V. Ogale;V. Garg
中科院分区：
文献类型：
--
作者：
V. Ogale;V. Garg
我们研究了在给定分布式程序执行轨迹的情况下检测嵌套时态谓词的问题。我们提出了一种技术，可以有效地检测相当大的一类谓词，我们称之为基本时间逻辑或BTL。有效的BTL谓词的例子是基于具有任意否定、析取、连接和可能（EF或$\Diamond$）和不变（AG或$\Box$）时态操作符的局部变量的嵌套时态谓词。我们引入基的概念，它是所有满足谓词的全局切的紧凑表示。我们提出了一种算法来计算给定任何BTL谓词的计算的基，并证明了它的时间复杂度相对于跟踪中的过程和事件的数量是多项式的，尽管它在公式的大小上不是多项式。我们不知道有任何其他技术可以检测到类似的谓词类，其时间复杂度是系统中过程和事件数量的多项式。我们已经基于我们的算法实现了一个谓词检测工具包，该工具包可以接受来自任何分布式程序的离线跟踪。
We examine the problem of detecting nested temporal predicates given the execution trace of a distributed program. We present a technique that allows efficient detection of a reasonably large class of predicates which we call the Basic Temporal Logic or BTL. Examples of valid BTL predicates are nested temporal predicates based on local variables with arbitrary negations, disjunctions, conjunctions and the possibly (EF or $\Diamond$) and invariant(AG or $\Box$) temporal operators. We introduce the concept of abasis, a compact representation of all global cuts which satisfy the predicate. We present an algorithm to compute a basis of a computation given any BTL predicate and prove that its time complexity is polynomial with respect to the number of processes and events in the trace although it is not polynomial in the size of the formula. We do not know of any other technique which detects a similar class of predicates with a time complexity that is polynomial in the number of processes and events in the system. We have implemented a predicate detection toolkit based on our algorithm that accepts offline traces from any distributed program.