Detection of Disjunctive Normal Form Predicate in Distributed Systems
Predicate detection in a distributed system is an important problem. It is useful in debugging and testing of the distributed system. Two modalities are introduced for predicate detection by Cooper and Marzullo. They are denoted by Possibly and Definitely
- PDF / 497,649 Bytes
- 12 Pages / 430 x 660 pts Page_size
- 36 Downloads / 263 Views
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China 2 Graduate University, Chinese Academy of Sciences, Beijing 100080, China [email protected]
Abstract. Predicate detection in a distributed system is an important problem. It is useful in debugging and testing of the distributed system. Two modalities are introduced for predicate detection by Cooper and Marzullo. They are denoted by P ossibly and Def initely. In general, the complexity of detecting predicates in the two modalities is NP-complete and coNP-complete. On detecting conjunctive predicates in Def initely modality, Garg and Waldecker proposed an efficient method. In this paper, we extend the notion of the conjunctive predicate to the notion of the disjunctive normal form (DNF) predicate, which is a disjunction of several conjunctive predicates. We are concerned with the problem of detecting DNF predicates in Def initely modality. We study two classes of DNF predicates called separation DNF predicates and separationinclusion DNF predicates, which can be detected in Def initely modality using an idea similar to that of Garg and Waldecker.
1
Introduction
Predicate detection in a distributed system is an important problem. It is useful in debugging and testing of the distributed system. A predicate is an interesting property that we want to check in the execution of a distributed system. Two modalities are introduced for predicate detection by Cooper and Marzullo [4]. They are denoted by P ossibly and Def initely. We know that the state space of an execution of a distributed system is a distributive lattice. Given a predicate Φ, P ossibly(Φ) means that there exists one path from the initial state to the final state in the lattice, which passes through a state satisfying Φ. Def initely(Φ) means that all paths from the initial state to the final state in the lattice pass through a state satisfying Φ. P ossibly(Φ) is usually used to check the property Φ that we want to avoid, such as, the number of tokens in a system is less than a constant. While Def initely(Φ) is usually used to check the desired property Φ that we want to guarantee, such as, a leader is elected.
Supported by the National Natural Science Foundation of China under Grant No. 60573012 and 60421001, and the National Grand Fundamental Research 973 Program of China under Grant No. 2002cb312200.
S. Rao et al. (Eds.): ICDCN 2008, LNCS 4904, pp. 158–169, 2008. c Springer-Verlag Berlin Heidelberg 2008
Detection of Disjunctive Normal Form Predicate in Distributed Systems
159
Predicate detection suffers from the state explosion problem. It has been shown that in general, detection of P ossibly(Φ) is NP-complete [3] and detection of Def initely(Φ) is coNP-complete [13]. The conjunctive predicate is an important class of predicates. A conjunctive predicate is a conjunction of local predicates. A local predicate is defined on only one process. Thus the truth of it can be easily verified by the process. On detecting conjunctive predicates in P
Data Loading...
