Relational semantics of linear logic and higher-order model checking
From MaRDI portal
Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
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)- A relation algebraic model of robust correctness
- Generalized bounded linear logic and its categorical semantics
- Relational Complexity and Higher Order Logics
- Finitary semantics of linear logic and higher-order model-checking
- An Analysis of Total Correctness Refinement Models for Partial Relation Semantics II
- Intersection types for unboundedness problems
- Domains for Higher-Order Games
- Streett Automata Model Checking of Higher-Order Recursion Schemes
- On the termination problem for probabilistic higher-order recursive programs
- Profinite lambda-terms and parametricity
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)
