Detection of Global State Predicates
CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
This paper examines algorithms for detecting when a property phi holds during the execution of a distributed system. The properties considered are expresses over the state of the system and are not assumed to have properties that facilitate detection, such as stability. Detection is done by a monitoring process within the system, which cannot perceive an execution of a distributed system as a total order because of this, we consider two interpretations for detecting phi. 1. There is an execution consistent with the observed behavior such that phi was true at a point in that execution. We refer to this property as possibly phi. 2. For all executions consistent with the observed behavior, there was some point in real time at which the global state of the system satisfied phi. We refer to this property as definitely phi. This paper gives formal definitions for these two interpretations and present algorithms for them. Protocols are given for both asynchronous and synchronous systems and, for synchronous systems, give upper bounds on the time between the occurrence of the property of interest and the time a monitor detects the property.
- Theoretical Mathematics