Using models to model-check recursive schemes

DOI10.1007/978-3-642-38946-7_15MaRDI QIDQ5300902zbMATH OpenOpenAlexFDO

Authors S. Salvati, Igor Walukiewicz

Publication date 28 June 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1503.04320

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

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 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.

Recommendations

• Using models to model-check recursive schemes
• Simple Models for Recursive Schemes
• Model checking higher-order programs
• A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata
• A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata

Cited in

(8)

• scientific article; zbMATH DE number 1670550 (Why is no real title available?)
• Using models to model-check recursive schemes
• Simply typed fixpoint calculus and collapsible pushdown automata
• Recursion schemes and the WMSO+U logic
• A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata
• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• Krivine machines and higher-order schemes
• A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata

This page was built for publication: Using models to model-check recursive schemes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5300902)