Relational semantics of linear logic and higher-order model checking

DOI10.4230/LIPICS.CSL.2015.260MaRDI QIDQ5351962zbMATH OpenOpenAlexFDO

Authors Charles Grellois, Paul-André Melliès

Publication date 31 August 2017

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

zbMATH Keywords

linear logicrelational semanticsparity gameshigher-order model-checkingparametric comonads

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Automata and formal grammars in connection with logical questions (03D05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Abstract: In this article, we develop a new and somewhat unexpected connection between higher-order model-checking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any higher-order recursion scheme (HORS) comes together with a dual Church encoding of an alternating tree automata (ATA) of the same signature. Moreover, the interaction between the relational interpretations of the HORS and of the ATA identifies the set of accepting states of the tree automaton against the infinite tree generated by the recursion scheme. We show how to extend this result to alternating parity automata (APT) by introducing a parametric version of the exponential modality of linear logic, capturing the formal properties of colors (or priorities) in higher-order model-checking. We show in particular how to reunderstand in this way the type-theoretic approach to higher-order model-checking developed by Kobayashi and Ong. We briefly explain in the end of the paper how his analysis driven by linear logic results in a new and purely semantic proof of decidability of the formulas of the monadic second-order logic for higher-order recursion schemes.

Recommendations

• Finitary semantics of linear logic and higher-order model-checking
• On the relationship between higher-order recursion schemes and higher-order fixpoint logic
• Practical alternating parity tree automata model checking of higher-order recursion schemes
• Higher-order model checking: an overview
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.

Cited in

(10)

• Domains for Higher-Order Games
• Generalized bounded linear logic and its categorical semantics
• On the termination problem for probabilistic higher-order recursive programs
• Finitary semantics of linear logic and higher-order model-checking
• A relation algebraic model of robust correctness
• Profinite lambda-terms and parametricity
• scientific article; zbMATH DE number 7526052 (Why is no real title available?)
• Relational Complexity and Higher Order Logics
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• An Analysis of Total Correctness Refinement Models for Partial Relation Semantics II

This page was built for publication: Relational semantics of linear logic and higher-order model checking

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