#Number
TR-PDS-2001-003

#Title
Detecting Temporal Logic Predicates on the Happened-Before Model

#Author
Alper Sen,
Vijay K. Garg

#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 $\EG$ and
$\AG$ 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 $\EG$ operator and co-NP-complete
under $\AG$ 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.

#Bib
@techreport{TR-PDS-2001-003, 
  author =       "Alper Sen and Vijay K. Garg",
  title =        "Detecting Temporal Logic Predicates on the Happened-Before Model",
  instituition = "The University of Texas at Austin",
  year =         "2001",
  number =       "TR-PDS-2001-003",
  note =         "available via ftp or WWW at maple.ece.utexas.edu
                  as technical report TR-PDS-2001-003"
}