A Complete Set of Satisfaction Rules for Property Detection in Distributed Computations

This paper presents a general framework for specification and detection of properties in distributed computations. A property of states in distributed computation in progress is defined by predicates (called behavioral patterns) and satisfaction rules (called modal operators). A behavioral pattern is obtained by combining basic predicates that are defined over either local states or consistent global states of the computation. In both cases, we model a distributed computation by a directed acyclic graph in which vertices represent (local or global) states and edges represent causal relation over the states. Specification and verification of behavioral patterns are formulated as instances of the language recognition problem, and basic concepts used in formal language theory are applied. A basic predicate is assimilated to a symbol, and a behavioral pattern is specified as a language (i.e., a set of words) defined over an alphabet of symbols. Based on this model and given a behavioral pattern, we define four modal operators (i.e., four different satisfaction rules). Three of them are equivalent to modal operators previously introduced in related works. Finally, we present algorithms to verify each of the four modal operators over a class of behavioral patterns, called regular patterns