文章基本信息

标题：Using models to model-check recursive schemes
本地全文：下载
作者：Sylvain Salvati ; Igor Walukiewicz
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2015
卷号：11
期号：2
页码：1
DOI：10.2168/LMCS-11(2:7)2015
出版社：Technical University of Braunschweig
摘要：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.
其他关键词：Higher-order model checking; simply typed lambda-calculus; tree automata; denotational semantics.