{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:04Z","timestamp":1753889764267,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,6,11]],"date-time":"2015-06-11T00:00:00Z","timestamp":1433980800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We propose a model-based approach to the model checking problem for recursive\nschemes. Since simply typed lambda calculus with the fixpoint operator,\nlambda-Y-calculus, is equivalent to schemes, we propose the use of a model of\nlambda-Y-calculus to discriminate the terms that satisfy a given property. If a\nmodel is finite in every type, this gives a decision procedure. We provide a\nconstruction of such a model for every property expressed by automata with\ntrivial acceptance conditions and divergence testing. Such properties pose\nalready interesting challenges for model construction. Moreover, we argue that\nhaving models capturing some class of properties has several other virtues in\naddition to providing decidability of the model-checking problem. As an\nillustration, we show a very simple construction transforming a scheme to a\nscheme reflecting a property captured by a given model.<\/jats:p>","DOI":"10.2168\/lmcs-11(2:7)2015","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T13:13:12Z","timestamp":1479733992000},"source":"Crossref","is-referenced-by-count":4,"title":["Using models to model-check recursive schemes"],"prefix":"10.46298","volume":"Volume 11, Issue 2","author":[{"given":"Sylvain","family":"Salvati","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2015,6,11]]},"reference":[{"key":"938:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1567\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1567\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:06:35Z","timestamp":1681243595000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1567"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,11]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(2:7)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1503.04320","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1503.04320","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"arxiv","id":"1503.04909","asserted-by":"subject"},{"id-type":"doi","id":"10.4204\/eptcs.177.4","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arxiv.1503.04909","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2015,6,11]]},"article-number":"1567"}}