Volume
LIPIcs, Volume 62
25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Publication Details
- published at: 2016-08-29
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-022-4
- DBLP: db/conf/csl/csl2016
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 62, CSL'16, Complete Volume
Abstract
LIPIcs, Volume 62, CSL'16, Complete Volume
Cite as
25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@Proceedings{talbot_et_al:LIPIcs.CSL.2016,
title = {{LIPIcs, Volume 62, CSL'16, Complete Volume}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016},
URN = {urn:nbn:de:0030-drops-66715},
doi = {10.4230/LIPIcs.CSL.2016},
annote = {Keywords: Conference Proceedings, Distributed Systems, Software/ Programs Verifications, Formal Definitions and Theory, Languages Constructs and Features, Knowledge Representations Formalisms and Methods, Theory of Computation, Mathematical Logic}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers
Abstract
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers
Cite as
25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{talbot_et_al:LIPIcs.CSL.2016.0,
author = {Talbot, Jean-Marc and Regnier, Laurent},
title = {{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {0:i--0:xvi},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.0},
URN = {urn:nbn:de:0030-drops-65405},
doi = {10.4230/LIPIcs.CSL.2016.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}
}
Document
The Ackermann Award 2016
Abstract
The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2016 edition of the award.
Cite as
Thierry Coquand and Anuj Dawar. The Ackermann Award 2016. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{coquand_et_al:LIPIcs.CSL.2016.1,
author = {Coquand, Thierry and Dawar, Anuj},
title = {{The Ackermann Award 2016}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.1},
URN = {urn:nbn:de:0030-drops-65419},
doi = {10.4230/LIPIcs.CSL.2016.1},
annote = {Keywords: Ackermann Award, Computer Science, Logic}
}
Document
Invited Talk
Infinite Domain Constraint Satisfaction Problem (Invited Talk)
Abstract
The computational and descriptive complexity of finite domain fixed template constraint satisfaction problem (CSP) is a well developed topic that combines several areas in mathematics and computer science. Allowing the domain to be infinite provides a way larger playground which covers many more computational problems and requires further mathematical tools. I will talk about some of the research challenges and recent progress on them.
Cite as
Libor Barto. Infinite Domain Constraint Satisfaction Problem (Invited Talk). In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{barto:LIPIcs.CSL.2016.2,
author = {Barto, Libor},
title = {{Infinite Domain Constraint Satisfaction Problem}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.2},
URN = {urn:nbn:de:0030-drops-65427},
doi = {10.4230/LIPIcs.CSL.2016.2},
annote = {Keywords: Descriptive complexity, Constraint Satisfaction Problem}
}
Document
Invited Talk
Automated Synthesis: Going Distributed (Invited Talk)
Abstract
Synthesis is particularly challenging for concurrent programs. At the same time it is a very promising approach, since concurrent programs are difficult to get right, or to analyze with traditional verification techniques. The talk provides an introduction to distributed synthesis in the setting of Mazurkiewicz traces, and its applications to decentralized runtime monitoring.
Cite as
Anca Muscholl. Automated Synthesis: Going Distributed (Invited Talk). In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{muscholl:LIPIcs.CSL.2016.3,
author = {Muscholl, Anca},
title = {{Automated Synthesis: Going Distributed}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {3:1--3:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.3},
URN = {urn:nbn:de:0030-drops-65436},
doi = {10.4230/LIPIcs.CSL.2016.3},
annote = {Keywords: Concurrent programs, Distributed synthesis, Runtime monitoring}
}
Document
Invited Talk
Analytic Calculi for Non-Classical Logics: Theory and Applications (Invited Talk)
Abstract
The possession of a suitable proof-calculus is the starting point for many investigations into a logic, including decidability and complexity, computational interpretations and automated theorem proving. By suitable proof-calculus we mean a calculus whose proofs exhibit some notion of subformula property ("analyticity"). In this talk we describe a method for the algorithmic introduction of analytic sequent-style calculi for a wide range of non-classical logics starting from Hilbert systems. To demonstrate the widespread applicability of this method, we discuss how to use the introduced calculi for proving various results ranging from Curry-Howard isomorphism to new interpretative tools for Indology.
Cite as
Agata Ciabattoni. Analytic Calculi for Non-Classical Logics: Theory and Applications (Invited Talk). In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{ciabattoni:LIPIcs.CSL.2016.4,
author = {Ciabattoni, Agata},
title = {{Analytic Calculi for Non-Classical Logics: Theory and Applications}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {4:1--4:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.4},
URN = {urn:nbn:de:0030-drops-65440},
doi = {10.4230/LIPIcs.CSL.2016.4},
annote = {Keywords: Proof theory, Fuzzy logic}
}
Document
Invited Talk
Coalgebraic Learning (Invited Talk)
Abstract
The area of automata learning was pioneered by Angluin in the 80's. Her original algorithm, which applied to regular languages and deterministic automata, has been extended to various types of automata and used in software and hardware verification. In this talk, we will take an abstract perspective at automata learning. We show how the correctness of the original algorithm and many extensions can be captured in one proof using coalgebraic techniques. We also show that a novel algorithm for nominal automata can be derived from the abstract framework.
Cite as
Alexandra Silva. Coalgebraic Learning (Invited Talk). In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{silva:LIPIcs.CSL.2016.5,
author = {Silva, Alexandra},
title = {{Coalgebraic Learning}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {5:1--5:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.5},
URN = {urn:nbn:de:0030-drops-65455},
doi = {10.4230/LIPIcs.CSL.2016.5},
annote = {Keywords: Automata learning, coalgebraic techniques}
}
Document
The Matrix Ring of a mu-Continuous Chomsky Algebra is mu-Continuous
Abstract
In the course of providing an (infinitary) axiomatization of the equational theory of the class of context-free languages, Grathwohl, Kozen and Henglein (2013) have introduced the class of mu-continuous Chomsky algebras. These are idempotent semirings where least solutions for systems of polynomial inequations (i.e. context-free grammars) can be computed iteratively and where multiplication is continuous with respect to the least fixed point operator mu. We prove that the matrix ring of a mu-continuous Chomsky algebra also is a mu-continuous Chomsky algebra.
Cite as
Hans Leiss. The Matrix Ring of a mu-Continuous Chomsky Algebra is mu-Continuous. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{leiss:LIPIcs.CSL.2016.6,
author = {Leiss, Hans},
title = {{The Matrix Ring of a mu-Continuous Chomsky Algebra is mu-Continuous}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {6:1--6:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.6},
URN = {urn:nbn:de:0030-drops-65467},
doi = {10.4230/LIPIcs.CSL.2016.6},
annote = {Keywords: context-free language, fixed point operator, idempotent semiring, matrix ring, Chomsky algebra}
}
Document
Completeness for Coalgebraic Fixpoint Logic
Abstract
We introduce an axiomatization for the coalgebraic fixed point logic which was introduced by Venema as a generalization, based on Moss' coalgebraic modality, of the well-known modal mu-calculus. Our axiomatization can be seen as a generalization of Kozen's proof system for the modal mu-calculus to the coalgebraic level of generality. It consists of a complete axiomatization for Moss'modality, extended with Kozen's axiom and rule for the fixpoint operators.
Our main result is a completeness theorem stating that, for functors that preserve weak pullbacks and restrict to finite sets, our axiomatization is sound and complete for the standard interpretation of the language in coalgebraic models. Our proof is based on automata-theoretic ideas: in particular, we introduce the notion of consequence game for modal automata, which plays a crucial role in the proof of our main result.
The result generalizes the celebrated Kozen-Walukiewicz completeness theorem for the modal mu-calculus, and our automata-theoretic methods simplify parts of Walukiewicz' proof.
Cite as
Sebastian Enqvist, Fatemeh Seifan, and Yde Venema. Completeness for Coalgebraic Fixpoint Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{enqvist_et_al:LIPIcs.CSL.2016.7,
author = {Enqvist, Sebastian and Seifan, Fatemeh and Venema, Yde},
title = {{Completeness for Coalgebraic Fixpoint Logic}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.7},
URN = {urn:nbn:de:0030-drops-65470},
doi = {10.4230/LIPIcs.CSL.2016.7},
annote = {Keywords: mu-calculus, coalgebra, coalgebraic modal logic, automata, completeness}
}
Document
AC Dependency Pairs Revisited
Abstract
Rewriting modulo AC, i.e., associativity and/or commutativity of certain symbols, is among the most frequently used extensions of term rewriting by equational theories. In this paper we present a generalization of the dependency pair framework for termination analysis to rewriting modulo AC. It subsumes existing variants of AC dependency pairs, admits standard dependency graph analyses, and in particular enjoys the minimality property in the standard sense. As a direct benefit, important termination techniques are easily extended; we describe usable rules and the subterm criterion for AC termination, which properly generalize the non-AC versions.
We also perform these extensions within IsaFoR - the Isabelle formalization of rewriting - and thereby provide the first formalization of AC dependency pairs. Consequently, our certifier CeTA now supports checking proofs of AC termination.
Cite as
Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari. AC Dependency Pairs Revisited. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{yamada_et_al:LIPIcs.CSL.2016.8,
author = {Yamada, Akihisa and Sternagel, Christian and Thiemann, Ren\'{e} and Kusakari, Keiichirou},
title = {{AC Dependency Pairs Revisited}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {8:1--8:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.8},
URN = {urn:nbn:de:0030-drops-65488},
doi = {10.4230/LIPIcs.CSL.2016.8},
annote = {Keywords: Equational Rewriting, Termination, Dependency Pairs, Certification}
}
Document
The Directed Homotopy Hypothesis
Abstract
The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be "equivalent" to (weak) infinite-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g., for rewriting, distributed systems, (homotopy) type theory etc.
But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be "equivalent" to a weak form of topologically enriched categories, still very close to (infinite,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.
Cite as
Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. The Directed Homotopy Hypothesis. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{dubut_et_al:LIPIcs.CSL.2016.9,
author = {Dubut, J\'{e}r\'{e}my and Goubault, Eric and Goubault-Larrecq, Jean},
title = {{The Directed Homotopy Hypothesis}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.9},
URN = {urn:nbn:de:0030-drops-65492},
doi = {10.4230/LIPIcs.CSL.2016.9},
annote = {Keywords: directed algebraic topology, partially enriched categories, homotopy hypothesis, geometric models for concurrency, higher category theory}
}
Document
Robust Linear Temporal Logic
Abstract
Although it is widely accepted that every system should be robust, in the sense that "small" violations of environment assumptions should lead to "small" violations of system guarantees, it is less clear how to make this intuitive notion of robustness mathematically precise. In this paper, we address the problem of how to specify robustness in temporal logic. Our solution consists of a robust version of the Linear Temporal Logic (LTL) fragment that only contains the always and eventually temporal operators.
Cite as
Paulo Tabuada and Daniel Neider. Robust Linear Temporal Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{tabuada_et_al:LIPIcs.CSL.2016.10,
author = {Tabuada, Paulo and Neider, Daniel},
title = {{Robust Linear Temporal Logic}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {10:1--10:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.10},
URN = {urn:nbn:de:0030-drops-65508},
doi = {10.4230/LIPIcs.CSL.2016.10},
annote = {Keywords: Linear Temporal Logic, Robustness}
}
Document
Models of Lambda-Calculus and the Weak MSO Logic
Abstract
We study the weak MSO logic in relationship to infinitary lambda-calculus. We show that for every formula phi of weak MSO there exists a finitary model of infinitary lambda-calculus recognizing the set of infinitary lambda-terms whose Böhm tree satisfies phi. The model is effective, in the sense that for every lambda-Y-term we can effectively compute its value in the model. In particular, given a finite lambda-Y-term, one can decide whether the resulting Böhm tree satisfies a given formula of weak MSO, which is a special case of the result of Ong, which concerns unrestricted MSO. The existence of effective models for weak MSO and MSO was proved earlier by Salvati and Walukiewicz but our proof uses a different method, as it does not involve automata, but works directly with logics.
Cite as
Pawel Parys and Szymon Torunczyk. Models of Lambda-Calculus and the Weak MSO Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{parys_et_al:LIPIcs.CSL.2016.11,
author = {Parys, Pawel and Torunczyk, Szymon},
title = {{Models of Lambda-Calculus and the Weak MSO Logic}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {11:1--11:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.11},
URN = {urn:nbn:de:0030-drops-65511},
doi = {10.4230/LIPIcs.CSL.2016.11},
annote = {Keywords: typed lambda-calculus, models, weak MSO logic}
}
Document
On the Parallel Complexity of Bisimulation on Finite Systems
Abstract
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. We also show that the simulation problem is P-complete even for graphs of bounded path-width.
Cite as
Moses Ganardi, Stefan Göller, and Markus Lohrey. On the Parallel Complexity of Bisimulation on Finite Systems. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{ganardi_et_al:LIPIcs.CSL.2016.12,
author = {Ganardi, Moses and G\"{o}ller, Stefan and Lohrey, Markus},
title = {{On the Parallel Complexity of Bisimulation on Finite Systems}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {12:1--12:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.12},
URN = {urn:nbn:de:0030-drops-65522},
doi = {10.4230/LIPIcs.CSL.2016.12},
annote = {Keywords: bisimulation, computational complexity, tree width}
}
Document
Monadic Second Order Finite Satisfiability and Unbounded Tree-Width
Abstract
The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese. We prove that the following problem is decidable:
Input: (i) A monadic second order logic sentence alpha, and (ii) a sentence beta in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of alpha and beta may intersect.
Output: Is there a finite structure which satisfies alpha and beta such that the restriction of the structure to the vocabulary of alpha has bounded tree-width? (The tree-width of the desired structure is not bounded.)
As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic MS^{exists card} extending monadic second order logic with linear cardinality constraints of the form |X_{1}|+...+|X_{r}| < |Y_{1}|+...+|Y_{s}| on the variables X_i, Y_j of the outer-most quantifier block. We prove the decidability of a similar extension of WS1S.
Cite as
Tomer Kotek, Helmut Veith, and Florian Zuleger. Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{kotek_et_al:LIPIcs.CSL.2016.13,
author = {Kotek, Tomer and Veith, Helmut and Zuleger, Florian},
title = {{Monadic Second Order Finite Satisfiability and Unbounded Tree-Width}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {13:1--13:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.13},
URN = {urn:nbn:de:0030-drops-65537},
doi = {10.4230/LIPIcs.CSL.2016.13},
annote = {Keywords: Monadic Second Order Logic MSO, Two variable Fragment with Counting C2, Finite decidability, Unbounded Tree-width, WS1S with Cardinality Constraints}
}
Document
Dependence Logic vs. Constraint Satisfaction
Abstract
During the past decade, dependence logic has emerged as a formalism suitable for expressing and analyzing notions of dependence and independence that arise in different scientific areas. The sentences of dependence logic have the same expressive power as those of existential second-order logic, hence dependence logic captures NP on the class of all finite structures. In this paper, we identify a natural fragment of universal dependence logic and show that, in a precise sense, it captures constraint satisfaction. This tight connection between dependence logic and constraint satisfaction contributes to the descriptive complexity of constraint satisfaction and elucidates the expressive power of universal dependence logic.
Cite as
Lauri Hella and Phokion G. Kolaitis. Dependence Logic vs. Constraint Satisfaction. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{hella_et_al:LIPIcs.CSL.2016.14,
author = {Hella, Lauri and Kolaitis, Phokion G.},
title = {{Dependence Logic vs. Constraint Satisfaction}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {14:1--14:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.14},
URN = {urn:nbn:de:0030-drops-65548},
doi = {10.4230/LIPIcs.CSL.2016.14},
annote = {Keywords: Dependence logic, constraint satisfaction, computational complexity, expressive power}
}
Document
Quantified Constraint Satisfaction on Monoids
Abstract
We contribute to a research program that aims to classify, for each finite structure, the computational complexity of the quantified constraint satisfaction problem on the structure. Employing an established algebraic viewpoint to studying this problem family, whereby this classification program can be phrased as a classification of algebras, we give a complete classification of all finite monoids.
Cite as
Hubie Chen and Peter Mayr. Quantified Constraint Satisfaction on Monoids. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.CSL.2016.15,
author = {Chen, Hubie and Mayr, Peter},
title = {{Quantified Constraint Satisfaction on Monoids}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {15:1--15:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.15},
URN = {urn:nbn:de:0030-drops-65553},
doi = {10.4230/LIPIcs.CSL.2016.15},
annote = {Keywords: quantified constraint satisfaction, universal algebra, computational complexity}
}
Document
Non-Homogenizable Classes of Finite Structures
Abstract
Homogenization is a powerful way of taming a class of finite structures with several interesting applications in different areas, from Ramsey theory in combinatorics to constraint satisfaction problems (CSPs) in computer science, through (finite) model theory. A few sufficient conditions for a class of finite structures to allow homogenization are known, and here we provide a necessary condition. This lets us show that certain natural classes are not homogenizable: 1) the class of locally consistent systems of linear equations over the two-element field or any finite Abelian group, and 2) the class of finite structures that forbid homomorphisms from a specific MSO-definable class of structures of treewidth two. In combination with known results, the first example shows that, up to pp-interpretability, the CSPs that are solvable by local consistency methods are distinguished from the rest by the fact that their classes of locally consistent instances are homogenizable. The second example shows that, for MSO-definable classes of forbidden patterns, treewidth one versus two is the dividing line to homogenizability.
Cite as
Albert Atserias and Szymon Torunczyk. Non-Homogenizable Classes of Finite Structures. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{atserias_et_al:LIPIcs.CSL.2016.16,
author = {Atserias, Albert and Torunczyk, Szymon},
title = {{Non-Homogenizable Classes of Finite Structures}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {16:1--16:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.16},
URN = {urn:nbn:de:0030-drops-65563},
doi = {10.4230/LIPIcs.CSL.2016.16},
annote = {Keywords: Fra\"{i}ss\'{e} class, amalgmation class, reduct, Constraint Satisfaction Problem, bounded width}
}
Document
Context-Free Graph Properties via Definable Decompositions
Abstract
Monadic-second order logic (MSO-logic) is successfully applied in both language theory and algorithm design. In the former, properties definable by MSO-formulas are exactly the regular properties on many structures like, most prominently, strings. In the latter, solving a problem for structures of bounded tree width is routinely done by defining it in terms of an MSO-formula and applying general formula-evaluation procedures like Courcelle's. The present paper furthers the study of second-order logics with close connections to language theory and algorithm design beyond MSO-logic.
We introduce a logic that allows to expand a given structure with an existentially quantified tree decomposition of bounded width and test an MSO-definable property for the resulting expanded structure. It is proposed as a candidate for capturing the notion of "context-free graph properties" since it corresponds to the context-free languages on strings, has the same closure properties, and an alternative definition similar to the one of Chomsky and Schützenberger for context-free languages. Besides studying its language-theoretic aspects, we consider its expressive power as well as the algorithmics of its satisfiability and evaluation problems.
Cite as
Michael Elberfeld. Context-Free Graph Properties via Definable Decompositions. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{elberfeld:LIPIcs.CSL.2016.17,
author = {Elberfeld, Michael},
title = {{Context-Free Graph Properties via Definable Decompositions}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {17:1--17:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.17},
URN = {urn:nbn:de:0030-drops-65575},
doi = {10.4230/LIPIcs.CSL.2016.17},
annote = {Keywords: finite model theory, monadic second-order logic, tree decomposition, context-free languages, expressive power}
}
Document
Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs
Abstract
We show that the model-checking problem for successor-invariant first-order logic is fixed-parameter tractable on graphs with excluded topological subgraphs when parameterised by both the size of the input formula and the size of the exluded topological subgraph. Furthermore, we show that model-checking for order-invariant first-order logic is tractable on coloured posets of bounded width, parameterised by both the size of the input formula and the width of the poset.
Results of this form, i.e. showing that model-checking for a certain logic is tractable on a certain class of structures, are often referred to as algorithmic meta-theorems since they give a unified proof for the tractability of a whole range of problems. First-order logic is arguably one of the most important logics in this context since it is powerful enough to express many computational problems (e.g. the existence of cliques, dominating sets etc.) and yet its model-checking problem is tractable on rich classes of graphs. In fact, Grohe et al have shown that model-checking for FO is tractable on all nowhere dense classes of graphs.
Successor-invariant FO is a semantic extension of FO by allowing the use of an additional binary relation which is interpreted as a directed Hamiltonian cycle, restricted to formulae whose truth value does not depend on the specific choice of a Hamiltonian cycle. While this is very natural in the context of model-checking (after all, storing a structure in computer memory usually brings with it a linear order on the structure), the question of how the computational complexity of the model-checking problem for this richer logic compares to that of plain FO is still open.
Our result for successor-invariant FO extends previous results for this logic on planar graphs and graphs with excluded minors, further narrowing the gap between what is known for FO and what is known for successor-invariant FO. The proof uses Grohe and Marx's structure theorem for graphs with excluded topological subgraphs. For order-invariant FO we show that Gajarský et al.'s recent result for FO carries over to order-invariant FO.
Cite as
Kord Eickmeyer and Ken-ichi Kawarabayashi. Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{eickmeyer_et_al:LIPIcs.CSL.2016.18,
author = {Eickmeyer, Kord and Kawarabayashi, Ken-ichi},
title = {{Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {18:1--18:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.18},
URN = {urn:nbn:de:0030-drops-65583},
doi = {10.4230/LIPIcs.CSL.2016.18},
annote = {Keywords: model-checking, algorithmic meta-theorem, successor-invariant, first-order logic, topological subgraphs, parameterised complexity}
}
Document
Definability of Cai-Fürer-Immerman Problems in Choiceless Polynomial Time
Abstract
Choiceless Polynomial Time (CPT) is one of the most promising candidates in the search for a logic capturing Ptime. The question whether there is a logic that expresses exactly the polynomial-time computable properties of finite structures, which has been open for more than 30 years, is one of the most important and challenging problems in finite model theory.
The strength of Choiceless Polynomial Time is its ability to perform isomorphism-invariant computations over structures, using hereditarily finite sets as data structures. But, as it preserves symmetries, it is choiceless in the sense that it cannot select an arbitrary element of a set - an operation which is crucial for many classical algorithms. CPT can define many interesting Ptime queries, including (the original version of) the Cai-Fürer-Immerman (CFI) query.
The CFI query is particularly interesting because it separates fixed-point logic with counting from Ptime, and has since remained the main benchmark for the expressibility of logics within Ptime. The CFI construction associates with each connected graph a set of CFI-graphs that can be partitioned into exactly two isomorphism classes called odd and even CFI-graphs. The problem is to decide, given a CFI-graph, whether it is odd or even. In the original version, the underlying graphs are linearly ordered, and for this case, Dawar, Richerby and Rossman proved that the CFI query is CPT-definable. However, the CFI query over general graphs remains one of the few known examples for which CPT-definability is open.
Our first contribution generalises the result by Dawar, Richerby and Rossman to the variant of the CFI query where the underlying graphs have colour classes of logarithmic size, instead of colour class size one. Secondly, we consider the CFI query over graph classes where the maximal degree is linear in the size of the graphs. For these classes, we establish CPT-definability using only sets of small, constant rank, which is known to be impossible for the general case.
In our CFI-recognising procedures we strongly make use of the ability of CPT to create sets, rather than tuples only, and we further prove that, if CPT worked over tuples instead, no such procedure would be definable. We introduce a notion of "sequence-like objects" based on the structure of the graphs' symmetry groups, and we show that no CPT-program which only uses sequence-like objects can decide the CFI query over complete graphs, which have linear maximal degree. From a broader perspective, this generalises a result by Blass, Gurevich, and van den Bussche about the power of isomorphism-invariant machine models (for polynomial time) to a setting with counting.
Cite as
Wied Pakusa, Svenja Schalthöfer, and Erkal Selman. Definability of Cai-Fürer-Immerman Problems in Choiceless Polynomial Time. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{pakusa_et_al:LIPIcs.CSL.2016.19,
author = {Pakusa, Wied and Schalth\"{o}fer, Svenja and Selman, Erkal},
title = {{Definability of Cai-F\"{u}rer-Immerman Problems in Choiceless Polynomial Time}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.19},
URN = {urn:nbn:de:0030-drops-65595},
doi = {10.4230/LIPIcs.CSL.2016.19},
annote = {Keywords: finite model theory, descriptive complexity, logic for textsc\{Ptime\}, Choiceless Polynomial Time, Cai-F\"{u}rer-Immerman}
}
Document
Descriptive Complexity of #AC^0 Functions
Abstract
We introduce a new framework for a descriptive complexity approach to arithmetic computations. We define a hierarchy of classes based on the idea of counting assignments to free function variables in first-order formulae. We completely determine the inclusion structure and show that #P and #AC^0 appear as classes of this hierarchy. In this way, we unconditionally place #AC^0 properly in a strict hierarchy of arithmetic classes within #P. We compare our classes with a hierarchy within #P defined in a model-theoretic way by Saluja et al. We argue that our approach is better suited to study arithmetic circuit classes such as #AC^0 which can be descriptively characterized as a class in our framework.
Cite as
Arnaud Durand, Anselm Haak, Juha Kontinen, and Heribert Vollmer. Descriptive Complexity of #AC^0 Functions. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{durand_et_al:LIPIcs.CSL.2016.20,
author = {Durand, Arnaud and Haak, Anselm and Kontinen, Juha and Vollmer, Heribert},
title = {{Descriptive Complexity of #AC^0 Functions}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {20:1--20:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.20},
URN = {urn:nbn:de:0030-drops-65601},
doi = {10.4230/LIPIcs.CSL.2016.20},
annote = {Keywords: finite model theory, Fagin's theorem, arithmetic circuits, counting classes, Skolem function}
}
Document
Extending Homotopy Type Theory with Strict Equality
Abstract
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an "outer" one, containing a strict equality type former, and an "inner" one, which is some version of HoTT. Our type theory is inspired by Voevodsky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we do not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of "infinite structures" which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with "schematic" definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.
Cite as
Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{altenkirch_et_al:LIPIcs.CSL.2016.21,
author = {Altenkirch, Thorsten and Capriotti, Paolo and Kraus, Nicolai},
title = {{Extending Homotopy Type Theory with Strict Equality}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {21:1--21:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.21},
URN = {urn:nbn:de:0030-drops-65612},
doi = {10.4230/LIPIcs.CSL.2016.21},
annote = {Keywords: homotopy type theory, coherences, strict equality, homotopy type system}
}
Document
The Seifert-van Kampen Theorem in Homotopy Type Theory
Abstract
Homotopy type theory is a recent research area connecting type theory with homotopy theory by interpreting types as spaces. In particular, one can prove and mechanize type-theoretic analogues of homotopy-theoretic theorems, yielding "synthetic homotopy theory". Here we consider the Seifert-van Kampen theorem, which characterizes the loop structure of spaces obtained by gluing. This is useful in homotopy theory because many spaces are constructed by gluing, and the loop structure helps distinguish distinct spaces. The synthetic proof showcases many new characteristics of synthetic homotopy theory, such as the "encode-decode" method, enforced homotopy-invariance, and lack of underlying sets.
Cite as
Kuen-Bang Hou (Favonia) and Michael Shulman. The Seifert-van Kampen Theorem in Homotopy Type Theory. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{hou(favonia)_et_al:LIPIcs.CSL.2016.22,
author = {Hou (Favonia), Kuen-Bang and Shulman, Michael},
title = {{The Seifert-van Kampen Theorem in Homotopy Type Theory}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {22:1--22:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.22},
URN = {urn:nbn:de:0030-drops-65626},
doi = {10.4230/LIPIcs.CSL.2016.22},
annote = {Keywords: homotopy type theory, fundamental group, homotopy pushout, mechanized reasoning}
}
Document
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
Abstract
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, is conjectured to have decidable type checking, and has an implemented type checker. Our new type theory, called guarded cubical type theory, provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation, and present semantics in a presheaf category.
Cite as
Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{birkedal_et_al:LIPIcs.CSL.2016.23,
author = {Birkedal, Lars and Bizjak, Ale\v{s} and Clouston, Ranald and Grathwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea},
title = {{Guarded Cubical Type Theory: Path Equality for Guarded Recursion}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {23:1--23:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.23},
URN = {urn:nbn:de:0030-drops-65638},
doi = {10.4230/LIPIcs.CSL.2016.23},
annote = {Keywords: Guarded Recursion, Dependent Type Theory, Cubical Type Theory, Denotational Semantics, Homotopy Type Theory}
}
Document
Axioms for Modelling Cubical Type Theory in a Topos
Abstract
The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an interval-like object I in a topos to give a model of type theory in which elements of identity types are 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. Furthermore, since our axioms can be satisfied in a number of different ways, we show that there is a range of topos-theoretic models of homotopy type theory in this style.
Cite as
Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{orton_et_al:LIPIcs.CSL.2016.24,
author = {Orton, Ian and Pitts, Andrew M.},
title = {{Axioms for Modelling Cubical Type Theory in a Topos}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {24:1--24:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.24},
URN = {urn:nbn:de:0030-drops-65647},
doi = {10.4230/LIPIcs.CSL.2016.24},
annote = {Keywords: models of dependent type theory, homotopy type theory, cubical sets, cubical type theory, topos, univalence}
}
Document
Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis
Abstract
This paper is about the bar recursion operator in the context of classical realizability. The pioneering work of Berardi, Bezem, Coquand was enhanced by Berger and Oliva. Then Streicher has shown, by means of their bar recursion operator, that the realizability models of ZF, obtained from usual models of lambda-calculus (Scott domains, coherent spaces, ...), satisfy the axiom of dependent choice. We give a proof of this result, using the tools of classical realizability. Moreover, we show that these realizability models satisfy the well ordering of R and the continuum hypothesis. These formulas are therefore realized by closed lambda_c-terms. This new result allows to obtain programs from proofs of arithmetical formulas using all these axioms.
Cite as
Jean-Louis Krivine. Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 25:1-25:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{krivine:LIPIcs.CSL.2016.25,
author = {Krivine, Jean-Louis},
title = {{Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {25:1--25:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.25},
URN = {urn:nbn:de:0030-drops-65650},
doi = {10.4230/LIPIcs.CSL.2016.25},
annote = {Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}
Document
Extracting Non-Deterministic Concurrent Programs
Abstract
We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of non-deterministic concurrent programs from proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code for real numbers.
Cite as
Ulrich Berger. Extracting Non-Deterministic Concurrent Programs. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 26:1-26:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{berger:LIPIcs.CSL.2016.26,
author = {Berger, Ulrich},
title = {{Extracting Non-Deterministic Concurrent Programs}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {26:1--26:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.26},
URN = {urn:nbn:de:0030-drops-65669},
doi = {10.4230/LIPIcs.CSL.2016.26},
annote = {Keywords: Proof theory, realizability, program extraction, non-determinism, concurrency, computable analysis}
}
Document
Polymorphic Game Semantics for Dynamic Binding
Abstract
We present a game semantics for an expressive typing system for block-structured programs with late binding of variables and System F style polymorphism. As well as generic programs and abstract datatypes, this combination may be used to represent behaviour such as dynamic dispatch and method overriding.
We give a denotational models for a hierarchy of programming languages based on our typing system, including variants of PCF and Idealized Algol. These are obtained by extending polymorphic game semantics to block-structured programs. We show that the categorical structure of our models can be used to give a new interpretation of dynamic binding, and establish definability properties by imposing constraints which are identical or similar to those used to characterize definability in PCF (innocence, well-bracketing, determinacy). Moreover, relaxing these can similarly allow the interpretation of side-effects (state, control, non-determinism) - we show that in particular we may obtain a fully abstract semantics of polymorphic Idealized Algol with dynamic binding by following exactly the methodology employed in the simply-typed case.
Cite as
James Laird. Polymorphic Game Semantics for Dynamic Binding. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{laird:LIPIcs.CSL.2016.27,
author = {Laird, James},
title = {{Polymorphic Game Semantics for Dynamic Binding}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {27:1--27:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.27},
URN = {urn:nbn:de:0030-drops-65671},
doi = {10.4230/LIPIcs.CSL.2016.27},
annote = {Keywords: Game semantics, denotational models, PCF, Idealized Algol}
}
Document
High-Quality Synthesis Against Stochastic Environments
Abstract
In the classical synthesis problem, we are given a linear temporal logic (LTL) formula psi over sets of input and output signals, and we synthesize a transducer that realizes psi: with every sequence of input signals, the transducer associates a sequence of output signals so that the generated computation satisfies psi. One weakness of automated synthesis in practice is that it pays no attention to the quality of the synthesized system. Indeed, the classical setting is Boolean: a computation satisfies a specification or does not satisfy it. Accordingly, while the synthesized system is correct, there is no guarantee about its quality. In recent years, researchers have considered extensions of the classical Boolean setting to a quantitative one. The logic FLTL is a multi-valued logic that augments LTL with quality operators. The satisfaction value of an FLTL formula is a real value in [0,1], where the higher the value is, the higher is the quality in which the computation satisfies the specification.
Decision problems for LTL become search or optimization problems for FLTL. In particular, in the synthesis problem, the goal is to generate a transducer that satisfies the specification in the highest possible quality. Previous work considered the worst-case setting, where the goal is to maximize the quality of the computation with the minimal quality. We introduce and solve the stochastic setting, where the goal is to generate a transducer that maximizes the expected quality of a computation, subject to a given distribution of the input signals. Thus, rather than being hostile, the environment is assumed to be probabilistic, which corresponds to many realistic settings. We show that the problem is 2EXPTIME-complete, like classical LTL synthesis. The complexity stays 2EXPTIME also in two extensions we consider: one that maximizes the expected quality while guaranteeing that the minimal quality is, with probability 1, above a given threshold, and one that allows assumptions on the environment.
Cite as
Shaull Almagor and Orna Kupferman. High-Quality Synthesis Against Stochastic Environments. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CSL.2016.28,
author = {Almagor, Shaull and Kupferman, Orna},
title = {{High-Quality Synthesis Against Stochastic Environments}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {28:1--28:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.28},
URN = {urn:nbn:de:0030-drops-65688},
doi = {10.4230/LIPIcs.CSL.2016.28},
annote = {Keywords: Stochastic and Quantitative Synthesis, Markov Decision Process}
}
Document
Hedging Bets in Markov Decision Processes
Abstract
The classical model of Markov decision processes with costs or rewards, while widely used to formalize optimal decision making, cannot capture scenarios where there are multiple objectives for the agent during the system evolution, but only one of these objectives gets actualized upon termination. We introduce the model of Markov decision processes with alternative objectives (MDPAO) for formalizing optimization in such scenarios. To compute the strategy to optimize the expected cost/reward upon termination, we need to figure out how to balance the values of the alternative objectives. This requires analysis of the underlying infinite-state process that tracks the accumulated values of all the objectives. While the decidability of the problem of computing the exact optimal strategy for the general model remains open, we present the following results. First, for a Markov chain with alternative objectives, the optimal expected cost/reward can be computed in polynomial-time. Second, for a single-state process with two actions and multiple objectives we show how to compute the optimal decision strategy. Third, for a process with only two alternative objectives, we present a reduction to the minimum expected accumulated reward problem for one-counter MDPs, and this leads to decidability for this case under some technical restrictions. Finally, we show that optimal cost/reward can be approximated up to a constant additive factor for the general problem.
Cite as
Rajeev Alur, Marco Faella, Sampath Kannan, and Nimit Singhania. Hedging Bets in Markov Decision Processes. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{alur_et_al:LIPIcs.CSL.2016.29,
author = {Alur, Rajeev and Faella, Marco and Kannan, Sampath and Singhania, Nimit},
title = {{Hedging Bets in Markov Decision Processes}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {29:1--29:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.29},
URN = {urn:nbn:de:0030-drops-65698},
doi = {10.4230/LIPIcs.CSL.2016.29},
annote = {Keywords: Markov decision processes, Infinite state systems, Multi-objective optimization}
}
Document
Minimizing Regret in Discounted-Sum Games
Abstract
In this paper, we study the problem of minimizing regret in discounted-sum games played on weighted game graphs. We give algorithms for the general problem of computing the minimal regret of the controller (Eve) as well as several variants depending on which strategies the environment (Adam) is permitted to use. We also consider the problem of synthesizing regret-free strategies for Eve in each of these scenarios.
Cite as
Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Minimizing Regret in Discounted-Sum Games. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{hunter_et_al:LIPIcs.CSL.2016.30,
author = {Hunter, Paul and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
title = {{Minimizing Regret in Discounted-Sum Games}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {30:1--30:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.30},
URN = {urn:nbn:de:0030-drops-65704},
doi = {10.4230/LIPIcs.CSL.2016.30},
annote = {Keywords: Quantitative games, Regret, Verification, Synthesis, Game theory}
}
Document
Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs
Abstract
The winning condition of a parity game with costs requires an arbitrary, but fixed bound on the distance between occurrences of odd colors and the next occurrence of a larger even one. Such games quantitatively extend parity games while retaining most of their attractive properties, i.e, determining the winner is in NP and co-NP and one player has positional winning strategies.
We show that the characteristics of parity games with costs are vastly different when asking for strategies realizing the minimal such bound: the solution problem becomes PSPACE-complete and exponential memory is both necessary in general and always sufficient. Thus, playing parity games with costs optimally is harder than just winning them. Moreover, we show that the tradeoff between the memory size and the realized bound is gradual in general.
Cite as
Alexander Weinert and Martin Zimmermann. Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{weinert_et_al:LIPIcs.CSL.2016.31,
author = {Weinert, Alexander and Zimmermann, Martin},
title = {{Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {31:1--31:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.31},
URN = {urn:nbn:de:0030-drops-65714},
doi = {10.4230/LIPIcs.CSL.2016.31},
annote = {Keywords: Parity Games with Costs, Optimal Strategies, Memory Requirements, Tradeoffs}
}
Document
A Sequent Calculus for a Modal Logic on Finite Data Trees
Abstract
We investigate the proof theory of a modal fragment of XPath equipped with data (in)equality tests over finite data trees, i.e., over finite unranked trees where nodes are labelled with both a symbol from a finite alphabet and a single data value from an infinite domain. We present a sound and complete sequent calculus for this logic, which yields the optimal PSPACE complexity bound for its validity problem.
Cite as
David Baelde, Simon Lunel, and Sylvain Schmitz. A Sequent Calculus for a Modal Logic on Finite Data Trees. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{baelde_et_al:LIPIcs.CSL.2016.32,
author = {Baelde, David and Lunel, Simon and Schmitz, Sylvain},
title = {{A Sequent Calculus for a Modal Logic on Finite Data Trees}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {32:1--32:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.32},
URN = {urn:nbn:de:0030-drops-65720},
doi = {10.4230/LIPIcs.CSL.2016.32},
annote = {Keywords: XPath, proof systems, modal logic, complexity}
}
Document
Axiomatizations for Propositional and Modal Team Logic
Abstract
A framework is developed that extends Hilbert-style proof systems for propositional and modal logics to comprehend their team-based counterparts. The method is applied to classical propositional logic and the modal logic K. Complete axiomatizations for their team-based extensions, propositional team logic PTL and modal team logic MTL, are presented.
Cite as
Martin Lück. Axiomatizations for Propositional and Modal Team Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{luck:LIPIcs.CSL.2016.33,
author = {L\"{u}ck, Martin},
title = {{Axiomatizations for Propositional and Modal Team Logic}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {33:1--33:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.33},
URN = {urn:nbn:de:0030-drops-65739},
doi = {10.4230/LIPIcs.CSL.2016.33},
annote = {Keywords: team logic, propositional team logic, modal team logic, proof system, axiomatization}
}
Document
Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4
Abstract
In this work we look at how Fitting's embedding of first-order classical logic into first-order S4 can help in reasoning when we are interested in satisfaction "in most cases", when first-order properties are allowed to fail in cases that are considered insignificant. We extend classical semantics by combining a Kripke-style model construction of "significant" events as possible worlds with the forcing-Fitting-style semantics construction by embedding classical logic into S4. We provide various examples. Our main running example is an application to symbolic security protocol verification with complexity-theoretic guarantees. In particular, we show how Fitting's embedding emerges entirely naturally when verifying trace properties in computer security.
Cite as
Gergei Bana and Mitsuhiro Okada. Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bana_et_al:LIPIcs.CSL.2016.34,
author = {Bana, Gergei and Okada, Mitsuhiro},
title = {{Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {34:1--34:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.34},
URN = {urn:nbn:de:0030-drops-65746},
doi = {10.4230/LIPIcs.CSL.2016.34},
annote = {Keywords: first-order logic, possible-world semantics, Fitting embedding, asymptotic probabilities, verification of complexity-theoretic properties}
}
Document
Counting in Team Semantics
Abstract
We explore several counting constructs for logics with team semantics. Counting is an important task in numerous applications, but with a somewhat delicate relationship to logic. Team semantics on the other side is the mathematical basis of modern logics of dependence and independence, in which formulae are evaluated not for a single assignment of values to variables, but for a set of such assignments. It is therefore interesting to ask what kind of counting constructs are adequate in this context, and how such constructs influence the expressive power, and the model-theoretic and algorithmic properties of logics with team semantics. Due to the second-order features of team semantics there is a rich variety of potential counting constructs. Here we study variations of two main ideas: forking atoms and counting quantifiers.
Forking counts how many different values for a tuple w occur in assignments with coinciding values for v. We call this the forking degree of bar v with respect to bar w. Forking is powerful enough to capture many of the previously studied atomic dependency properties. In particular we exhibit logics with forking atoms that have, respectively, precisely the power of dependence logic and independence logic.
Our second approach uses counting quantifiers E^{geq mu} of a similar kind as used in logics with Tarski semantics. The difference is that these quantifiers are now applied to teams of assignments that may give different values to mu. We show that, on finite structures, there is an intimate connection between inclusion logic with counting quantifiers and FPC, fixed-point logic with counting, which is a logic of fundamental importance for descriptive complexity theory. For sentences, the two logics have the same expressive power. Our analysis is based on a new variant of model-checking games, called threshold safety games, on a trap condition for such games, and on game interpretations.
Cite as
Erich Grädel and Stefan Hegselmann. Counting in Team Semantics. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{gradel_et_al:LIPIcs.CSL.2016.35,
author = {Gr\"{a}del, Erich and Hegselmann, Stefan},
title = {{Counting in Team Semantics}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {35:1--35:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.35},
URN = {urn:nbn:de:0030-drops-65757},
doi = {10.4230/LIPIcs.CSL.2016.35},
annote = {Keywords: logics with counting, team semantics, fixed-point logic with counting}
}
Document
The Logical Strength of Büchi's Decidability Theorem
Abstract
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, less_or_equal). We prove that the following are equivalent over the weak second-order arithmetic theory RCA:
1. Büchi's complementation theorem for nondeterministic automata on infinite words,
2. the decidability of the depth-n fragment of the MSO theory of (N, less_or_equal), for each n greater than 5,
3. the induction scheme for Sigma^0_2 formulae of arithmetic.
Moreover, each of (1)-(3) is equivalent to the additive version of Ramsey's Theorem for pairs, often used in proofs of (1); each of (1)-(3) implies McNaughton's determinisation theorem for automata on infinite words; and each of (1)-(3) implies the "bounded-width" version of König's Lemma, often used in proofs of McNaughton's theorem.
Cite as
Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, and Michal Skrzypczak. The Logical Strength of Büchi's Decidability Theorem. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{kolodziejczyk_et_al:LIPIcs.CSL.2016.36,
author = {Kolodziejczyk, Leszek Aleksander and Michalewski, Henryk and Pradic, Pierre and Skrzypczak, Michal},
title = {{The Logical Strength of B\"{u}chi's Decidability Theorem}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {36:1--36:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.36},
URN = {urn:nbn:de:0030-drops-65765},
doi = {10.4230/LIPIcs.CSL.2016.36},
annote = {Keywords: nondeterministic automata, monadic second-order logic, B\"{u}chi's theorem, additive Ramsey's theorem, reverse mathematics}
}
Document
The Height of Piecewise-Testable Languages with Applications in Logical Complexity
Abstract
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 paper 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 FO^2(A^*, subword), 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.
Cite as
Prateek Karandikar and Philippe Schnoebelen. The Height of Piecewise-Testable Languages with Applications in Logical Complexity. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 37:1-37:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{karandikar_et_al:LIPIcs.CSL.2016.37,
author = {Karandikar, Prateek and Schnoebelen, Philippe},
title = {{The Height of Piecewise-Testable Languages with Applications in Logical Complexity}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {37:1--37:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.37},
URN = {urn:nbn:de:0030-drops-65776},
doi = {10.4230/LIPIcs.CSL.2016.37},
annote = {Keywords: Descriptive complexity}
}
Document
One-Dimensional Logic over Words
Abstract
One-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential quantifiers that leave at most one variable free. We investigate one-dimensional fragment over words and over omega-words. We show that it is expressively equivalent to the two-variable fragment of first-order logic. We also show that its satisfiability problem is NExpTime-complete. Further, we show undecidability of some extensions, whose two-variable counterparts remain decidable.
Cite as
Emanuel Kieronski. One-Dimensional Logic over Words. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 38:1-38:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{kieronski:LIPIcs.CSL.2016.38,
author = {Kieronski, Emanuel},
title = {{One-Dimensional Logic over Words}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {38:1--38:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.38},
URN = {urn:nbn:de:0030-drops-65782},
doi = {10.4230/LIPIcs.CSL.2016.38},
annote = {Keywords: satisfiability, expressivity, words, fragments of first-order logic}
}
Document
Quine's Fluted Fragment is Non-Elementary
Abstract
We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified by W.V. Quine. We show that the satisfiability problem for this fragment has non-elementary complexity, thus refuting an earlier published claim by W.C. Purdy that it is in NExpTime. More precisely, we consider, for all m greater than 1, the intersection of the fluted fragment and the m-variable fragment of first-order logic. We show that this sub-fragment forces (m/2)-tuply exponentially large models, and that its satisfiability problem is (m/2)-NExpTime-hard. We round off by using a corrected version of Purdy's construction to show that the m-variable fluted fragment has the m-tuply exponential model property, and that its satisfiability problem is in m-NExpTime.
Cite as
Ian Pratt-Hartmann, Wieslaw Szwast, and Lidia Tendera. Quine's Fluted Fragment is Non-Elementary. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{pratthartmann_et_al:LIPIcs.CSL.2016.39,
author = {Pratt-Hartmann, Ian and Szwast, Wieslaw and Tendera, Lidia},
title = {{Quine's Fluted Fragment is Non-Elementary}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {39:1--39:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.39},
URN = {urn:nbn:de:0030-drops-65791},
doi = {10.4230/LIPIcs.CSL.2016.39},
annote = {Keywords: Quine, fluted fragment, Purdy, non-elementary, satisfiability, decidability}
}
Document
Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic
Abstract
We prove a general form of 'free-cut elimination' for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing theorem for a fragment of this arithmetic via the `witness function method', showing that the provably convergent functions are precisely the polynomial-time functions. The programs extracted are implemented in the framework of 'safe' recursive functions, due to Bellantoni and Cook, where the ! modality of linear logic corresponds to normal inputs of a safe recursive program.
Cite as
Patrick Baillot and Anupam Das. Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{baillot_et_al:LIPIcs.CSL.2016.40,
author = {Baillot, Patrick and Das, Anupam},
title = {{Free-Cut Elimination in Linear Logic and an Application to a Feasible Arithmetic}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {40:1--40:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.40},
URN = {urn:nbn:de:0030-drops-65807},
doi = {10.4230/LIPIcs.CSL.2016.40},
annote = {Keywords: proof theory, linear logic, bounded arithmetic, polynomial time computation, implicit computational complexity}
}
Document
The Relational Model Is Injective for Multiplicative Exponential Linear Logic
Abstract
We prove a completeness result for Multiplicative Exponential Linear Logic (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.
Cite as
Daniel de Carvalho. The Relational Model Is Injective for Multiplicative Exponential Linear Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{decarvalho:LIPIcs.CSL.2016.41,
author = {de Carvalho, Daniel},
title = {{The Relational Model Is Injective for Multiplicative Exponential Linear Logic}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {41:1--41:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.41},
URN = {urn:nbn:de:0030-drops-65815},
doi = {10.4230/LIPIcs.CSL.2016.41},
annote = {Keywords: Linear Logic, Denotational semantics, Proof-nets}
}
Document
Infinitary Proof Theory: the Multiplicative Additive Case
Abstract
Infinitary and regular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, very little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is notably based on two fundamental properties of a proof system: cut elimination and focalization. The first one is only known to hold for restricted (purely additive) infinitary calculi, thanks to the work of Santocanale and Fortier; the second one has never been studied in infinitary systems. In this paper, we consider the infinitary proof system muMALLi for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish muMALLi as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems.
Cite as
David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{baelde_et_al:LIPIcs.CSL.2016.42,
author = {Baelde, David and Doumane, Amina and Saurin, Alexis},
title = {{Infinitary Proof Theory: the Multiplicative Additive Case}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {42:1--42:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.42},
URN = {urn:nbn:de:0030-drops-65825},
doi = {10.4230/LIPIcs.CSL.2016.42},
annote = {Keywords: Infinitary proofs, linear logic}
}