Synthesis of strategies for autonomous surveillance on adversarial targets

We study the problem of synthesizing a controller for an agent with imperfect sensing and a quantitative surveillance objective, that is, an agent is required to maintain knowledge of the location of a moving, possibly adversarial target. We formulate the problem as a one-sided partial-information game with a winning condition expressed as a temporal logic specification. The specification encodes the quantitative surveillance requirement as well as any additional tasks. Solving a partial-information game typically involves transforming it into a perfect-information belief game using a belief-set construction. Such a transformation leads to a state-space explosion, rendering the belief game computationally intractable to solve for most realistic settings. We present a belief-set abstraction technique to transform the partial-information game to a provably sound abstract belief game that can be solved efficiently using off-the-shelf reactive synthesis tools. We introduce a counterexample-guided refinement approach to automatically achieve the abstraction precision sufficient to synthesize a strategy that is provably winning on the original partial-information game. We evaluate the proposed method on multiple case-studies, implemented on hardware as well as high-fidelity ROS/Gazebo simulations where the agent must respond in real-time to a human-controlled adversary.