The Complexity of Model Checking Higher Order Fixpoint Logic

This paper analyses the computational complexity of the model checking problem for Higher Order Fixpoint Logic – the modal µ-calculus enriched with a typed λ-calculus. It is hard for every level of the elementary time/space hierarchy and in elementary time/space when restricted to formulas of bounded type order.

• Type: Conference
• Year: 2005
• Where: MFCS
• Authors: Martin Lange, Rafal Somla
• Keywords: Elementary Time/space, Elementary Time/space Hierarchy, MFCS 2005, Model Checking Problem