Using models to model-check recursive schemes

DOI10.1007/978-3-642-38946-7_15zbMATH Open1381.68179arXiv1503.04320OpenAlexW2168984090MaRDI QIDQ5300902FDOQ5300902

Authors: S. Salvati, Igor Walukiewicz 

Publication date: 28 June 2013

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

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.

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

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

Mathematics Subject Classification ID

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

Cited In (9)

• Recursion schemes and the WMSO+U logic
• Using models to model-check recursive schemes
• A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata
• Typing Weak MSOL Properties
• Krivine machines and higher-order schemes
• Simply typed fixpoint calculus and collapsible pushdown automata
• Title not available (Why is that?)
• A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata
• Title not available (Why is that?)

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)