The Complexity of Independence-Friendly Fixpoint Logic

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 ExpSpace-hard, and moreover the logic includes second order logic (on finite structures).

• Type: Conference
• Year: 2005
• Where: CSL
• Authors: Julian C. Bradfield, Stephan Kreutzer
• Keywords: CSL 2005, Logic Captures Exptime, Order Logic, Sandu’s Independence-friendly Logic