A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes

We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the $\mu^p$-calculus. We show that PHFL is strictly more expressive than the $\mu^p$-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the $\mu$-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky's $\mu$-arithmetic to PHFL, which implies that PHFL model checking is $\Pi^1_1$-hard and $\Sigma^1_1$-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.

Download Full-text

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

Fundamenta Informaticae ◽

10.3233/fi-2021-1996 ◽

2021 ◽

Vol 178 (1-2) ◽

pp. 1-30

Author(s):

Florian Bruse ◽

Martin Lange ◽

Etienne Lozes

Keyword(s):

Model Checking ◽

Lower Bounds ◽

Expressive Power ◽

Higher Order ◽

Order Logic ◽

High Complexity ◽

Transition Systems ◽

Recursive Formulas ◽

Second Order Logic ◽

Monadic Second Order Logic

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.

Download Full-text

Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

ACM Transactions on Computational Logic ◽

10.1145/3452917 ◽

2021 ◽

Vol 22 (2) ◽

pp. 1-37

Author(s):

Christopher H. Broadbent ◽

Arnaud Carayol ◽

C.-H. Luke Ong ◽

Olivier Serre

Keyword(s):

Model Checking ◽

Free Variable ◽

Higher Order ◽

Second Order ◽

Effective Solution ◽

Parity Games ◽

Transition Graphs ◽

Second Order Logic ◽

Pushdown Automata ◽

Monadic Second Order Logic

This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal -calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.

Download Full-text

Higher-Order Model Checking: An Overview

2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science ◽

10.1109/lics.2015.9 ◽

2015 ◽

Cited By ~ 7

Author(s):

Luke Ong

Keyword(s):

Model Checking ◽

Higher Order ◽

Order Model

Download Full-text

A system of constructor classes: overloading and implicit higher-order polymorphism

Journal of Functional Programming ◽

10.1017/s0956796800001210 ◽

1995 ◽

Vol 5 (1) ◽

pp. 1-35 ◽

Cited By ~ 32

Author(s):

Mark P. Jones

Keyword(s):

Type System ◽

Type Systems ◽

Natural Generalization ◽

Higher Order ◽

Functional Language ◽

Effective Algorithm ◽

Prototype Implementation ◽

Type Classes

AbstractThis paper describes a flexible type system that combines overloading and higher-order polymorphism in an implicitly typed language using a system of constructor classes—a natural generalization of type classes in Haskell. We present a range of examples to demonstrate the usefulness of such a system. In particular, we show how constructor classes can be used to support the use of monads in a functional language. The underlying type system permits higher-order polymorphism but retains many of the attractive features that have made Hindley/Milner type systems so popular. In particular, there is an effective algorithm that can be used to calculate principal types without the need for explicit type or kind annotations. A prototype implementation has been developed providing, amongst other things, the first concrete implementation of monad comprehensions known to us at the time of writing.

Download Full-text