Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal μ-calculus, and strictly more expressive than the modal μ-calculus. It has recently been shown that various program verification problems can naturally be reduced to HFL model checking: the problem of whether a given finite state system satisfies a given HFL formula. In this paper, we propose a novel algorithm for HFL model checking: it is the first practical algorithm in that it runs fast for typical inputs, despite the hyper-exponential worst-case complexity of the HFL model checking problem. Our algorithm is based on Kobayashi et al.’s type-based characterization of HFL model checking, and was inspired by a saturation-based algorithm for HORS model checking, another higher-order extension of model checking. We prove the correctness of the algorithm and report on an implementation and experimental results.
CITATION STYLE
Hosoi, Y., Kobayashi, N., & Tsukada, T. (2019). A type-based HFL model checking algorithm. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11893 LNCS, pp. 136–155). Springer. https://doi.org/10.1007/978-3-030-34175-6_8
Mendeley helps you to discover research relevant for your work.