Games and model checking for guarded logics

Abstract

We investigate the model checking problems for guarded first-order and fixed point logics byreducing them to paritygames. This approach is known to provide good results for the modal μ-calculus and is verycloselyrelated to automata-based methods. To obtain good results also for guarded logics, optimized constructions of games have to be provided. Further, we studythe structure of paritygames, isolate 'easy' cases that admit efficient algorithmic solutions, and determine their relationship to specific fragments of guarded fixed point logics.