The complexity of independence-friendly fixpoint logic

Abstract

We study the complexity of model-checking for the fixpoint extension of Hintikka and Sandu's independence-friendly logic. We show that this logic captures EXPTIME; and by embedding PFP, we show that its combined complexity is ExpSPACB-hard, and moreover the logic includes second order logic (on finite structures). © Springer-Verlag Berlin Heidelberg 2005.