A unified framework for the specification and run-time detection of dynamic properties in distributed computations

To a large extent, the dependability of complex distributed programs relies on our ability to effectively test and debug their executions. Such an activity requires that we be able to specify dynamic properties that the distributed computation must (or must not) exhibit and that we be able to construct algorithms to detect these properties at run time. In this article we formulate dynamic property specification and detection as instances of the language recognition problem. Considering boolean predicates on states of the computation as an alphabet, dynamic property specification is akin to defining a language over this alphabet. Detecting a property, on the other hand, is akin to recognizing at run time if the sentence produced by a distributed execution belongs to the language. This formal language-oriented view not only unifies a large body of work on distributed debugging and property detection, it also leads to simple and efficient detection algorithms. We give examples for the case of properties that can be specified as regular grammars through finite automata.