Model Checking Knowledge in Pursuit-Evasion Games
Xiaowei Huang and Ron van der Meyden
In a pursuit-evasion game, one or more pursuers aim to discover the existence of, and then capture, an evader. The paper studies pursuit-evasion games in which players may have incomplete information concerning the game state. A methodology is presented for the application of a model checker for the logic of knowledge and time to verify epistemic properties in such games, as well as to synthesize game strategies. Experimental results are provided from a number of case studies that validate the feasibility of the approach.