Detecting Temporal Logic Predicates in Distributed Programs Using Computation Slicing

Detecting whether a finite execution trace (or a computation) of a distributed program satisfies a given predicate, called predicate detection, is a fundamental problem in distributed systems. It finds applications in many domains such as testing, debugging, and monitoring of distributed programs. However predicate detection suffers from the state explosion problem – the number of possible global states of the program increases exponentially with the number of processes. To solve this problem, we generalize an effective abstraction technique called computation slicing. We present polynomialtime algorithms to compute slices with respect to temporal logic predicates from a “regular” subset of CTL, that contains temporal operators EF, EG, and AG. Furthermore, we show that these slices contain precisely those global states of the original computation that satisfy the predicate. Using temporal predicate slices, we give an efficient (polynomial in the number of processes) predicat...

• Type: Conference
• Year: 2003
• Where: OPODIS
• Authors: Alper Sen, Vijay K. Garg
• Keywords: OPODIS 2003, OPODIS 2007, Predicate Detection, Predicate Detection Algorithms, Temporal Predicates