A Complete Set Of Satisfaction Rules For Property Detection In Distributed Computations
Michel Hurfin, Mizuno, Mazaaki, 35 - Rennes (France). Inst. de Recherche en Informatique et Systemes Aleatoires (IRISA) Centre National de la Recherche Scientifique (CNRS), 35 (France). Inst. de Recherche en Informatique et Systemes Aleatoires (IRISA) Rennes-1 Univ., 35 (France). Inst . de Recherche en Informatique et Systemes Aleatoires (IRISA) Institut National des Sciences Appliquees de Rennes (INSA), 35 - Rennes (France). Inst. de Recherche en= Informatique et Systemes Aleatoires (IRISA) Institut National de Recherche en Informatique et en Automatique (INRIA) · 1996
This paper presents a general framework to specify and detect properties of states in distributed computations. A property in a computation 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. Based on this model and given a behavioral pattern, we define four modal operators. Three of them are equivalent to modal operators previously introduced in related work. Finally, we present algorithms to verify each of the four modal operators over a class of behavioral patterns, called regular patt...