Big Brother Logic: visual-epistemic reasoning in stationary multi-agent systems

摘要: We consider multi-agent scenarios where each agent controls a surveillance camera in the plane, with fixed position and angle of vision, but rotating freely. The agents can thus observe surroundings other. They also reason about other's observation abilities knowledge derived from these observations. introduce suitable logical languages for reasoning such which involve atomic formulae stating what see, epistemic operators individual, distributed common knowledge, as well dynamic reflecting ability cameras to turn around order reach positions satisfying language. effects public announcements. several different equivalent versions semantics languages, discuss their expressiveness provide translations PDL style. Using we develop algorithms obtain complexity results model checking satisfiability testing basic logic BBL that here some its extensions. Notably, show even extension remain PSPACE. sensitivity set validities admissible angles vision agents' cameras. Finally, further extensions: adding obstacles, positioning 3D or enabling them change positions. Our work has potential applications automated reasoning, formal specification verification observational multi-robot systems.