Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Using models to model-check recursive schemes

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 to use a model of lambda-Y 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. We argue that having a model capable of recognizing terms satisfying a given property has other benefits than just providing decidability of the model-checking problem. We show a very simple construction transforming a scheme to a scheme reflecting a given property.
Document type :
Preprints, Working Papers, ...
Complete list of metadata
Contributor : Sylvain Salvati Connect in order to contact the contributor
Submitted on : Thursday, October 11, 2012 - 4:27:22 PM
Last modification on : Friday, February 15, 2019 - 2:46:10 PM
Long-term archiving on: : Saturday, December 17, 2016 - 12:05:22 AM


Files produced by the author(s)


  • HAL Id : hal-00741077, version 1


Sylvain Salvati, Igor Walukiewicz. Using models to model-check recursive schemes. 2012. ⟨hal-00741077v1⟩



Record views


Files downloads