Volume
LIPIcs, Volume 82
26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2017, August 20-24, 2017, Stockholm, SwedenEditors
Publication Details
- published at: 2017-08-16
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-045-3
- DBLP: db/conf/csl/csl2017
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 82, CSL'17, Complete Volume
Abstract
LIPIcs, Volume 82, CSL'17, Complete Volume
Cite as
26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Proceedings{goranko_et_al:LIPIcs.CSL.2017,
title = {{LIPIcs, Volume 82, CSL'17, Complete Volume}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017},
URN = {urn:nbn:de:0030-drops-78103},
doi = {10.4230/LIPIcs.CSL.2017},
annote = {Keywords: Conference Proceedings, Software/Program Verification, Formal Definitions and Theory, Language Constructs and Features, Theory of Computation}
}
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
26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{goranko_et_al:LIPIcs.CSL.2017.0,
author = {Goranko, Valentin and Dam, Mads},
title = {{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.0},
URN = {urn:nbn:de:0030-drops-76671},
doi = {10.4230/LIPIcs.CSL.2017.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}
}
Document
The Ackermann Award 2017
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 2017 edition of the award.
Cite as
Anuj Dawar and Daniel Leivant. The Ackermann Award 2017. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2017.1,
author = {Dawar, Anuj and Leivant, Daniel},
title = {{The Ackermann Award 2017}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.1},
URN = {urn:nbn:de:0030-drops-76938},
doi = {10.4230/LIPIcs.CSL.2017.1},
annote = {Keywords: Ackermann Award, jury report, citation}
}
Document
Invited Talk
Schema Mappings: Structural Properties and Limits (Invited Talk)
Abstract
A schema mapping is a high-level specification of the relationship between two database schemas. For the past fifteen years, schema mappings have played an essential role in the modeling and analysis of important data inter-operability tasks, such as data exchange and data integration. Syntactically, schema mappings are expressed in some schema-mapping language, which, typically, is a fragment of first-order logic or second-order logic. In the first part of the talk, we will introduce the main schema-mapping languages, will discuss the fundamental structural properties of these languages, and will then use these structural properties to obtain characterizations of various schema-mapping languages in the spirit of abstract model theory. In the second part of the talk, we will examine schema mappings from a dynamic viewpoint by considering sequences of schema mappings and studying the convergence properties of such sequences. To this effect, we will introduce a metric space that is based on a natural notion of distance between sets of database instances and will investigate pointwise limits and uniform limits of sequences of schema mappings. Among other findings, it will turn out that the completion of this metric space can be described in terms of graph limits arising from converging sequences of homomorphism densities.
Cite as
Phokion G. Kolaitis. Schema Mappings: Structural Properties and Limits (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kolaitis:LIPIcs.CSL.2017.2,
author = {Kolaitis, Phokion G.},
title = {{Schema Mappings: Structural Properties and Limits}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.2},
URN = {urn:nbn:de:0030-drops-76707},
doi = {10.4230/LIPIcs.CSL.2017.2},
annote = {Keywords: logic and databases, schema mappings, data exchange, metric spaces}
}
Document
Invited Talk
First-Order Interpolation and Grey Areas of Proofs (Invited Talk)
Abstract
Interpolation is an important technique in computer aided verification and static analysis of programs. In particular, interpolants extracted from so-called local proofs are used in invariant generation and bounded model checking. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof.
In this talk we first describe a technique of generating and optimizing interpolants based on transformations of what we call the “grey area” of local proofs. Local changes in proofs can change the extracted interpolant. Our method can describe properties of extracted interpolants obtained by such proof changes as a pseudo-boolean constraint. By optimizing solutions of this constraint we also improve the extracted interpolants. Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear integer arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants.
While local proofs admit efficient interpolation algorithms, standard complete proof systems, such as superposition,
for theories having the interpolation property are not necessarily complete for local proofs.
In this talk we therefore also investigate interpolant extraction from non-local proofs in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants. In particular, we prove that the number of quantifier alternations in first-order interpolants of formulas without quantifier alternations is unbounded. This result has far-reaching consequences for using local proofs as a foundation for interpolating proof systems - any such proof system should deal with formulas of arbitrary quantifier complexity.
Cite as
Laura Kovács. First-Order Interpolation and Grey Areas of Proofs (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kovacs:LIPIcs.CSL.2017.3,
author = {Kov\'{a}cs, Laura},
title = {{First-Order Interpolation and Grey Areas of Proofs}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.3},
URN = {urn:nbn:de:0030-drops-76912},
doi = {10.4230/LIPIcs.CSL.2017.3},
annote = {Keywords: theorem proving, interpolation, proof transformations, constraint solving, program analysis}
}
Document
Invited Talk
Current Trends and New Perspectives for First-Order Model Checking (Invited Talk)
Abstract
The model-checking problem for a logic LLL is the problem
of decidig for a given formula phi in LLL and structure
AA whether the formula is true in the structure, i.e. whether
AA models phi.
Model-checking for logics such as First-Order Logic (FO) or
Monadic Second-Order Logic (MSO) has been studied intensively
in the literature, especially in the context of algorithmic meta-theorems
within the framework of parameterized complexity. However, in the past the
focus of this line of research was model-checking on classes of
sparse graphs, e.g. planar graphs, graph classes excluding a
minor or classes which are nowhere dense. By now, the complexity of
first-order model-checking on sparse classes of graphs is completely
understood. Hence, current research now focusses mainly on classes of
dense graphs.
In this talk we will briefly review the known results on sparse classes
of graphs and explain the complete classification of classes of sparse
graphs on which first-order model-checking is tractable.
In the second part we will then focus on recent and ongoing research
analysing the complexity of first-order model-checking on classes of
dense graphs.
Cite as
Stephan Kreutzer. Current Trends and New Perspectives for First-Order Model Checking (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 4:1-4:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kreutzer:LIPIcs.CSL.2017.4,
author = {Kreutzer, Stephan},
title = {{Current Trends and New Perspectives for First-Order Model Checking}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {4:1--4:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.4},
URN = {urn:nbn:de:0030-drops-77095},
doi = {10.4230/LIPIcs.CSL.2017.4},
annote = {Keywords: Finite Model Theory, Computational Model Theory, Algorithmic Meta Theorems, Model-Checking, Logical Approaches in Graph Theory}
}
Document
Invited Talk
Arithmetic Circuits: An Overview (Invited Talk)
Abstract
This talk reviews recent developments in algebraic complexity
theory. It outlines some major results concerning structure,
completeness, closure, and lower bounds. It describes some techniques
that have been central to obtaining these results, including extreme
depth reduction, partial derivatives, and padding.
Cite as
Meena Mahajan. Arithmetic Circuits: An Overview (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{mahajan:LIPIcs.CSL.2017.5,
author = {Mahajan, Meena},
title = {{Arithmetic Circuits: An Overview}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {5:1--5:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.5},
URN = {urn:nbn:de:0030-drops-76858},
doi = {10.4230/LIPIcs.CSL.2017.5},
annote = {Keywords: algebraic complexity, circuits, formulas, branching programs, determinant, permanent}
}
Document
Invited Talk
Determinacy of Infinite Games: Perspectives of the Algorithmic Approach (Invited Talk)
Abstract
Determinacy of infinite two-player games is a topic of descriptive set theory that has triggered intensive research in theoretical computer science since 1957 when A. Church formulated his "synthesis problem" (regarding the construction of circuits with infinite behavior from logical specifications). In the first part of the lecture we review the fascinating development of the algorithmic theory of infinite games that was started by Church's problem, that enriched automata theory and related fields, and that led to interesting applications in verification and program synthesis. In the second part we turn to the question how to lift this theory from the case of the Cantor space (where a play is a sequence of bits) to the case of the Baire space (where a play is a sequence of natural numbers). While this step does not involve difficulties in classical descriptive set theory, the algorithmic approach raises non-trivial questions since it requires to consider automata that work over infinite alphabets. We present recent results (joint work with B. Brütsch) that provide a solution of Church's synthesis problem in this context, and we point to numerous questions that are still open.
Cite as
Wolfgang Thomas. Determinacy of Infinite Games: Perspectives of the Algorithmic Approach (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 6:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{thomas:LIPIcs.CSL.2017.6,
author = {Thomas, Wolfgang},
title = {{Determinacy of Infinite Games: Perspectives of the Algorithmic Approach}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {6:1--6:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.6},
URN = {urn:nbn:de:0030-drops-77083},
doi = {10.4230/LIPIcs.CSL.2017.6},
annote = {Keywords: Infinite games, descriptive set theory, automata theory, transducers, automatic synthesis}
}
Document
Invited Talk
Symbolic Automata Theory with Applications (Invited Talk)
Abstract
Symbolic automata extend classic finite state automata by allowing
transitions to carry predicates over rich alphabet theories. The
key algorithmic difference to classic automata is the ability to
efficiently operate over very large or infinite alphabets. In this
talk we give an overview of what is currently known about symbolic
automata, what their main applications are, and what challenges
arise when reasoning about them. We also discuss some of the open
problems and research directions in symbolic automata theory.
Cite as
Margus Veanes. Symbolic Automata Theory with Applications (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 7:1-7:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{veanes:LIPIcs.CSL.2017.7,
author = {Veanes, Margus},
title = {{Symbolic Automata Theory with Applications}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {7:1--7:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.7},
URN = {urn:nbn:de:0030-drops-76872},
doi = {10.4230/LIPIcs.CSL.2017.7},
annote = {Keywords: automaton, transducer, symbolic}
}
Document
Categorical Structures for Type Theory in Univalent Foundations
Abstract
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in the setting of univalent foundations, where the relationships between them can be stated more transparently. Specifically, we construct maps between the different structures and show that these maps are equivalences under suitable assumptions.
We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure.
We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.
Cite as
Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical Structures for Type Theory in Univalent Foundations. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{ahrens_et_al:LIPIcs.CSL.2017.8,
author = {Ahrens, Benedikt and Lumsdaine, Peter LeFanu and Voevodsky, Vladimir},
title = {{Categorical Structures for Type Theory in Univalent Foundations}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {8:1--8:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.8},
URN = {urn:nbn:de:0030-drops-76960},
doi = {10.4230/LIPIcs.CSL.2017.8},
annote = {Keywords: Categorical Semantics, Type Theory, Univalence Axiom}
}
Document
Removing Cycles from Proofs
Abstract
If we track atom occurrences in classical propositional proofs in deep inference, we see that they can form cyclic structures between cuts and identity steps. These cycles are an obstacle to a very natural form of normalisation, that simply unfolds all the contractions in a proof. This mechanism, which we call ‘decomposition’, has many points of contact with explicit substitutions in lambda calculi. In the presence of cycles, decomposition does not terminate, and this is an obvious drawback if we want to interpret proofs computationally. One way of eliminating cycles is eliminating cuts. However, we could ask ourselves whether it is possible to eliminate cycles independently of (general) cut elimination. This paper shows an efficient way to do so, therefore establishing the independence of decomposition from cut elimination. In other words, cut elimination in propositional logic can be separated into three separate procedures: 1) cycle elimination, 2) unfolding of contractions, 3) elimination of cuts in the linear fragment.
Cite as
Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph. Removing Cycles from Proofs. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{alertubella_et_al:LIPIcs.CSL.2017.9,
author = {Aler Tubella, Andrea and Guglielmi, Alessio and Ralph, Benjamin},
title = {{Removing Cycles from Proofs}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {9:1--9:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.9},
URN = {urn:nbn:de:0030-drops-77008},
doi = {10.4230/LIPIcs.CSL.2017.9},
annote = {Keywords: proof theory, deep inference, proof complexity}
}
Document
Query Learning of Derived Omega-Tree Languages in Polynomial Time
Abstract
We present the first polynomial time algorithm to learn nontrivial classes of languages of infinite trees. Specifically, our algorithm uses membership and equivalence queries to learn classes of omega-tree languages derived from weak regular omega-word languages in polynomial time. The method is a general polynomial time reduction
of learning a class of derived omega-tree languages to learning the underlying class of omega-word languages, for any class of omega-word languages recognized by a deterministic Büchi acceptor.
Our reduction, combined with the polynomial time learning algorithm of Maler and Pnueli [Maler and Pneuli, Inform. Comput., 1995]
for the class of weak regular omega-word languages yields the main result. We also show that subset queries that return counterexamples
can be implemented in polynomial time using subset queries that return no counterexamples for deterministic or non-deterministic finite word acceptors, and deterministic or non-deterministic Büchi
omega-word acceptors.
A previous claim of an algorithm to learn regular omega-trees
due to Jayasrirani, Begam and Thomas [Jayasrirani et al., ICGI, 2008] is unfortunately incorrect, as shown in [Angluin, YALEU/DCS/TR-1528, 2016].
Cite as
Dana Angluin, Timos Antonopoulos, and Dana Fisman. Query Learning of Derived Omega-Tree Languages in Polynomial Time. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{angluin_et_al:LIPIcs.CSL.2017.10,
author = {Angluin, Dana and Antonopoulos, Timos and Fisman, Dana},
title = {{Query Learning of Derived Omega-Tree Languages in Polynomial Time}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {10:1--10:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.10},
URN = {urn:nbn:de:0030-drops-77022},
doi = {10.4230/LIPIcs.CSL.2017.10},
annote = {Keywords: Learning, queries, infinite trees, derived tree languages, reactive systems}
}
Document
Extending Two-Variable Logic on Trees
Abstract
The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.
Cite as
Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieronski. Extending Two-Variable Logic on Trees. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bednarczyk_et_al:LIPIcs.CSL.2017.11,
author = {Bednarczyk, Bartosz and Charatonik, Witold and Kieronski, Emanuel},
title = {{Extending Two-Variable Logic on Trees}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {11:1--11:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.11},
URN = {urn:nbn:de:0030-drops-76794},
doi = {10.4230/LIPIcs.CSL.2017.11},
annote = {Keywords: two-variable logic, trees, satisfiability, expressivity, counting quantifiers}
}
Document
On the (In)Succinctness of Muller Automata
Abstract
There are several types of finite automata on infinite words, differing in their acceptance conditions. As each type has its own advantages, there is an extensive research on the size blowup involved in translating one automaton type to another.
Of special interest is the Muller type, providing the most detailed acceptance condition. It turns out that there is inconsistency and incompleteness in the literature results regarding the translations to and from Muller automata. Considering the automaton size, some results take into account, in addition to the number of states, the alphabet length and the number of transitions while ignoring the length of the acceptance condition, whereas other results consider the length of the acceptance condition while ignoring the two other parameters.
We establish a full picture of the translations to and from Muller automata, enhancing known results and adding new ones. Overall, Muller automata can be considered less succinct than parity, Rabin, and Streett automata: translating nondeterministic Muller automata to the other nondeterministic types involves a polynomial size blowup, while the other way round is exponential; translating between the deterministic versions is exponential in both directions; and translating nondeterministic automata of all types to deterministic Muller automata is doubly exponential, as opposed to a single exponent in the translations to the other deterministic types.
Cite as
Udi Boker. On the (In)Succinctness of Muller Automata. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{boker:LIPIcs.CSL.2017.12,
author = {Boker, Udi},
title = {{On the (In)Succinctness of Muller Automata}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {12:1--12:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.12},
URN = {urn:nbn:de:0030-drops-76751},
doi = {10.4230/LIPIcs.CSL.2017.12},
annote = {Keywords: Automata, Omega-regular languages, Determinization}
}
Document
Stone Duality and the Substitution Principle
Abstract
In this paper we relate two generalisations of the finite monoid recognisers of automata theory for the study of circuit complexity classes: Boolean spaces with internal monoids and typed monoids. Using the setting of stamps, this allows us to generalise a number of results from algebraic automata theory as it relates to Büchi's logic on words. We obtain an Eilenberg theorem, a substitution principle based on Stone duality, a block product principle for typed stamps and, as our main result, a topological semidirect product construction, which corresponds to the application of a general form of quantification. These results provide tools for the study of language classes given by logic fragments such as the Boolean circuit complexity classes.
Cite as
Célia Borlido, Silke Czarnetzki, Mai Gehrke, and Andreas Krebs. Stone Duality and the Substitution Principle. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{borlido_et_al:LIPIcs.CSL.2017.13,
author = {Borlido, C\'{e}lia and Czarnetzki, Silke and Gehrke, Mai and Krebs, Andreas},
title = {{Stone Duality and the Substitution Principle}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {13:1--13:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.13},
URN = {urn:nbn:de:0030-drops-77060},
doi = {10.4230/LIPIcs.CSL.2017.13},
annote = {Keywords: C-variety of languages, typed monoid, Boolean space with an internal monoid, substitution principle, semidirect product}
}
Document
A Decidable Intuitionistic Temporal Logic
Abstract
We introduce the logic ITL^e, an intuitionistic temporal logic
based on structures (W,R,S), where R is used to interpret intuitionistic implication and S is an R-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for ITL^e are decidable.
We prove this by showing that the logic enjoys the strong finite model property. In contrast, we also consider a 'persistent' version of the logic, ITL^p, whose models are similar to Cartesian products.
We prove that, unlike ITL^e, ITL^p does not have the finite model property.
Cite as
Joseph Boudou, Martín Diéguez, and David Fernández-Duque. A Decidable Intuitionistic Temporal Logic. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{boudou_et_al:LIPIcs.CSL.2017.14,
author = {Boudou, Joseph and Di\'{e}guez, Mart{\'\i}n and Fern\'{a}ndez-Duque, David},
title = {{A Decidable Intuitionistic Temporal Logic}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {14:1--14:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.14},
URN = {urn:nbn:de:0030-drops-77016},
doi = {10.4230/LIPIcs.CSL.2017.14},
annote = {Keywords: intuitionistic logic, temporal logic, products of modal logics}
}
Document
Decidable Logics with Associative Binary Modalities
Abstract
A new family of modal logics with an associative binary modality, called counting logics is proposed. These propositional logics allow to express finite cardinalities of sets and more generally to count the number of subsets satisfying some properties. We show that these logics can be seen both as specializations of the Boolean logic of bunched implications and as generalizations of the propositional dependence logic. Moreover, whereas most logics with an associative binary modality are undecidable, we prove that some counting logics are decidable, in particular the basic counting logic bCL. We conjecture that this interesting result is due to the valuation constraints in counting logics' semantics and prove that the logic corresponding to bCL without these constraints is undecidable. Finally, we give lower and upper bounds for the complexity of bCL's validity problem.
Cite as
Joseph Boudou. Decidable Logics with Associative Binary Modalities. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{boudou:LIPIcs.CSL.2017.15,
author = {Boudou, Joseph},
title = {{Decidable Logics with Associative Binary Modalities}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {15:1--15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.15},
URN = {urn:nbn:de:0030-drops-76863},
doi = {10.4230/LIPIcs.CSL.2017.15},
annote = {Keywords: modal logics, abstract separation logics, team semantics, resource logics, substructural logics}
}
Document
Noetherian Quasi-Polish spaces
Abstract
In the presence of suitable power spaces, compactness of X can be characterized as the singleton {X} being open in the space O(X) of open subsets of X. Equivalently, this means that universal quantification over a compact space preserves open predicates.
Using the language of represented spaces, one can make sense of notions such as a Sigma^0_2-subset of the space of Sigma^0_2-subsets of a given space. This suggests higher-order analogues to compactness: We can, e.g., investigate the spaces X where {X} is a Delta^0_2-subset of the space of Delta^0_2-subsets of X. Call this notion nabla-compactness. As Delta^0_2 is self-dual, we find that both universal and existential quantifier over nabla-compact spaces preserve Delta^0_2 predicates.
Recall that a space is called Noetherian iff every subset is compact. Within the setting of Quasi-Polish spaces, we can fully characterize the nabla-compact spaces: A Quasi-Polish space is Noetherian iff it is nabla-compact. Note that the restriction to Quasi-Polish spaces is sufficiently general to include plenty of examples.
Cite as
Matthew de Brecht and Arno Pauly. Noetherian Quasi-Polish spaces. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{debrecht_et_al:LIPIcs.CSL.2017.16,
author = {de Brecht, Matthew and Pauly, Arno},
title = {{Noetherian Quasi-Polish spaces}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {16:1--16:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.16},
URN = {urn:nbn:de:0030-drops-76988},
doi = {10.4230/LIPIcs.CSL.2017.16},
annote = {Keywords: Descriptive set theory, synthetic topology, well-quasi orders, Noetherian spaces, compactness}
}
Document
Fast(er) Reasoning in Interval Temporal Logic
Abstract
Clausal forms of logics are of great relevance in Artificial Intelligence, because they couple a high expressivity with a low complexity of reasoning problems. They have been studied for a wide range of classical, modal and temporal logics to obtain tractable fragments of intractable formalisms. In this paper we show that such restrictions can be exploited to lower the complexity of interval temporal logics as well. In particular, we show that for the Horn fragment of the interval logic AAbar (that is, the logic with the modal operators for Allen’s relations meets and met by) without diamonds the complexity lowers from NEXPTIME-complete to P-complete. We prove also that the tractability of the Horn fragments of interval temporal logics is lost as soon as other interval temporal operators are added to AAbar, in most of the cases.
Cite as
Davide Bresolin, Emilio Muñoz-Velasco, and Guido Sciavicco. Fast(er) Reasoning in Interval Temporal Logic. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bresolin_et_al:LIPIcs.CSL.2017.17,
author = {Bresolin, Davide and Mu\~{n}oz-Velasco, Emilio and Sciavicco, Guido},
title = {{Fast(er) Reasoning in Interval Temporal Logic}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {17:1--17:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.17},
URN = {urn:nbn:de:0030-drops-76782},
doi = {10.4230/LIPIcs.CSL.2017.17},
annote = {Keywords: Temporal Logic, Horn Fragments, Satisfiability, Complexity}
}
Document
Improved Set-Based Symbolic Algorithms for Parity Games
Abstract
Graph games with omega-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify omega-regular winning conditions. Graph games with parity conditions are equivalent to mu-calculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finite-state systems, as well as algorithms for the analysis of infinite-state systems with finite quotient. A set-based symbolic algorithm uses the basic set operations and the one-step predecessor operators.
We consider graph games with n vertices and parity conditions with c priorities (equivalently, a mu-calculus formula with c alternations of least and greatest fixed points). While many explicit algorithms exist for graph games with parity conditions, for set-based symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires O(n^c) symbolic operations and linear space; and (b) an improved algorithm that requires O(n^{c/2+1}) symbolic operations but also O(n^{c/2+1}) space (i.e., exponential space).
In this work we present two set-based symbolic algorithms for parity games: (a) our first algorithm requires O(n^{c/2+1}) symbolic operations and only requires linear space; and (b) developing on our first algorithm, we present an algorithm that requires O(n^{c/3+1}) symbolic operations and only linear space. We also present the first linear space set-based symbolic algorithm for parity games that requires at most a sub-exponential number of symbolic operations.
Cite as
Krishnendu Chatterjee, Wolfgang Dvorák, Monika Henzinger, and Veronika Loitzenbauer. Improved Set-Based Symbolic Algorithms for Parity Games. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 18:1-18:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{chatterjee_et_al:LIPIcs.CSL.2017.18,
author = {Chatterjee, Krishnendu and Dvor\'{a}k, Wolfgang and Henzinger, Monika and Loitzenbauer, Veronika},
title = {{Improved Set-Based Symbolic Algorithms for Parity Games}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {18:1--18:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.18},
URN = {urn:nbn:de:0030-drops-76830},
doi = {10.4230/LIPIcs.CSL.2017.18},
annote = {Keywords: model checking, graph games, parity games, symbolic computation, progress measure}
}
Document
Slicewise Definability in First-Order Logic with Bounded Quantifier Rank
Abstract
For every natural number q let FO_q denote the class of sentences of
first-order logic FO of quantifier rank at most q. If a graph property can be defined in FO_q, then it can be decided in time O(n^q). Thus, minimizing q has favorable algorithmic consequences. Many graph properties amount to the existence of a certain set of vertices of size k. Usually this can only be expressed by a sentence of quantifier rank at least k. We use the color coding method to demonstrate that some (hyper)graph problems can be defined in FO_q where q is independent of k. This property of a graph problem is equivalent to the question of whether the corresponding parameterized problem is in the class para-AC^0.
It is crucial for our results that the FO-sentences have access to built-in addition and multiplication (and constants for an initial segment of natural numbers whose length depends only on k). It is known that then FO corresponds to the circuit complexity class uniform AC^0. We explore the connection between the quantifier rank of FO-sentences and the depth of AC^0-circuits, and prove that FO_q is strictly contained in FO_{q+1} for structures with built-in addition and multiplication.
Cite as
Yijia Chen, Jörg Flum, and Xuangui Huang. Slicewise Definability in First-Order Logic with Bounded Quantifier Rank. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.CSL.2017.19,
author = {Chen, Yijia and Flum, J\"{o}rg and Huang, Xuangui},
title = {{Slicewise Definability in First-Order Logic with Bounded Quantifier Rank}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {19:1--19:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.19},
URN = {urn:nbn:de:0030-drops-76742},
doi = {10.4230/LIPIcs.CSL.2017.19},
annote = {Keywords: first-order logic, quantifier rank, parameterized AC^0, circuit depth}
}
Document
Integral Categories and Calculus Categories
Abstract
Differential categories are now an established abstract setting for differentiation. The paper presents the parallel development for integration by axiomatizing
an integral transformation in a symmetric monoidal category with a coalgebra modality. When integration is combined with differentiation, the two fundamental theorems of calculus are expected to hold (in a suitable sense): a differential category with integration which satisfies
these two theorem is called a calculus category.
Modifying an approach to antiderivatives by T. Ehrhard, it is shown how examples of calculus categories arise as differential categories with antiderivatives in this new sense. Having antiderivatives amounts to demanding that a certain natural transformation K, is invertible. We observe that a differential category having antiderivatives, in this sense, is always a calculus category and we provide examples of such categories.
Cite as
Robin Cockett and Jean-Simon Lemay. Integral Categories and Calculus Categories. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{cockett_et_al:LIPIcs.CSL.2017.20,
author = {Cockett, Robin and Lemay, Jean-Simon},
title = {{Integral Categories and Calculus Categories}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {20:1--20:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.20},
URN = {urn:nbn:de:0030-drops-76687},
doi = {10.4230/LIPIcs.CSL.2017.20},
annote = {Keywords: Differential Categories, Integral Categories, Calculus Categories}
}
Document
Partial Elements and Recursion via Dominances in Univalent Type Theory
Abstract
We begin by revisiting partiality in univalent type theory via the notion of dominance. We then perform first steps in constructive computability theory, discussing the consequences of working with computability as property or structure, without assuming countable choice or Markov’s principle. A guiding question is what, if any, notion of partial function allows the proposition “all partial functions on natural numbers are Turing computable” to be consistent.
Cite as
Martín H. Escardó and Cory M. Knapp. Partial Elements and Recursion via Dominances in Univalent Type Theory. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{escardo_et_al:LIPIcs.CSL.2017.21,
author = {Escard\'{o}, Mart{\'\i}n H. and Knapp, Cory M.},
title = {{Partial Elements and Recursion via Dominances in Univalent Type Theory}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {21:1--21:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.21},
URN = {urn:nbn:de:0030-drops-76822},
doi = {10.4230/LIPIcs.CSL.2017.21},
annote = {Keywords: univalent type theory, homotopy type theory, partial function, dominance, recursion theory, computability theory}
}
Document
Polishness of Some Topologies Related to Automata
Abstract
We prove that the Büchi topology, the automatic topology, the alphabetic topology and the strong alphabetic topology are Polish, and provide consequences of this.
Cite as
Olivier Carton, Olivier Finkel, and Dominique Lecomte. Polishness of Some Topologies Related to Automata. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{carton_et_al:LIPIcs.CSL.2017.22,
author = {Carton, Olivier and Finkel, Olivier and Lecomte, Dominique},
title = {{Polishness of Some Topologies Related to Automata}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {22:1--22:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.22},
URN = {urn:nbn:de:0030-drops-76728},
doi = {10.4230/LIPIcs.CSL.2017.22},
annote = {Keywords: Automata and formal languages; logic in computer science; infinite words; B\"{u}chi automaton; regular omega-language; Cantor space; finer topologies; B\"{u}c}
}
Document
Separating Functional Computation from Relations
Abstract
The logical foundation of arithmetic generally starts with a
quantificational logic over relations. Of course, one often wishes to have a formal treatment of functions within this setting. Both
Hilbert and Church added choice operators (such as the epsilon
operator) to logic in order to coerce relations that happen to encode functions into actual functions. Others have extended the term language with confluent term rewriting in order to encode functional computation as rewriting to a normal form. We take a different approach that does not extend the underlying logic with either choice principles or with an equality theory. Instead, we use the familiar two-phase construction of focused proofs and capture functional computation entirely within one of these phases. As a result, our logic remains purely relational even when it is computing functions.
Cite as
Ulysse Gérard and Dale Miller. Separating Functional Computation from Relations. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{gerard_et_al:LIPIcs.CSL.2017.23,
author = {G\'{e}rard, Ulysse and Miller, Dale},
title = {{Separating Functional Computation from Relations}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {23:1--23:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.23},
URN = {urn:nbn:de:0030-drops-77040},
doi = {10.4230/LIPIcs.CSL.2017.23},
annote = {Keywords: focused proof systems, fixed points, computation and deduction}
}
Document
Diagrammatic Semantics for Digital Circuits
Abstract
We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about parametrised circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.
Cite as
Dan R. Ghica, Achim Jung, and Aliaume Lopez. Diagrammatic Semantics for Digital Circuits. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{ghica_et_al:LIPIcs.CSL.2017.24,
author = {Ghica, Dan R. and Jung, Achim and Lopez, Aliaume},
title = {{Diagrammatic Semantics for Digital Circuits}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {24:1--24:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.24},
URN = {urn:nbn:de:0030-drops-76715},
doi = {10.4230/LIPIcs.CSL.2017.24},
annote = {Keywords: digital circuits, monoidal categories, string diagrams, rewriting, operational semantics}
}
Document
Precongruence Formats with Lookahead through Modal Decomposition
Abstract
Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.
Cite as
Wan Fokkink and Rob J. van Glabbeek. Precongruence Formats with Lookahead through Modal Decomposition. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{fokkink_et_al:LIPIcs.CSL.2017.25,
author = {Fokkink, Wan and van Glabbeek, Rob J.},
title = {{Precongruence Formats with Lookahead through Modal Decomposition}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {25:1--25:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.25},
URN = {urn:nbn:de:0030-drops-76776},
doi = {10.4230/LIPIcs.CSL.2017.25},
annote = {Keywords: Structural Operational Semantics, Compositionality, Congruence, Modal Logic, Modal Decomposition, Lookahead}
}
Document
Capturing Logarithmic Space and Polynomial Time on Chordal Claw-Free Graphs
Abstract
We show that the class of chordal claw-free graphs admits LREC=-definable canonization. LREC= is a logic that extends first-order logic with counting by an operator that allows it to formalize a limited form of recursion. This operator can be evaluated in logarithmic space. It follows that there exists a logarithmic-space canonization algorithm for the class of chordal claw-free graphs, and that LREC= captures logarithmic space on this graph class. Since LREC= is contained in fixed-point logic with counting, we also obtain that fixed-point logic with counting captures polynomial time on the class of chordal claw-free graphs.
Cite as
Berit Grußien. Capturing Logarithmic Space and Polynomial Time on Chordal Claw-Free Graphs. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{gruien:LIPIcs.CSL.2017.26,
author = {Gru{\ss}ien, Berit},
title = {{Capturing Logarithmic Space and Polynomial Time on Chordal Claw-Free Graphs}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {26:1--26:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.26},
URN = {urn:nbn:de:0030-drops-76900},
doi = {10.4230/LIPIcs.CSL.2017.26},
annote = {Keywords: Descriptive complexity, logarithmic space, polynomial time, chordal claw-free graphs}
}
Document
The Model-Theoretic Expressiveness of Propositional Proof Systems
Abstract
We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory.
Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded width resolution, and the polynomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory.
Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded width resolution captures existential least fixed-point logic, and that the (monomial restriction of the) polynomial calculus of bounded degree solves precisely the problems definable in fixed-point logic with counting.
Cite as
Erich Grädel, Benedikt Pago, and Wied Pakusa. The Model-Theoretic Expressiveness of Propositional Proof Systems. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{gradel_et_al:LIPIcs.CSL.2017.27,
author = {Gr\"{a}del, Erich and Pago, Benedikt and Pakusa, Wied},
title = {{The Model-Theoretic Expressiveness of Propositional Proof Systems}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.27},
URN = {urn:nbn:de:0030-drops-76897},
doi = {10.4230/LIPIcs.CSL.2017.27},
annote = {Keywords: Propositional proof systems, fixed-point logics, resolution, polynomial calculus, generalized quantifiers}
}
Document
Validity and Entailment in Modal and Propositional Dependence Logics
Abstract
The computational properties of modal and propositional dependence logics have been extensively studied over the past few years, starting from a result by Sevenster showing NEXPTIME-completeness of the satisfiability problem for modal dependence logic. Thus far, however, the validity and entailment properties of these logics have remained uncharacterised to a great extent. This paper establishes a complete classification of the complexity of validity and entailment in modal and propositional dependence logics. In particular, we address the question of the complexity of validity in modal dependence logic. By showing that it is NEXPTIME-complete we refute an earlier conjecture proposing a higher complexity for the problem.
Cite as
Miika Hannula. Validity and Entailment in Modal and Propositional Dependence Logics. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{hannula:LIPIcs.CSL.2017.28,
author = {Hannula, Miika},
title = {{Validity and Entailment in Modal and Propositional Dependence Logics}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {28:1--28:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.28},
URN = {urn:nbn:de:0030-drops-76691},
doi = {10.4230/LIPIcs.CSL.2017.28},
annote = {Keywords: modal logic, propositional logic, dependence logic, entailment, validity, complexity}
}
Document
CALF: Categorical Automata Learning Framework
Abstract
Automata learning is a technique that has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata have to be developed from scratch because there was no abstract theory offering guidelines. This makes it hard to devise such algorithms, and it obscures their correctness proofs. We introduce a simple category-theoretic formalism that provides an appropriately abstract foundation for studying automata learning. Furthermore, our framework establishes formal relations between algorithms for learning, testing, and minimization. We illustrate its generality with two examples: deterministic and weighted automata.
Cite as
Gerco van Heerdt, Matteo Sammartino, and Alexandra Silva. CALF: Categorical Automata Learning Framework. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 29:1-29:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{vanheerdt_et_al:LIPIcs.CSL.2017.29,
author = {van Heerdt, Gerco and Sammartino, Matteo and Silva, Alexandra},
title = {{CALF: Categorical Automata Learning Framework}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {29:1--29:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.29},
URN = {urn:nbn:de:0030-drops-76950},
doi = {10.4230/LIPIcs.CSL.2017.29},
annote = {Keywords: automata learning, category theory}
}
Document
Modal mu-Calculus with Atoms
Abstract
We introduce an extension of modal mu-calculus to sets with atoms and study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show some limitations to the expressiveness of the calculus and argue that a naive way to remove these limitations results in a logic whose model checking is undecidable.
Cite as
Bartek Klin and Mateusz Lelyk. Modal mu-Calculus with Atoms. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{klin_et_al:LIPIcs.CSL.2017.30,
author = {Klin, Bartek and Lelyk, Mateusz},
title = {{Modal mu-Calculus with Atoms}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {30:1--30:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.30},
URN = {urn:nbn:de:0030-drops-76991},
doi = {10.4230/LIPIcs.CSL.2017.30},
annote = {Keywords: modal mu-calculus, sets with atoms}
}
Document
The Power of the Filtration Technique for Modal Logics with Team Semantics
Abstract
Modal Team Logic (MTL) extends Väänänen's Modal Dependence Logic (MDL) by Boolean negation. Its satisfiability problem is decidable, but the exact complexity is not yet understood very well. We investigate a model-theoretical approach and generalize the successful filtration technique to work in team semantics. We identify an "existential" fragment of MTL that enjoys the exponential model property and is therefore, like Propositional Team Logic (PTL), complete for the class AEXP(poly). Moreover, superexponential filtration lower bounds for different fragments of MTL are proven, up to the full logic having no filtration for any elementary size bound. As a corollary, superexponential gaps of succinctness between MTL fragments of equal expressive power are shown.
Cite as
Martin Lück. The Power of the Filtration Technique for Modal Logics with Team Semantics. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{luck:LIPIcs.CSL.2017.31,
author = {L\"{u}ck, Martin},
title = {{The Power of the Filtration Technique for Modal Logics with Team Semantics}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {31:1--31:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.31},
URN = {urn:nbn:de:0030-drops-76739},
doi = {10.4230/LIPIcs.CSL.2017.31},
annote = {Keywords: dependence logic,team logic,modal logic,finite model theory}
}
Document
The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter
Abstract
Girard's Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been also successfully applied to programming languages. One way is to use abstract machines that pass a token in a fixed graph, along a path indicated by the GoI. These token-passing abstract machines are space efficient, because they handle duplicated computation by repeating the same moves of a token on the fixed graph. Although they can be adapted to obtain sound models with regard to the equational theories of various evaluation strategies for the lambda calculus, it can be at the expense of significant time costs. In this paper we show a token-passing abstract machine that can implement evaluation strategies for the lambda calculus, with certified time efficiency. Our abstract machine, called the Dynamic GoI Machine (DGoIM), rewrites the graph to avoid replicating computation, using the token to find the redexes. The flexibility of interleaving token transitions and graph rewriting allows the DGoIM to balance the trade-off of space and time costs. This paper shows that the DGoIM can implement call-by-need evaluation for the lambda calculus by using a strategy of interleaving token passing with as much graph rewriting as possible. Our quantitative analysis confirms that the DGoIM with this strategy of interleaving the two kinds of possible operations on graphs can be classified as “efficient” following Accattoli’s taxonomy of abstract machines.
Cite as
Koko Muroya and Dan R. Ghica. The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{muroya_et_al:LIPIcs.CSL.2017.32,
author = {Muroya, Koko and Ghica, Dan R.},
title = {{The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {32:1--32:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.32},
URN = {urn:nbn:de:0030-drops-76886},
doi = {10.4230/LIPIcs.CSL.2017.32},
annote = {Keywords: Geometry of Interaction, cost analysis, call-by-need reduction}
}
Document
On Supergraphs Satisfying CMSO Properties
Abstract
Let CMSO denote the counting monadic second order logic of graphs. We give a constructive proof that for some computable function f, there is an algorithm A that takes as input a CMSO sentence F, a positive integer t, and a connected graph G of maximum degree at most D, and determines, in time f(|F|,t)*2^O(D*t)*|G|^O(t), whether G has a supergraph G' of treewidth at most t such that G' satisfies F.
The algorithmic metatheorem described above sheds new light on certain unresolved questions within the framework of graph completion algorithms. In particular, using this metatheorem, we provide an explicit algorithm that determines, in time f(d)*2^O(D*d)*|G|^O(d), whether a connected graph of maximum degree D has a planar supergraph of diameter at most d. Additionally, we show that for each fixed k, the problem of determining whether G has a k-outerplanar supergraph of diameter at most d is strongly uniformly fixed parameter tractable with respect to the parameter d.
This result can be generalized in two directions. First, the diameter parameter can be replaced by any contraction-closed effectively CMSO-definable parameter p. Examples of such parameters are vertex-cover number, dominating number, and many other contraction-bidimensional parameters. In the second direction, the planarity requirement can be relaxed to bounded genus, and more generally, to bounded local treewidth.
Cite as
Mateus de Oliveira Oliveira. On Supergraphs Satisfying CMSO Properties. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{deoliveiraoliveira:LIPIcs.CSL.2017.33,
author = {de Oliveira Oliveira, Mateus},
title = {{On Supergraphs Satisfying CMSO Properties}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {33:1--33:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.33},
URN = {urn:nbn:de:0030-drops-77058},
doi = {10.4230/LIPIcs.CSL.2017.33},
annote = {Keywords: On Supergraphs Satisfying CMSO Properties}
}
Document
Inductive and Functional Types in Ludics
Abstract
Ludics is a logical framework in which types/formulas are modelled by sets of terms with the same computational behaviour. This paper investigates the representation of inductive data types and functional types in ludics. We study their structure following a game semantics approach. Inductive types are interpreted as least fixed points, and we prove an internal completeness result giving an explicit construction for such fixed points. The interactive properties of the ludics interpretation of inductive and functional types are then studied. In particular, we identify which higher-order functions types fail to satisfy type safety, and we give a computational explanation.
Cite as
Alice Pavaux. Inductive and Functional Types in Ludics. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{pavaux:LIPIcs.CSL.2017.34,
author = {Pavaux, Alice},
title = {{Inductive and Functional Types in Ludics}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {34:1--34:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.34},
URN = {urn:nbn:de:0030-drops-77035},
doi = {10.4230/LIPIcs.CSL.2017.34},
annote = {Keywords: Ludics, Inductive types, Fixed point, Linear logic, Game semantics}
}
Document
Advice Automatic Structures and Uniformly Automatic Classes
Abstract
We study structures that are automatic with advice. These are structures that admit a presentation by finite automata (over finite or infinite words or trees) with access to an additional input,called an advice. Over finite words, a standard example of a structure that is automatic with advice, but not automatic in the classical sense, is the additive group of rational numbers (Q,+).
By using a set of advices rather than a single advice, this leads to the new concept of a parameterised automatic presentation as a means to uniformly represent a whole class of structures. The decidability of the first-order theory of such a uniformly automatic class reduces to the decidability of the monadic second-order theory of the set of advices that are used in the presentation. Such decidability results also hold for extensions of first-order logic by regularity preserving quantifiers, such as cardinality quantifiers and Ramsey quantifiers.
To investigate the power of this concept, we present examples of structures and classes of structures that are automatic with advice but not without advice, and we prove classification theorems for the structures with an advice automatic presentation for several algebraic domains.
In particular, we prove that the class of all torsion-free Abelian groups of rank one is uniformly omega-automatic and that there is a uniform omega-tree-automatic presentation of the class of all Abelian groups up to elementary equivalence and of the class of all countable divisible Abelian groups.
On the other hand we show that every uniformly omega-automatic class of Abelian groups must have bounded rank.
While for certain domains, such as trees and Abelian groups, it turns out that automatic presentations with advice are capable of presenting significantly more complex structures than ordinary automatic presentations, there are other domains, such as Boolean algebras, where this is provably not the case. Further, advice seems to not be of much help for representing some particularly relevant examples of structures with decidable theories, most notably the field of
reals.
Finally we study closure properties for several kinds of uniformly automatic classes, and decision problems concerning the number of non-isomorphic models in uniformly automatic classes with the unique representation property.
Cite as
Faried Abu Zaid, Erich Grädel, and Frederic Reinhardt. Advice Automatic Structures and Uniformly Automatic Classes. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 35:1-35:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{abuzaid_et_al:LIPIcs.CSL.2017.35,
author = {Abu Zaid, Faried and Gr\"{a}del, Erich and Reinhardt, Frederic},
title = {{Advice Automatic Structures and Uniformly Automatic Classes}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {35:1--35:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.35},
URN = {urn:nbn:de:0030-drops-76971},
doi = {10.4230/LIPIcs.CSL.2017.35},
annote = {Keywords: automatic structures, algorithmic model theory, decidable theories, torsion-free abelian groups, first-order logic}
}
Document
Strongly Normalizing Audited Computation
Abstract
Auditing is an increasingly important operation for computer programming, for example in security (e.g. to enable history-based access control) and to enable reproducibility and accountability (e.g. provenance in scientific programming). Most proposed auditing techniques are ad hoc or treat auditing as a second-class, extralinguistic operation; logical or semantic foundations for auditing are not yet well-established. Justification Logic (JL) offers one such foundation; Bavera and Bonelli introduced a computational interpretation of JL called lambda^h that supports auditing. However, lambda^h is technically complex and strong normalization was only established for special cases. In addition, we show that the equational theory of lambda^h is inconsistent. We introduce a new calculus lambda^hc that is simpler than lambda^hc, consistent, and strongly normalizing. Our proof of strong normalization is formalized in Nominal Isabelle.
Cite as
Wilmer Ricciotti and James Cheney. Strongly Normalizing Audited Computation. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 36:1-36:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{ricciotti_et_al:LIPIcs.CSL.2017.36,
author = {Ricciotti, Wilmer and Cheney, James},
title = {{Strongly Normalizing Audited Computation}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {36:1--36:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.36},
URN = {urn:nbn:de:0030-drops-76817},
doi = {10.4230/LIPIcs.CSL.2017.36},
annote = {Keywords: lambda calculus, justification logic, strong normalization, audited computation}
}
Document
A Finitary Analogue of the Downward Löwenheim-Skolem Property
Abstract
We present a model-theoretic property of finite structures, that can be seen to be a finitary analogue of the well-studied downward Löwenheim-Skolem property from classical model theory. We call this property the *L-equivalent bounded substructure property*, denoted L-EBSP, where L is either FO or MSO. Intuitively, L-EBSP states that a large finite structure contains a small "logically similar" substructure, where logical similarity means indistinguishability with respect to sentences of L having a given quantifier nesting depth. It turns out that this simply stated property is enjoyed by a variety of classes of interest in computer science: examples include regular languages of words, trees (unordered, ordered or ranked) and nested words, and various classes of graphs, such as cographs, graph classes of bounded tree-depth, those of bounded shrub-depth and n-partite cographs. Further, L-EBSP remains preserved in the classes generated from the above by operations that are implementable using quantifier-free translation schemes. All of the aforementioned classes admit natural tree representations for their structures. We use this fact to show that the small and logically similar substructure of a large structure in any of these classes, can be computed in time linear in the size of the tree representation of the structure, giving linear time fixed parameter tractable (f.p.t.) algorithms for checking L-definable properties of the large structure. We conclude by presenting a strengthening of L-EBSP, that asserts "logical self-similarity at all scales" for a suitable notion of scale. We call this the *logical fractal* property and show that most of the classes mentioned above are indeed, logical fractals.
Cite as
Abhisekh Sankaran. A Finitary Analogue of the Downward Löwenheim-Skolem Property. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{sankaran:LIPIcs.CSL.2017.37,
author = {Sankaran, Abhisekh},
title = {{A Finitary Analogue of the Downward L\"{o}wenheim-Skolem Property}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {37:1--37:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.37},
URN = {urn:nbn:de:0030-drops-77074},
doi = {10.4230/LIPIcs.CSL.2017.37},
annote = {Keywords: downward Lowenheim-Skolem theorem, trees, nested words, tree-depth, cographs, tree representation, translation schemes, composition lemma, f.p.t., log}
}
Document
Aleph1 and the Modal mu-Calculus
Abstract
For a regular cardinal kappa, a formula of the modal mu-calculus is kappa-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of kappa-directed sets. We define the fragment C1 (x) of the modal mu-calculus and prove that all the formulas in this fragment are aleph_1-continuous. For each formula phi(x) of the modal mu-calculus, we construct a formula psi(x) in C1 (x) such that phi(x) is kappa-continuous, for some kappa, if and only if psi(x) is equivalent to phi(x). Consequently, we prove that (i) the problem whether a formula is kappa-continuous for some kappa is decidable, (ii) up to equivalence, there are only two fragments determined by continuity at some regular cardinal: the fragment C0(x) studied by Fontaine and the fragment C1 (x). We apply our considerations to the problem of characterizing closure ordinals of formulas of the modal mu-calculus. An ordinal alpha is the closure ordinal of a formula phi(x) if its interpretation on every model converges to its least fixed-point in at most alpha steps and if there is a model where the convergence occurs exactly in alpha steps. We prove that omega_1, the least uncountable ordinal, is such a closure ordinal. Moreover we prove that closure ordinals are closed under ordinal sum. Thus, any formal expression built from 0, 1, omega, omega_1 by using the binary operator symbol + gives rise to a closure ordinal.
Cite as
Maria João Gouveia and Luigi Santocanale. Aleph1 and the Modal mu-Calculus. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{gouveia_et_al:LIPIcs.CSL.2017.38,
author = {Gouveia, Maria Jo\~{a}o and Santocanale, Luigi},
title = {{Aleph1 and the Modal mu-Calculus}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {38:1--38:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.38},
URN = {urn:nbn:de:0030-drops-76926},
doi = {10.4230/LIPIcs.CSL.2017.38},
annote = {Keywords: Modal mu-calculus, regular cardinal, continuous function, aleph1, omega1, closure ordinal, ordinal sum}
}
Document
Taylor Expansion, lambda-Reduction and Normalization
Abstract
We introduce a notion of reduction on resource vectors, i.e. infinite linear combinations of resource lambda-terms. The latter form the multilinear fragment of the differential lambda-calculus introduced by Ehrhard and Regnier, and resource vectors are the target of the Taylor expansion of lambda-terms.
We show that the reduction of resource vectors contains the image, through Taylor expansion, of beta-reduction in the algebraic lambda-calculus, i.e. lambda-calculus extended with weighted sums: in particular, Taylor expansion and normalization commute.
We moreover exhibit a class of algebraic lambda-terms, having a normalizable Taylor expansion, subsuming both arbitrary pure lambda-terms, and normalizable algebraic lambda-terms. For these, we prove the commutation of Taylor expansion and normalization in a more denotational sense, mimicking the Böhm tree construction.
Cite as
Lionel Vaux. Taylor Expansion, lambda-Reduction and Normalization. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 39:1-39:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{vaux:LIPIcs.CSL.2017.39,
author = {Vaux, Lionel},
title = {{Taylor Expansion, lambda-Reduction and Normalization}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {39:1--39:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.39},
URN = {urn:nbn:de:0030-drops-76948},
doi = {10.4230/LIPIcs.CSL.2017.39},
annote = {Keywords: lambda-calculus, non-determinism, normalization, denotational semantics}
}
Document
On the First-Order Complexity of Induced Subgraph Isomorphism
Abstract
Given a graph F, let I(F) be the class of graphs containing F
as an induced subgraph. Let W[F] denote the minimum k such that
I(F) is definable in k-variable first-order logic. The recognition
problem of I(F), known as Induced Subgraph Isomorphism (for the pattern graph F), is solvable in time O(n^{W[F]}). Motivated by this fact, we are interested in determining or estimating the value of W[F]. Using Olariu's characterization of paw-free graphs, we show that I(K_3+e) is definable by a first-order sentence of quantifier depth 3, where K_3+e denotes the paw graph. This provides an example of a graph F with W[F] strictly less than the number of vertices in F.
On the other hand, we prove that W[F]=4 for all F on 4 vertices
except the paw graph and its complement. If F is a graph on t vertices, we prove a general lower bound W[F]>(1/2-o(1))t, where the function in the little-o notation approaches 0 as t increases. This bound holds true even for a related parameter W^*[F], which is
defined as the minimum k such that I(F) is definable in the k-variable
infinitary logic. We show that W^*[F] can be strictly less than W[F]. Specifically, W^*[P_4]=3 for P_4 being the path graph on 4 vertices.
Cite as
Oleg Verbitsky and Maksim Zhukovskii. On the First-Order Complexity of Induced Subgraph Isomorphism. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 40:1-40:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{verbitsky_et_al:LIPIcs.CSL.2017.40,
author = {Verbitsky, Oleg and Zhukovskii, Maksim},
title = {{On the First-Order Complexity of Induced Subgraph Isomorphism}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {40:1--40:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.40},
URN = {urn:nbn:de:0030-drops-76841},
doi = {10.4230/LIPIcs.CSL.2017.40},
annote = {Keywords: the induced subgraph isomorphism problem, descriptive and computational complexity, finite-variable first-order logic, quantifier depth and variable w}
}
Document
Strategies with Parallel Causes
Abstract
We imagine a team Player engaging a team Opponent in a distributed game. Such games and their strategies have been formalised within event structures. However there are limitations in founding strategies on traditional event structures. Sometimes a probabilistic distributed strategy relies on benign races where, intuitively, several members of team Player may race each other to make a common move. Although there exist event structures which support such parallel causes, in which an event is enabled in several compatible ways, they do not support an operation of hiding central to the composition of strategies; nor do they support probability adequately. An extension of traditional event structures is devised which supports parallel causes and hiding, as well as the mix of probability and nondeterminism needed to account for probabilistic distributed strategies. The extension is located within existing models for concurrency and tested in the construction of a bicategory of probabilistic distributed strategies with parallel causes.
Cite as
Marc de Visme and Glynn Winskel. Strategies with Parallel Causes. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 41:1-41:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{devisme_et_al:LIPIcs.CSL.2017.41,
author = {de Visme, Marc and Winskel, Glynn},
title = {{Strategies with Parallel Causes}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {41:1--41:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.41},
URN = {urn:nbn:de:0030-drops-76800},
doi = {10.4230/LIPIcs.CSL.2017.41},
annote = {Keywords: Games, Strategies, Event Structures, Parallel Causes, Probability}
}
Document
An Algebraic Approach to Valued Constraint Satisfaction
Abstract
We study the complexity of the valued CSP (VCSP, for short) over arbitrary templates, taking the general framework of integral bounded linearly order monoids as valuation structures. The class of problems considered here subsumes and generalizes the most common one in VCSP literature, since both monoidal and lattice conjunction operations are allowed in the formulation of constraints. Restricting to locally finite monoids, we introduce a notion of polymorphism that captures the pp-definability in the style of Geiger’s result. As a consequence, sufficient conditions for tractability of the classical CSP, related to the existence of certain polymorphisms, are shown to serve also for the valued case. Finally, we establish the dichotomy conjecture for the VCSP, modulo the dichotomy for classical CSP.
Cite as
Rostislav Horcík, Tommaso Moraschini, and Amanda Vidal. An Algebraic Approach to Valued Constraint Satisfaction. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 42:1-42:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{horcik_et_al:LIPIcs.CSL.2017.42,
author = {Horc{\'\i}k, Rostislav and Moraschini, Tommaso and Vidal, Amanda},
title = {{An Algebraic Approach to Valued Constraint Satisfaction}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {42:1--42:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-045-3},
ISSN = {1868-8969},
year = {2017},
volume = {82},
editor = {Goranko, Valentin and Dam, Mads},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.42},
URN = {urn:nbn:de:0030-drops-76767},
doi = {10.4230/LIPIcs.CSL.2017.42},
annote = {Keywords: Valued CSP, Polymorphism, pp-definability, Geiger’s Theorem.}
}