Using models to model-check recursive schemes

TL;DR

This paper introduces a model-based method for model checking recursive schemes by leveraging lambda-Y-calculus models, enabling decision procedures for properties expressed by automata with trivial acceptance conditions.

Contribution

It proposes a novel approach using lambda-Y-calculus models for model checking recursive schemes, including constructions for properties with automata-based specifications.

Findings

Finite models enable decision procedures for certain properties.

Construction of models for properties expressed by automata with trivial acceptance.

Transforming schemes to reflect properties captured by models.

Abstract

We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, lambda-Y-calculus, is equivalent to schemes, we propose the use of a model of lambda-Y-calculus to discriminate the terms that satisfy a given property. If a model is finite in every type, this gives a decision procedure. We provide a construction of such a model for every property expressed by automata with trivial acceptance conditions and divergence testing. Such properties pose already interesting challenges for model construction. Moreover, we argue that having models capturing some class of properties has several other virtues in addition to providing decidability of the model-checking problem. As an illustration, we show a very simple construction transforming a scheme to a scheme reflecting a property captured by a given model.