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

2009 ◽  
Author(s):  
Naoki Kobayashi ◽  
C.-H. Luke Ong
Keyword(s):  
Model Checking ◽  
Type System ◽  
Higher Order

scholarly journals A Probabilistic Higher-order Fixpoint Logic

2021 ◽  
Vol Volume 17, Issue 4 ◽  
Author(s):  
Yo Mitani ◽  
Naoki Kobayashi ◽  
Takeshi Tsukada
Keyword(s):  
Model Checking ◽  
Markov Chains ◽  
Positive Result ◽  
Type System ◽  
Higher Order ◽  
Temporal Logics ◽  
Decidable Fragment ◽  
Finite Markov Chains ◽  
Order Extension

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.

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

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.

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

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.

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

1995 ◽  
Vol 5 (1) ◽  
pp. 1-35 ◽  
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.

Automata theory and higher-order model-checking

2016 ◽  
Vol 3 (4) ◽  
pp. 13-31 ◽  
Author(s):  
Igor Walukiewicz
Keyword(s):  
Model Checking ◽  
Higher Order ◽  
Automata Theory ◽  
Order Model
Sign in / Sign up

Export Citation Format

Share Document