|
Abstract : |
Abstract. We investigate the model checking problems for guarded rst-order and xed point logics by reducing them to parity games. This approach is known to provide good results for the modal -calculus and is very closely related to automata-based methods. To obtain good results also for guarded logics, optimized constructions of games have to be provided. Further, we study the structure of parity games, isolate `easy ' cases that admit ecient algorithmic solutions, and determine their relationship to speci c fragments of guarded xed point logics. 1, |