A Type-Based HFL Model Checking Algorithm

TL;DR

This paper introduces a practical, efficient algorithm for higher-order modal fixpoint logic (HFL) model checking, enabling verification of complex systems despite theoretical complexity challenges.

Contribution

It presents the first practical, fast algorithm for HFL model checking based on a type-based approach and inspired by saturation techniques.

Findings

Algorithm runs efficiently on typical inputs

Proven correctness of the model checking algorithm

Experimental results demonstrate practical effectiveness

Abstract

Higher-order modal fixpoint logic (HFL) is a higher-order extension of the modal mu-calculus, and strictly more expressive than the modal mu-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.