A Note on Modalities for Nonconjunctive Global Predicates

Abstract

Global predicate detection is an important problem in distributed executions. A conjunctive predicate is one in which each conjunct is defined over variables local to a single process. Polynomial space and time algorithms exist for detecting conjunctive predicates under the Possibly and Definitely modalities, as well as under a richer class of fine-grained modalities based on the temporal interaction of intervals. However, it is much more difficult to detect nonconjunctive predicates under the various modalities because the entire state lattice may need to be examined. We examine the feasibility of detecting nonconjunctive predicates under the fine-grained temporal modalities using the interval-based approach. We gain some insightful observations into how nonconjunctive predicates can be decomposed, and into the relationships among the intervals (at different processes) in which the local variables have values that can satisfy the nonconjunctive predicate.