The Complexity of Model Checking Higher-Order Fixpoint Logic

Roland Axelsson, Martin Lange, Rafal Somla

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 expressin…