Detecting Temporal Logic Predicates on the Happened-Before Model

                                             Alper Sen and Vijay K. Garg
                               Department of Electrical and Computer Engineering
                                          The University of Texas at Austin
                                                   Austin, TX, 78712, USA
                                                   sen,garg @ece.utexas.edu
                                                          ¡



























































































































































































































































                                                          Abstract

   Detection of a global predicate is a fundamental problem in distributed computing. In this paper we describe new predicate
detection algorithms for certain temporal logic predicates. We use a temporal logic, CTL, for specifying properties of a
distributed computation and interpret it on a finite lattice of global states. We present solutions to the predicate detection
of linear and observer-independent predicates under controllable and invariant operators of CTL. For linear predicates
we develop polynomial-time predicate detection algorithms which exploit the structure of finite distributive lattices. For
observer-independent predicates we prove that predicate detection is NP-complete under controllable operator and co-NP-
complete under invariant operator. We also present polynomial-time algorithms for a CTL operator called until , for which
such algorithms did not exist. Finally, our work unifies many earlier results in predicate detection in a single framework.

   Keywords: predicate detection, model checking, distributed systems, temporal logic, CTL.