A fine-grained modality classification for global predicates

Specifying and detecting predicates in a distributed execution is an important problem. Distributed execution observation has classically used two modalities-Possibly(Φ) and Definitely(Φ)-for predicate Φ. Based on the temporal interactions of intervals, the author identified a complete, orthogonal set of relationships ℜ; between pairs of intervals in a distributed execution. We show how to map the rich, orthogonal classification of modalities of pairwise interval interactions, to the classical coarse-grained classification, Possibly(Φ) and Definitely(Φ), for specifying predicates defined on any number of processes. This increases the power of expressing the temporal modalities under which predicates can be specified, beyond the current Possibly/Definitely classification. We give some timestamp-based tests for the orthogonal modalities in the refined classification.