Name
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 (lambda )-calculus into the modal (mu )-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 u003e 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. |
Year | Venue | Field |
|---|---|---|
2017 | RP | Specification language,Modal μ-calculus,Discrete mathematics,Model checking,Decidability,Fixed point,Monad (functional programming),Mathematics,Modal,Lambda |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
9 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Florian Bruse | 1 | 4 | 2.43 |
| Martin Lange | 2 | 13 | 4.00 |
| Étienne Lozes | 3 | 121 | 14.32 |