Model Checking FLC and HFL1

Higher-Order Fixpoint Logic (HFL):

M. and R. Viswanathan's Higher-Order Fixpoint Logic is a highly expressive temporal logic. It enriches μ-calculus with a simply typed λ-calculus. The first-order fragment restricts λ-expressions to type τ_k := Pr → Pr...→ Pr with k function arrows and Pr being the set of subsets of the state space, i.e. to first-order with arbitrary arity. The following BNF defines its syntax in positive normal form:

φ ::= p | ¬p | X | ¬X | φ ∨ φ | φ ∧ φ | <a>φ | [a]φ | φφ | λX.φ | μ(X:τ_k).φ | ν(X:τ_k).φ

Its semantics is defined similar to μ-calculus with the following supplements: fixpoints are interpreted over the domain of k-ary functions which form a complete lattice with pointwise inclusion ordering. λ-expressions may only occur as function applicators in type-correct HFL1 formulas.

For a more detailled introduction see e.g. [1] [2] below.

Model Checking HFL1:

Model checking is in general undecidable for HFL1. For finite models however the computation of the semantics of an expression (remember that it is only the value of a function at a certain argument) is finite and hence decidable.
In [2] there is a complete description of such a procedure. It is a straightforward adaption of a μ-calculus model checker except for the more involved and ressource-intensive case of a fixpoint computation. The basic principle is to do a fixpoint approximation on the partial function of the needed arguments only (they are unknown in advance, yet may be considered on-the-fly).

This improves the straightforward complete function computation approach from a best-case O(|S| 2^k|S|) to a worst-case O(|S| 2^k|S|) time complexity algorithm (where |S| is the size of the model and k the arity of the function). For a discussion about the complexity of general HFL model checking see [3].

Fixpoint Logic with Chop (FLC):

M. Müller-Olm's Fixpoint Logic with Chop is another extension to modal μ-calculus achieved by adding a sequential composition operator called 'chop' (the expression stems from interval temporal logics). Formulas in branching time logics are usually interpreted as sets of states, namely those which satisfy the formula, i.e. predicates on the total state set. In FLC, the semantics is lifted to functions [|⋅|] : 2^S → 2^S where S is the state space; i.e. a formula is basically a predicate transformer.
Sequential composition of formulas φ;ψ is now interpreted as function composition ( [|φ|] ∘ [|ψ|] )(x). As a consequence, e.g. [a] is a valid FLC formula.The following BNF defines the FLC syntax:

φ ::= p | X | τ | φ ∨ φ | φ ∧ φ | <a> | [a] | φ;φ | μ X.φ | ν X.φ

Note that fixpoint formulas are also interpreted as functions: The set of all monotone functions 2^S → 2^S forms a complete lattice with pointwise inclusion ordering which guarantees the existence of least and greatest fixpoints.

An introduction to FLC can be found in [4] below.

Model Checking FLC:

As for HFL, model checking is in general undecidable for FLC, but not on finite models. Furthermore, FLC is contained in HFL1: there is a direct and easy translation from FLC to HFL1 such that it is no coincidence that there is a model checking procedure which in principle can be used for both logics.
So in our implementation, we simply translate a given FLC formula to HFL1 and feed it to the HFL1 model checker.

Download & Documentation:

An implementation of the above outlined model checking algorithms is available on the tool documentation page.
The tools come with a model specification language in which the input for the model checkers can be defined, i.e. a labeled transition system and a specification formula in the desired logic.

For installation and other instructions see the included README file or follow the links above.

Literature:

1. M.Viswanathan and R. Viswanathan.
   A Higher-Order Modal Fixed Point Logic.
   In: Proc. of the 15th Int. Conference on Concurrency Theory, CONCUR'04,
   London, UK, 2004, volume 3170 of Lecture Notes in Computer Science, pages 512-528, © Springer-Verlag
   
2. R.Axelsson and M. Lange.
   Model Checking the First Order Fragment of Higher-Order Fixpoint Logic.
   In: Proc. of the 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'07,
   Yerevan, Armenia, 2007, volume 4790 of Lecture Notes in Computer Science, pages 62-76, © Springer-Verlag
   
3. R.Axelsson and M. Lange and R.Somla.
   The Complexity of Model Checking Higher-Order Fixpoint Logic.
   In: Logical Methods in Computer Science, 3(2:7):1-33, 2007
   
4. M. Müller-Olm.
   A Modal Fixpoint Logic with Chop.
   In: Proc.of the 16th. Symposium on Theoretical Aspects in Computer Science, STACS'99,
   Trier, Germany, 1999, volume 1563 of Lecture Notes in Computer Science, pages 510-520, © Springer-Verlag