License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.260
URN: urn:nbn:de:0030-drops-54190
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5419/
Go to the corresponding LIPIcs Volume Portal

Grellois, Charles ; Melliès, Paul-André

Relational Semantics of Linear Logic and Higher-order Model Checking

pdf-format:
16.pdf (0.5 MB)

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

BibTeX - Entry

@InProceedings{grellois_et_al:LIPIcs:2015:5419,
  author =	{Charles Grellois and Paul-Andr{\'e} Melli{\`e}s},
  title =	{{Relational Semantics of Linear Logic and Higher-order Model Checking}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{260--276},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5419},
  URN =		{urn:nbn:de:0030-drops-54190},
  doi =		{10.4230/LIPIcs.CSL.2015.260},
  annote =	{Keywords: Higher-order model-checking, linear logic, relational semantics, parity games, parametric comonads.}
}

Keywords: Higher-order model-checking, linear logic, relational semantics, parity games, parametric comonads.
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI