THE COMPLEXITY OF MODEL CHECKING HIGHER ORDER FIXPOINT LOGIC

Abstract. 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 its fragments HFL k,m which are formed using types of bounded order k and arity m only. We establish kExpTime-completeness for model checking each HFL k,m 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 ExpTime upper bound on the expression complexity of each HFL k,m. The lower bound is established by a reduction from the word problem for alternating (k − 1)-fold exponential space bounded Turing Machines. Since there are fixed machines of that type whose word problems are kExpTime-hard already we obtain, as a corollary, kExpTime-completeness for the data complexity of HFL k,m already when m ≥ 4. This also yields a hierarchy result in expressive power. 1