Synthesis of surveillance strategies via belief abstraction
This work addresses surveillance strategy synthesis for robotics, offering an incremental improvement in handling partial information and scalability.
The authors tackled the problem of synthesizing a controller for a robot to surveil a moving target by formulating it as a partial-information game with temporal logic specifications, and they developed a method using belief abstraction and counterexample-guided refinement to enable synthesis for large state-spaces, demonstrating applicability in case studies.
We study the problem of synthesizing a controller for a robot with a surveillance objective, that is, the robot is required to maintain knowledge of the location of a moving, possibly adversarial target. We formulate this problem as a one-sided partial-information game in which the winning condition for the agent is specified as a temporal logic formula. The specification formalizes the surveillance requirement given by the user, including additional non-surveillance tasks. In order to synthesize a surveillance strategy that meets the specification, we transform the partial-information game into a perfect-information one, using abstraction to mitigate the exponential blow-up typically incurred by such transformations. This enables the use of off-the-shelf tools for reactive synthesis. We use counterexample-guided refinement to automatically achieve abstraction precision that is sufficient to synthesize a surveillance strategy. We evaluate the proposed method on two case-studies, demonstrating its applicability to large state-spaces and diverse requirements.