Decentralized Observation of Discrete-Event Systems: At Least One Can Tell

TL;DR

This paper introduces the 'at least one can tell' (OCT) condition for decentralized observation in discrete-event systems, ensuring at least one observer can determine system behavior as good or bad, with decidability and finite-state observer implications.

Contribution

The paper proposes a new OCT condition for decentralized observation, providing equivalent formulations, establishing its decidability, and demonstrating the existence of finite-state observers when it holds.

Findings

OCT condition is decidable unlike joint observability.

Finite-state decentralized observers exist under OCT.

OCT differs from previously known observability concepts.

Abstract

We introduce a new decentralized observation condition which we call "at least one can tell" (OCT) and which attempts to capture the idea that for any possible behavior that a system can generate, at least one decentralized observation agent can tell whether that behavior was "good" or "bad", for given formal specifications of "good" and "bad". We provide several equivalent formulations of the OCT condition, and we relate it to (and show that it is different from) previously introduced joint observability. In fact, contrary to joint observability which is undecidable, we show that the OCT condition is decidable. We also show that when the condition holds, finite-state decentralized observers exist.