In this paper, we examine the problem of detecting nested temporal predicates in the execution trace of a distributed program. We present a technique that allows efficient detection of a reasonably large class of predicates that we call the Multislicing Temporal Logic or MTL. Examples of valid MTL predicates are nested temporal predicates based on local variables with arbitrary negations, disjunctions, conjunctions and the possibly (EF) and invariant(AG) temporal operators. We do not know of any other technique that detects a similar class of predicates with a time complexity that is polynomial in the number of processes and events in the system. We introduce the concept of a multislice of an execution trace and use it for detecting predicates efficiently. A multislice is a set of traces (slices) that exactly represents all the global states which satisfy the predicate. We present an algorithm to compute the multislice of a computation 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 also present algorithms for computation slicing using vector clock timestamps instead of the conventional skeletal edge representation. This results in more efficient algorithms when the slice is much smaller than the original computation.
We compare the implementation of our technique with existing tools like POTA and Spin model checker by verifying traces generated by a Java implementation of the distributed dining philosophers algorithm.