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

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

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

Automated Logical Verification based on Trace Abstractions

BRICS Report Series ◽

10.7146/brics.v2i53.19954 ◽

1995 ◽

Vol 2 (53) ◽

Cited By ~ 1

Author(s):

Nils Klarlund ◽

Mogens Nielsen ◽

Kim Sunesen

Keyword(s):

Distributed Systems ◽

Model Checking ◽

State Space ◽

Temporal Logic ◽

Second Order ◽

Order Logic ◽

Verification Problem ◽

Finite State ◽

Second Order Logic ◽

Monadic Second Order Logic

We propose a new and practical framework for integrating the behavioral reasoning about distributed systems with model-checking methods. Our proof methods are based on trace abstractions, which relate the behaviors of the program and the specification. We show that for finite-state systems such symbolic abstractions can be specified conveniently in Monadic Second-Order Logic (M2L). Model-checking is then made possible by the reduction of non-determinism implied by the trace abstraction. Our method has been applied to a recent verification problem by Broy and Lamport. We have transcribed their behavioral description of a distributed program into temporal logic and verified it against another distributed system without constructing the global program state space. The reasoning is expressed entirely within M2L and is carried out by a decision procedure. Thus M2L is a practical vehicle for handling complex temporal logic specifications, where formulas decided by a push of a button are as long as 10-15 pages.

Download Full-text