Decentralized Observation of Discrete-Event Systems: At Least One Can Tell
This work addresses decentralized monitoring for systems with formal specifications, offering a decidable alternative to undecidable joint observability, which is incremental in the field of discrete-event systems.
The paper tackles the problem of decentralized observation in discrete-event systems by introducing a new condition called 'at least one can tell' (OCT), which ensures that at least one agent can distinguish between good and bad behaviors, and shows that this condition is decidable and allows for finite-state observers.
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.