The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

Issue title: Special Issue on the 11th International Workshop on Reachability Problems (RP 2017)

Guest editors: Matthew Hague and Igor Potapov

Article type: Research Article

Authors: Bruse, Florian^{a; *} | Lange, Martin^a | Lozes, Etienne^b

Affiliations: [a] University of Kassel, Kassel, Germany. [email protected], [email protected] | [b] University of Nice Sophia Antipolis, I3S, CNRS, France. [email protected]

Correspondence: [*] Address for correspondence: University of Kassel, School of Electrical Engineering and Computer Science, Kassel, Germany

Abstract: Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ-calculus into the modal μ-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most k < 0. In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in (k − 1)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

DOI: 10.3233/FI-2021-1996

Journal: Fundamenta Informaticae, vol. 178, no. 1-2, pp. 1-30, 2021