Volume
LIPIcs, Volume 41
24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2015, September 7-10, 2015, Berlin, GermanyEditor
Publication Details
- published at: 2015-09-07
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-90-3
- DBLP: db/conf/csl/csl2015
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 41, CSL'15, Complete Volume
Abstract
LIPIcs, Volume 41, CSL'15, Complete Volume
Cite as
24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@Proceedings{kreutzer:LIPIcs.CSL.2015,
title = {{LIPIcs, Volume 41, CSL'15, Complete Volume}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015},
URN = {urn:nbn:de:0030-drops-54670},
doi = {10.4230/LIPIcs.CSL.2015},
annote = {Keywords: Conference Proceedings, Distributed Systems, Software/ Programs Verifications, Formal Definitions and Theory, Languages Constructs and Features, Knowledge Representations Formalisms and Methods, Theory of Computation, Mathematical Logic}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organisation, External Reviewers
Abstract
Front Matter, Table of Contents, Preface, Conference Organisation, External Reviewers
Cite as
24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kreutzer:LIPIcs.CSL.2015.i,
author = {Kreutzer, Stephan},
title = {{Front Matter, Table of Contents, Preface, Conference Organisation, External Reviewers}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {i--xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.i},
URN = {urn:nbn:de:0030-drops-54489},
doi = {10.4230/LIPIcs.CSL.2015.i},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organisation, External Reviewers}
}
Document
The Ackermann Award 2015
Abstract
The eleventh Ackermann Award is presented at CSL'15 in Berlin, Germany. This year, again, the EACSL Ackermann Award is generously sponsored by the Kurt Gödel Society. Besides providing financial support for the Ackermann Award, the Kurt Gödel Society has also committed to inviting the recipients of the Award for a special lecture to be given to the Society in Vienna.
Cite as
Anuj Dawar, Dexter Kozen, and Simona Ronchi Della Rocca. The Ackermann Award 2015. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 15-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2015.xv,
author = {Dawar, Anuj and Kozen, Dexter and Ronchi Della Rocca, Simona},
title = {{The Ackermann Award 2015}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {15--18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.xv},
URN = {urn:nbn:de:0030-drops-54470},
doi = {10.4230/LIPIcs.CSL.2015.xv},
annote = {Keywords: Ackermann Award}
}
Document
Invited Talk
The Prophecy of Timely Rollback (Invited Talk)
Abstract
Techniques for rollback recovery play a central role in ensuring fault-tolerance in many distributed systems. This talk addresses the formal specification and analysis of those techniques. In particular, we will discuss the relevance of prophecy variables (auxiliary program variables whose values are defined in terms of current program state and future behavior) to reasoning about systems with undo operations. We will then focus on a model for data-parallel computation with a notion of virtual time. In this model, rollbacks allow the selective undo of work at particular virtual times. A refinement theorem ensures the consistency of rollbacks.
This talk is largely based on joint work with Michael Isard.
Cite as
Martín Abadi. The Prophecy of Timely Rollback (Invited Talk). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{abadi:LIPIcs.CSL.2015.1,
author = {Abadi, Mart{\'\i}n},
title = {{The Prophecy of Timely Rollback}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {1--1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.1},
URN = {urn:nbn:de:0030-drops-54452},
doi = {10.4230/LIPIcs.CSL.2015.1},
annote = {Keywords: Dataflow, refinement, rollback}
}
Document
Invited Talk
Temporal Logics with Local Constraints (Invited Talk)
Abstract
Recent decidability results on the satisfiability problem for temporal logics, in particular LTL, CTL* and ECTL*, with constraints over external structures like the integers with the order or infinite trees are surveyed in this paper.
Cite as
Claudia Carapelle and Markus Lohrey. Temporal Logics with Local Constraints (Invited Talk). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 2-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{carapelle_et_al:LIPIcs.CSL.2015.2,
author = {Carapelle, Claudia and Lohrey, Markus},
title = {{Temporal Logics with Local Constraints}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {2--13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.2},
URN = {urn:nbn:de:0030-drops-54465},
doi = {10.4230/LIPIcs.CSL.2015.2},
annote = {Keywords: Temporal logics with constraints, concrete domains, LTL, CTL*, ECTL*}
}
Document
Invited Talk
Thinking Algorithmically About Impossibility (Invited Talk)
Abstract
Complexity lower bounds like P != NP assert impossibility results for all possible programs of some restricted form. As there are presently enormous gaps in our lower bound knowledge, a central question on the minds of today's complexity theorists is how will we find better ways to reason about all efficient programs?
I argue that some progress can be made by (very deliberately) thinking algorithmically about lower bounds. Slightly more precisely, to prove a lower bound against some class C of programs, we can start by treating C as a set of inputs to another (larger) process, which is intended to perform some basic analysis of programs in C. By carefully studying the algorithmic "meta-analysis" of programs in C, we can learn more about the limitations of the programs being analyzed.
This essay is mostly self-contained; scant knowledge is assumed of the reader.
Cite as
R. Ryan Williams. Thinking Algorithmically About Impossibility (Invited Talk). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 14-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{williams:LIPIcs.CSL.2015.14,
author = {Williams, R. Ryan},
title = {{Thinking Algorithmically About Impossibility}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {14--23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.14},
URN = {urn:nbn:de:0030-drops-54396},
doi = {10.4230/LIPIcs.CSL.2015.14},
annote = {Keywords: satisfiability, derandomization, circuit complexity}
}
Document
Simple Parsimonious Types and Logarithmic Space
Abstract
We present a functional characterization of deterministic logspace-computable predicates based on a variant (although not a subsystem) of propositional linear logic, which we call parsimonious logic. The resulting calculus is simply-typed and contains no primitive besides those provided by the underlying logical system, which makes it one of the simplest higher-order languages capturing logspace currently known. Completeness of the calculus uses the descriptive complexity characterization of logspace (we encode first-order logic with deterministic closure), whereas soundness is established by executing terms on a token machine (using the geometry of interaction).
Cite as
Damiano Mazza. Simple Parsimonious Types and Logarithmic Space. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 24-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{mazza:LIPIcs.CSL.2015.24,
author = {Mazza, Damiano},
title = {{Simple Parsimonious Types and Logarithmic Space}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {24--40},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.24},
URN = {urn:nbn:de:0030-drops-54053},
doi = {10.4230/LIPIcs.CSL.2015.24},
annote = {Keywords: implicit computational complexity, linear logic, geometry of interaction}
}
Document
First-Order Queries on Finite Abelian Groups
Abstract
We study the computational problem of checking whether a logical sentence is true in a finite abelian group. We prove that model checking first-order sentences on finite abelian groups is fixed-parameter tractable, when parameterized by the size of the sentence. We also prove that model checking monadic second-order sentences on finite abelian groups finitely presented by integer matrices is not fixed-parameter tractable (under standard assumptions in parameterized complexity).
Cite as
Simone Bova and Barnaby Martin. First-Order Queries on Finite Abelian Groups. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 41-59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bova_et_al:LIPIcs.CSL.2015.41,
author = {Bova, Simone and Martin, Barnaby},
title = {{First-Order Queries on Finite Abelian Groups}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {41--59},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.41},
URN = {urn:nbn:de:0030-drops-54060},
doi = {10.4230/LIPIcs.CSL.2015.41},
annote = {Keywords: Finite Abelian Groups, First-Order Logic, Monadic Second-Order Logic}
}
Document
A Definability Dichotomy for Finite Valued CSPs
Abstract
Finite valued constraint satisfaction problems are a formalism for describing many natural optimisation problems, where constraints on the values that variables can take come with rational weights and the aim is to find an assignment of minimal cost. Thapper and Zivny have recently established a complexity dichotomy for valued constraint languages. They show that each such languages either gives rise to a polynomial-time solvable optimisation problem, or to an NP-hard one, and establish a criterion to distinguish the two cases. We refine the dichotomy by showing that all optimisation problems in the first class are definable in fixed-point language with counting, while all languages in the second class are not definable, even in infinitary logic with counting. Our definability dichotomy is not conditional on any complexity-theoretic assumption.
Cite as
Anuj Dawar and Pengming Wang. A Definability Dichotomy for Finite Valued CSPs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 60-77, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2015.60,
author = {Dawar, Anuj and Wang, Pengming},
title = {{A Definability Dichotomy for Finite Valued CSPs}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {60--77},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.60},
URN = {urn:nbn:de:0030-drops-54078},
doi = {10.4230/LIPIcs.CSL.2015.60},
annote = {Keywords: descriptive complexity, constraint satisfaction, definability, fixed-point logic, optimization}
}
Document
Evidence for Fixpoint Logic
Abstract
For many modal logics, dedicated model checkers offer diagnostics (e.g., counterexamples) that help the user understand the result provided by the solver. Fixpoint logic offers a unifying framework in which such problems can be expressed and solved, but a drawback of this framework is that it lacks comprehensive diagnostics generation. We extend the framework with a notion of evidence, which can be specialized to obtain diagnostics for various model checking problems, behavioural equivalence and refinement checking problems. We demonstrate this by showing how our notion of evidence can be used to obtain diagnostics for the problem of deciding stuttering bisimilarity. Moreover, we show that our notion generalizes the existing notions of counterexample and witness for LTL and ACTL* model checking.
Cite as
Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse. Evidence for Fixpoint Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 78-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{cranen_et_al:LIPIcs.CSL.2015.78,
author = {Cranen, Sjoerd and Luttik, Bas and Willemse, Tim A. C.},
title = {{Evidence for Fixpoint Logic}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {78--93},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.78},
URN = {urn:nbn:de:0030-drops-54080},
doi = {10.4230/LIPIcs.CSL.2015.78},
annote = {Keywords: fixpoint logic, diagnostics, counterexample, model checking, stuttering bisimilarity, ACTL*}
}
Document
Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic
Abstract
The size of shortest cut-free proofs of first-order formulas in intuitionistic sequent calculus is known to be non-elementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cut-free proofs for disjunction-free intuitionistic logic for the case where the cut-formulas of the original proof are prenex. Moreover, we establish non-elementary lower bounds for classical disjunction-free proofs with prenex cut-formulas and intuitionistic disjunction-free proofs with non-prenex cut-formulas.
Cite as
Matthias Baaz and Christian G. Fermüller. Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 94-109, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{baaz_et_al:LIPIcs.CSL.2015.94,
author = {Baaz, Matthias and Ferm\"{u}ller, Christian G.},
title = {{Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {94--109},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.94},
URN = {urn:nbn:de:0030-drops-54097},
doi = {10.4230/LIPIcs.CSL.2015.94},
annote = {Keywords: Cut-elimination, sequent calculus, intuitionistic logic}
}
Document
Tree Grammars for the Elimination of Non-prenex Cuts
Abstract
Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs with prenex Pi_1-cuts in classical first-order logic corresponds to computing the language of a particular type of tree grammars. The present paper extends this connection to arbitrary (i.e. non-prenex) cuts without quantifier alternations. The key to treating non-prenex cuts lies in using a new class of tree grammars, constraint grammars, which describe the relationship of the applicability of its productions by a propositional formula.
Cite as
Stefan Hetzl and Sebastian Zivota. Tree Grammars for the Elimination of Non-prenex Cuts. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 110-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hetzl_et_al:LIPIcs.CSL.2015.110,
author = {Hetzl, Stefan and Zivota, Sebastian},
title = {{Tree Grammars for the Elimination of Non-prenex Cuts}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {110--127},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.110},
URN = {urn:nbn:de:0030-drops-54103},
doi = {10.4230/LIPIcs.CSL.2015.110},
annote = {Keywords: proof theory, cut-elimination, Herbrand's theorem, tree grammars}
}
Document
Automata Theoretic Account of Proof Search
Abstract
Automata theoretical techniques are developed that handle inhabitant search in the simply typed lambda calculus. The automata-theoretic model for inhabitant search, which can be viewed as proof search by the Curry-Howard isomorphism, is proven to be adequate by reduction of the inhabitant existence problem to the emptiness problem for the automata. To strengthen the claim, it is demonstrated that the latter has the same complexity as the former. We also discuss the basic closure properties of the automata.
Cite as
Aleksy Schubert, Wil Dekkers, and Henk P. Barendregt. Automata Theoretic Account of Proof Search. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 128-143, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{schubert_et_al:LIPIcs.CSL.2015.128,
author = {Schubert, Aleksy and Dekkers, Wil and Barendregt, Henk P.},
title = {{Automata Theoretic Account of Proof Search}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {128--143},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.128},
URN = {urn:nbn:de:0030-drops-54113},
doi = {10.4230/LIPIcs.CSL.2015.128},
annote = {Keywords: simple types, automata, trees, languages of proofs}
}
Document
Maximal Partition Logic: Towards a Logical Characterization of Copyless Cost Register Automata
Abstract
It is highly desirable for a computational model to have a logic characterization like in the seminal work from Buchi that connects MSO with finite automata. For example, weighted automata are the quantitative extension of finite automata for computing functions over words and they can be naturally characterized by a subframent of weighted logic introduced by Droste and Gastin. Recently, cost register automata (CRA) were introduced by Alur et al. as an alternative model for weighted automata. In hope of finding decidable subclasses of weighted automata, they proposed to restrict their model with the so-called copyless restriction. Unfortunately, copyless CRA do not enjoy good closure properties and, therefore, a logical characterization of this class seems to be unlikely.
In this paper, we introduce a new logic called maximal partition logic (MPL) for studying the expressiveness of copyless CRA. In contrast from the previous approaches (i.e. weighted logics), MPL is based on a new set of "regular" quantifiers that partition a word into maximal subwords, compute the output of a subformula over each subword separately, and then aggregate these outputs with a semiring operation. We study the expressiveness of MPL and compare it with weighted logics. Furthermore, we show that MPL is equally expressive to a natural subclass of copyless CRA. This shows the first logical characterization of copyless CRA and it gives a better understanding of the copyless restriction in weighted automata.
Cite as
Filip Mazowiecki and Cristian Riveros. Maximal Partition Logic: Towards a Logical Characterization of Copyless Cost Register Automata. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 144-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{mazowiecki_et_al:LIPIcs.CSL.2015.144,
author = {Mazowiecki, Filip and Riveros, Cristian},
title = {{Maximal Partition Logic: Towards a Logical Characterization of Copyless Cost Register Automata}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {144--159},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.144},
URN = {urn:nbn:de:0030-drops-54127},
doi = {10.4230/LIPIcs.CSL.2015.144},
annote = {Keywords: MSO, Finite Automata, Cost Register Automata, Weighted Automata, Weighted Logics, Semirings}
}
Document
Aperiodic Two-way Transducers and FO-Transductions
Abstract
Deterministic two-way transducers on finite words have been shown by Engelfriet and Hoogeboom to have the same expressive power as MSO-transductions. We introduce a notion of aperiodicity for these transducers and we show that aperiodic transducers correspond exactly to FO-transductions. This lifts to transducers the classical equivalence for languages between FO-definability, recognition by aperiodic monoids and acceptance by counter-free automata.
Cite as
Olivier Carton and Luc Dartois. Aperiodic Two-way Transducers and FO-Transductions. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 160-174, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{carton_et_al:LIPIcs.CSL.2015.160,
author = {Carton, Olivier and Dartois, Luc},
title = {{Aperiodic Two-way Transducers and FO-Transductions}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {160--174},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.160},
URN = {urn:nbn:de:0030-drops-54133},
doi = {10.4230/LIPIcs.CSL.2015.160},
annote = {Keywords: Transducer, first-order, two-way, transition monoid, aperiodic}
}
Document
On Relative and Probabilistic Finite Counterability
Abstract
A counterexample to the satisfaction of a linear property psi in a system S is an infinite computation of S that violates psi. Counterexamples are of great help in detecting design errors and in modeling methodologies such as CEGAR. When psi is a safety property, a counterexample to its satisfaction need not be infinite. Rather, it is a bad-prefix for psi: a finite word all whose extensions violate psi. The existence of finite counterexamples is very helpful in practice. Liveness properties do not have bad-prefixes and thus do not have finite counterexamples.
We extend the notion of finite counterexamples to non-safety properties. We study counterable languages - ones that have at least one bad-prefix. Thus, a language is counterable iff it is not liveness. Three natural problems arise: (1) Given a language, decide whether it is counterable, (2) study the length of minimal bad-prefixes for counterable languages, and (3) develop algorithms for detecting bad-prefixes for counterable languages. We solve the problems for languages given by means of LTL formulas or nondeterministic Büchi automata. In particular, our EXPSPACE-completeness proof for the problem of deciding whether a given LTL formula is counterable, and hence also for deciding whether it is liveness, settles a long-standing open problem.
We also make finite counterexamples more relevant and helpful by introducing two variants of the traditional definition of bad-prefixes. The first adds a probabilistic component to the definition. There, a prefix is bad if almost all its extensions violate the property. The second makes it relative to the system. There, a prefix is bad if all its extensions in the system violate the property. We also study the combination of the probabilistic and relative variants. Our framework suggests new variants also of safety and liveness languages. We solve the above three problems for the different variants. Interestingly, the probabilistic variant not only increases the chances to return finite counterexamples, but also makes the solution of the three problems exponentially easier.
Cite as
Orna Kupferman and Gal Vardi. On Relative and Probabilistic Finite Counterability. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 175-192, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kupferman_et_al:LIPIcs.CSL.2015.175,
author = {Kupferman, Orna and Vardi, Gal},
title = {{On Relative and Probabilistic Finite Counterability}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {175--192},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.175},
URN = {urn:nbn:de:0030-drops-54147},
doi = {10.4230/LIPIcs.CSL.2015.175},
annote = {Keywords: Model Checking, Counterexamples, Safety, Liveness, Probability, omega-Regular Languages}
}
Document
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives
Abstract
Model checking is commonly recognized as one of the most effective tool in system verification. While it has been systematically investigated in the context of classical, point-based temporal logics, it is still largely unexplored in the interval logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS, interpreted over finite Kripke structures, has been proposed, together with a proof of the EXPSPACE-hardness of the problem. In this paper, we devise an EXPSPACE model checking procedure for two meaningful HS fragments. It exploits a suitable contraction technique, that allows one to replace long enough tracks of a Kripke structure by equivalent shorter ones.
Cite as
Alberto Molinari, Angelo Montanari, and Adriano Peron. A Model Checking Procedure for Interval Temporal Logics based on Track Representatives. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 193-210, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{molinari_et_al:LIPIcs.CSL.2015.193,
author = {Molinari, Alberto and Montanari, Angelo and Peron, Adriano},
title = {{A Model Checking Procedure for Interval Temporal Logics based on Track Representatives}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {193--210},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.193},
URN = {urn:nbn:de:0030-drops-54150},
doi = {10.4230/LIPIcs.CSL.2015.193},
annote = {Keywords: Interval Temporal Logic, Model Checking, Complexity}
}
Document
Contextuality, Cohomology and Paradox
Abstract
Contextuality is a key feature of quantum mechanics that provides an important non-classical resource for quantum information and computation. Abramsky and Brandenburger used sheaf theory to give a general treatment of contextuality in quantum theory [New Journal of Physics 13 (2011) 113036]. However, contextual phenomena are found in other fields as well, for example database theory. In this paper, we shall develop this unified view of contextuality. We provide two main contributions: firstly, we expose a remarkable connection between contexuality and logical paradoxes; secondly, we show that an important class of contextuality arguments has a topological origin. More specifically, we show that "All-vs-Nothing" proofs of contextuality are witnessed by cohomological obstructions.
Cite as
Samson Abramsky, Rui Soares Barbosa, Kohei Kishida, Raymond Lal, and Shane Mansfield. Contextuality, Cohomology and Paradox. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 211-228, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{abramsky_et_al:LIPIcs.CSL.2015.211,
author = {Abramsky, Samson and Soares Barbosa, Rui and Kishida, Kohei and Lal, Raymond and Mansfield, Shane},
title = {{Contextuality, Cohomology and Paradox}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {211--228},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.211},
URN = {urn:nbn:de:0030-drops-54166},
doi = {10.4230/LIPIcs.CSL.2015.211},
annote = {Keywords: Quantum mechanics, contextuality, sheaf theory, cohomology, logical paradoxes}
}
Document
A Model for Behavioural Properties of Higher-order Programs
Abstract
We consider simply typed lambda-calculus with fixpoints as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as a potentially infinite tree of calls to built-in operations. Properties of such trees are properties of executions of programs and monadic second-order logic (MSOL) is well suited to express them.
For a given MSOL property we show how to construct a finitary model recognizing it. In other words, the value of a lambda-term in the model determines if the tree that is the result of the execution of the term satisfies the property. The finiteness of the construction has as consequences many known results about the verification of higher-order programs in this framework.
Cite as
Sylvain Salvati and Igor Walukiewicz. A Model for Behavioural Properties of Higher-order Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 229-243, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{salvati_et_al:LIPIcs.CSL.2015.229,
author = {Salvati, Sylvain and Walukiewicz, Igor},
title = {{A Model for Behavioural Properties of Higher-order Programs}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {229--243},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.229},
URN = {urn:nbn:de:0030-drops-54173},
doi = {10.4230/LIPIcs.CSL.2015.229},
annote = {Keywords: Simply typed lambda-Y-calculus, Monadic second order logic, semantic models}
}
Document
Reachability Analysis of First-order Definable Pushdown Systems
Abstract
We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are first-order definable in a fixed countably-infinite structure. We show that the reachability analysis can be addressed with the well-known saturation technique for the wide class of oligomorphic structures. Moreover, for the more restrictive homogeneous structures, we are able to give concrete complexity upper bounds. We show ample applicability of our technique by presenting several concrete examples of homogeneous structures, subsuming, with optimal complexity, known results from the literature. We show that infinitely many such examples of homogeneous structures can be obtained with the classical wreath product construction.
Cite as
Lorenzo Clemente and Slawomir Lasota. Reachability Analysis of First-order Definable Pushdown Systems. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 244-259, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{clemente_et_al:LIPIcs.CSL.2015.244,
author = {Clemente, Lorenzo and Lasota, Slawomir},
title = {{Reachability Analysis of First-order Definable Pushdown Systems}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {244--259},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.244},
URN = {urn:nbn:de:0030-drops-54185},
doi = {10.4230/LIPIcs.CSL.2015.244},
annote = {Keywords: automata theory, pushdown systems, sets with atoms, saturation technique}
}
Document
Relational Semantics of Linear Logic and Higher-order Model Checking
Abstract
In this article, we develop a new and somewhat unexpected connection between higher-order model-checking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any higher-order recursion scheme (HORS) comes together with a dual Church encoding of an alternating tree automata (ATA) of the same signature. Moreover, the interaction between the relational interpretations of the HORS and of the ATA identifies the set of accepting states of the tree automaton against the infinite tree generated by the recursion scheme. We show how to extend this result to alternating parity automata (APT) by introducing a parametric version of the exponential modality of linear logic, capturing the formal properties of colors (or priorities) in higher-order model-checking. We show in particular how to reunderstand in this way the type-theoretic approach to higher-order model-checking developed by Kobayashi and Ong. We briefly explain in the end of the paper how this analysis driven by linear logic results in a new and purely semantic proof of decidability of the formulas of the monadic second-order logic for higher-order recursion schemes.
Cite as
Charles Grellois and Paul-André Melliès. Relational Semantics of Linear Logic and Higher-order Model Checking. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 260-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{grellois_et_al:LIPIcs.CSL.2015.260,
author = {Grellois, Charles and Melli\`{e}s, Paul-Andr\'{e}},
title = {{Relational Semantics of Linear Logic and Higher-order Model Checking}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {260--276},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.260},
URN = {urn:nbn:de:0030-drops-54190},
doi = {10.4230/LIPIcs.CSL.2015.260},
annote = {Keywords: Higher-order model-checking, linear logic, relational semantics, parity games, parametric comonads.}
}
Document
A Van Benthem Theorem for Modal Team Semantics
Abstract
The famous van Benthem theorem states that modal logic corresponds exactly to the fragment of first-order logic that is invariant under bisimulation. In this article we prove an exact analogue of this theorem in the framework of modal dependence logic (MDL) and team semantics. We show that Modal Team Logic (MTL) extending MDL by classical negation captures exactly the FO-definable bisimulation invariant properties of Kripke structures and teams. We also compare the expressive power of MTL to most of the variants and extensions of MDL recently studied in the area.
Cite as
Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. A Van Benthem Theorem for Modal Team Semantics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 277-291, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kontinen_et_al:LIPIcs.CSL.2015.277,
author = {Kontinen, Juha and M\"{u}ller, Julian-Steffen and Schnoor, Henning and Vollmer, Heribert},
title = {{A Van Benthem Theorem for Modal Team Semantics}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {277--291},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.277},
URN = {urn:nbn:de:0030-drops-54206},
doi = {10.4230/LIPIcs.CSL.2015.277},
annote = {Keywords: modal logic, dependence logic, team semantics, expressivity, bisimulation, independence, inclusion, generalized dependence atom}
}
Document
Axiomatizing Propositional Dependence Logics
Abstract
We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi.
Cite as
Katsuhiko Sano and Jonni Virtema. Axiomatizing Propositional Dependence Logics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 292-307, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{sano_et_al:LIPIcs.CSL.2015.292,
author = {Sano, Katsuhiko and Virtema, Jonni},
title = {{Axiomatizing Propositional Dependence Logics}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {292--307},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.292},
URN = {urn:nbn:de:0030-drops-54215},
doi = {10.4230/LIPIcs.CSL.2015.292},
annote = {Keywords: propositional dependence logic, modal dependence logic, axiomatization, tableau calculus}
}
Document
Static Analysis for Logic-based Dynamic Programs
Abstract
The goal of dynamic programs as introduced by Patnaik and Immerman (1994) is to maintain the result of a fixed query for an input database which is subject to tuple insertions and deletions. To this end such programs store an auxiliary database whose relations are updated via first-order formulas upon modifications of the input database. One of those auxiliary relations is supposed to store the answer to the query.
Several static analysis problems can be associated to such dynamic programs. Is the answer relation of a given dynamic program always empty? Does a program actually maintain a query? That is, is the answer given of the program the same when an input database was reached by two different modification sequences? Even more, is the content of auxiliary relations independent of the modification sequence that lead to an input database?
We study the algorithmic properties of those and similar static analysis problems. Since all these problems can easily be seen to be undecidable for full first-order programs, we examine the exact borderline for decidability for restricted programs. Our focus is on restricting the arity of the input databases as well as the auxiliary databases, and to restrict the use of quantifiers.
Cite as
Thomas Schwentick, Nils Vortmeier, and Thomas Zeume. Static Analysis for Logic-based Dynamic Programs. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 308-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{schwentick_et_al:LIPIcs.CSL.2015.308,
author = {Schwentick, Thomas and Vortmeier, Nils and Zeume, Thomas},
title = {{Static Analysis for Logic-based Dynamic Programs}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {308--324},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.308},
URN = {urn:nbn:de:0030-drops-54221},
doi = {10.4230/LIPIcs.CSL.2015.308},
annote = {Keywords: Dynamic descriptive complexity, algorithmic problems, emptiness, history independence, consistency}
}
Document
Sub-classical Boolean Bunched Logics and the Meaning of Par
Abstract
We investigate intermediate logics between the bunched logics Boolean BI and Classical BI, obtained by combining classical propositional logic with various flavours of Hyland and De Paiva's full intuitionistic linear logic. Thus, in addition to the usual multiplicative conjunction (with its adjoint implication and unit), our logics also feature a multiplicative disjunction (with its adjoint co-implication and unit). The multiplicatives behave "sub-classically", in that disjunction and conjunction are related by a weak distribution principle, rather than by De Morgan equivalence.
We formulate a Kripke semantics, covering all our sub-classical bunched logics, in which the multiplicatives are naturally read in terms of resource operations. Our main theoretical result is that validity according to this semantics coincides with provability in a corresponding Hilbert-style proof system.
Our logical investigation sheds considerable new light on how one can understand the multiplicative disjunction, better known as linear logic's "par", in terms of resource operations. In particular, and in contrast to the earlier Classical BI, the models of our logics include the heap-like memory models of separation logic, in which disjunction can be interpreted as a property of intersection operations over heaps.
Cite as
James Brotherston and Jules Villard. Sub-classical Boolean Bunched Logics and the Meaning of Par. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 325-342, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{brotherston_et_al:LIPIcs.CSL.2015.325,
author = {Brotherston, James and Villard, Jules},
title = {{Sub-classical Boolean Bunched Logics and the Meaning of Par}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {325--342},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.325},
URN = {urn:nbn:de:0030-drops-54234},
doi = {10.4230/LIPIcs.CSL.2015.325},
annote = {Keywords: Bunched logic, linear logic, modal logic, Kripke semantics, model theory}
}
Document
Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness
Abstract
Assume that we may prove in Classical Functional Analysis that a primitive recursive relation R is well-founded, using the inductive definition of well-founded. In this paper we prove that such a proof of well-foundation may be made intuitionistic. We conclude that if we are able to formulate any mathematical problem as the inductive well-foundation of some primitive recursive relation, then intuitionistic and classical provability coincide, and for such a statement of well-foundation we may always find an intuitionistic proof if we may find a proof at all.
The core of intuitionism are the methods for computing out data with given properties from input data with given properties: these are the results we are looking for when we do constructive mathematics. Proving that a primitive recursive relation R is inductively well-founded is a more abstract kind of result, but it is crucial as well, because once we proved that R is inductively well-founded, then we may write programs by induction over R. This is the way inductive relation are currently used in intuitionism and in proof assistants based on intuitionism, like Coq.
In the paper we introduce the comprehension axiom for Functional Analysis in the form of introduction and elimination rules for predicates of types Prop, Nat->Prop, ..., in order to use Girard's method of candidates for impredicative arithmetic.
Cite as
Stefano Berardi. Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 343-358, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{berardi:LIPIcs.CSL.2015.343,
author = {Berardi, Stefano},
title = {{Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {343--358},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.343},
URN = {urn:nbn:de:0030-drops-54246},
doi = {10.4230/LIPIcs.CSL.2015.343},
annote = {Keywords: Intuitionism, Inductive Definitions, Proof Theory, impredicativity, omega rule}
}
Document
Functions out of Higher Truncations
Abstract
In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B that are constant on all (n+1)-st loop spaces. We give one "elementary" proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct "set-based" representations of 1-types, as long as they have "braided" loop spaces. The main result with one of its proofs and the application have been formalised in Agda.
Cite as
Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of Higher Truncations. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 359-373, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{capriotti_et_al:LIPIcs.CSL.2015.359,
author = {Capriotti, Paolo and Kraus, Nicolai and Vezzosi, Andrea},
title = {{Functions out of Higher Truncations}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {359--373},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.359},
URN = {urn:nbn:de:0030-drops-54257},
doi = {10.4230/LIPIcs.CSL.2015.359},
annote = {Keywords: homotopy type theory, truncation elimination, constancy on loop spaces}
}
Document
Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes
Abstract
We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. delta x.M) is handled by explicit name-creation and name-destruction brackets (e.g. <delta x M x>) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics.
Cite as
Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan. Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 374-389, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{gabbay_et_al:LIPIcs.CSL.2015.374,
author = {Gabbay, Murdoch J. and Ghica, Dan R. and Petrisan, Daniela},
title = {{Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {374--389},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.374},
URN = {urn:nbn:de:0030-drops-54262},
doi = {10.4230/LIPIcs.CSL.2015.374},
annote = {Keywords: nominal sets, scope, alpha equivalence, dynamic sequences}
}
Document
Rank Logic is Dead, Long Live Rank Logic!
Abstract
Motivated by the search for a logic for polynomial time, we study rank logic (FPR) which extends fixed-point logic with counting (FPC) by operators that determine the rank of matrices over finite fields. While FPR can express most of the known queries that separate FPC from PTIME, nearly nothing was known about the limitations of its expressive power.
In our first main result we show that the extensions of FPC by rank operators over different prime fields are incomparable. This solves an open question posed by Dawar and Holm and also implies that rank logic, in its original definition with a distinct rank operator for every field, fails to capture polynomial time. In particular we show that the variant of rank logic FPR* with an operator that uniformly expresses the matrix rank over finite fields is more expressive than FPR.
One important step in our proof is to consider solvability logic FPS which is the analogous extension of FPC by quantifiers which express the solvability problem for linear equation systems over finite fields. Solvability logic can easily be embedded into rank logic, but it is open whether it is a strict fragment. In our second main result we give a partial answer to this question: in the absence of counting, rank operators are strictly more expressive than solvability quantifiers.
Cite as
Erich Grädel and Wied Pakusa. Rank Logic is Dead, Long Live Rank Logic!. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 390-404, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{gradel_et_al:LIPIcs.CSL.2015.390,
author = {Gr\"{a}del, Erich and Pakusa, Wied},
title = {{Rank Logic is Dead, Long Live Rank Logic!}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {390--404},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.390},
URN = {urn:nbn:de:0030-drops-54279},
doi = {10.4230/LIPIcs.CSL.2015.390},
annote = {Keywords: logic, descriptive complexity, polynomial time, rank logic}
}
Document
Two-Restricted One Context Unification is in Polynomial Time
Abstract
One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.
Cite as
Adrià Gascón, Manfred Schmidt-Schauß, and Ashish Tiwari. Two-Restricted One Context Unification is in Polynomial Time. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 405-422, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{gascon_et_al:LIPIcs.CSL.2015.405,
author = {Gasc\'{o}n, Adri\`{a} and Schmidt-Schau{\ss}, Manfred and Tiwari, Ashish},
title = {{Two-Restricted One Context Unification is in Polynomial Time}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {405--422},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.405},
URN = {urn:nbn:de:0030-drops-54289},
doi = {10.4230/LIPIcs.CSL.2015.405},
annote = {Keywords: context unification, first-order unification, deduction, type checking}
}
Document
Confluence of Layered Rewrite Systems
Abstract
We investigate a new, Turing-complete class of layered systems, whose linearized lefthand sides of rules can only be overlapped at the root position. Layered systems define a natural notion of rank for terms: the maximal number of redexes along a path from the root to a leaf. Overlappings are allowed in finite or infinite trees. Rules may be non-terminating, non-left-linear, or non-right- linear. Using a novel unification technique, cyclic unification, we show that rank non-increasing layered systems are confluent provided their cyclic critical pairs have cyclic-joinable decreasing diagrams.
Cite as
Jiaxiang Liu, Jean-Pierre Jouannaud, and Mizuhito Ogawa. Confluence of Layered Rewrite Systems. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 423-440, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{liu_et_al:LIPIcs.CSL.2015.423,
author = {Liu, Jiaxiang and Jouannaud, Jean-Pierre and Ogawa, Mizuhito},
title = {{Confluence of Layered Rewrite Systems}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {423--440},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.423},
URN = {urn:nbn:de:0030-drops-54293},
doi = {10.4230/LIPIcs.CSL.2015.423},
annote = {Keywords: Layers, confluence, decreasing diagrams, critical pairs, cyclic unification}
}
Document
A Unified Approach to Boundedness Properties in MSO
Abstract
In the past years, extensions of monadic second-order logic (MSO) that can specify boundedness properties by the use of operators referring to the sizes of sets have been considered. In particular, the logics costMSO introduced by T. Colcombet and MSO+U by M. Bojanczyk were analyzed and connections to automaton models have been established to obtain decision procedures for these logics. In this work, we propose the logic quantitative counting MSO (qcMSO for short), which combines aspects from both costMSO and MSO+U. We show that both logics can be embedded into qcMSO in a natural way. Moreover, we provide a decidability proof for the theory of its weak variant (quantification only over finite sets) for the natural numbers with order and the infinite binary tree. These decidability results are obtained using a regular cost function extension of automatic structures called resource-automatic structures.
Cite as
Lukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding. A Unified Approach to Boundedness Properties in MSO. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 441-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kaiser_et_al:LIPIcs.CSL.2015.441,
author = {Kaiser, Lukasz and Lang, Martin and Le{\ss}enich, Simon and L\"{o}ding, Christof},
title = {{A Unified Approach to Boundedness Properties in MSO}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {441--456},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.441},
URN = {urn:nbn:de:0030-drops-54309},
doi = {10.4230/LIPIcs.CSL.2015.441},
annote = {Keywords: quantitative logics, monadic second order logic, boundedness, automatic structures, tree automata}
}
Document
Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction
Abstract
We construct, for any sentence of the modal mu calculus Psi, derived sentences in the modal fragment and the fragment without least fixpoints of the modal mu calculus such that Psi is equivalent to a formula in these fragments if and only if it is equivalent to these formulas. The formula without greatest fixpoints that Psi is equivalent to if and only if it is equivalent to any formula without greatest fixpoint is obtained by duality. This yields a constructive proof of decidability of the first levels of the modal mu alternation hierarchy. The blow-up incurred by turning Psi into the modal formula is shown to be necessary: there are modal formulas that can be expressed sub-exponentially more efficiently with the use of fixpoints. For the fragments with only greatest or least fixpoints however, as long as formulas are in disjunctive form, the transformation into a formula syntactically in these fragments does not increase the size of the formula.
Cite as
Karoliina Lehtinen and Sandra Quickert. Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 457-471, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{lehtinen_et_al:LIPIcs.CSL.2015.457,
author = {Lehtinen, Karoliina and Quickert, Sandra},
title = {{Deciding the First Levels of the Modal mu Alternation Hierarchy by Formula Construction}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {457--471},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.457},
URN = {urn:nbn:de:0030-drops-54316},
doi = {10.4230/LIPIcs.CSL.2015.457},
annote = {Keywords: modal mu calculus, fixpoint logic, alternation hierarchy}
}
Document
Infinite and Bi-infinite Words with Decidable Monadic Theories
Abstract
We study word structures of the form (D,<=,P) where D is either N or Z, <= is a linear ordering on D and P in D is a predicate on D. In particular we show:
(a) The set of recursive omega-words with decidable monadic second order theories is Sigma_3-complete.
(b) We characterise those sets P subset of Z that yield bi-infinite words (Z,<=,P) with decidable monadic second order theories.
(c) We show that such "tame" predicates P exist in every Turing degree.
(d) We determine, for P subset of Z, the number of predicates Q subset of Z such that (Z,<=,P) and (Z,<=,Q) are indistinguishable.
Through these results we demonstrate similarities and differences between logical properties of infinite and bi-infinite words.
Cite as
Dietrich Kuske, Jiamou Liu, and Anastasia Moskvina. Infinite and Bi-infinite Words with Decidable Monadic Theories. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 472-486, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kuske_et_al:LIPIcs.CSL.2015.472,
author = {Kuske, Dietrich and Liu, Jiamou and Moskvina, Anastasia},
title = {{Infinite and Bi-infinite Words with Decidable Monadic Theories}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {472--486},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.472},
URN = {urn:nbn:de:0030-drops-54325},
doi = {10.4230/LIPIcs.CSL.2015.472},
annote = {Keywords: infinite words, bi-infinite words, monadic second order logic}
}
Document
A Coalgebraic Decision Procedure for WS1S
Abstract
Weak monadic second-order logic of one successor (WS1S) is a simple and natural formalism to specify regular properties. WS1S is decidable, although the decision procedure's complexity is non-elementary. Typically, decision procedures for WS1S exploit the logic-automaton connection, i.e. they escape the simple and natural formalism by translating formulas into equally expressive regular structures such as finite automata, regular expressions, or games. In this work, we devise a coalgebraic decision procedure for WS1S that stays within the logical world by directly operating on formulas. The key operation is the derivative of a formula, modeled after Brzozowski's derivatives of regular expressions. The presented decision procedure has been formalized and proved correct in the interactive proof assistant Isabelle.
Cite as
Dmitriy Traytel. A Coalgebraic Decision Procedure for WS1S. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 487-503, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{traytel:LIPIcs.CSL.2015.487,
author = {Traytel, Dmitriy},
title = {{A Coalgebraic Decision Procedure for WS1S}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {487--503},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.487},
URN = {urn:nbn:de:0030-drops-54335},
doi = {10.4230/LIPIcs.CSL.2015.487},
annote = {Keywords: WS1S, decision procedure, coalgebra, Brzozowski derivatives, Isabelle}
}
Document
Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability
Abstract
We study n-player turn-based games played on a finite directed graph. For each play, the players have to pay a cost that they want to minimize. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. We also study natural variants of SPE, named weak (resp. very weak) SPE, where players who deviate cannot use the full class of strategies but only a subclass with a finite number of (resp. a unique) deviation step(s).
Our results are threefold. Firstly, we characterize in the form of a Folk theorem the set of all plays that are the outcome of a weak SPE. Secondly, for the class of quantitative reachability games, we prove the existence of a finite-memory SPE and provide an algorithm for computing it (only existence was known with no information regarding the memory). Moreover, we show that the existence of a constrained SPE, i.e. an SPE such that each player pays a cost less than a given constant, can be decided. The proofs rely on our Folk theorem for weak SPEs (which coincide with SPEs in the case of quantitative reachability games) and on the decidability of MSO logic on infinite words. Finally with similar techniques, we provide a second general class of games for which the existence of a (constrained) weak SPE is decidable.
Cite as
Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-Francois Raskin. Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 504-518, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{brihaye_et_al:LIPIcs.CSL.2015.504,
author = {Brihaye, Thomas and Bruy\`{e}re, V\'{e}ronique and Meunier, No\'{e}mie and Raskin, Jean-Francois},
title = {{Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {504--518},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.504},
URN = {urn:nbn:de:0030-drops-54345},
doi = {10.4230/LIPIcs.CSL.2015.504},
annote = {Keywords: multi-player games on graphs, quantitative objectives, Nash equilibrium, subgame perfect equilibrium, quantitative reachability}
}
Document
What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead
Abstract
We investigate determinacy of delay games with Borel winning conditions, infinite-duration two-player games in which one player may delay her moves to obtain a lookahead on her opponent's moves.
First, we prove determinacy of such games with respect to a fixed evolution of the lookahead. However, strategies in such games may depend on information about the evolution. Thus, we introduce different notions of universal strategies for both players, which are evolution-independent, and determine the exact amount of information a universal strategy needs about the history of a play and the evolution of the lookahead to be winning. In particular, we show that delay games with Borel winning conditions are determined with respect to universal strategies. Finally, we consider decidability problems, e.g., "Does a player have a universal winning strategy for delay games with a given winning condition?", for omega-regular and omega-context-free winning conditions.
Cite as
Felix Klein and Martin Zimmermann. What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 519-533, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{klein_et_al:LIPIcs.CSL.2015.519,
author = {Klein, Felix and Zimmermann, Martin},
title = {{What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {519--533},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.519},
URN = {urn:nbn:de:0030-drops-54354},
doi = {10.4230/LIPIcs.CSL.2015.519},
annote = {Keywords: Determinacy, Infinite Games, Delay Games, Borel Hierarchy}
}
Document
On Unambiguous Regular Tree Languages of Index (0,2)
Abstract
Unambiguous automata are usually seen as a natural class of automata in-between deterministic and nondeterministic ones. We show that in case of infinite tree languages, the unambiguous ones are topologically far more complicated than the deterministic ones. We do so by providing operations that generate a family (A_{alpha})_{alpha < phi_2(0)} of unambiguous automata such that:
1. It respects the strict Wadge ordering: alpha < beta if and only if A_{alpha} <_W A_{beta}. This can be established without the help of any determinacy principle, simply by providing effective winning strategies in the underlying games.
2. Its length (phi_2(0)) is the first fixpoint of the ordinal function that itself enumerates all fixpoints of the ordinal exponentiation x |-> omega^x: an ordinal tremendously larger than (omega^(omega))^3 +3 which is the height of the Wadge hierarchy of deterministic tree languages as uncovered by Filip Murlak.
3. The priorities of all these parity automata only range from 0 to 2.
Cite as
Jacques Duparc, Kevin Fournier, and Szczepan Hummel. On Unambiguous Regular Tree Languages of Index (0,2). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 534-548, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{duparc_et_al:LIPIcs.CSL.2015.534,
author = {Duparc, Jacques and Fournier, Kevin and Hummel, Szczepan},
title = {{On Unambiguous Regular Tree Languages of Index (0,2)}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {534--548},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.534},
URN = {urn:nbn:de:0030-drops-54369},
doi = {10.4230/LIPIcs.CSL.2015.534},
annote = {Keywords: Tree Automata, Unambiguity, Wadge Hierarchy.}
}
Document
Least and Greatest Fixed Points in Ludics
Abstract
Various logics have been introduced in order to reason over (co)inductive specifications and, through the Curry-Howard correspondence, to study computation over inductive and coinductive data. The logic mu-MALL is one of those logics, extending multiplicative and additive linear logic with least and greatest fixed point operators.
In this paper, we investigate the semantics of mu-MALL proofs in (computational) ludics. This framework is built around the notion of design, which can be seen as an analogue of the strategies of game semantics. The infinitary nature of designs makes them particularly well suited for representing computations over infinite data.
We provide mu-MALL with a denotational semantics, interpreting proofs by designs and formulas by particular sets of designs called behaviours. Then we prove a completeness result for the class of "essentially finite designs", which are those designs performing a finite computation followed by a copycat. On the way to completeness, we investigate semantic inclusion, proving its decidability (given two formulas, we can decide whether the semantics of one is included in the other's) and completeness (if semantic inclusion holds, the corresponding implication is provable in mu-MALL).
Cite as
David Baelde, Amina Doumane, and Alexis Saurin. Least and Greatest Fixed Points in Ludics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 549-566, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{baelde_et_al:LIPIcs.CSL.2015.549,
author = {Baelde, David and Doumane, Amina and Saurin, Alexis},
title = {{Least and Greatest Fixed Points in Ludics}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {549--566},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.549},
URN = {urn:nbn:de:0030-drops-54374},
doi = {10.4230/LIPIcs.CSL.2015.549},
annote = {Keywords: proof theory, fixed points, linear logic, ludics, game semantics, completeness, circular proofs, infinitary proof systems}
}
Document
Modelling Coeffects in the Relational Semantics of Linear Logic
Abstract
Various typing system have been recently introduced giving a parametric version of the exponential modality of linear logic. The parameters are taken from a semi-ring, and allow to express coeffects - i.e. specific requirements of a program with respect to the environment (availability of a resource, some prerequisite of the input, etc.).
We show that all these systems can be interpreted in the relational category (Rel) of sets and relations. This is possible because of the notion of multiplicity semi-ring and allowing a great variety of exponential comonads in Rel. The interpretation of a particular typing system corresponds then to give a suitable notion of stratification of the exponential comonad associated with the semi-ring parametrising the exponential modality.
Cite as
Flavien Breuvart and Michele Pagani. Modelling Coeffects in the Relational Semantics of Linear Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 567-581, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{breuvart_et_al:LIPIcs.CSL.2015.567,
author = {Breuvart, Flavien and Pagani, Michele},
title = {{Modelling Coeffects in the Relational Semantics of Linear Logic}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {567--581},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.567},
URN = {urn:nbn:de:0030-drops-54384},
doi = {10.4230/LIPIcs.CSL.2015.567},
annote = {Keywords: relational semantics, bounded linear logic, lambda calculus}
}
Document
On Classical PCF, Linear Logic and the MIX Rule
Abstract
We study a classical version of PCF from a semantical point of view. We define a general notion of model based on categorical models of Linear Logic, in the spirit of earlier work by Girard, Regnier and Laurent. We give a concrete example based on the relational model of Linear Logic, that we present as a non-idempotents intersection type system, and we prove an Adequacy Theorem using ideas introduced by Krivine. Following Danos and Krivine, we also consider an extension of this language with a MIX construction introducing a form of must non-determinism; in this language, a program of type integer can have more than one value (or no value at all, raising an error). We propose a refinement of the relational model of classical PCF in which programs of type integer are single valued; this model rejects the MIX syntactical constructs (and the MIX rule of Linear Logic).
Cite as
Shahin Amini and Thomas Erhard. On Classical PCF, Linear Logic and the MIX Rule. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 582-596, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{amini_et_al:LIPIcs.CSL.2015.582,
author = {Amini, Shahin and Erhard, Thomas},
title = {{On Classical PCF, Linear Logic and the MIX Rule}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {582--596},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.582},
URN = {urn:nbn:de:0030-drops-54402},
doi = {10.4230/LIPIcs.CSL.2015.582},
annote = {Keywords: lambda-calculus, linear logic, classical logic, denotational semantics}
}
Document
Uniform One-Dimensional Fragments with One Equivalence Relation
Abstract
The uniform one-dimensional fragment U1 of first-order logic was introduced recently as a natural generalization of the two-variable fragment FO2 to contexts with relation symbols of all arities. It was shown that U1 has the exponential model property and NEXPTIME-complete satisfiability problem. In this paper we investigate two restrictions of U1 that still contain FO2. We call these logics RU1 and SU1, or the restricted and strongly restricted uniform one-dimensional fragments. We introduce Ehrenfeucht-Fraisse games for the logics and prove that while SU1 and RU1 are expressively equivalent, they are strictly contained in U1. Furthermore, we consider extensions of the logics SU1, RU1 and U1 with unrestricted use of a single built-in equivalence relation E. We prove that while all the obtained systems retain the finite model property, their complexities differ. Namely, the satisfiability problem is NEXPTIME-complete for SU1(E) and 2NEXPTIME-complete for both RU1(E) and U1(E). Finally, we show undecidability of some natural extensions of SU1.
Cite as
Emanuel Kierónski and Antti Kuusisto. Uniform One-Dimensional Fragments with One Equivalence Relation. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 597-615, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kieronski_et_al:LIPIcs.CSL.2015.597,
author = {Kier\'{o}nski, Emanuel and Kuusisto, Antti},
title = {{Uniform One-Dimensional Fragments with One Equivalence Relation}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {597--615},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.597},
URN = {urn:nbn:de:0030-drops-54418},
doi = {10.4230/LIPIcs.CSL.2015.597},
annote = {Keywords: two-variable logic, uniform one-dimensional fragments, complexity, expressivity, equivalence relations}
}
Document
Finite-Degree Predicates and Two-Variable First-Order Logic
Abstract
We consider two-variable first-order logic on finite words with a fixed number of quantifier alternations. We show that all languages with a neutral letter definable using the order and finite-degree predicates are also definable with the order predicate only. From this result we derive the separation of the alternation hierarchy of two-variable logic on this signature. Replacing finite-degree by arbitrary numerical predicates in the statement would entail a long standing conjecture on the circuit complexity of the addition function. Thus, this result can be viewed as a uniform version of this circuit lower bound.
Cite as
Charles Paperman. Finite-Degree Predicates and Two-Variable First-Order Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 616-630, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{paperman:LIPIcs.CSL.2015.616,
author = {Paperman, Charles},
title = {{Finite-Degree Predicates and Two-Variable First-Order Logic}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {616--630},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.616},
URN = {urn:nbn:de:0030-drops-54420},
doi = {10.4230/LIPIcs.CSL.2015.616},
annote = {Keywords: First order logic, automata theory, semigroup, modular predicates}
}
Document
Two-variable Logic with Counting and a Linear Order
Abstract
We study the finite satisfiability problem for the two-variable fragment of the first-order logic extended with counting quantifiers (C2) and interpreted over linearly ordered structures. We show that the problem is undecidable in the case of two linear orders (in presence of two other binary symbols). In the case of one linear order it is NEXPTIME-complete, even in presence of the successor relation. Surprisingly, the complexity of the problem explodes when we add one binary symbol more: C2 with one linear order and its successor, in presence of other binary predicate symbols, is decidable, but it is as expressive (and as complex) as Vector Addition Systems.
Cite as
Witold Charatonik and Piotr Witkowski. Two-variable Logic with Counting and a Linear Order. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 631-647, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{charatonik_et_al:LIPIcs.CSL.2015.631,
author = {Charatonik, Witold and Witkowski, Piotr},
title = {{Two-variable Logic with Counting and a Linear Order}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {631--647},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.631},
URN = {urn:nbn:de:0030-drops-54436},
doi = {10.4230/LIPIcs.CSL.2015.631},
annote = {Keywords: Two-variable logic, counting quantifiers, linear order, satisfiability, complexity}
}
Document
Binding Forms in First-Order Logic
Abstract
Aiming to pinpoint the reasons behind the decidability of some complex extensions of modal logic, we propose a new classification criterion for sentences of first-order logic, which is based on the kind of binding forms admitted in their expressions, i.e., on the way the arguments of a relation can be bound to a variable. In particular, we describe a hierarchy of four fragments focused on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with several first-order limitations proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel model-theoretic technique, that our logic enjoys the finite-model property, Craig's interpolation, and Beth's definability. Furthermore, the associated model-checking and satisfiability problems are solvable in PTime and Sigma_3^P, respectively.
Cite as
Fabio Mogavero and Giuseppe Perelli. Binding Forms in First-Order Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 648-665, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{mogavero_et_al:LIPIcs.CSL.2015.648,
author = {Mogavero, Fabio and Perelli, Giuseppe},
title = {{Binding Forms in First-Order Logic}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {648--665},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Kreutzer, Stephan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.648},
URN = {urn:nbn:de:0030-drops-54443},
doi = {10.4230/LIPIcs.CSL.2015.648},
annote = {Keywords: First-Order Logic, Decidable Fragments, Satisfiability, Model Checking}
}