Volume
LIPIcs, Volume 12
Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2011, September 12-15, 2011, Bergen, NorwayEditor
Publication Details
- published at: 2011-08-31
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-32-3
- DBLP: db/conf/csl/csl2011
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 12, CSL'11, Complete Volume
Abstract
LIPIcs, Volume 12, CSL'11, Complete Volume
Cite as
Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
Copy BibTex To Clipboard
@Proceedings{bezem:LIPIcs.CSL.2011,
title = {{LIPIcs, Volume 12, CSL'11, Complete Volume}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2013},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011},
URN = {urn:nbn:de:0030-drops-41066},
doi = {10.4230/LIPIcs.CSL.2011},
annote = {Keywords: Conference Proceedings; Software; Theory of Computation; Graph Theory; Probability and Statistics; Artificial Intelligence}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Conference Organization
Abstract
Frontmatter, Table of Contents, Preface, Conference Organization
Cite as
Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. i-xix, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{bezem:LIPIcs.CSL.2011.i,
author = {Bezem, Marc},
title = {{Frontmatter, Table of Contents, Preface, Conference Organization}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {i--xix},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.i},
URN = {urn:nbn:de:0030-drops-32144},
doi = {10.4230/LIPIcs.CSL.2011.i},
annote = {Keywords: Frontmatter, Table of Contents, Preface, Conference Organization}
}
Document
Resource Lambda-Calculus: the Differential Viewpoint
Abstract
We present differential linear logic and its models, the associated resource and differential lambda-calculi, and the Taylor expansion of promotion boxes. We also describe an antiderivative which seems to be available in many models of differential Linear Logic, and we present a very simple categorical axiom for this operation.
Cite as
Thomas Ehrhard. Resource Lambda-Calculus: the Differential Viewpoint. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{ehrhard:LIPIcs.CSL.2011.1,
author = {Ehrhard, Thomas},
title = {{Resource Lambda-Calculus: the Differential Viewpoint}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {1--1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.1},
URN = {urn:nbn:de:0030-drops-32152},
doi = {10.4230/LIPIcs.CSL.2011.1},
annote = {Keywords: proof theory, lambda-calculus, linear logic, denotational semantics}
}
Document
The Freedoms of Guarded Bisimulation
Abstract
Guarded logics have been shown to be amazingly versatile and tractable
logics since their inception by Andréka, van Benthem, Németi.
Results to be surveyed include finite and small model properties,
decidability results, complexity and expressive completeness issues,
and guarded bisimulations.
Cite as
Martin Otto. The Freedoms of Guarded Bisimulation. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, p. 2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{otto:LIPIcs.CSL.2011.2,
author = {Otto, Martin},
title = {{The Freedoms of Guarded Bisimulation}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {2--2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.2},
URN = {urn:nbn:de:0030-drops-32163},
doi = {10.4230/LIPIcs.CSL.2011.2},
annote = {Keywords: model theory, guarded logic, bisimulation, hypergraphs}
}
Document
Branching vs. Linear Time: Semantical Perspective
Abstract
The discussion of the relative merits of linear- versus
branching-time frameworks goes back to the early 1980s.
We revisit here this issue from a fresh perspective and postulate three
principles that we view as fundamental to any discussion of process
equivalence. We show that our principles yield a unique notion of
process equivalence, which is trace based, rather than tree based.
Cite as
Moshe Y. Vardi. Branching vs. Linear Time: Semantical Perspective. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, p. 3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{vardi:LIPIcs.CSL.2011.3,
author = {Vardi, Moshe Y.},
title = {{Branching vs. Linear Time: Semantical Perspective}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {3--3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.3},
URN = {urn:nbn:de:0030-drops-32173},
doi = {10.4230/LIPIcs.CSL.2011.3},
annote = {Keywords: linear time, branching time, process equivalence, contextual equivalence}
}
Document
Ontology-Based Data Access and Constraint Satisfaction
Abstract
We present first results on the relationship between ontology-based data access using description logics and constraint satisfaction problems.
Cite as
Frank Wolter. Ontology-Based Data Access and Constraint Satisfaction. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, p. 4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{wolter:LIPIcs.CSL.2011.4,
author = {Wolter, Frank},
title = {{Ontology-Based Data Access and Constraint Satisfaction}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {4--4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.4},
URN = {urn:nbn:de:0030-drops-32186},
doi = {10.4230/LIPIcs.CSL.2011.4},
annote = {Keywords: description logic, constraint satisfaction, conjunctive query}
}
Document
Power-Set Functors and Saturated Trees
Abstract
We combine ideas coming from several fields, including modal logic, coalgebra, and set theory. Modally saturated trees were introduced by K. Fine in 1975. We give a new purely combinatorial formulation of modally saturated trees, and we prove that they form the limit of the final omega-op-chain of the finite power-set functor Pf. From that, we derive an alternative proof of J. Worrell's description of the final coalgebra as the coalgebra of all strongly extensional, finitely branching trees. In the other direction, we represent the final coalgebra for Pf in terms of certain maximal consistent sets in the modal logic K. We also generalize Worrell's result to M-labeled trees for a commutative monoid M, yielding a final coalgebra for the corresponding functor Mf studied by H. P. Gumm and T. Schröder. We introduce the concept of an i-saturated tree for all ordinals i, and then prove that the i-th step in the final chain of the power set functor consists of all i-saturated trees. This leads to a new description of the final coalgebra for the restricted power-set functors Plambda (of subsets of cardinality smaller than lambda).
Cite as
Jiri Adamek, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. Power-Set Functors and Saturated Trees. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 5-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{adamek_et_al:LIPIcs.CSL.2011.5,
author = {Adamek, Jiri and Milius, Stefan and Moss, Lawrence S. and Sousa, Lurdes},
title = {{Power-Set Functors and Saturated Trees}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {5--19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.5},
URN = {urn:nbn:de:0030-drops-32194},
doi = {10.4230/LIPIcs.CSL.2011.5},
annote = {Keywords: saturated tree, extensional tree, final coalgebra, power-set functor, modal logic}
}
Document
Transfinite Update Procedures for Predicative Systems of Analysis
Abstract
We present a simple-to-state, abstract computational problem, whose solution implies the 1-consistency of various systems of predicative Analysis and offers a way of extracting witnesses from classical proofs. In order to state the problem, we formulate the concept of transfinite update procedure, which extends Avigad's notion of update procedure to the transfinite and can be seen as an axiomatization of learning as it implicitly appears in various computational interpretations of predicative Analysis. We give iterative and bar recursive solutions to the problem.
Cite as
Federico Aschieri. Transfinite Update Procedures for Predicative Systems of Analysis. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 20-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{aschieri:LIPIcs.CSL.2011.20,
author = {Aschieri, Federico},
title = {{Transfinite Update Procedures for Predicative Systems of Analysis}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {20--34},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.20},
URN = {urn:nbn:de:0030-drops-32200},
doi = {10.4230/LIPIcs.CSL.2011.20},
annote = {Keywords: update procedure, epsilon substitution method, predicative classical analysis, bar recursion}
}
Document
A Non-Standard Semantics for Kahn Networks in Continuous Time
Abstract
In a seminal article, Kahn has introduced the notion of process network and given a semantics for those using Scott domains whose elements are (possibly infinite) sequences of values. This model has since then become a standard tool for studying distributed asynchronous computations. From the beginning, process networks have been drawn as particular graphs, but this syntax is never formalized. We take the opportunity to clarify it by giving a precise definition of these graphs, that we call nets. The resulting category is shown to be a fixpoint category, i.e. a cartesian category which is traced wrt the monoidal structure given by the product, and interestingly this structure characterizes the category: we show that it is the free fixpoint category containing a given set of morphisms, thus providing a complete axiomatics that models of process networks should satisfy. We then use these tools to build a model of networks in which data vary over a continuous time, in order to elaborate on the idea that process networks should also be able to encompass computational models such as hybrid systems or electric circuits. We relate this model to Kahn's semantics by introducing a third model of networks based on non-standard analysis, whose elements form an internal complete partial order for which many properties of standard domains can be reformulated. The use of hyperreals in this model allows it to formally consider the notion of infinitesimal, and thus to make a bridge between discrete and continuous time: time is "discrete", but the duration between two instants is infinitesimal. Finally, we give some examples of uses of the model by describing some networks implementing common constructions in analysis.
Cite as
Romain Beauxis and Samuel Mimram. A Non-Standard Semantics for Kahn Networks in Continuous Time. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 35-50, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{beauxis_et_al:LIPIcs.CSL.2011.35,
author = {Beauxis, Romain and Mimram, Samuel},
title = {{A Non-Standard Semantics for Kahn Networks in Continuous Time}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {35--50},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.35},
URN = {urn:nbn:de:0030-drops-32212},
doi = {10.4230/LIPIcs.CSL.2011.35},
annote = {Keywords: Kahn network, non-standard analysis, fixpoint category, internal cpo}
}
Document
Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism
Abstract
This paper revisits models of typed lambda calculus based on filters of intersection types:
By using non-idempotent intersections, we simplify a methodology that produces modular proofs of strong normalisation based on filter models. Building such a model for some type theory shows that typed terms can be typed with intersections only, and are therefore strongly normalising. Non-idempotent intersections provide a decreasing measure proving a key termination property, simpler than the reducibility techniques used with idempotent intersections.
Such filter models are shown to be captured by orthogonality techniques: we formalise an abstract notion of orthogonality model inspired by classical realisability, and express a filter model as one of its instances, along with two term-models (one of which captures a now common technique for strong normalisation).
Applying the above range of model constructions to Curry-style System F describes at different levels of detail how the infinite polymorphism of System F can systematically be reduced to the finite polymorphism of intersection types.
Cite as
Alexis Bernadet and Stéphane Lengrand. Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 51-66, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{bernadet_et_al:LIPIcs.CSL.2011.51,
author = {Bernadet, Alexis and Lengrand, St\'{e}phane},
title = {{Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {51--66},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.51},
URN = {urn:nbn:de:0030-drops-32226},
doi = {10.4230/LIPIcs.CSL.2011.51},
annote = {Keywords: non-idempotent intersections, System F, realisability}
}
Document
Algebraic Characterization of FO for Scattered Linear Orderings
Abstract
We prove that for the class of sets of words indexed by countable scattered linear orderings, there is an equivalence between definability in first-order logic, star-free expressions with marked product, and recognizability by finite aperiodic semigroups which satisfy some additional equation.
Cite as
Alexis Bès and Olivier Carton. Algebraic Characterization of FO for Scattered Linear Orderings. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 67-81, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{bes_et_al:LIPIcs.CSL.2011.67,
author = {B\`{e}s, Alexis and Carton, Olivier},
title = {{Algebraic Characterization of FO for Scattered Linear Orderings}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {67--81},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.67},
URN = {urn:nbn:de:0030-drops-32233},
doi = {10.4230/LIPIcs.CSL.2011.67},
annote = {Keywords: linear orderings, first-order logic, semigroups, rational sets}
}
Document
Determinizing Discounted-Sum Automata
Abstract
A discounted-sum automaton (NDA) is a nondeterministic finite automaton with edge weights, which values a run by the discounted sum of visited edge weights. More precisely, the weight in the i-th position of the run is divided by lambda^i, where the discount factor lambda is a fixed rational number greater than 1. Discounted summation is a common and useful measuring scheme, especially for infinite sequences, which reflects the assumption that earlier weights are more important than later weights. Determinizing automata is often essential, for example, in formal verification, where there are polynomial algorithms for comparing two deterministic NDAs, while the equivalence problem for NDAs is not known to be decidable.
Unfortunately, however, discounted-sum automata are, in general, not determinizable: it is currently known that for every rational discount factor 1 < lambda < 2, there is an NDA
with lambda (denoted lambda-NDA) that cannot be determinized.
We provide positive news, showing that every NDA with an integral factor is determinizable. We also complete the picture by proving that the integers characterize exactly the discount factors that guarantee determinizability: we show that for every non-integral rational factor lambda, there is a nondeterminizable lambda-NDA.
Finally, we prove that the class of NDAs with integral discount factors enjoys closure under the algebraic operations min, max, addition, and subtraction, which is not the case for general NDAs nor for deterministic NDAs. This shows that for integral discount factors, the class of NDAs forms an attractive specification formalism in quantitative formal verification. All our results hold equally for automata over finite words and for automata over infinite words.
Cite as
Udi Boker and Thomas A. Henzinger. Determinizing Discounted-Sum Automata. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 82-96, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{boker_et_al:LIPIcs.CSL.2011.82,
author = {Boker, Udi and Henzinger, Thomas A.},
title = {{Determinizing Discounted-Sum Automata}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {82--96},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.82},
URN = {urn:nbn:de:0030-drops-32243},
doi = {10.4230/LIPIcs.CSL.2011.82},
annote = {Keywords: Discounted-sum automata, determinization, quantitative verification}
}
Document
Full Abstraction for Resource Calculus with Tests
Abstract
We study the semantics of a resource sensitive extension of the lambda-calculus in a canonical reflexive object of a category of sets and relations, a relational version of the original Scott D infinity model of the pure lambda-calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda-calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a ``must'' parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda-calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula.
Cite as
Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full Abstraction for Resource Calculus with Tests. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 97-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{bucciarelli_et_al:LIPIcs.CSL.2011.97,
author = {Bucciarelli, Antonio and Carraro, Alberto and Ehrhard, Thomas and Manzonetto, Giulio},
title = {{Full Abstraction for Resource Calculus with Tests}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {97--111},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.97},
URN = {urn:nbn:de:0030-drops-32250},
doi = {10.4230/LIPIcs.CSL.2011.97},
annote = {Keywords: resource lambda calculus, relational semantics, full abstraction, differential linear logic}
}
Document
Tight Upper Bounds for Streett and Parity Complementation
Abstract
Complementation of finite automata on infinite words is not only a fundamental problem in automata theory, but also serves as a cornerstone for solving numerous decision problems in mathematical logic, model-checking, program analysis and verification. For Streett complementation, a significant gap exists between the current lower bound 2^{Omega(n*log(n*k))} and upper bound 2^{O(n*k*log(n*k))}, where n is the state size, k is the number of Streett pairs, and k can be as large as 2^{n}. Determining the complexity of Streett complementation has been an open question since the late 80's. In this paper we show a complementation construction with upper bound 2^{O(n*log(n)+n*k*log(k))} for k=O(n) and 2^{O(n^{2}*log(n))} for k=Omega(n), which matches well the lower bound obtained in the paper arXiv:1102.2963. We also obtain a tight upper bound 2^{O(n*log(n))} for parity complementation.
Cite as
Yang Cai and Ting Zhang. Tight Upper Bounds for Streett and Parity Complementation. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 112-128, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{cai_et_al:LIPIcs.CSL.2011.112,
author = {Cai, Yang and Zhang, Ting},
title = {{Tight Upper Bounds for Streett and Parity Complementation}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {112--128},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.112},
URN = {urn:nbn:de:0030-drops-32269},
doi = {10.4230/LIPIcs.CSL.2011.112},
annote = {Keywords: Streett automata, omega-automata, parity automata, complementation, upper bounds}
}
Document
A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics
Abstract
We present a decision procedure for a quantified fragment of
set theory involving ordered pairs and some operators to manipulate them. When our decision procedure is applied to formulae in this fragment whose quantifier prefixes have length bounded by a fixed constant, it runs in nondeterministic polynomial-time.
Related to this fragment, we also introduce a description logic which
provides an unusually large set of constructs, such as, for instance,
Boolean constructs among roles. The set-theoretic nature of the description logics semantics yields a straightforward reduction of the
knowledge base consistency problem to the satisfiability problem for formulae of our fragment with quantifier prefixes of length at most 2, from which the NP-completeness of reasoning in this novel description logic follows. Finally, we extend this reduction to cope also with SWRL rules.
Cite as
Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo. A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 129-143, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{cantone_et_al:LIPIcs.CSL.2011.129,
author = {Cantone, Domenico and Longo, Cristiano and Nicolosi Asmundo, Marianna},
title = {{A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {129--143},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.129},
URN = {urn:nbn:de:0030-drops-32278},
doi = {10.4230/LIPIcs.CSL.2011.129},
annote = {Keywords: NP-complete decision procedures, set theory, description logic}
}
Document
Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas
Abstract
Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-space and continuous-time labelled Markov processes (CMPs). The modalities of CML approximate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions. In this paper we present a sound and complete Hilbert-style axiomatization of CML for the CMP-semantics and prove some metaproperties including the small model property. CML characterizes stochastic bisimulation and supports the definition of a quantified extension of satisfiability relation that measures the compatibility of a model and a property. Relying on the small model property, we prove that this measure can be approximated, within a given error, by using a distance between logical formulas.
Cite as
Luca Cardelli, Kim G. Larsen, and Radu Mardare. Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 144-158, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{cardelli_et_al:LIPIcs.CSL.2011.144,
author = {Cardelli, Luca and Larsen, Kim G. and Mardare, Radu},
title = {{Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {144--158},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.144},
URN = {urn:nbn:de:0030-drops-32281},
doi = {10.4230/LIPIcs.CSL.2011.144},
annote = {Keywords: probabilistic logic, axiomatization, Markov processes, metric semantics}
}
Document
The Focused Calculus of Structures
Abstract
The focusing theorem identifies a complete class of sequent proofs that have no inessential non-deterministic choices and restrict the essential choices to a particular normal form. Focused proofs are therefore well suited both for the search and for the representation of sequent proofs. The calculus of structures is a proof formalism that allows rules to be applied deep inside a formula. Through this freedom it can be used to give analytic proof systems for a wider variety of logics than the sequent calculus, but standard presentations of this calculus are too permissive, allowing too many proofs. In order to make it more amenable to proof search, we transplant the focusing theorem from the sequent calculus to the calculus of structures. The key technical contribution is an incremental treatment of focusing that avoids trivializing the calculus of structures. We give a direct inductive proof of the completeness of the focused calculus of structures with respect to a more standard unfocused form. We also show that any focused sequent proof can be represented in the focused calculus of structures, and, conversely, any proof in the focused calculus of structures corresponds to a focused sequent proof.
Cite as
Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The Focused Calculus of Structures. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 159-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{chaudhuri_et_al:LIPIcs.CSL.2011.159,
author = {Chaudhuri, Kaustuv and Guenot, Nicolas and Stra{\ss}burger, Lutz},
title = {{The Focused Calculus of Structures}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {159--173},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.159},
URN = {urn:nbn:de:0030-drops-32297},
doi = {10.4230/LIPIcs.CSL.2011.159},
annote = {Keywords: focusing, polarity, calculus of structures, linear logic}
}
Document
A Semantic Approach to Illative Combinatory Logic
Abstract
This work introduces the theory of illative combinatory algebras,
which is closely related to systems of illative combinatory logic. We
thus provide a semantic interpretation for a formal framework in which
both logic and computation may be expressed in a unified
manner. Systems of illative combinatory logic consist of combinatory
logic extended with constants and rules of inference intended to
capture logical notions. Our theory does not correspond strictly to
any traditional system, but draws inspiration from many. It differs
from them in that it couples the notion of truth with the notion of
equality between terms, which enables the use of logical formulas in
conditional expressions. We give a consistency proof for first-order
illative combinatory algebras. A complete embedding of classical
predicate logic into our theory is also provided. The translation is
very direct and natural.
Cite as
Lukasz Czajka. A Semantic Approach to Illative Combinatory Logic. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 174-188, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{czajka:LIPIcs.CSL.2011.174,
author = {Czajka, Lukasz},
title = {{A Semantic Approach to Illative Combinatory Logic}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {174--188},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.174},
URN = {urn:nbn:de:0030-drops-32303},
doi = {10.4230/LIPIcs.CSL.2011.174},
annote = {Keywords: illative combinatory logic, term rewriting, first-order logic}
}
Document
Enumeration Complexity of Logical Query Problems with Second-order Variables
Abstract
We consider query problems defined by first order formulas of the form F(x,T) with free first order and second order variables and study the data complexity of enumerating results of such queries. By considering the number of alternations in the quantifier prefixes of formulas, we show that such query problems either admit a constant delay or a polynomial delay enumeration algorithm or are hard to enumerate.
We also exhibit syntactically defined fragments inside the hard cases that still admit good enumeration algorithms and discuss the case of some restricted classes of database structures as inputs.
Cite as
Arnaud Durand and Yann Strozecki. Enumeration Complexity of Logical Query Problems with Second-order Variables. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 189-202, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{durand_et_al:LIPIcs.CSL.2011.189,
author = {Durand, Arnaud and Strozecki, Yann},
title = {{Enumeration Complexity of Logical Query Problems with Second-order Variables}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {189--202},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.189},
URN = {urn:nbn:de:0030-drops-32313},
doi = {10.4230/LIPIcs.CSL.2011.189},
annote = {Keywords: descriptive complexity, enumeration, query problem}
}
Document
On Constraint Satisfaction Problems below P*
Abstract
Symmetric Datalog, a fragment of the logic programming language Datalog, is conjectured to capture all constraint satisfaction problems (CSP) in L. Therefore developing tools that help us understand whether or not a CSP can be defined in symmetric Datalog is an important task. It is widely known that a CSP is definable in Datalog and linear Datalog iff that CSP has bounded treewidth and bounded pathwidth duality, respectively. In the case of symmetric Datalog, Bulatov, Krokhin and Larose ask for such a duality [2008]. We provide two such dualities, and give applications. In particular, we give a short and simple new proof of the result of Dalmau and Larose that "Maltsev + Datalog -> symmetric Datalog" [2008].
In the second part of the paper, we provide some evidence for the conjecture of Dalmau [2002] that every CSP in NL is definable in linear Datalog. Our results also show that a wide class of CSPs ---CSPs which do not have bounded pathwidth duality (e.g. the P-complete Horn-3Sat problem)--- cannot be defined by any polynomial size family of monotone read-once nondeterministic branching programs.
We consider the following restrictions of the previous models: read-once linDat(suc) (1-linDat(suc)), and monotone readonce nondeterministic branching programs (mnBP1). Although restricted, these models can still define NL-complete problems such as directed st-Connectivity, and also nontrivial problems in NL which are not definable in linear Datalog. We show that any CSP definable by a 1-linDat(suc) program or by a poly-size family of mnBP1s can also be defined by a linear Datalog program. It also follows that a wide class of CSPs ---CSPs which do not have bounded pathwidth duality (e.g. the P-complete Horn-3Sat problem)--- cannot be defined by any 1-linDat(suc) program or by any poly-size family of mnBP1s.
Cite as
László Egri. On Constraint Satisfaction Problems below P*. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 203-217, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{egri:LIPIcs.CSL.2011.203,
author = {Egri, L\'{a}szl\'{o}},
title = {{On Constraint Satisfaction Problems below P*}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {203--217},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.203},
URN = {urn:nbn:de:0030-drops-32320},
doi = {10.4230/LIPIcs.CSL.2011.203},
annote = {Keywords: constraint satisfaction problems, complexity classes, Datalog fragments}
}
Document
Non-Definability Results for Randomised First-Order Logic
Abstract
We investigate the expressive power of randomised first-order logic
(BPFO) on restricted classes of structures. While BPFO is
stronger than FO in general, even on structures with a built-in
addition relation, we show that BPFO is not stronger than FO
on structures with a unary vocabulary, nor on the class of
equivalence relations. The same techniques can be applied to show
that evenness of a linear order, and therefore graph connectivity,
can not be defined in BPFO. Finally, we show that there is an
FO[<]-definable query on word structures which can not be
defined in BPFO[+1].
Cite as
Kord Eickmeyer. Non-Definability Results for Randomised First-Order Logic. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 218-232, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{eickmeyer:LIPIcs.CSL.2011.218,
author = {Eickmeyer, Kord},
title = {{Non-Definability Results for Randomised First-Order Logic}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {218--232},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.218},
URN = {urn:nbn:de:0030-drops-32333},
doi = {10.4230/LIPIcs.CSL.2011.218},
annote = {Keywords: descriptive complexity, randomised logics, derandomisation}
}
Document
System T and the Product of Selection Functions
Abstract
We show that the finite product of selection functions (for all finite types) is primitive recursively equivalent to Goedel's higher-type recursor (for all finite types). The correspondence is shown to hold for similar restricted fragments of both systems: The recursor for type level n+1 is primitive recursively equivalent to the finite product of selection functions of type level n. Whereas the recursor directly interprets induction, we show that other classical arithmetical principles such as bounded collection and finite choice are more naturally interpreted via the product of selection functions.
Cite as
Martin Escardo, Paulo Oliva, and Thomas Powell. System T and the Product of Selection Functions. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 233-247, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{escardo_et_al:LIPIcs.CSL.2011.233,
author = {Escardo, Martin and Oliva, Paulo and Powell, Thomas},
title = {{System T and the Product of Selection Functions}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {233--247},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.233},
URN = {urn:nbn:de:0030-drops-32341},
doi = {10.4230/LIPIcs.CSL.2011.233},
annote = {Keywords: primitive recursion, product of selection functions, finite choice, dialectica interpretation}
}
Document
Unifying Büchi Complementation Constructions
Abstract
Complementation of Buechi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that embodies all runs of the automaton. This approach is based on the observation that the vertices of this DAG can be ranked in a certain way, termed an odd ranking, iff all runs are rejecting. The second is the slice-based approach of Kahler and Wilke. This approach tracks levels of "split trees" - run trees in which only essential information about the history of each run is maintained. While the slice-based construction is conceptually simple, the complementing automata it generates are exponentially larger than those of the recent rank-based construction of Schewe, and it suffers from the difficulty of symbolically encoding levels of split trees.
In this work we reformulate the slice-based approach in terms of run DAGs and preorders over states. In doing so, we begin to draw parallels between the rank-based and slice-based approaches. Through deeper analysis of the slice-based approach, we strongly restrict the nondeterminism it generates. We are then able to employ the slice-based approach to provide a new odd ranking, called a retrospective ranking, that is different from the one provided by Kupferman and Vardi. This new ranking allows us to construct a deterministic-in-the-limit rank-based automaton with a highly restricted transition function. Further, by phrasing the slice-based approach in terms of ranks, our approach affords a simple symbolic encoding and achieves Schewe's tight bound.
Cite as
Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, and Thomas Wilke. Unifying Büchi Complementation Constructions. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 248-263, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{fogarty_et_al:LIPIcs.CSL.2011.248,
author = {Fogarty, Seth and Kupferman, Orna and Vardi, Moshe Y. and Wilke, Thomas},
title = {{Unifying B\"{u}chi Complementation Constructions}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {248--263},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.248},
URN = {urn:nbn:de:0030-drops-32357},
doi = {10.4230/LIPIcs.CSL.2011.248},
annote = {Keywords: B\"{u}chi automata, complementation, ranks, determinism in the limit}
}
Document
Degrees of Lookahead in Context-free Infinite Games
Abstract
We continue the investigation of delay games, infinite games in which one player may postpone her moves for some time to obtain a lookahead on her opponent's moves. We show that the problem of determining the winner of such a game is undecidable for deterministic context-free winning conditions. Furthermore, we show that the necessary lookahead to win a deterministic context-free delay game cannot be bounded by any elementary function. Both results hold already for restricted classes of deterministic context-free winning conditions.
Cite as
Wladimir Fridman, Christof Löding, and Martin Zimmermann. Degrees of Lookahead in Context-free Infinite Games. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 264-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{fridman_et_al:LIPIcs.CSL.2011.264,
author = {Fridman, Wladimir and L\"{o}ding, Christof and Zimmermann, Martin},
title = {{Degrees of Lookahead in Context-free Infinite Games}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {264--276},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.264},
URN = {urn:nbn:de:0030-drops-32365},
doi = {10.4230/LIPIcs.CSL.2011.264},
annote = {Keywords: infinite games, delay, context-free languages}
}
Document
L-Recursion and a new Logic for Logarithmic Space
Abstract
We extend first-order logic with counting by a new operator that
allows it to formalise a limited form of recursion which can be
evaluated in logarithmic space. The resulting logic LREC has a
data complexity in LOGSPACE, and it defines LOGSPACE-complete
problems like deterministic reachability and Boolean formula
evaluation. We prove that LREC is strictly more expressive than
deterministic transitive closure logic with counting and
incomparable in expressive power with symmetric transitive closure
logic STC and transitive closure logic (with or without counting).
LREC is strictly contained in fixed-point logic with counting FPC.
We also study an extension LREC= of LREC that has nicer closure
properties and is more expressive than both LREC and STC, but is
still contained in FPC and has a data complexity in LOGSPACE.
Our main results are that LREC captures LOGSPACE on the class of
directed trees and that LREC= captures LOGSPACE on the class of
interval graphs.
Cite as
Martin Grohe, Berit Grußien, André Hernich, and Bastian Laubner. L-Recursion and a new Logic for Logarithmic Space. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 277-291, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{grohe_et_al:LIPIcs.CSL.2011.277,
author = {Grohe, Martin and Gru{\ss}ien, Berit and Hernich, Andr\'{e} and Laubner, Bastian},
title = {{L-Recursion and a new Logic for Logarithmic Space}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {277--291},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.277},
URN = {urn:nbn:de:0030-drops-32373},
doi = {10.4230/LIPIcs.CSL.2011.277},
annote = {Keywords: descriptive complexity, logarithmic space, fixed-point logics}
}
Document
The Lax Braided Structure of Streaming I/O
Abstract
We investigate and implement a model of typed streaming I/O. Each type
determines a language of traces analogous to regular expressions on
strings, and programs are modelled by certain monotone functions on
these traces. We show that sequential composition forms a lax braided
monoid in the category of types and programs. This lax braided
structure allows programs to be represented diagrammatically using
Joyal and Street's string diagrams in 3D space.
Monotone functions over traces cannot be executed efficiently, so we
present an equivalent monoidal category of transducers. We demonstrate
that transducers can be executed efficiently, theoretically by showing
that programs with diagrams embedded in the plane can be executed in
O(1) space, and experimentally by an implementation in the Agda
dependently typed functional language. Agda supports machine-assisted
proof: we have mechanically verified that the transducer
implementation and the I/O model form lax braided monoidal categories.
Cite as
Alan Jeffrey and Julian Rathke. The Lax Braided Structure of Streaming I/O. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 292-306, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{jeffrey_et_al:LIPIcs.CSL.2011.292,
author = {Jeffrey, Alan and Rathke, Julian},
title = {{The Lax Braided Structure of Streaming I/O}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {292--306},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.292},
URN = {urn:nbn:de:0030-drops-32386},
doi = {10.4230/LIPIcs.CSL.2011.292},
annote = {Keywords: semantics, categorical models, streaming I/O, Agda}
}
Document
The Church Synthesis Problem with Metric
Abstract
Church's Problem asks for the construction of a procedure which, given a logical specification S(I,O) between input strings I and output strings O, determines whether there exists an operator F that implements the specification in the sense that S(I,F(I)) holds for all inputs I. Buechi and Landweber gave a procedure to solve Church's problem for MSO specifications and operators computable by finite-state automata.
We consider extensions of Church's problem in two orthogonal directions: (i) we address the problem in a more general logical setting, where not only the specifications but also the solutions are presented in a logical system; (ii) we consider not only the canonical discrete time domain of the natural numbers, but also the continuous domain of reals.
We show that for every fixed bounded length interval of the reals, Church's problem is decidable when specifications and implementations are described in the monadic second-order logics over the reals with order and the +1 function.
Cite as
Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, and James Worrell. The Church Synthesis Problem with Metric. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 307-321, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{jenkins_et_al:LIPIcs.CSL.2011.307,
author = {Jenkins, Mark and Ouaknine, Jo\"{e}l and Rabinovich, Alexander and Worrell, James},
title = {{The Church Synthesis Problem with Metric}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {307--321},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.307},
URN = {urn:nbn:de:0030-drops-32390},
doi = {10.4230/LIPIcs.CSL.2011.307},
annote = {Keywords: Church's Problem, monadic logic, games, uniformization}
}
Document
A Pumping Lemma for Collapsible Pushdown Graphs of Level 2
Abstract
We present a pumping lemma for the class of collapsible pushdown graphs of level 2. This pumping lemma even applies to epsilon-contractions of level 2 collapsible pushdown graphs. Our pumping lemma also improves the bounds of Hayashi's pumping lemma for indexed languages.
Cite as
Alexander Kartzow. A Pumping Lemma for Collapsible Pushdown Graphs of Level 2. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 322-336, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{kartzow:LIPIcs.CSL.2011.322,
author = {Kartzow, Alexander},
title = {{A Pumping Lemma for Collapsible Pushdown Graphs of Level 2}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {322--336},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.322},
URN = {urn:nbn:de:0030-drops-32406},
doi = {10.4230/LIPIcs.CSL.2011.322},
annote = {Keywords: collapsible pushdown graph, epsilon-contraction, pumping lemma}
}
Document
Decidability Issues for Two-Variable Logics with Several Linear Orders
Abstract
We show that the satisfiability and the finite satisfiability problems for two-variable logic, FO2, over the class of structures with three linear orders, are undecidable. This sharpens an earlier result that FO2 with eight linear orders is undecidable. The theorem holds for a restricted case in which linear orders are the only non-unary relations. Recently, a contrasting result has been shown, that the finite satisfiability problem for FO2 with two linear orders and with no additional non-unary relations is decidable. We observe that our proof can be adapted to some interesting fragments of FO2, in particular it works for the two-variable guarded fragment, GF2, even if the order relations are used only as guards. Finally, we show that GF2 with an arbitrary number of linear orders which can be used only as guards becomes decidable if except linear orders only unary relations are allowed.
Cite as
Emanuel Kieronski. Decidability Issues for Two-Variable Logics with Several Linear Orders. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 337-351, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{kieronski:LIPIcs.CSL.2011.337,
author = {Kieronski, Emanuel},
title = {{Decidability Issues for Two-Variable Logics with Several Linear Orders}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {337--351},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.337},
URN = {urn:nbn:de:0030-drops-32415},
doi = {10.4230/LIPIcs.CSL.2011.337},
annote = {Keywords: two-variable logic, linear orders, guarded fragment, decidability}
}
Document
Coalgebraic Derivations in Logic Programming
Abstract
Coalgebra may be used to provide semantics for SLD-derivations, both finite and infinite. We first give such semantics to classical SLD-derivations, proving results such as adequacy, soundness and completeness. Then, based upon coalgebraic semantics, we propose a new sound and complete algorithm for parallel derivations. We analyse this new algorithm in terms of the Theory of Observables, and we prove correctness and full abstraction results.
Cite as
Ekaterina Komendantskaya and John Power. Coalgebraic Derivations in Logic Programming. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 352-366, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{komendantskaya_et_al:LIPIcs.CSL.2011.352,
author = {Komendantskaya, Ekaterina and Power, John},
title = {{Coalgebraic Derivations in Logic Programming}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {352--366},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.352},
URN = {urn:nbn:de:0030-drops-32424},
doi = {10.4230/LIPIcs.CSL.2011.352},
annote = {Keywords: Logic programming, SLD-resolution, concurrency, coinduction, Lawvere theoriesm, coinductive logic programming, concurrent logic programming}
}
Document
Trees in Trees: Is the Incomplete Information about a Tree Consistent?
Abstract
We are interested in the following problem: given a tree automaton Aut and an incomplete tree description P, does a tree T exist such that T is accepted by Aut and consistent with P? A tree description is a tree-like structure which provides incomplete information about the shape of T. We show that this problem can be solved in polynomial time as long as Aut and the set of possible arrangements that can be forced by P are fixed. We show how our result is related to an open problem in the theory of incomplete XML information.
Cite as
Eryk Kopczynski. Trees in Trees: Is the Incomplete Information about a Tree Consistent?. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 367-380, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{kopczynski:LIPIcs.CSL.2011.367,
author = {Kopczynski, Eryk},
title = {{Trees in Trees: Is the Incomplete Information about a Tree Consistent?}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {367--380},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.367},
URN = {urn:nbn:de:0030-drops-32434},
doi = {10.4230/LIPIcs.CSL.2011.367},
annote = {Keywords: XML, tree automata, incomplete tree descriptions, Euler cycle}
}
Document
A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem
Abstract
Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem. He proved that several other problems are complete for CC, including the stable marriage problem, and finding the lexicographical first maximal matching in a bipartite graph. We suggest alternative definitions of CC based on different reducibilities and introduce a two-sorted theory VCC* based on one of them. We sharpen and simplify Subramanian's completeness proofs for the above two problems and formalize them in VCC*.
Cite as
Dai Tri Man Lê, Stephen A. Cook, and Yuli Ye. A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 381-395, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{le_et_al:LIPIcs.CSL.2011.381,
author = {L\^{e}, Dai Tri Man and Cook, Stephen A. and Ye, Yuli},
title = {{A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {381--395},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.381},
URN = {urn:nbn:de:0030-drops-32440},
doi = {10.4230/LIPIcs.CSL.2011.381},
annote = {Keywords: bounded arithmetic, complexity theory, comparator circuits}
}
Document
Relating Two Semantics of Locally Scoped Names
Abstract
The operational semantics of programming constructs involving locally
scoped names typically makes use of stateful "dynamic allocation": a
set of currently-used names forms part of the state and upon entering
a scope the set is augmented by a new name bound to the scoped
identifier. More abstractly, one can see this as a transformation of
local scopes by expanding them outward to an implicit top-level. By
contrast, in a neglected paper from 1994, Odersky gave a stateless
lambda calculus with locally scoped names whose dynamics contracts
scopes inward. The properties of "Odersky-style" local names are quite
different from dynamically allocated ones and it has not been clear,
until now, what is the expressive power of Odersky's notion. We show
that in fact it provides a direct semantics of locally scoped names
from which the more familiar dynamic allocation semantics can be
obtained by continuation-passing style (CPS) translation. More
precisely, we show that there is a CPS translation of typed lambda
calculus with dynamically allocated names (the Pitts-Stark
nu-calculus) into Odersky's lambda-nu-calculus which is
computationally adequate with respect to observational equivalence in
the two calculi.
Cite as
Steffen Lösch and Andrew M. Pitts. Relating Two Semantics of Locally Scoped Names. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 396-411, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{losch_et_al:LIPIcs.CSL.2011.396,
author = {L\"{o}sch, Steffen and Pitts, Andrew M.},
title = {{Relating Two Semantics of Locally Scoped Names}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {396--411},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.396},
URN = {urn:nbn:de:0030-drops-32454},
doi = {10.4230/LIPIcs.CSL.2011.396},
annote = {Keywords: local names, continuations, typed lambda-calculus, observational equivalence}
}
Document
Synthesis from Probabilistic Components
Abstract
Synthesis is the automatic construction of a system from its specification. In classical synthesis algorithms, it is always assumed that the system is "constructed from scratch" rather than composed from reusable components. This, of course, rarely happens in real life, where almost every non-trivial commercial software system relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web-service orchestration, can be modeled as synthesis of a system from a library of components. Recently, Lustig and Vardi introduced dataflow and control-flow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while control-flow synthesis is decidable. In this work, we consider the problem of control-flow synthesis from libraries of probabilistic components. We show that this more general problem is also decidable.
Cite as
Yoad Lustig, Sumit Nain, and Moshe Y. Vardi. Synthesis from Probabilistic Components. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 412-427, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{lustig_et_al:LIPIcs.CSL.2011.412,
author = {Lustig, Yoad and Nain, Sumit and Vardi, Moshe Y.},
title = {{Synthesis from Probabilistic Components}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {412--427},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.412},
URN = {urn:nbn:de:0030-drops-32461},
doi = {10.4230/LIPIcs.CSL.2011.412},
annote = {Keywords: temporal synthesis, probabilistic components}
}
Document
Synthesizing Reactive Programs
Abstract
Current theoretical solutions to the classical Church's synthesis problem are focused on synthesizing transition systems and not programs. Programs are compact and often the true aim in many synthesis problems, while the transition systems that correspond to them are often large and not very useful as synthesized artefacts. Consequently, current practical techniques first synthesize a transition system, and then extract a more compact representation from it. We reformulate the synthesis of reactive systems directly in terms of program synthesis, and develop a theory to show that the problem of synthesizing programs over a fixed set of Boolean variables in a simple imperative programming language is decidable for regular omega-specifications. We also present results for synthesizing programs with recursion against both regular specifications as well as visibly-pushdown language specifications. Finally, we show applications to program repair, and conclude with open problems in synthesizing distributed programs.
Cite as
Parthasarathy Madhusudan. Synthesizing Reactive Programs. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 428-442, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{madhusudan:LIPIcs.CSL.2011.428,
author = {Madhusudan, Parthasarathy},
title = {{Synthesizing Reactive Programs}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {428--442},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.428},
URN = {urn:nbn:de:0030-drops-32479},
doi = {10.4230/LIPIcs.CSL.2011.428},
annote = {Keywords: program synthesis, boolean programs, automata theory, temporal logics}
}
Document
Concurrency Semantics for the Geiger-Paz-Pearl Axioms of Independence
Abstract
Independence between two sets of random variables is a well-known relation in probability theory. Its origins trace back to Abraham de Moivre's work in the 18th century. The propositional theory of this relation was axiomatized by Geiger, Paz, and Pearl.
Sutherland introduced a relation in information flow theory that later became known as "nondeducibility." Subsequently, the first two authors generalized this relation from a relation between two arguments to a relation between two sets of arguments and proved that it is completely described by essentially the same axioms as independence in probability theory.
This paper considers a non-interference relation between two groups of concurrent processes sharing common resources. Two such groups are called non-interfering if, when executed concurrently, the only way for them to reach deadlock is for one of the groups to deadlock internally. The paper shows that a complete axiomatization of this relation is given by the same Geiger-Paz-Pearl axioms.
Cite as
Sara Miner More, Pavel Naumov, and Benjamin Sapp. Concurrency Semantics for the Geiger-Paz-Pearl Axioms of Independence. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 443-457, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{minermore_et_al:LIPIcs.CSL.2011.443,
author = {Miner More, Sara and Naumov, Pavel and Sapp, Benjamin},
title = {{Concurrency Semantics for the Geiger-Paz-Pearl Axioms of Independence}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {443--457},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.443},
URN = {urn:nbn:de:0030-drops-32480},
doi = {10.4230/LIPIcs.CSL.2011.443},
annote = {Keywords: independence, concurrency, information flow, axiomatization}
}
Document
Axiomatizing the Quote
Abstract
We study reflection in the Lambda Calculus from an axiomatic point of view. Specifically, we consider various properties that the quote operator must satisfy as a function on lambda terms. The most important of these is the existence of a definable left inverse, a so-called evaluator for the quote operator. Usually the quote operator encodes the syntax of a given term, and the evaluator proceeds by analyzing the syntax and reifying all constructors by their actual meaning in the calculus. Working in Combinatory Logic, Raymond Smullyan (1994) investigated which elements of the syntax must be accessible via the quote in order for an evaluator to exist. He asked three specific questions, to which we provide negative answers. On the positive side, we give a characterization of quotes which possess all of the desired properties, equivalently defined as being equitranslatable with a standard quote. As an application, we show that Scott's coding is not complete in this sense, but can be slightly modified to be such. This results in a minimal definition of a complete quoting for Combinatory Logic.
Cite as
Andrew Polonsky. Axiomatizing the Quote. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 458-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{polonsky:LIPIcs.CSL.2011.458,
author = {Polonsky, Andrew},
title = {{Axiomatizing the Quote}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {458--469},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.458},
URN = {urn:nbn:de:0030-drops-32493},
doi = {10.4230/LIPIcs.CSL.2011.458},
annote = {Keywords: lambda calculus, combinatory logic, quote operator, enumerator}
}
Document
Relative Completeness for Logics of Functional Programs
Abstract
We prove a relative completeness result for a logic of functional programs extending D. Scott's LCF. For such a logic, contrary to results for Hoare logic, it does not make sense to ask whether it is complete relative to the full theory of its first-order part, since the first order part does not determine uniquely the model at higher-order types. Therefore, one has to fix a model and choose an appropriate data theory w.r.t. which the logic is relatively complete. We establish relative completeness for two models: for the Scott model we use the theory of Baire Space as data theory, and for the effective Scott model we take first-order arithmetic. In both cases we need to extend traditional LCF in order to capture a sufficient amount of domain theory.
Cite as
Bernhard Reus and Thomas Streicher. Relative Completeness for Logics of Functional Programs. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 470-480, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{reus_et_al:LIPIcs.CSL.2011.470,
author = {Reus, Bernhard and Streicher, Thomas},
title = {{Relative Completeness for Logics of Functional Programs}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {470--480},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.470},
URN = {urn:nbn:de:0030-drops-32509},
doi = {10.4230/LIPIcs.CSL.2011.470},
annote = {Keywords: completeness, program logics, LCF}
}
Document
The Exact Hardness of Deciding Derivational and Runtime Complexity
Abstract
For any class C of computable total functions satisfying some mild conditions, we prove that the following decision problems are complete for the existential part of the second level of the arithmetical hierarchy: (A) Deciding whether a term rewriting system (TRS for short) has runtime complexity bounded by a function in C. (B) Deciding whether a TRS has derivational complexity bounded by a function in C.
In particular, the problems of deciding whether a TRS has polynomially (exponentially) bounded runtime complexity (respectively derivational complexity) are complete for this level of the arithmetical ierarchy. This places deciding polynomial derivational or runtime complexity of TRSs at the same level as deciding nontermination or nonconfluence of TRSs. We proceed to show that the related problem of deciding for a single computable function f whether a TRS has runtime complexity bounded from above by f is complete for the universal part of the first level of the arithmetical hierarchy. We further prove that analysing the implicit complexity of TRSs is even more difficult: The problem of deciding whether a TRS accepts a language of terms accepted by some TRS with runtime complexity bounded by a function in C is complete for the existential part of the third level of the arithmetical hierarchy.
All of our results are easily extended to the notion of minimal complexity (where the length of shortest reductions to normal form is considered) and remain valid under any computable reduction strategy. Finally, all results hold both for unrestricted TRSs and for the class of orthogonal TRSs.
Cite as
Andreas Schnabl and Jakob Grue Simonsen. The Exact Hardness of Deciding Derivational and Runtime Complexity. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 481-495, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{schnabl_et_al:LIPIcs.CSL.2011.481,
author = {Schnabl, Andreas and Simonsen, Jakob Grue},
title = {{The Exact Hardness of Deciding Derivational and Runtime Complexity}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {481--495},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.481},
URN = {urn:nbn:de:0030-drops-32516},
doi = {10.4230/LIPIcs.CSL.2011.481},
annote = {Keywords: term rewriting, derivational complexity, arithmetical hierarchy}
}
Document
A Category Theoretic View of Nondeterministic Recursive Program Schemes
Abstract
Deterministic recursive program schemes (RPS's) have a clear category theoretic semantics presented by Ghani et al. and by Milius and Moss. Here we extend it to nondeterministic RPS's. We provide a category theoretic notion of guardedness and of solutions. Our main result is a description of the canonical greatest solution for every guarded nondeterministic RPS, thereby giving a category theoretic semantics for nondeterministic RPS's. We show how our notions and results are connected to classical work.
Cite as
Daniel Schwencke. A Category Theoretic View of Nondeterministic Recursive Program Schemes. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 496-511, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{schwencke:LIPIcs.CSL.2011.496,
author = {Schwencke, Daniel},
title = {{A Category Theoretic View of Nondeterministic Recursive Program Schemes}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {496--511},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.496},
URN = {urn:nbn:de:0030-drops-32529},
doi = {10.4230/LIPIcs.CSL.2011.496},
annote = {Keywords: recursive program scheme, nondeterminism, powerset monad, distributive law, final coalgebra}
}
Document
Step-Indexed Relational Reasoning for Countable Nondeterminism
Abstract
Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Because countable choice introduces non-continuous behaviour, it is well-known that developing semantic models for programming languages with countable nondeterminism is challenging. We present a step-indexed logical relations model of a higher-order functional programming language with countable nondeterminism and demonstrate how it can be used to reason about contextually defined may- and must-equivalence. In earlier step-indexed models, the indices have been drawn from omega. Here the step-indexed relations for must-equivalence are indexed over an ordinal greater than omega.
Cite as
Jan Schwinghammer and Lars Birkedal. Step-Indexed Relational Reasoning for Countable Nondeterminism. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 512-524, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{schwinghammer_et_al:LIPIcs.CSL.2011.512,
author = {Schwinghammer, Jan and Birkedal, Lars},
title = {{Step-Indexed Relational Reasoning for Countable Nondeterminism}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {512--524},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.512},
URN = {urn:nbn:de:0030-drops-32535},
doi = {10.4230/LIPIcs.CSL.2011.512},
annote = {Keywords: countable choice, lambda calculus, program equivalence}
}
Document
Algebraic Characterization of the Alternation Hierarchy in FO^2[<] on Finite Words
Abstract
We give an algebraic characterization of the quantifier alternation hierarchy in first-order two-variable logic on finite words. As a result, we obtain a new proof that this hierarchy is strict. We also show that the first two levels of the hierarchy have decidable membership problems, and conjecture an algebraic decision procedure for the other levels.
Cite as
Howard Straubing. Algebraic Characterization of the Alternation Hierarchy in FO^2[<] on Finite Words. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 525-537, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{straubing:LIPIcs.CSL.2011.525,
author = {Straubing, Howard},
title = {{Algebraic Characterization of the Alternation Hierarchy in FO^2\lbrack\langle\rbrack on Finite Words}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {525--537},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.525},
URN = {urn:nbn:de:0030-drops-32549},
doi = {10.4230/LIPIcs.CSL.2011.525},
annote = {Keywords: automata, finite model theory}
}
Document
Non-Commutative Infinitary Peano Arithmetic
Abstract
Does there exist any sequent calculus such that it is a subclassical logic and it becomes classical logic when the exchange rules are added? The first contribution of this paper is answering this question for infinitary Peano arithmetic. This paper defines infinitary Peano arithmetic with non-commutative sequents, called non-commutative infinitary Peano arithmetic, so that the system becomes equivalent to Peano arithmetic with the omega-rule if the the exchange rule is added to this system. This system is unique among other non-commutative systems, since all the logical connectives have standard meaning and specifically the commutativity for conjunction and disjunction is derivable. This paper shows that the provability in non-commutative infinitary Peano arithmetic is equivalent to Heyting arithmetic with the recursive omega rule and the law of excluded middle for Sigma-0-1 formulas. Thus, non-commutative infinitary Peano arithmetic is shown to be a subclassical logic. The cut elimination theorem in this system is also proved. The second contribution of this paper is introducing infinitary Peano arithmetic having antecedent-grouping and no right exchange rules. The first contribution of this paper is achieved through this system. This system is obtained from the positive fragment of infinitary Peano arithmetic without the exchange rules by extending it from a positive fragment to a full system, preserving its 1-backtracking game semantics. This paper shows that this system is equivalent to both non-commutative infinitary Peano arithmetic, and Heyting arithmetic with the recursive omega rule and the Sigma-0-1 excluded middle.
Cite as
Makoto Tatsuta and Stefano Berardi. Non-Commutative Infinitary Peano Arithmetic. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 538-552, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{tatsuta_et_al:LIPIcs.CSL.2011.538,
author = {Tatsuta, Makoto and Berardi, Stefano},
title = {{Non-Commutative Infinitary Peano Arithmetic}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {538--552},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.538},
URN = {urn:nbn:de:0030-drops-32551},
doi = {10.4230/LIPIcs.CSL.2011.538},
annote = {Keywords: proof theory, cut elimination, intuitionistic logic, infinitary logic, recursive omega rules, substructural logic}
}
Document
Model Theory in Computer Science: My Own Recurrent Themes
Abstract
I review my own experiences in research and the management of science.
Cite as
Johann A. Makowsky. Model Theory in Computer Science: My Own Recurrent Themes. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 553-567, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
Copy BibTex To Clipboard
@InProceedings{makowsky:LIPIcs.CSL.2011.553,
author = {Makowsky, Johann A.},
title = {{Model Theory in Computer Science: My Own Recurrent Themes}},
booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
pages = {553--567},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Bezem, Marc},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.553},
URN = {urn:nbn:de:0030-drops-32567},
doi = {10.4230/LIPIcs.CSL.2011.553},
annote = {Keywords: model theory, finite model theory, databases, graph invariants}
}