Paper Info
Title
The Complexity of Model Checking Higher-Order Fixpoint Logic
Abstract
Higher-Order Fixpoint Logic (HFL) is a hybrid of the simply typed \lambda-calculus and the modal \lambda-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 \lambda-calculus. This paper provides complexity results for its model checking problem. In particular we consider those fragments of HFL 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 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 already hard with respect to k-fold exponential time, we obtain, as a corollary, k-fold exponential time completeness for the data complexity of our fragments of HFL, provided m exceeds 3. This also yields a hierarchy result in expressive power.
Year
DOI
Venue
2007
10.2168/lmcs-3(2:7)2007
Logical Methods in Computer Science
Keywords
DocType
Volume
lower bound,word problem,higher order,turing machine,computer and information science,model checking,upper bound,temporal logic,linear time,expressive power
Journal
abs/0704.3931
ISSN
Citations 
PageRank 
Logical Methods in Computer Science, Volume 3, Issue 2 (June 29, 2007) lmcs:754
16
0.83
References 
Authors
11
3
Name
Order
Citations
PageRank
Roland Axelsson1493.44
Martin Lange2844.86
Rafal Somla3211.35