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 :
Conference papers
TLCA 2013, 2013, Eindhoven, Netherlands. 7941, pp.189-204, 2013, LNCS


https://hal.inria.fr/hal-00741077
Contributor : Sylvain Salvati <>
Submitted on : Friday, October 12, 2012 - 10:57:30 AM
Last modification on : Monday, March 17, 2014 - 11:59:31 AM

File

m.pdf
fileSource_public_author

Identifiers

  • HAL Id : hal-00741077, version 2

Collections

Citation

Sylvain Salvati, Igor Walukiewicz. Using models to model-check recursive schemes. TLCA 2013, 2013, Eindhoven, Netherlands. 7941, pp.189-204, 2013, LNCS. <hal-00741077v2>

Export

Share

Metrics

Consultation de
la notice

99

Téléchargement du document

25