2021/08/10 by Stavros Tripakis, Tripakis, Stavros, Karen Rudie +1
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Multiagent Systems (cs.MA) #Petri Nets in System Modeling #Software Engineering (cs.SE) #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.2108.04523
openalex publication_date 2021/08/10 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
We introduce a new decentralized observation condition which we call "at\nleast one can tell" (OCT) and which attempts to capture the idea that for any\npossible behavior that a system can generate, at least one decentralized\nobservation agent can tell whether that behavior was "good" or "bad", for given\nformal specifications of "good" and "bad". We provide several equivalent\nformulations of the OCT condition, and we relate it to (and show that it is\ndifferent from) previously introduced joint observability. In fact, contrary to\njoint observability which is undecidable, we show that the OCT condition is\ndecidable. We also show that when the condition holds, finite-state\ndecentralized observers exist.\n