A logical framework for multi-agent visual-epistemic reasoning (2015)
(Valentin Goranko, Stockholm University, SE)
We study a logical framework for multi-agent epistemic reasoning based on processing of visual information. This framework is modelled by multi-agent systems where each agent receives visual information from the environment via mobile camera with a given angle of vision in the plane. The agents can thus observe their surroundings and each other and can reason about each other's observation abilities and knowledge derived from these observations. We introduce suitable logical languages for describing such scenarios and formalising such reasoning, involving atomic formulae stating what agents can see, multi-agent epistemic operators for individual, distributed and common knowledge, as well as dynamic operators reflecting the ability of agents (or, their cameras) to move and turn around in order to reach positions satisfying formally specified visual-epistemic requirements. We introduce and study different versions of the semantics for these languages and develop algorithmic methods for automated reasoning in our basic logical system, called 'Big Brother Logic’, and some natural extensions of it.
In this talk I will present the logical framework of BBL and will discuss the interaction between observational abilities and knowledge, both of which essentially depend on the underlying geometric constraints and assumptions. Besides being of purely logical interest, this work has potential applications to formal specification, verification and automated reasoning in multi-robot systems.
(based on joint work with Olivier Gasquet and Francois Schwarzentruber)
Click for slides.
Due to technical difficulties, the lecture had to be split into two parts and some minutes of the talk may be missing.
Below is a playlist:
In this talk I will present the logical framework of BBL and will discuss the interaction between observational abilities and knowledge, both of which essentially depend on the underlying geometric constraints and assumptions. Besides being of purely logical interest, this work has potential applications to formal specification, verification and automated reasoning in multi-robot systems.
(based on joint work with Olivier Gasquet and Francois Schwarzentruber)
Click for slides.
Due to technical difficulties, the lecture had to be split into two parts and some minutes of the talk may be missing.
Below is a playlist:
