#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"
}