A pursuit-evasion game is an adversarial hybrid game that combines both continuous and discrete dynamics that is widely used to model robotics tasks in the literature. We model the game rules formally, present a formal verification approach for the winning strategies and prove the design correctness of the proposed algorithms. To accomplish this, we use Differential Game Logic (dGL) to implement the proofs with the KeYmaera X theorem prover, which rigorously proves the safety of the model and the correctness of the winning strategies. The games we consider have two different models of motion: discrete dynamics and continuous dynamics. In particular, we focus on two types of games: Cops-and-Robbers games, which are placed on discrete graphs with movements by stepping the graph edges and Lion-and-Man games, which are played on continuous planes with continuous movement. We set up the model in dGL, identify variants and invariants to reason about winning strategies for different types of game regions and discuss pursuer/evader winning conditions. We separately considered game regions with certain properties, i.e. different families of graphs and planes with selected properties, and conducted proofs that serve for the most general cases.

61 pages

Thesis Committee:
André Platzer (Chair)
Stefan Mitsch

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu