Detection of a Set of States in Distributed Systems

This paper discusses detection of a set of states in Definitely modality in a distributed system, which means determining whether all paths from the initial state to the final state in the state space of the distributed computation pass through a state in the set. It is associated with predicate detection in Definitely modality in distributed systems, which is useful in debugging and testing of distributed systems. We study some properties of inevitable states and inevitable sets. In this paper we introduce the concept of independence of zones, which is closely related to detection of disjunctive normal form predicates, and helps us for better understanding of local detection of disjunctive normal form predicates. And we give some results on independence of zones.