The Complexity of Model Checking Higher-Order Fixpoint Logic

Details The Complexity of Model Checking Higher-Order Fixpoint Logic The Complexity of Model Checking Higher-Order Fixpoint Logic

2007-04-30

arxiv.org/abs/0704.3931v2

LMCS 3 (2:7) 2007

Computer Science

Logic in Computer Science

33 pages, 2 figures, to be published in Logical Methods in Computer Science

Scientific paper

10.2168/LMCS-3(2:7)2007

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.

Affiliated with

Also associated with

No associations

Rating

The Complexity of Model Checking Higher-Order Fixpoint Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with The Complexity of Model Checking Higher-Order Fixpoint Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The Complexity of Model Checking Higher-Order Fixpoint Logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-415385