s'authentifier
version française rss feed

hal-00741077, version 2

Using models to model-check recursive schemes

Sylvain Salvati () a1, Igor Walukiewicz 2

TLCA 2013 7941 (2013) 189-204

Résumé : 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.

 
  • hal-00741077, version 2
  • oai:hal.inria.fr:hal-00741077
  • Contributeur : 
  • Soumis le : Vendredi 12 Octobre 2012, 10:57:30
  • Dernière modification le : Lundi 17 Mars 2014, 11:59:31
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...