Sylvain Salvati ; Igor Walukiewicz - Using models to model-check recursive schemes

lmcs:1567 - Logical Methods in Computer Science, June 11, 2015, Volume 11, Issue 2 - https://doi.org/10.2168/LMCS-11(2:7)2015
Using models to model-check recursive schemesArticle

Authors: Sylvain Salvati ; Igor Walukiewicz

    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.


    Volume: Volume 11, Issue 2
    Published on: June 11, 2015
    Submitted on: November 22, 2013
    Keywords: Computer Science - Logic in Computer Science

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1339 times.
    This article's PDF has been downloaded 327 times.