Detecting temporal logic predicates on distributed computations.

*(English)*Zbl 1145.68379
Pelc, Andrzej (ed.), Distributed computing. 21st international symposium, DISC 2007, Lemesos, Cyprus, September 24–26, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75141-0/pbk). Lecture Notes in Computer Science 4731, 420-434 (2007).

Summary: 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 \(\diamondsuit\)) and invariant(AG or \(\square\)) temporal operators. We introduce the concept of a basis, 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.

For the entire collection see [Zbl 1142.68009].

For the entire collection see [Zbl 1142.68009].