The Complexity of Model Checking Higher-Order Fixpoint Logic

Higher-Order Fixpoint Logic (HFL) is a hybrid of the simply typed λ-calculus and the modal µ-calculus. This makes it a highly expressive temporal logic that is capable of expressing various interesting correctness properties of programs that are not expressible in the modal µ-calculus. This paper provides complexity results for its model checking problem. In particular, we consider those fragments of HFL that are built by using only types of bounded order k and arity m. We establish k-fold exponential time completeness for model checking each such fragment. For the upper bound we use fixpoint elimination to obtain reachability games that are singly-exponential in the size of the formula and k-fold exponential in the size of the underlying transition system. These games can be solved in deterministic linear time. As a simple consequence, we obtain an exponential time upper bound on the expression complexity of each such fragment. The lower bound is established by a reduction from th...

• Type: Journal
• Year: 2007
• Where: LMCS
• Authors: Roland Axelsson, Martin Lange, Rafal Somla
• Keywords: Exponential Time Completeness, K-fold Exponential Time, LMCS 2007, Upper Bound