 |
 |
Special Issue for the Conference on Computer Science Logic (CSL) 2016
Editors: Jean-Marc Talbot, Laurent Regnier
CSL is an annual conference devoted to the applications of various aspects of mathematical logic in computer science. In 2016 the conference proposed 37 papers selected out of 97 submissions. Each submission was assigned to at least three programme committee members. The overall quality of the submissions was very high, making the work of the programme committee a difficult task.
After the conference papers of major scientific interest were selected and their authors invited to submit an extended version. Each extended versions have been reviewed by two external referees applying the high standard of LMCS. Revised versions are published in this special issue.
We want to thank all authors of the conference, the members of the CSL 2016 programme committee. We are particularly grateful to the authors and the external reviewers of this special issue, who made all efforts providing their expertise and have proposed many valuable comments, contributing to greatly improve these contributions.
Laurent Regnier, Jean-Marc Talbot
Guest Editors of the CSL 2016 Special Issue
1. The Complexity of Bisimulation and Simulation on Finite Systems
In this paper the computational complexity of the (bi)simulation problem over restricted graph classes is studied. For trees given as pointer structures or terms the (bi)simulation problem is complete for logarithmic space or NC$^1$, respectively. This solves an open problem from Balcázar, Gabarró, and Sántha. Furthermore, if only one of the input graphs is required to be a tree, the bisimulation (simulation) problem is contained in AC$^1$ (LogCFL). In contrast, it is also shown that the simulation problem is P-complete already for graphs of bounded path-width.
2. Taylor expansion in linear logic is invertible
Each Multiplicative Exponential Linear Logic (MELL) proof-net can be expanded into a differential net, which is its Taylor expansion. We prove that two different MELL proof-nets have two different Taylor expansions. As a corollary, we prove a completeness result for MELL: We show that the relational model is injective for MELL proof-nets, i.e. the equality between MELL proof-nets in the relational model is exactly axiomatized by cut-elimination.
3. Axioms for Modelling Cubical Type Theory in a Topos
The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object $I$ in a topos to give such a path-based model of type theory in which paths are just functions with domain $I$. Cohen, Coquand, Huber and Mörtberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. (This paper is a revised and expanded version of a paper of the same name that appeared in the proceedings of the 25th EACSL Annual Conference on Computer Science Logic, CSL 2016.)
4. The height of piecewise-testable languages and the complexity of the logic of subwords
The height of a piecewise-testable language $L$ is the maximum length of the words needed to define $L$ by excluding and requiring given subwords. The height of $L$ is an important descriptive complexity measure that has not yet been investigated in a systematic way. This article develops a series of new techniques for bounding the height of finite languages and of languages obtained by taking closures by subwords, superwords and related operations. As an application of these results, we show that $\mathsf{FO}^2(A^*,\sqsubseteq)$, the two-variable fragment of the first-order logic of sequences with the subword ordering, can only express piecewise-testable properties and has elementary complexity.
5. The logical strength of Büchi's decidability theorem
We study the strength of axioms needed to prove various results related to automata on infinite words and Büchi's theorem on the decidability of the MSO theory of $(N, {\le})$. We prove that the following are equivalent over the weak second-order arithmetic theory $RCA_0$: (1) the induction scheme for $\Sigma^0_2$ formulae of arithmetic, (2) a variant of Ramsey's Theorem for pairs restricted to so-called additive colourings, (3) Büchi's complementation theorem for nondeterministic automata on infinite words, (4) the decidability of the depth-$n$ fragment of the MSO theory of $(N, {\le})$, for each $n \ge 5$. Moreover, each of (1)-(4) implies McNaughton's determinisation theorem for automata on infinite words, as well as the "bounded-width" version of König's Lemma, often used in proofs of McNaughton's theorem.