Decentralized Observation Problems

A fundamental observation problem is, given a model of the system to be observed and a specification of the property to be observed, to check whether the property is observable (i.e., the observer can resolve potential ambiguities due to partial observation capabilities) and if so to (automatically) synthesize an observer. We consider a simple case of the above setting, namely, where the system model and specifications are expressed as regular languages over a finite alphabet. In this setting, and in the case of one observer (centralized observation), both checking observability and synthesizing an observer can be done automatically, and the observer is guaranteed to be finite-state. The situation is more complicated in the case of more than one observers (decentralized observation). Here, many definitions are possiblle, depending on where the decisions are taken, as well as on whether the observers are required to be finite-state. We examine some of these possibilities, surveying recent results on the topic and providing some new results as well.