| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 428639 | Information Processing Letters | 2011 | 6 Pages |
Given a conjunctive predicate ϕ over a distributed execution, this paper gives an algorithm to detect all interval sets, each interval set containing one interval per process, in which the local values satisfy the Definitely(ϕ)Definitely(ϕ) modality. The time complexity of the algorithm is O(n3p)O(n3p), where n is the number of processes and p is the bound on the number of times a local predicate becomes true at any process. The paper also proves that unlike the Possibly(ϕ)Possibly(ϕ) modality which admits O(pn)O(pn) solution interval sets, the Definitely(ϕ)Definitely(ϕ) modality admits O(np)O(np) solution interval sets. The paper also gives an on-line test to determine whether all solution interval sets can be detected in polynomial time under arbitrary fine-grained causality-based modality specifications.
Research highlights► We detect repeated occurrences of a conjunctive predicate in a distributed execution. ► Consider a distributed system with n processes. ► Assume a local predicate becomes true at most p times at a process. ► The algorithm has a time complexity of O(n3p)O(n3p).
