Volume
LIPIcs, Volume 119
27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2018, September 4-7, 2018, Birmingham, GBEditors
Publication Details
- published at: 2018-08-29
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-088-0
- DBLP: db/conf/csl/csl2018
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 119, CSL'18, Complete Volume
Abstract
LIPIcs, Volume 119, CSL'18, Complete Volume
Cite as
27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Proceedings{ghica_et_al:LIPIcs.CSL.2018,
title = {{LIPIcs, Volume 119, CSL'18, Complete Volume}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018},
URN = {urn:nbn:de:0030-drops-97444},
doi = {10.4230/LIPIcs.CSL.2018},
annote = {Keywords: Theory of computation, Software and its engineering, Formal language definitions, Formal software verification}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ghica_et_al:LIPIcs.CSL.2018.0,
author = {Ghica, Dan R. and Jung, Achim},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.0},
URN = {urn:nbn:de:0030-drops-96679},
doi = {10.4230/LIPIcs.CSL.2018.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
The Ackermann Award 2018
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 2018 edition of the award.
Cite as
Dexter Kozen and Thomas Schwentick. The Ackermann Award 2018. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kozen_et_al:LIPIcs.CSL.2018.1,
author = {Kozen, Dexter and Schwentick, Thomas},
title = {{The Ackermann Award 2018}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {1:1--1:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.1},
URN = {urn:nbn:de:0030-drops-96686},
doi = {10.4230/LIPIcs.CSL.2018.1},
annote = {Keywords: Ackermann Award}
}
Document
Relating Structure and Power: Comonadic Semantics for Computational Resources
Abstract
Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraïssé games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraïssé comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory.
Cite as
Samson Abramsky and Nihil Shah. Relating Structure and Power: Comonadic Semantics for Computational Resources. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{abramsky_et_al:LIPIcs.CSL.2018.2,
author = {Abramsky, Samson and Shah, Nihil},
title = {{Relating Structure and Power: Comonadic Semantics for Computational Resources}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {2:1--2:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.2},
URN = {urn:nbn:de:0030-drops-96698},
doi = {10.4230/LIPIcs.CSL.2018.2},
annote = {Keywords: Finite model theory, combinatorial games, Ehrenfeucht-Fra\"{i}ss\'{e} games, pebble games, bisimulation, comonads, coKleisli category, coalgebras of a comonad}
}
Document
Climbing up the Elementary Complexity Classes with Theories of Automatic Structures
Abstract
Automatic structures are structures that admit a finite presentation via automata. Their most prominent feature is that their theories are decidable. In the literature, one finds automatic structures with non-elementary theory (e.g., the complete binary tree with equal-level predicate) and automatic structures whose theories are at most 3-fold exponential (e.g., Presburger arithmetic or infinite automatic graphs of bounded degree). This observation led Durand-Gasselin to the question whether there are automatic structures of arbitrary high elementary complexity.
We give a positive answer to this question. Namely, we show that for every h >=0 the forest of (infinitely many copies of) all finite trees of height at most h+2 is automatic and it's theory is complete for STA(*, exp_h(n, poly(n)), poly(n)), an alternating complexity class between h-fold exponential time and space. This exact determination of the complexity of the theory of these forests might be of independent interest.
Cite as
Faried Abu Zaid, Dietrich Kuske, and Peter Lindner. Climbing up the Elementary Complexity Classes with Theories of Automatic Structures. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{abuzaid_et_al:LIPIcs.CSL.2018.3,
author = {Abu Zaid, Faried and Kuske, Dietrich and Lindner, Peter},
title = {{Climbing up the Elementary Complexity Classes with Theories of Automatic Structures}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {3:1--3:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.3},
URN = {urn:nbn:de:0030-drops-96701},
doi = {10.4230/LIPIcs.CSL.2018.3},
annote = {Keywords: Automatic Structures, Complexity Theory, Model Theory}
}
Document
High-Level Signatures and Initial Semantics
Abstract
We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we consider a general notion of "signature" for specifying syntactic constructions. Our signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend to much more general examples.
In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object - if it exists - in a suitable category of models. Our notions of signature and syntax are suited for compositionality and provide, beyond the desired algebra of terms, a well-behaved substitution and the associated inductive/recursive principles.
Our signatures are "general" in the sense that the existence of an associated syntax is not automatically guaranteed. In this work, we identify a large and simple class of signatures which do generate a syntax.
This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu.
The main results presented in the paper are computer-checked within the UniMath system.
Cite as
Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. High-Level Signatures and Initial Semantics. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ahrens_et_al:LIPIcs.CSL.2018.4,
author = {Ahrens, Benedikt and Hirschowitz, Andr\'{e} and Lafont, Ambroise and Maggesi, Marco},
title = {{High-Level Signatures and Initial Semantics}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {4:1--4:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.4},
URN = {urn:nbn:de:0030-drops-96713},
doi = {10.4230/LIPIcs.CSL.2018.4},
annote = {Keywords: initial semantics, signatures, syntax, monadic substitution, computer-checked proofs}
}
Document
The True Concurrency of Herbrand's Theorem
Abstract
Herbrand's theorem, widely regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. In the general case, it reduces first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers.
In this paper, we show that Herbrand's theorem in its general form can be elegantly stated and proved as a theorem in the framework of concurrent games, a denotational semantics designed to faithfully represent causality and independence in concurrent systems, thereby exposing the concurrency underlying the computational content of classical proofs. The causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers implicit in proofs. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a well-chosen denotational model.
Cite as
Aurore Alcolei, Pierre Clairambault, Martin Hyland, and Glynn Winskel. The True Concurrency of Herbrand's Theorem. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{alcolei_et_al:LIPIcs.CSL.2018.5,
author = {Alcolei, Aurore and Clairambault, Pierre and Hyland, Martin and Winskel, Glynn},
title = {{The True Concurrency of Herbrand's Theorem}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {5:1--5:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.5},
URN = {urn:nbn:de:0030-drops-96723},
doi = {10.4230/LIPIcs.CSL.2018.5},
annote = {Keywords: Herbrand's theorem, Game semantics, True concurrency}
}
Document
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities
Abstract
We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.
Cite as
Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{angiuli_et_al:LIPIcs.CSL.2018.6,
author = {Angiuli, Carlo and Hou (Favonia), Kuen-Bang and Harper, Robert},
title = {{Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {6:1--6:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6},
URN = {urn:nbn:de:0030-drops-96734},
doi = {10.4230/LIPIcs.CSL.2018.6},
annote = {Keywords: Homotopy Type Theory, Two-Level Type Theory, Computational Type Theory, Cubical Sets}
}
Document
Definable Inapproximability: New Challenges for Duplicator
Abstract
We consider the hardness of approximation of optimization problems from the point of view of definability. For many NP-hard optimization problems it is known that, unless P = NP, no polynomial-time algorithm can give an approximate solution guaranteed to be within a fixed constant factor of the optimum. We show, in several such instances and without any complexity theoretic assumption, that no algorithm that is expressible in fixed-point logic with counting (FPC) can compute an approximate solution. Since important algorithmic techniques for approximation algorithms (such as linear or semidefinite programming) are expressible in FPC, this yields lower bounds on what can be achieved by such methods. The results are established by showing lower bounds on the number of variables required in first-order logic with counting to separate instances with a high optimum from those with a low optimum for fixed-size instances.
Cite as
Albert Atserias and Anuj Dawar. Definable Inapproximability: New Challenges for Duplicator. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{atserias_et_al:LIPIcs.CSL.2018.7,
author = {Atserias, Albert and Dawar, Anuj},
title = {{Definable Inapproximability: New Challenges for Duplicator}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {7:1--7:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.7},
URN = {urn:nbn:de:0030-drops-96742},
doi = {10.4230/LIPIcs.CSL.2018.7},
annote = {Keywords: Descriptive Compleixty, Hardness of Approximation, MAX SAT, Vertex Cover, Fixed-point logic with counting}
}
Document
Safety, Absoluteness, and Computability
Abstract
The semantic notion of dependent safety is a common generalization of the notion of absoluteness used in set theory and the notion of domain independence used in database theory for characterizing safe queries. This notion has been used in previous works to provide a unified theory of constructions and operations as they are used in different branches of mathematics and computer science, including set theory, computability theory, and database theory. In this paper we provide a complete syntactic characterization of general first-order dependent safety. We also show that this syntactic safety relation can be used for characterizing the set of strictly decidable relations on the natural numbers, as well as for characterizing rudimentary set theory and absoluteness of formulas within it.
Cite as
Arnon Avron, Shahar Lev, and Nissan Levi. Safety, Absoluteness, and Computability. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{avron_et_al:LIPIcs.CSL.2018.8,
author = {Avron, Arnon and Lev, Shahar and Levi, Nissan},
title = {{Safety, Absoluteness, and Computability}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {8:1--8:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.8},
URN = {urn:nbn:de:0030-drops-96754},
doi = {10.4230/LIPIcs.CSL.2018.8},
annote = {Keywords: Dependent Safety, Computability, Absoluteness, Decidability, Domain Independence}
}
Document
Combining Linear Logic and Size Types for Implicit Complexity
Abstract
Several type systems have been proposed to statically control the time complexity of lambda-calculus programs and characterize complexity classes such as FPTIME or FEXPTIME. A first line of research stems from linear logic and restricted versions of its !-modality controlling duplication. A second approach relies on the idea of tracking the size increase between input and output, and together with a restricted recursion scheme, to deduce time complexity bounds. However both approaches suffer from limitations : either a limited intensional expressivity, or linearity restrictions. In the present work we incorporate both approaches into a common type system, in order to overcome their respective constraints. Our system is based on elementary linear logic combined with linear size types, called sEAL, and leads to characterizations of the complexity classes FPTIME and 2k-FEXPTIME, for k >= 0.
Cite as
Patrick Baillot and Alexis Ghyselen. Combining Linear Logic and Size Types for Implicit Complexity. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{baillot_et_al:LIPIcs.CSL.2018.9,
author = {Baillot, Patrick and Ghyselen, Alexis},
title = {{Combining Linear Logic and Size Types for Implicit Complexity}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {9:1--9:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.9},
URN = {urn:nbn:de:0030-drops-96763},
doi = {10.4230/LIPIcs.CSL.2018.9},
annote = {Keywords: Implicit computational complexity, lambda-calculus, linear logic, type systems, polynomial time complexity, size types}
}
Document
Beyond Admissibility: Dominance Between Chains of Strategies
Abstract
Admissible strategies, i.e. those that are not dominated by any other strategy, are a typical rationality notion in game theory. In many classes of games this is justified by results showing that any strategy is admissible or dominated by an admissible strategy. However, in games played on finite graphs with quantitative objectives (as used for reactive synthesis), this is not the case.
We consider increasing chains of strategies instead to recover a satisfactory rationality notion based on dominance in such games. We start with some order-theoretic considerations establishing sufficient criteria for this to work. We then turn our attention to generalised safety/reachability games as a particular application. We propose the notion of maximal uniform chain as the desired dominance-based rationality concept in these games. Decidability of some fundamental questions about uniform chains is established.
Cite as
Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-François Raskin, and Marie Van den Bogaard. Beyond Admissibility: Dominance Between Chains of Strategies. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{basset_et_al:LIPIcs.CSL.2018.10,
author = {Basset, Nicolas and Jecker, Isma\"{e}l and Pauly, Arno and Raskin, Jean-Fran\c{c}ois and Van den Bogaard, Marie},
title = {{Beyond Admissibility: Dominance Between Chains of Strategies}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {10:1--10:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.10},
URN = {urn:nbn:de:0030-drops-96774},
doi = {10.4230/LIPIcs.CSL.2018.10},
annote = {Keywords: dominated strategies, admissible strategies, games played on finite graphs, reactive synthesis, reachability games, safety games, cofinal, order theory}
}
Document
Rule Algebras for Adhesive Categories
Abstract
We show that every adhesive category gives rise to an associative algebra of rewriting rules induced by the notion of double-pushout (DPO) rewriting and the associated notion of concurrent production. In contrast to the original formulation of rule algebras in terms of relations between (a concrete notion of) graphs, here we work in an abstract categorical setting. Doing this, we extend the classical concurrency theorem of DPO rewriting and show that the composition of DPO rules along abstract dependency relations is, in a natural sense, an associative operation. If in addition the adhesive category possesses a strict initial object, the resulting rule algebra is also unital. We demonstrate that in this setting the canonical representation of the rule algebras is obtainable, which opens the possibility of applying the concept to define and compute the evolution of statistical moments of observables in stochastic DPO rewriting systems.
Cite as
Nicolas Behr and Pawel Sobocinski. Rule Algebras for Adhesive Categories. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 11:1-11:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{behr_et_al:LIPIcs.CSL.2018.11,
author = {Behr, Nicolas and Sobocinski, Pawel},
title = {{Rule Algebras for Adhesive Categories}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {11:1--11:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.11},
URN = {urn:nbn:de:0030-drops-96781},
doi = {10.4230/LIPIcs.CSL.2018.11},
annote = {Keywords: Adhesive categories, rule algebras, Double Pushout (DPO) rewriting}
}
Document
Submodular Functions and Valued Constraint Satisfaction Problems over Infinite Domains
Abstract
Valued constraint satisfaction problems (VCSPs) are a large class of combinatorial optimisation problems. It is desirable to classify the computational complexity of VCSPs depending on a fixed set of allowed cost functions in the input. Recently, the computational complexity of all VCSPs for finite sets of cost functions over finite domains has been classified in this sense. Many natural optimisation problems, however, cannot be formulated as VCSPs over a finite domain. We initiate the systematic investigation of infinite-domain VCSPs by studying the complexity of VCSPs for piecewise linear homogeneous cost functions. We remark that in this paper the infinite domain will always be the set of rational numbers. We show that such VCSPs can be solved in polynomial time when the cost functions are additionally submodular, and that this is indeed a maximally tractable class: adding any cost function that is not submodular leads to an NP-hard VCSP.
Cite as
Manuel Bodirsky, Marcello Mamino, and Caterina Viola. Submodular Functions and Valued Constraint Satisfaction Problems over Infinite Domains. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bodirsky_et_al:LIPIcs.CSL.2018.12,
author = {Bodirsky, Manuel and Mamino, Marcello and Viola, Caterina},
title = {{Submodular Functions and Valued Constraint Satisfaction Problems over Infinite Domains}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {12:1--12:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.12},
URN = {urn:nbn:de:0030-drops-96792},
doi = {10.4230/LIPIcs.CSL.2018.12},
annote = {Keywords: Valued constraint satisfaction problems, Piecewise linear functions, Submodular functions, Semilinear, Constraint satisfaction, Optimisation, Model Theory}
}
Document
Graphical Conjunctive Queries
Abstract
The Calculus of Conjunctive Queries (CCQ) has foundational status in database theory. A celebrated theorem of Chandra and Merlin states that CCQ query inclusion is decidable. Its proof transforms logical formulas to graphs: each query has a natural model - a kind of graph - and query inclusion reduces to the existence of a graph homomorphism between natural models.
We introduce the diagrammatic language Graphical Conjunctive Queries (GCQ) and show that it has the same expressivity as CCQ. GCQ terms are string diagrams, and their algebraic structure allows us to derive a sound and complete axiomatisation of query inclusion, which turns out to be exactly Carboni and Walters' notion of cartesian bicategory of relations. Our completeness proof exploits the combinatorial nature of string diagrams as (certain cospans of) hypergraphs: Chandra and Merlin's insights inspire a theorem that relates such cospans with spans. Completeness and decidability of the (in)equational theory of GCQ follow as a corollary. Categorically speaking, our contribution is a model-theoretic completeness theorem of free cartesian bicategories (on a relational signature) for the category of sets and relations.
Cite as
Filippo Bonchi, Jens Seeber, and Pawel Sobocinski. Graphical Conjunctive Queries. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 13:1-13:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CSL.2018.13,
author = {Bonchi, Filippo and Seeber, Jens and Sobocinski, Pawel},
title = {{Graphical Conjunctive Queries}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {13:1--13:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.13},
URN = {urn:nbn:de:0030-drops-96805},
doi = {10.4230/LIPIcs.CSL.2018.13},
annote = {Keywords: conjunctive query inclusion, string diagrams, cartesian bicategories}
}
Document
Approximating Probabilistic Automata by Regular Languages
Abstract
A probabilistic finite automaton (PFA) A is said to be regular-approximable with respect to (x,y), if there is a regular language that contains all words accepted by A with probability at least x+y, but does not contain any word accepted with probability at most x. We show that the problem of determining if a PFA A is regular-approximable with respect to (x,y) is not recursively enumerable. We then show that many tractable sub-classes of PFAs identified in the literature - hierarchical PFAs, polynomially ambiguous PFAs, and eventually weakly ergodic PFAs - are regular-approximable with respect to all (x,y). Establishing the regular-approximability of a PFA has the nice consequence that its value can be effectively approximated, and the emptiness problem can be decided under the assumption of isolation.
Cite as
Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Approximating Probabilistic Automata by Regular Languages. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{chadha_et_al:LIPIcs.CSL.2018.14,
author = {Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh},
title = {{Approximating Probabilistic Automata by Regular Languages}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {14:1--14:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.14},
URN = {urn:nbn:de:0030-drops-96815},
doi = {10.4230/LIPIcs.CSL.2018.14},
annote = {Keywords: Probabilistic Finite Automata, Regular Languages, Ambiguity}
}
Document
An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets
Abstract
We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose some constraint on switching paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction.
Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative exponential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfy our constraints.
In the present work, we stick to the unit-free and weakening-free fragment of linear logic, which is rich enough to showcase our techniques, while allowing for a very simple kind of constraint: a bound on the number of cuts that are crossed by any switching path.
Cite as
Jules Chouquet and Lionel Vaux Auclair. An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{chouquet_et_al:LIPIcs.CSL.2018.15,
author = {Chouquet, Jules and Vaux Auclair, Lionel},
title = {{An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.15},
URN = {urn:nbn:de:0030-drops-96828},
doi = {10.4230/LIPIcs.CSL.2018.15},
annote = {Keywords: linear logic, proof nets, cut elimination, differential linear logic}
}
Document
Fully Abstract Models of the Probabilistic lambda-calculus
Abstract
We compare three models of the probabilistic lambda-calculus: the probabilistic Böhm trees of Leventis, the probabilistic concurrent games of Winskel et al., and the weighted relational model of Ehrhard et al. Probabilistic Böhm trees and probabilistic strategies are shown to be related by a precise correspondence theorem, in the spirit of existing work for the pure lambda-calculus. Using Leventis' theorem (probabilistic Böhm trees characterise observational equivalence), we derive a full abstraction result for the games model. Then, we relate probabilistic strategies to the weighted relational model, using an interpretation-preserving functor from the former to the latter. We obtain that the relational model is also fully abstract.
Cite as
Pierre Clairambault and Hugo Paquet. Fully Abstract Models of the Probabilistic lambda-calculus. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{clairambault_et_al:LIPIcs.CSL.2018.16,
author = {Clairambault, Pierre and Paquet, Hugo},
title = {{Fully Abstract Models of the Probabilistic lambda-calculus}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {16:1--16:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.16},
URN = {urn:nbn:de:0030-drops-96835},
doi = {10.4230/LIPIcs.CSL.2018.16},
annote = {Keywords: Game Semantics, Lambda-calculus, Probabilistic programming, Relational model, Full abstraction}
}
Document
Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
Abstract
Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e. cyclic) proofs provides the basis for an effective system for automating inductive reasoning.
Cite as
Liron Cohen and Reuben N. S. Rowe. Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{cohen_et_al:LIPIcs.CSL.2018.17,
author = {Cohen, Liron and Rowe, Reuben N. S.},
title = {{Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {17:1--17:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.17},
URN = {urn:nbn:de:0030-drops-96841},
doi = {10.4230/LIPIcs.CSL.2018.17},
annote = {Keywords: Induction, Transitive Closure, Infinitary Proof Systems, Cyclic Proof Systems, Soundness, Completeness, Standard Semantics, Henkin Semantics}
}
Document
A Recursion-Theoretic Characterisation of the Positive Polynomial-Time Functions
Abstract
We extend work of Lautemann, Schwentick and Stewart [Clemens Lautemann et al., 1996] on characterisations of the "positive" polynomial-time predicates (posP, also called mP by Grigni and Sipser [Grigni and Sipser, 1992]) to function classes. Our main result is the obtention of a function algebra for the positive polynomial-time functions (posFP) by imposing a simple uniformity constraint on the bounded recursion operator in Cobham's characterisation of FP. We show that a similar constraint on a function algebra based on safe recursion, in the style of Bellantoni and Cook [Stephen Bellantoni and Stephen A. Cook, 1992], yields an "implicit" characterisation of posFP, mentioning neither explicit bounds nor explicit monotonicity constraints.
Cite as
Anupam Das and Isabel Oitavem. A Recursion-Theoretic Characterisation of the Positive Polynomial-Time Functions. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.CSL.2018.18,
author = {Das, Anupam and Oitavem, Isabel},
title = {{A Recursion-Theoretic Characterisation of the Positive Polynomial-Time Functions}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.18},
URN = {urn:nbn:de:0030-drops-96851},
doi = {10.4230/LIPIcs.CSL.2018.18},
annote = {Keywords: Monotone complexity, Positive complexity, Function classes, Function algebras, Recursion-theoretic characterisations, Implicit complexity, Logic}
}
Document
Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices)
Abstract
We prove cut-elimination for a sequent-style proof system which is sound and complete for the equational theory of Kleene algebra, and where proofs are (potentially) non-wellfounded infinite trees. We extend these results to systems with meets and residuals, capturing `star-continuous' action lattices in a similar way. We recover the equational theory of all action lattices by restricting to regular proofs (with cut) - those proofs that are unfoldings of finite graphs.
Cite as
Anupam Das and Damien Pous. Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices). In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.CSL.2018.19,
author = {Das, Anupam and Pous, Damien},
title = {{Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices)}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {19:1--19:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.19},
URN = {urn:nbn:de:0030-drops-96869},
doi = {10.4230/LIPIcs.CSL.2018.19},
annote = {Keywords: Kleene algebra, proof theory, sequent system, non-wellfounded proofs}
}
Document
Symmetric Circuits for Rank Logic
Abstract
Fixed-point logic with rank (FPR) is an extension of fixed-point logic with counting (FPC) with operators for computing the rank of a matrix over a finite field. The expressive power of FPR properly extends that of FPC and is contained in P, but it is not known if that containment is proper. We give a circuit characterization for FPR in terms of families of symmetric circuits with rank gates, along the lines of that for FPC given by [Anderson and Dawar 2017]. This requires the development of a broad framework of circuits in which the individual gates compute functions that are not symmetric (i.e., invariant under all permutations of their inputs). This framework also necessitates the development of novel techniques to prove the equivalence of circuits and logic. Both the framework and the techniques are of greater generality than the main result.
Cite as
Anuj Dawar and Gregory Wilsenach. Symmetric Circuits for Rank Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2018.20,
author = {Dawar, Anuj and Wilsenach, Gregory},
title = {{Symmetric Circuits for Rank Logic}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {20:1--20:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.20},
URN = {urn:nbn:de:0030-drops-96870},
doi = {10.4230/LIPIcs.CSL.2018.20},
annote = {Keywords: fixed-point logic with rank, circuits, symmetric circuits, uniform families of circuits, circuit characterization, circuit framework, finite model theory, descriptive complexity}
}
Document
Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing
Abstract
The study of polarity in computation has revealed that an "ideal" programming language combines both call-by-value and call-by-name evaluation; the two calling conventions are each ideal for half the types in a programming language. But this binary choice leaves out call-by-need which is used in practice to implement lazy-by-default languages like Haskell. We show how the notion of polarity can be extended beyond the value/name dichotomy to include call-by-need by only adding a mechanism for sharing and the extra polarity shifts to connect them, which is enough to compile a Haskell-like functional language with user-defined types.
Cite as
Paul Downen and Zena M. Ariola. Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{downen_et_al:LIPIcs.CSL.2018.21,
author = {Downen, Paul and Ariola, Zena M.},
title = {{Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {21:1--21:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.21},
URN = {urn:nbn:de:0030-drops-96886},
doi = {10.4230/LIPIcs.CSL.2018.21},
annote = {Keywords: call-by-need, polarity, call-by-push-value, control}
}
Document
Expressivity Within Second-Order Transitive-Closure Logic
Abstract
Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is interesting to understand the expressivity of different features of the language. This paper focuses on the fragment MSO(TC), as well on the purely existential fragment SO(2TC)(exists); in 2TC, the TC operator binds only tuples of relation variables. We establish that, with respect to expressive power, SO(2TC)(exists) collapses to existential first-order logic. In addition we study the relationship of MSO(TC) to an extension of MSO(TC) with counting features (CMSO(TC)) as well as to order-invariant MSO. We show that the expressive powers of CMSO(TC) and MSO(TC) coincide. Moreover we establish that, over unary vocabularies, MSO(TC) strictly subsumes order-invariant MSO.
Cite as
Flavio Ferrarotti, Jan Van den Bussche, and Jonni Virtema. Expressivity Within Second-Order Transitive-Closure Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ferrarotti_et_al:LIPIcs.CSL.2018.22,
author = {Ferrarotti, Flavio and Van den Bussche, Jan and Virtema, Jonni},
title = {{Expressivity Within Second-Order Transitive-Closure Logic}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {22:1--22:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.22},
URN = {urn:nbn:de:0030-drops-96896},
doi = {10.4230/LIPIcs.CSL.2018.22},
annote = {Keywords: Expressive power, Higher order logics, Descriptive complexity}
}
Document
Quantifying Bounds in Strategy Logic
Abstract
Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multi-agent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define Bounded-Outcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the model-checking problems for both these logics.
Cite as
Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin. Quantifying Bounds in Strategy Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 23:1-23:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{fijalkow_et_al:LIPIcs.CSL.2018.23,
author = {Fijalkow, Nathana\"{e}l and Maubert, Bastien and Murano, Aniello and Rubin, Sasha},
title = {{Quantifying Bounds in Strategy Logic}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {23:1--23:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.23},
URN = {urn:nbn:de:0030-drops-96901},
doi = {10.4230/LIPIcs.CSL.2018.23},
annote = {Keywords: Prompt LTL, Strategy Logic, Model checking, Automata with counters}
}
Document
A Fully Abstract Game Semantics for Countable Nondeterminism
Abstract
The concept of fairness for a concurrent program means that the program must be able to exhibit an unbounded amount of nondeterminism without diverging. Game semantics models of nondeterminism show that this is hard to implement; for example, Harmer and McCusker's model only admits infinite nondeterminism if there is also the possibility of divergence. We solve a long standing problem by giving a fully abstract game semantics for a simple stateful language with a countably infinite nondeterminism primitive. We see that doing so requires us to keep track of infinitary information about strategies, as well as their finite behaviours. The unbounded nondeterminism gives rise to further problems, which can be formalized as a lack of continuity in the language. In order to prove adequacy for our model (which usually requires continuity), we develop a new technique in which we simulate the nondeterminism using a deterministic stateful construction, and then use combinatorial techniques to transfer the result to the nondeterministic language. Lastly, we prove full abstraction for the model; because of the lack of continuity, we cannot deduce this from definability of compact elements in the usual way, and we have to use a stronger universality result instead. We discuss how our techniques yield proofs of adequacy for models of nondeterministic PCF, such as those given by Tsukada and Ong.
Cite as
W. John Gowers and James D. Laird. A Fully Abstract Game Semantics for Countable Nondeterminism. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{gowers_et_al:LIPIcs.CSL.2018.24,
author = {Gowers, W. John and Laird, James D.},
title = {{A Fully Abstract Game Semantics for Countable Nondeterminism}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {24:1--24:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.24},
URN = {urn:nbn:de:0030-drops-96918},
doi = {10.4230/LIPIcs.CSL.2018.24},
annote = {Keywords: semantics, nondeterminism, games and logic}
}
Document
Dependency Concepts up to Equivalence
Abstract
Modern logics of dependence and independence are based on different variants of atomic dependency statements (such as dependence, exclusion, inclusion, or independence) and on team semantics: A formula is evaluated not with a single assignment of values to the free variables, but with a set of such assignments, called a team.
In this paper we explore logics of dependence and independence where the atomic dependency statements cannot distinguish elements up to equality, but only up to a given equivalence relation (which may model observational indistinguishabilities, for instance between states of a computational process or between values obtained in an experiment).
Our main goal is to analyse the power of such logics, by identifying equally expressive fragments of existential second-order logic or greatest fixed-point logic, with relations that are closed under the given equivalence. Using an adaptation of the Ehrenfeucht-Fraïssé method we further study conditions on the given equivalences under which these logics collapse to first-order logic, are equivalent to full existential second-order logic, or are strictly between first-order and existential second-order logic.
Cite as
Erich Grädel and Matthias Hoelzel. Dependency Concepts up to Equivalence. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 25:1-25:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{gradel_et_al:LIPIcs.CSL.2018.25,
author = {Gr\"{a}del, Erich and Hoelzel, Matthias},
title = {{Dependency Concepts up to Equivalence}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {25:1--25:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.25},
URN = {urn:nbn:de:0030-drops-96921},
doi = {10.4230/LIPIcs.CSL.2018.25},
annote = {Keywords: Logics of dependence and independence, Team semantics, Existential second-order logic, Observational equivalence, Expressive power}
}
Document
Finite Bisimulations for Dynamical Systems with Overlapping Trajectories
Abstract
Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.
Cite as
Béatrice Bérard, Patricia Bouyer, and Vincent Jugé. Finite Bisimulations for Dynamical Systems with Overlapping Trajectories. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{berard_et_al:LIPIcs.CSL.2018.26,
author = {B\'{e}rard, B\'{e}atrice and Bouyer, Patricia and Jug\'{e}, Vincent},
title = {{Finite Bisimulations for Dynamical Systems with Overlapping Trajectories}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {26:1--26:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.26},
URN = {urn:nbn:de:0030-drops-96932},
doi = {10.4230/LIPIcs.CSL.2018.26},
annote = {Keywords: Reachability properties, dynamical systems, o-minimal structures, intersecting trajectories, finite bisimulations}
}
Document
A Contextual Reconstruction of Monadic Reflection
Abstract
With the help of an idea of contextual modal logic, we define a logical system lambda^{refl} that incorporates monadic reflection, and then investigate delimited continuations through the lens of monadic reflection. Technically, we firstly prove a certain universality of continuation monad, making the character of monadic reflection a little more clear. Next, moving focus to delimited continuations, we present a macro definition of shift/reset by monadic reflection. We then prove that lambda^{refl}_{2cont}, a restriction of lambda^{refl}, has exactly the same provability as lambda^{s/r}_{pure}, a system that incorporates shift/reset. Our reconstruction of monadic reflection opens up a path for investigation of delimited continuations with familiar monadic language.
Cite as
Toru Kawata. A Contextual Reconstruction of Monadic Reflection. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kawata:LIPIcs.CSL.2018.27,
author = {Kawata, Toru},
title = {{A Contextual Reconstruction of Monadic Reflection}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {27:1--27:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.27},
URN = {urn:nbn:de:0030-drops-96947},
doi = {10.4230/LIPIcs.CSL.2018.27},
annote = {Keywords: Monadic Reflection, Delimited Continuations, shift/reset, Contextual Modal Logic, Curry-Howard Isomorphism}
}
Document
An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation
Abstract
In earlier work (LICS 2016), the authors introduced two-variable first-order logic supplemented by a binary relation that allows one to say that a letter appears between two positions. We found an effective algebraic criterion that is a necessary condition for definability in this logic, and conjectured that the criterion is also sufficient, although we proved this only in the case of two-letter alphabets. Here we prove the general conjecture. The proof is quite different from the arguments in the earlier work, and required the development of novel techniques concerning factorizations of words. We extend the results to binary relations specifying that a factor appears between two positions.
Cite as
Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{krebs_et_al:LIPIcs.CSL.2018.28,
author = {Krebs, Andreas and Lodaya, Kamal and Pandya, Paritosh K. and Straubing, Howard},
title = {{An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {28:1--28:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.28},
URN = {urn:nbn:de:0030-drops-96953},
doi = {10.4230/LIPIcs.CSL.2018.28},
annote = {Keywords: two-variable logic, finite model theory, algebraic automata theory}
}
Document
Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular
Abstract
The "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.
Cite as
Aliaume Lopez and Alex Simpson. Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{lopez_et_al:LIPIcs.CSL.2018.29,
author = {Lopez, Aliaume and Simpson, Alex},
title = {{Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {29:1--29:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.29},
URN = {urn:nbn:de:0030-drops-96965},
doi = {10.4230/LIPIcs.CSL.2018.29},
annote = {Keywords: contextual equivalence, algebraic effects, operational semantics, domain theory, nondeterminism, probabilistic choice, Markov decision process}
}
Document
Canonical Models and the Complexity of Modal Team Logic
Abstract
We study modal team logic MTL, the team-semantical extension of classical modal logic closed under Boolean negation. Its fragments, such as modal dependence, independence, and inclusion logic, are well-understood. However, due to the unrestricted Boolean negation, the satisfiability problem of full MTL has been notoriously resistant to a complexity theoretical classification.
In our approach, we adapt the notion of canonical models for team semantics. By construction of such a model, we reduce the satisfiability problem of MTL to simple model checking. Afterwards, we show that this method is optimal in the sense that MTL-formulas can efficiently enforce canonicity.
Furthermore, to capture these results in terms of computational complexity, we introduce a non-elementary complexity class, TOWER(poly), and prove that the satisfiability and validity problem of MTL are complete for it. We also show that the fragments of MTL with bounded modal depth are complete for the levels of the elementary hierarchy (with polynomially many alternations).
Cite as
Martin Lück. Canonical Models and the Complexity of Modal Team Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{luck:LIPIcs.CSL.2018.30,
author = {L\"{u}ck, Martin},
title = {{Canonical Models and the Complexity of Modal Team Logic}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {30:1--30:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.30},
URN = {urn:nbn:de:0030-drops-96979},
doi = {10.4230/LIPIcs.CSL.2018.30},
annote = {Keywords: team semantics, modal logic, complexity, satisfiability}
}
Document
A Decidable Fragment of Second Order Logic With Applications to Synthesis
Abstract
We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an exists^*forall^* quantifier prefix (over variables, functions and relations) making EQSMT conducive for modeling synthesis problems. Moreover, EQSMT allows reasoning using a combination of background theories provided that they have a decidable satisfiability problem for the exists^*forall^* FO-fragment (e.g., linear arithmetic). Our decision procedure reduces the satisfiability of EQSMT formulae to satisfiability queries of exists^*forall^* formulae of each individual background theory, allowing us to use existing efficient SMT solvers supporting exists^*forall^* reasoning for these theories; hence our procedure can be seen as effectively quantified SMT (EQSMT) reasoning.
Cite as
P. Madhusudan, Umang Mathur, Shambwaditya Saha, and Mahesh Viswanathan. A Decidable Fragment of Second Order Logic With Applications to Synthesis. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{madhusudan_et_al:LIPIcs.CSL.2018.31,
author = {Madhusudan, P. and Mathur, Umang and Saha, Shambwaditya and Viswanathan, Mahesh},
title = {{A Decidable Fragment of Second Order Logic With Applications to Synthesis}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {31:1--31:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.31},
URN = {urn:nbn:de:0030-drops-96987},
doi = {10.4230/LIPIcs.CSL.2018.31},
annote = {Keywords: second order logic, synthesis, decidable fragment}
}
Document
Quantitative Foundations for Resource Theories
Abstract
Considering resource usage is a powerful insight in the analysis of many phenomena in the sciences. Much of the current research on these resource theories focuses on the analysis of specific resources such quantum entanglement, purity, randomness or asymmetry. However, the mathematical foundations of resource theories are at a much earlier stage, and there has been no satisfactory account of quantitative aspects such as costs, rates or probabilities.
We present a categorical foundation for quantitative resource theories, derived from enriched category theory. Our approach is compositional, with rich algebraic structure facilitating calculations. The resulting theory is parameterized, both in the quantities under consideration, for example costs or probabilities, and in the structural features of the resources such as whether they can be freely copied or deleted. We also achieve a clear separation of concerns between the resource conversions that are freely available, and the costly resources that are typically the object of study. By using an abstract categorical approach, our framework is naturally open to extension. We provide many examples throughout, emphasising the resource theoretic intuitions for each of the mathematical objects under consideration.
Cite as
Dan Marsden and Maaike Zwart. Quantitative Foundations for Resource Theories. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{marsden_et_al:LIPIcs.CSL.2018.32,
author = {Marsden, Dan and Zwart, Maaike},
title = {{Quantitative Foundations for Resource Theories}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {32:1--32:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.32},
URN = {urn:nbn:de:0030-drops-96996},
doi = {10.4230/LIPIcs.CSL.2018.32},
annote = {Keywords: Resource Theory, Enriched Category, Profunctor, Monad, Combinatorial Species, Multicategory, Operad, Bimodule}
}
Document
On Compositionality of Dinatural Transformations
Abstract
Natural transformations are ubiquitous in mathematics, logic and computer science. For operations of mixed variance, such as currying and evaluation in the lambda-calculus, Eilenberg and Kelly's notion of extranatural transformation, and often the even more general dinatural transformation, is required. Unfortunately dinaturals are not closed under composition except in special circumstances. This paper presents a new sufficient condition for composability.
We propose a generalised notion of dinatural transformation in many variables, and extend the Eilenberg-Kelly account of composition for extranaturals to these transformations. Our main result is that a composition of dinatural transformations which creates no cyclic connections between arguments yields a dinatural transformation.
We also extend the classical notion of horizontal composition to our generalized dinaturals and demonstrate that it is associative and has identities.
Cite as
Guy McCusker and Alessio Santamaria. On Compositionality of Dinatural Transformations. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 33:1-33:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{mccusker_et_al:LIPIcs.CSL.2018.33,
author = {McCusker, Guy and Santamaria, Alessio},
title = {{On Compositionality of Dinatural Transformations}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {33:1--33:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.33},
URN = {urn:nbn:de:0030-drops-97006},
doi = {10.4230/LIPIcs.CSL.2018.33},
annote = {Keywords: Dinatural transformation, categorical logic, compositionality}
}
Document
Synthesizing Optimally Resilient Controllers
Abstract
Recently, Dallal, Neider, and Tabuada studied a generalization of the classical game-theoretic model used in program synthesis, which additionally accounts for unmodeled intermittent disturbances. In this extended framework, one is interested in computing optimally resilient strategies, i.e., strategies that are resilient against as many disturbances as possible. Dallal, Neider, and Tabuada showed how to compute such strategies for safety specifications.
In this work, we compute optimally resilient strategies for a much wider range of winning conditions and show that they do not require more memory than winning strategies in the classical model. Our algorithms only have a polynomial overhead in comparison to the ones computing winning strategies. In particular, for parity conditions optimally resilient strategies are positional and can be computed in quasipolynomial time.
Cite as
Daniel Neider, Alexander Weinert, and Martin Zimmermann. Synthesizing Optimally Resilient Controllers. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{neider_et_al:LIPIcs.CSL.2018.34,
author = {Neider, Daniel and Weinert, Alexander and Zimmermann, Martin},
title = {{Synthesizing Optimally Resilient Controllers}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {34:1--34:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.34},
URN = {urn:nbn:de:0030-drops-97010},
doi = {10.4230/LIPIcs.CSL.2018.34},
annote = {Keywords: Controller Synthesis, Infinite Games, Resilient Strategies, Disturbances}
}
Document
Local Validity for Circular Proofs in Linear Logic with Fixed Points
Abstract
Circular (ie. non-wellfounded but regular) proofs have received increasing interest in recent years with the simultaneous development of their applications and meta-theory: infinitary proof theory is now well-established in several proof-theoretical frameworks such as Martin Löf's inductive predicates, linear logic with fixed points, etc. In the setting of non-wellfounded proofs, a validity criterion is necessary to distinguish, among all infinite derivation trees (aka. pre-proofs), those which are logically valid proofs. A standard approach is to consider a pre-proof to be valid if every infinite branch is supported by an infinitely progressing thread.
The paper focuses on circular proofs for MALL with fixed points. Among all representations of valid circular proofs, a new fragment is described, based on a stronger validity criterion. This new criterion is based on a labelling of formulas and proofs, whose validity is purely local. This allows this fragment to be easily handled, while being expressive enough to still contain all circular embeddings of Baelde's muMALL finite proofs with (co)inductive invariants: in particular deciding validity and computing a certifying labelling can be done efficiently. Moreover the Brotherston-Simpson conjecture holds for this fragment: every labelled representation of a circular proof in the fragment is translated into a standard finitary proof. Finally we explore how to extend these results to a bigger fragment, by relaxing the labelling discipline while retaining (i) the ability to locally certify the validity and (ii) to some extent, the ability to finitize circular proofs.
Cite as
Rémi Nollet, Alexis Saurin, and Christine Tasson. Local Validity for Circular Proofs in Linear Logic with Fixed Points. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 35:1-35:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{nollet_et_al:LIPIcs.CSL.2018.35,
author = {Nollet, R\'{e}mi and Saurin, Alexis and Tasson, Christine},
title = {{Local Validity for Circular Proofs in Linear Logic with Fixed Points}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {35:1--35:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.35},
URN = {urn:nbn:de:0030-drops-97025},
doi = {10.4230/LIPIcs.CSL.2018.35},
annote = {Keywords: sequent calculus, non-wellfounded proofs, circular proofs, induction, coinduction, fixed points, proof-search, linear logic, muMALL, finitization, infinite descent}
}
Document
Parity Games with Weights
Abstract
Quantitative extensions of parity games have recently attracted significant interest. These extensions include parity games with energy and payoff conditions as well as finitary parity games and their generalization to parity games with costs. Finitary parity games enjoy a special status among these extensions, as they offer a native combination of the qualitative and quantitative aspects in infinite games: the quantitative aspect of finitary parity games is a quality measure for the qualitative aspect, as it measures the limit superior of the time it takes to answer an odd color by a larger even one. Finitary parity games have been extended to parity games with costs, where each transition is labelled with a non-negative weight that reflects the costs incurred by taking it. We lift this restriction and consider parity games with costs with arbitrary integer weights. We show that solving such games is in NP cap co-NP, the signature complexity for games of this type. We also show that the protagonist has finite-state winning strategies, and provide tight exponential bounds for the memory he needs to win the game. Naturally, the antagonist may need infinite memory to win. Finally, we present tight bounds on the quality of winning strategies for the protagonist.
Cite as
Sven Schewe, Alexander Weinert, and Martin Zimmermann. Parity Games with Weights. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{schewe_et_al:LIPIcs.CSL.2018.36,
author = {Schewe, Sven and Weinert, Alexander and Zimmermann, Martin},
title = {{Parity Games with Weights}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {36:1--36:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.36},
URN = {urn:nbn:de:0030-drops-97037},
doi = {10.4230/LIPIcs.CSL.2018.36},
annote = {Keywords: Infinite Games, Quantitative Games, Parity Games}
}
Document
MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics
Abstract
Buchholz' Omega-rule is a way to give a syntactic, possibly ordinal-free proof of cut elimination for various subsystems of second order arithmetic. Our goal is to understand it from an algebraic point of view. Among many proofs of cut elimination for higher order logics, Maehara and Okada's algebraic proofs are of particular interest, since the essence of their arguments can be algebraically described as the (Dedekind-)MacNeille completion together with Girard's reducibility candidates. Interestingly, it turns out that the Omega-rule, formulated as a rule of logical inference, finds its algebraic foundation in the MacNeille completion.
In this paper, we consider a family of sequent calculi LIP = cup_{n >= -1} LIP_n for the parameter-free fragments of second order intuitionistic logic, that corresponds to the family ID_{<omega} = cup_{n <omega} ID_n of arithmetical theories of inductive definitions up to omega. In this setting, we observe a formal connection between the Omega-rule and the MacNeille completion, that leads to a way of interpreting second order quantifiers in a first order way in Heyting-valued semantics, called the Omega-interpretation. Based on this, we give a (partly) algebraic proof of cut elimination for LIP_n, in which quantification over reducibility candidates, that are genuinely second order, is replaced by the Omega-interpretation, that is essentially first order. As a consequence, our proof is locally formalizable in ID-theories.
Cite as
Kazushige Terui. MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{terui:LIPIcs.CSL.2018.37,
author = {Terui, Kazushige},
title = {{MacNeille Completion and Buchholz' Omega Rule for Parameter-Free Second Order Logics}},
booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
pages = {37:1--37:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-088-0},
ISSN = {1868-8969},
year = {2018},
volume = {119},
editor = {Ghica, Dan R. and Jung, Achim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.37},
URN = {urn:nbn:de:0030-drops-97049},
doi = {10.4230/LIPIcs.CSL.2018.37},
annote = {Keywords: Algebraic cut elimination, Parameter-free second order logic, MacNeille completion, Omega-rule}
}