eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
0
0
10.4230/LIPIcs.CSL.2020
article
LIPIcs, Volume 152, CSL'20, Complete Volume
Fernández, Maribel
1
Muscholl, Anca
2
King’s College London, UK
University of Bordeaux, France
LIPIcs, Volume 152, CSL'20, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020/LIPIcs.CSL.2020.pdf
Theory of computation, Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
0:i
0:xviii
10.4230/LIPIcs.CSL.2020.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Fernández, Maribel
1
Muscholl, Anca
2
King’s College London, UK
University of Bordeaux, France
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.0/LIPIcs.CSL.2020.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
1:1
1:2
10.4230/LIPIcs.CSL.2020.1
article
Verification of Security Protocols (Invited Talk)
Cortier, Véronique
1
LORIA - CNRS, INRIA, Université de Lorraine, Nancy, France
Cryptographic protocols aim at securing communications over insecure networks like the Internet. Over the past decades, numerous decision procedures and tools have been developed to automatically analyse the security of protocols. The field has now reached a good level of maturity with efficient techniques for the automatic security analysis of protocols
After an overview of some famous protocols and flaws, we will describe the current techniques for security protocols analysis, often based on logic, and review the key challenges towards a fully automated verification.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.1/LIPIcs.CSL.2020.1.pdf
Security protocols
automated deduction
security
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
2:1
2:12
10.4230/LIPIcs.CSL.2020.2
article
Symmetric Computation (Invited Talk)
Dawar, Anuj
1
https://orcid.org/0000-0003-4014-8248
Department of Computer Science and Technology, University of Cambridge, U.K.
We discuss a recent convergence of notions of symmetric computation arising in the theory of linear programming, in logic and in circuit complexity. This leads us to a coherent and robust definition of problems that are efficiently and symmetrically solvable. This is at once a rich class of problems and one for which we have methods for proving lower bounds. In this paper, we take a tour through results which show applications of these methods in a number of areas.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.2/LIPIcs.CSL.2020.2.pdf
Descriptive Complexity
Fixed-point Logic with Counting
Circuit Complexity
Linear Programming
Hardness of Approximation
Arithmetic Circuits
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
3:1
3:17
10.4230/LIPIcs.CSL.2020.3
article
Solving Word Equations (And Other Unification Problems) by Recompression (Invited Talk)
Jeż, Artur
1
https://orcid.org/0000-0003-4321-3105
University of Wrocław, Poland
In word equation problem we are given an equation u = v, where both u and v are words of letters and variables, and ask for a substitution of variables by words that equalizes the sides of the equation. This problem was first solved by Makanin and a different solution was proposed by Plandowski only 20 years later, his solution works in PSPACE, which is the best computational complexity bound known for this problem; on the other hand, the only known lower-bound is NP-hardness. In both cases the algorithms (and proofs) employed nontrivial facts on word combinatorics.
In the paper I will present an application of a recent technique of recompression, which simplifies the known proofs and (slightly) lowers the complexity to linear nondeterministic space. The technique is based on employing simple compression rules (replacement of two letters ab by a new letter c, replacement of maximal repetitions of a by a new letter), and modifying the equations (replacing a variable X by bX or Xa) so that those operations are sound and complete. In particular, no combinatorial properties of strings are used.
The approach turns out to be quite robust and can be applied to various generalizations and related scenarios (context unification, i.e. equations over terms; equations over traces, i.e. partially ordered words; ...).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.3/LIPIcs.CSL.2020.3.pdf
word equation
context unification
equations in groups
compression
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
4:1
4:23
10.4230/LIPIcs.CSL.2020.4
article
Strong Bisimulation for Control Operators (Invited Talk)
Kesner, Delia
1
2
Bonelli, Eduardo
3
Viso, Andrés
4
5
https://orcid.org/0000-0002-6822-8453
IRIF, Université de Paris and CNRS, France
Institut Universitaire de France (IUF), France
Stevens Institute of Technology, Hoboken, NJ, USA
Universidad de Buenos Aires, Argentina
Universidad Nacional de Quilmes, Bernal, Buenos Aires, Argentina
The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation ≃, defined over a revised presentation of Parigot’s λμ-calculus we dub ΛM.
Our result builds on two fundamental ingredients: (1) factorization of λμ-reduction into multiplicative and exponential steps by means of explicit term operators of ΛM, and (2) translation of ΛM-terms into Laurent’s polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation ≃ is shown to characterize structural equivalence in PPN. Most notably, ≃ is shown to be a strong bisimulation with respect to reduction in ΛM, i.e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s σ-equivalence in λ-calculus as well as for Laurent’s σ-equivalence in λμ.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.4/LIPIcs.CSL.2020.4.pdf
Lambda-mu calculus
proof-nets
strong bisimulation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
5:1
5:2
10.4230/LIPIcs.CSL.2020.5
article
From Classical Proof Theory to P versus NP: a Guide to Bounded Theories (Invited Talk)
Tzameret, Iddo
1
Royal Holloway, University of London, UK
This talk explores the question of what does logic and specifically proof theory can tell us about the fundamental hardness questions in computational complexity. We start with a brief description of the main concepts behind bounded arithmetic which is a family of weak formal theories of arithmetic that mirror in a precise manner the world of propositional proofs: if a statement of a given form is provable in a given bounded arithmetic theory then the same statement is suitably translated to a family of propositional formulas with short (polynomial-size) proofs in a corresponding propositional proof system.
We will proceed to describe the motivations behind the study of bounded arithmetic theories, their corresponding propositional proof systems, and how they relate to the fundamental complexity class separations and circuit lower bounds questions in computational complexity. We provide a collage of results and recent developments showing how bounded arithmetic and propositional proof complexity form a cohesive framework in which both concrete combinatorial questions about complexity as well as meta-mathematical questions about provability of statements of complexity theory itself, are studied.
Specific topics we shall mention are: (i) The bounded reverse mathematics program [Stephen Cook and Phuong Nguyen, 2010]: studying the weakest possible axiomatic assumptions that can prove important results in mathematics and computing (cf. [Iddo Tzameret and Stephen A. Cook, 2017; Pavel Hrubeš and Iddo Tzameret, 2015]), and the correspondence between circuit classes and theories. (ii) The meta-mathematics of computational complexity: what kind of reasoning power do we need in order to prove major results in complexity theory itself, and applications to complexity lower bounds (cf. [Razborov, 1995; Rahul Santhanam and Jan Pich, 2019]). (iii) Proof complexity: the systematic treatment of propositional proofs as combinatorial and algebraic objects and their algorithmic applications (cf. [Samuel Buss, 2012; Tonnian Pitassi and Iddo Tzameret, 2016; Noah Fleming et al., 2019]).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.5/LIPIcs.CSL.2020.5.pdf
Bounded arithmetic
complexity class separations
circuit complexity
proof complexity
weak theories of arithmetic
feasible mathematics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
6:1
6:16
10.4230/LIPIcs.CSL.2020.6
article
Generalized Connectives for Multiplicative Linear Logic
Acclavio, Matteo
1
https://orcid.org/0000-0002-0425-2825
Maieli, Roberto
2
https://orcid.org/0000-0001-9723-7183
Samovar, UMR 5157 Télécom SudParis and CNRS, 9 rue Charles Fourier, 91011 Évry, France
Mathematics & Physics Department, Roma Tre University, L.go S. L. Murialdo 1, 00146 Rome, Italy
In this paper we investigate the notion of generalized connective for multiplicative linear logic. We introduce a notion of orthogonality for partitions of a finite set and we study the family of connectives which can be described by two orthogonal sets of partitions.
We prove that there is a special class of connectives that can never be decomposed by means of the multiplicative conjunction ⊗ and disjunction ⅋, providing an infinite family of non-decomposable connectives, called Girard connectives. We show that each Girard connective can be naturally described by a type (a set of partitions equal to its double-orthogonal) and its orthogonal type. In addition, one of these two types is the union of the types associated to a family of MLL-formulas in disjunctive normal form, and these formulas only differ for the cyclic permutations of their atoms.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.6/LIPIcs.CSL.2020.6.pdf
Linear Logic
Partitions Sets
Proof Nets
Sequent Calculus
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
7:1
7:21
10.4230/LIPIcs.CSL.2020.7
article
On Free Completely Iterative Algebras
Adámek, Jiří
1
Czech Technical University Prague, Czech Republic
For every finitary set functor F we demonstrate that free algebras carry a canonical partial order. In case F is bicontinuous, we prove that the cpo obtained as the conservative completion of the free algebra is the free completely iterative algebra. Moreover, the algebra structure of the latter is the unique continuous extension of the algebra structure of the free algebra.
For general finitary functors the free algebra and the free completely iterative algebra are proved to be posets sharing the same conservative completion. And for every recursive equation in the free completely iterative algebra the solution is obtained as the join of an ω-chain of approximate solutions in the free algebra.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.7/LIPIcs.CSL.2020.7.pdf
free algebra
completely iterative algebra
terminal coalgebra
initial algebra
finitary functor
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
8:1
8:17
10.4230/LIPIcs.CSL.2020.8
article
Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries
Angluin, Dana
1
https://orcid.org/0000-0002-6907-2999
Antonopoulos, Timos
1
Fisman, Dana
2
https://orcid.org/0000-0002-6015-4170
Yale University, New Haven, CT, USA
Ben-Gurion University, Beer-Sheva, Israel
A Büchi automaton is strongly unambiguous if every word w ∈ Σ^ω has at most one final path. Many properties of strongly unambiguous Büchi automata (SUBAs) are known. They are fully expressive: every regular ω-language can be represented by a SUBA. Equivalence and containment of SUBAs can be decided in polynomial time. SUBAs may be exponentially smaller than deterministic Muller automata and may be exponentially bigger than deterministic Büchi automata. In this work we show that SUBAs can be learned in polynomial time using membership and certain non-proper equivalence queries, which implies that they are polynomially predictable with membership queries. In contrast, under plausible cryptographic assumptions, non-deterministic Büchi automata are not polynomially predictable with membership queries.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.8/LIPIcs.CSL.2020.8.pdf
Polynomially predictable languages
Automata learning
Strongly unambiguous Büchi automata
Automata succinctness
Regular ω-languages
Grammatical inference
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
9:1
9:16
10.4230/LIPIcs.CSL.2020.9
article
A Robust Class of Linear Recurrence Sequences
Barloy, Corentin
1
Fijalkow, Nathanaël
2
3
Lhote, Nathan
4
Mazowiecki, Filip
5
École Normale Supérieure de Paris, France
CNRS, LaBRI, Bordeaux, France
The Alan Turing Institute of data science, London, United Kingdom
University of Warsaw, Poland
LaBRI, Université de Bordeaux, France
We introduce a subclass of linear recurrence sequences which we call poly-rational sequences because they are denoted by rational expressions closed under sum and product. We show that this class is robust by giving several characterisations: polynomially ambiguous weighted automata, copyless cost-register automata, rational formal series, and linear recurrence sequences whose eigenvalues are roots of rational numbers.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.9/LIPIcs.CSL.2020.9.pdf
linear recurrence sequences
weighted automata
cost-register automata
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
10:1
10:18
10.4230/LIPIcs.CSL.2020.10
article
Coverage and Vacuity in Network Formation Games
Bielous, Gili
1
Kupferman, Orna
1
School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel
The frameworks of coverage and vacuity in formal verification analyze the effect of mutations applied to systems or their specifications. We adopt these notions to network formation games, analyzing the effect of a change in the cost of a resource. We consider two measures to be affected: the cost of the Social Optimum and extremums of costs of Nash Equilibria. Our results offer a formal framework to the effect of mutations in network formation games and include a complexity analysis of related decision problems. They also tighten the relation between algorithmic game theory and formal verification, suggesting refined definitions of coverage and vacuity for the latter.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.10/LIPIcs.CSL.2020.10.pdf
Network Formation Games
Vacuity
Coverage
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
11:1
11:15
10.4230/LIPIcs.CSL.2020.11
article
A Complete Axiomatisation of a Fragment of Language Algebra
Brunet, Paul
1
https://orcid.org/0000-0002-9762-6872
University College London, United Kingdom
We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.11/LIPIcs.CSL.2020.11.pdf
Kleene algebra
language algebra
completeness theorem
axiomatisation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
12:1
12:17
10.4230/LIPIcs.CSL.2020.12
article
Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs
Buss, Sam
1
Das, Anupam
2
Knop, Alexander
1
Dept. of Mathematics, UC San Diego, USA
Dept. of Computer Science, University of Copenhagen, Denmark
This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs, deterministic or non-deterministic. Decision trees (DTs) are represented by a natural term syntax, inducing the system LDT, and non-determinism is modelled by including disjunction, ∨, as primitive (system LNDT). Branching programs generalise DTs to dag-like structures and are duly handled by extension variables in our setting, as is common in proof complexity (systems eLDT and eLNDT).
Deterministic and non-deterministic branching programs are natural nonuniform analogues of log-space (L) and nondeterministic log-space (NL), respectively. Thus eLDT and eLNDT serve as natural systems of reasoning corresponding to L and NL, respectively.
The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in LDT, LNDT, eLDT and eLNDT. We also compare them with Frege systems, constant-depth Frege systems and extended Frege systems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.12/LIPIcs.CSL.2020.12.pdf
proof complexity
decision trees
branching programs
logspace
sequent calculus
non-determinism
low-depth complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
13:1
13:17
10.4230/LIPIcs.CSL.2020.13
article
Internal Parametricity for Cubical Type Theory
Cavallo, Evan
1
https://orcid.org/0000-0001-8174-7496
Harper, Robert
1
https://orcid.org/0000-0002-9400-2941
Carnegie Mellon University, Pittsburgh, PA, USA
We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, and we give an account of the identity extension lemma for internal parametricity.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.13/LIPIcs.CSL.2020.13.pdf
parametricity
cubical type theory
higher inductive types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
14:1
14:17
10.4230/LIPIcs.CSL.2020.14
article
Unifying Cubical Models of Univalent Type Theory
Cavallo, Evan
1
https://orcid.org/0000-0001-8174-7496
Mörtberg, Anders
1
2
Swan, Andrew W
3
School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA
Department of Mathematics, Stockholm University, Sweden
Institute for Logic, Language and Computation, University of Amsterdam, The Netherlands
We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.14/LIPIcs.CSL.2020.14.pdf
Cubical Set Models
Cubical Type Theory
Homotopy Type Theory
Univalent Foundations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
15:1
15:16
10.4230/LIPIcs.CSL.2020.15
article
FO-Definability of Shrub-Depth
Chen, Yijia
1
https://orcid.org/0000-0001-7033-9593
Flum, Jörg
2
Fudan University, Shanghai, China
Albert-Ludwigs-Universität Freiburg, Germany
Shrub-depth is a graph invariant often considered as an extension of tree-depth to dense graphs. We show that the model-checking problem of monadic second-order logic on a class of graphs of bounded shrub-depth can be decided by AC^0-circuits after a precomputation on the formula. This generalizes a similar result on graphs of bounded tree-depth [Y. Chen and J. Flum, 2018]. At the core of our proof is the definability in first-order logic of tree-models for graphs of bounded shrub-depth.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.15/LIPIcs.CSL.2020.15.pdf
shrub-depth
model-checking
monadic second-order logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
16:1
16:16
10.4230/LIPIcs.CSL.2020.16
article
Taylor expansion for Call-By-Push-Value
Chouquet, Jules
1
https://orcid.org/0000-0003-2676-0297
Tasson, Christine
2
https://orcid.org/0000-0001-8098-9944
IRIF UMR 8243, Université de Paris, CNRS, France
IRIF UMR 8243, Université Paris Diderot, Sorbonne Paris Cité, CNRS, France
The connection between the Call-By-Push-Value lambda-calculus introduced by Levy and Linear Logic introduced by Girard has been widely explored through a denotational view reflecting the precise ruling of resources in this language. We take a further step in this direction and apply Taylor expansion introduced by Ehrhard and Regnier. We define a resource lambda-calculus in whose terms can be used to approximate terms of Call-By-Push-Value. We show that this approximation is coherent with reduction and with the translations of Call-By-Name and Call-By-Value strategies into Call-By-Push-Value.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.16/LIPIcs.CSL.2020.16.pdf
Call-By-Push-Value
Quantitative semantics
Taylor expansion
Linear Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
17:1
17:17
10.4230/LIPIcs.CSL.2020.17
article
Tangent Categories from the Coalgebras of Differential Categories
Cockett, Robin
1
Lemay, Jean-Simon Pacaud
2
Lucyshyn-Wright, Rory B. B.
3
University of Calgary, Department of Computer Science, Canada
University of Oxford, Department of Computer Science, UK
Brandon University, Department of of Mathematics and Computer Science, Canada
Following the pattern from linear logic, the coKleisli category of a differential category is a Cartesian differential category. What then is the coEilenberg-Moore category of a differential category? The answer is a tangent category! A key example arises from the opposite of the category of Abelian groups with the free exponential modality. The coEilenberg-Moore category, in this case, is the opposite of the category of commutative rings. That the latter is a tangent category captures a fundamental aspect of both algebraic geometry and Synthetic Differential Geometry. The general result applies when there are no negatives and thus encompasses examples arising from combinatorics and computer science.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.17/LIPIcs.CSL.2020.17.pdf
Differential categories
Tangent categories
Coalgebra Modalities
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
18:1
18:16
10.4230/LIPIcs.CSL.2020.18
article
Reverse Derivative Categories
Cockett, Robin
1
Cruttwell, Geoffrey
2
Gallagher, Jonathan
3
Lemay, Jean-Simon Pacaud
4
MacAdam, Benjamin
1
Plotkin, Gordon
5
Pronk, Dorette
3
University of Calgary, Department of Computer Science, Canada
Mount Allison University, Department of , Mathematics and Computer Science, Canada
Dalhousie University, Department of , Mathematics and Statistics, Canada
University of Oxford, Department of Computer Science, UK
Google Research
The reverse derivative is a fundamental operation in machine learning and automatic differentiation [Martín Abadi et al., 2015; Griewank, 2012]. This paper gives a direct axiomatization of a category with a reverse derivative operation, in a similar style to that given by [Blute et al., 2009] for a forward derivative. Intriguingly, a category with a reverse derivative also has a forward derivative, but the converse is not true. In fact, we show explicitly what a forward derivative is missing: a reverse derivative is equivalent to a forward derivative with a dagger structure on its subcategory of linear maps. Furthermore, we show that these linear maps form an additively enriched category with dagger biproducts.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.18/LIPIcs.CSL.2020.18.pdf
Reverse Derivatives
Cartesian Reverse Differential Categories
Categorical Semantics
Cartesian Differential Categories
Dagger Categories
Automatic Differentiation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
19:1
19:18
10.4230/LIPIcs.CSL.2020.19
article
Internal Calculi for Separation Logics
Demri, Stéphane
1
Lozes, Etienne
2
Mansutti, Alessio
1
LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay, France
Université Côte d’Azur, CNRS, I3S, France
We present a general approach to axiomatise separation logics with heaplet semantics with no external features such as nominals/labels. To start with, we design the first (internal) Hilbert-style axiomatisation for the quantifier-free separation logic SL(∗, -*). We instantiate the method by introducing a new separation logic with essential features: it is equipped with the separating conjunction, the predicate ls, and a natural guarded form of first-order quantification. We apply our approach for its axiomatisation. As a by-product of our method, we also establish the exact expressive power of this new logic and we show PSpace-completeness of its satisfiability problem.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.19/LIPIcs.CSL.2020.19.pdf
Separation logic
internal calculus
adjunct/quantifier elimination
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
20:1
20:16
10.4230/LIPIcs.CSL.2020.20
article
Monitoring Event Frequencies
Ferrère, Thomas
1
https://orcid.org/0000-0001-5199-3143
Henzinger, Thomas A.
1
https://orcid.org/0000-0002-2985-7724
Kragl, Bernhard
1
https://orcid.org/0000-0001-7745-9117
IST Austria, Klosterneuburg, Austria
The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.20/LIPIcs.CSL.2020.20.pdf
monitoring
frequency property
Markov chain
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
21:1
21:16
10.4230/LIPIcs.CSL.2020.21
article
Automatic Equivalence Structures of Polynomial Growth
Ganardi, Moses
1
Khoussainov, Bakhadyr
2
University of Siegen, Siegen, Germany
University of Auckland, Auckland, New Zealand
In this paper we study the class EqP of automatic equivalence structures of the form ?=(D, E) where the domain D is a regular language of polynomial growth and E is an equivalence relation on D. Our goal is to investigate the following two foundational problems (in the theory of automatic structures) aimed for the class EqP. The first is to find algebraic characterizations of structures from EqP, and the second is to investigate the isomorphism problem for the class EqP. We provide full solutions to these two problems. First, we produce a characterization of structures from EqP through multivariate polynomials. Second, we present two contrasting results. On the one hand, we prove that the isomorphism problem for structures from the class EqP is undecidable. On the other hand, we prove that the isomorphism problem is decidable for structures from EqP with domains of quadratic growth.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.21/LIPIcs.CSL.2020.21.pdf
automatic structures
polynomial growth
isomorphism problem
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
22:1
22:17
10.4230/LIPIcs.CSL.2020.22
article
Guarded Teams: The Horizontally Guarded Case
Grädel, Erich
1
Otto, Martin
2
RWTH Aachen University, Germany
Technische Universität Darmstadt, Germany
Team semantics admits reasoning about large sets of data, modelled by sets of assignments (called teams), with first-order syntax. This leads to high expressive power and complexity, particularly in the presence of atomic dependency properties for such data sets. It is therefore interesting to explore fragments and variants of logic with team semantics that permit model-theoretic tools and algorithmic methods to control this explosion in expressive power and complexity.
We combine here the study of team semantics with the notion of guarded logics, which are well-understood in the case of classical Tarski semantics, and known to strike a good balance between expressive power and algorithmic manageability. In fact there are two strains of guardedness for teams. Horizontal guardedness requires the individual assignments of the team to be guarded in the usual sense of guarded logics. Vertical guardedness, on the other hand, posits an additional (or definable) hypergraph structure on relational structures in order to interpret a constraint on the component-wise variability of assignments within teams.
In this paper we investigate the horizontally guarded case. We study horizontally guarded logics for teams and appropriate notions of guarded team bisimulation. In particular, we establish characterisation theorems that relate invariance under guarded team bisimulation with guarded team logics, but also with logics under classical Tarski semantics.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.22/LIPIcs.CSL.2020.22.pdf
Team semantics
guarded logics
bisimulation
characterisation theorems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
23:1
23:16
10.4230/LIPIcs.CSL.2020.23
article
Order-Invariant First-Order Logic over Hollow Trees
Grange, Julien
1
Segoufin, Luc
2
ENS Paris & PSL & INRIA & CNRS, France
INRIA & ENS Paris & PSL, France
We show that the expressive power of order-invariant first-order logic collapses to first-order logic over hollow trees. A hollow tree is an unranked ordered tree where every non leaf node has at most four adjacent nodes: two siblings (left and right) and its first and last children. In particular there is no predicate for the linear order among siblings nor for the descendant relation. Moreover only the first and last nodes of a siblinghood are linked to their parent node, and the parent-child relation cannot be completely reconstructed in first-order.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.23/LIPIcs.CSL.2020.23.pdf
order-invariance
first-order logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
24:1
24:18
10.4230/LIPIcs.CSL.2020.24
article
Glueability of Resource Proof-Structures: Inverting the Taylor Expansion
Guerrieri, Giulio
1
https://orcid.org/0000-0002-0469-4279
Pellissier, Luc
2
https://orcid.org/0000-0003-1923-8193
Tortora de Falco, Lorenzo
3
University of Bath, Department of Computer Science, Bath, UK
Université de Paris, IRIF, CNRS, F-75013 Paris, France
Università Roma Tre, Dipartimento di Matematica e Fisica, Rome, Italy
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.24/LIPIcs.CSL.2020.24.pdf
linear logic
Taylor expansion
proof-net
natural transformation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
25:1
25:16
10.4230/LIPIcs.CSL.2020.25
article
On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics
Hoelzel, Matthias
1
Wilke, Richard
1
Mathematical Foundations of Computer Science, RWTH Aachen University, Aachen, Germany
We present syntactic characterisations for the union closed fragments of existential second-order logic and of logics with team semantics. Since union closure is a semantical and undecidable property, the normal form we introduce enables the handling and provides a better understanding of this fragment. We also introduce inclusion-exclusion games that turn out to be precisely the corresponding model-checking games. These games are not only interesting in their own right, but they also are a key factor towards building a bridge between the semantic and syntactic fragments. On the level of logics with team semantics we additionally present restrictions of inclusion-exclusion logic to capture the union closed fragment. Moreover, we define a team based atom that when adding it to first-order logic also precisely captures the union closed fragment of existential second-order logic which answers an open question by Galliani and Hella.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.25/LIPIcs.CSL.2020.25.pdf
Higher order logic
Existential second-order logic
Team semantics
Closure properties
Union closure
Model-checking games
Syntactic charactisations of semantical fragments
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
26:1
26:18
10.4230/LIPIcs.CSL.2020.26
article
Expressive Logics for Coinductive Predicates
Kupke, Clemens
1
Rot, Jurriaan
2
Strathclyde University, United Kingdom
University College London, United Kingdom and Radboud University, The Netherlands
The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.26/LIPIcs.CSL.2020.26.pdf
Coalgebra
Fibration
Modal Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
27:1
27:16
10.4230/LIPIcs.CSL.2020.27
article
State Space Reduction For Parity Automata
Löding, Christof
1
Tollkötter, Andreas
1
https://orcid.org/0000-0003-2685-2132
RWTH Aachen University, Germany
Exact minimization of ω-automata is a difficult problem and heuristic algorithms are a subject of current research. We propose several new approaches to reduce the state space of deterministic parity automata. These are based on extracting information from structures within the automaton, such as strongly connected components, coloring of the states, and equivalence classes of given relations, to determine states that can safely be merged. We also establish a framework to generalize the notion of quotient automata and uniformly describe such algorithms. The description of these procedures consists of a theoretical analysis as well as data collected from experiments.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.27/LIPIcs.CSL.2020.27.pdf
automata
ω-automata
parity
minimization
state space reduction
deterministic
simulation relations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
28:1
28:16
10.4230/LIPIcs.CSL.2020.28
article
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
Lyon, Tim
1
https://orcid.org/0000-0003-3214-0828
Tiu, Alwen
2
Goré, Rajeev
2
Clouston, Ranald
2
Institut für Logic and Computation, Technische Universität Wien, Austria
Research School of Computer Science, The Australian National University, Australia
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.28/LIPIcs.CSL.2020.28.pdf
Bi-intuitionistic logic
Interpolation
Nested calculi
Proof theory
Sequents
Tense logics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
29:1
29:16
10.4230/LIPIcs.CSL.2020.29
article
The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas
Mascle, Corto
1
Zimmermann, Martin
2
https://orcid.org/0000-0002-8038-2453
ENS Paris-Saclay, Cachan, France
University of Liverpool, Liverpool, United Kingdom
HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protocols and coding theory. However, HyperLTL satisfiability is undecidable as soon as there are existential quantifiers in the scope of a universal one. To overcome this severe limitation to applicability, we investigate here restricted variants of the satisfiability problem to pinpoint the decidability border.
First, we restrict the space of admissible models and show decidability when restricting the search space to models of bounded size or to finitely representable ones. Second, we consider formulas with restricted nesting of temporal operators and show that nesting depth one yields decidability for a slightly larger class of quantifier prefixes. We provide tight complexity bounds in almost all cases.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.29/LIPIcs.CSL.2020.29.pdf
Hyperproperties
Linear Temporal Logic
Satisfiability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
30:1
30:18
10.4230/LIPIcs.CSL.2020.30
article
Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models
Miquey, Étienne
1
Équipe Gallinette, INRIA, LS2N, Université de Nantes, France
In an impressive series of papers, Krivine showed at the edge of the last decade how classical realizability provides a surprising technique to build models for classical theories. In particular, he proved that classical realizability subsumes Cohen’s forcing, and even more, gives rise to unexpected models of set theories. Pursuing the algebraic analysis of these models that was first undertaken by Streicher, Miquel recently proposed to lay the algebraic foundation of classical realizability and forcing within new structures which he called implicative algebras. These structures are a generalization of Boolean algebras based on an internal law representing the implication. Notably, implicative algebras allow for the adequate interpretation of both programs (i.e. proofs) and their types (i.e. formulas) in the same structure.
The very definition of implicative algebras takes position on a presentation of logic through universal quantification and the implication and, computationally, relies on the call-by-name λ-calculus. In this paper, we investigate the relevance of this choice, by introducing two similar structures. On the one hand, we define disjunctive algebras, which rely on internal laws for the negation and the disjunction and which we show to be particular cases of implicative algebras. On the other hand, we introduce conjunctive algebras, which rather put the focus on conjunctions and on the call-by-value evaluation strategy. We finally show how disjunctive and conjunctive algebras algebraically reflect the well-known duality of computation between call-by-name and call-by-value.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.30/LIPIcs.CSL.2020.30.pdf
realizability
model theory
forcing
proofs-as-programs
λ-calculus
classical logic
duality
call-by-value
call-by-name
lattices
tripos
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
31:1
31:17
10.4230/LIPIcs.CSL.2020.31
article
Separation and Renaming in Nominal Sets
Moerman, Joshua
1
Rot, Jurriaan
2
RWTH Aachen University, Germany
University College London, United Kingdom and Radboud University, The Netherlands
Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. We show that these automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.31/LIPIcs.CSL.2020.31.pdf
Nominal sets
Separated product
Adjunction
Automata
Coalgebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
32:1
32:15
10.4230/LIPIcs.CSL.2020.32
article
Parity Games: Another View on Lehtinen’s Algorithm
Parys, Paweł
1
https://orcid.org/0000-0001-7247-1408
Institute of Informatics, University of Warsaw, Poland
Recently, five quasi-polynomial-time algorithms solving parity games were proposed. We elaborate on one of the algorithms, by Lehtinen (2018).
Czerwiński et al. (2019) observe that four of the algorithms can be expressed as constructions of separating automata (of quasi-polynomial size), that is, automata that accept all plays decisively won by one of the players, and rejecting all plays decisively won by the other player. The separating automata corresponding to three of the algorithms are deterministic, and it is clear that deterministic separating automata can be used to solve parity games. The separating automaton corresponding to the algorithm of Lehtinen is nondeterministic, though. While this particular automaton can be used to solve parity games, this is not true for every nondeterministic separating automaton. As a first (more conceptual) contribution, we specify when a nondeterministic separating automaton can be used to solve parity games.
We also repeat the correctness proof of the Lehtinen’s algorithm, using separating automata. In this part, we prove that her construction actually leads to a faster algorithm than originally claimed in her paper: its complexity is n^{O(log n)} rather than n^{O(log d ⋅ log n)} (where n is the number of nodes, and d the number of priorities of a considered parity game), which is similar to complexities of the other quasi-polynomial-time algorithms.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.32/LIPIcs.CSL.2020.32.pdf
Parity games
quasi-polynomial time
separating automata
good-for-games automata
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
33:1
33:16
10.4230/LIPIcs.CSL.2020.33
article
De Jongh’s Theorem for Intuitionistic Zermelo-Fraenkel Set Theory
Passmann, Robert
1
https://orcid.org/0000-0002-7170-3286
Institute for Logic, Language and Computation, University of Amsterdam, The Netherlands
We prove that the propositional logic of intuitionistic set theory IZF is intuitionistic propositional logic IPC. More generally, we show that IZF has the de Jongh property with respect to every intermediate logic that is complete with respect to a class of finite trees. The same results follow for constructive set theory CZF.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.33/LIPIcs.CSL.2020.33.pdf
Intuitionistic Logic
Intuitionistic Set Theory
Constructive Set Theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
34:1
34:17
10.4230/LIPIcs.CSL.2020.34
article
Computing Haar Measures
Pauly, Arno
1
https://orcid.org/0000-0002-0173-3295
Seon, Dongseong
2
Ziegler, Martin
2
Swansea University, UK
KAIST, Daejeon, Republic of Korea
According to Haar’s Theorem, every compact topological group G admits a unique (regular, right and) left-invariant Borel probability measure μ_G. Let the Haar integral (of G) denote the functional ∫_G:?(G)∋ f ↦ ∫ f d μ_G integrating any continuous function f:G → ℝ with respect to μ_G. This generalizes, and recovers for the additive group G=[0;1)mod 1, the usual Riemann integral: computable (cmp. Weihrauch 2000, Theorem 6.4.1), and of computational cost characterizing complexity class #P_1 (cmp. Ko 1991, Theorem 5.32).
We establish that in fact, every computably compact computable metric group renders the Haar measure/integral computable: once using an elegant synthetic argument, exploiting uniqueness in a computably compact space of probability measures; and once presenting and analyzing an explicit, imperative algorithm based on "maximum packings" with rigorous error bounds and guaranteed convergence. Regarding computational complexity, for the groups SO(3) and SU(2), we reduce the Haar integral to and from Euclidean/Riemann integration. In particular both also characterize #P_1.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.34/LIPIcs.CSL.2020.34.pdf
Computable analysis
topological groups
exact real arithmetic
Haar measure
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
35:1
35:12
10.4230/LIPIcs.CSL.2020.35
article
The Call-By-Value Lambda-Calculus with Generalized Applications
Espírito Santo, José
1
https://orcid.org/0000-0002-6348-5653
Centre of Mathematics, University of Minho, Portugal
The lambda-calculus with generalized applications is the Curry-Howard counterpart to the system of natural deduction with generalized elimination rules for intuitionistic implicational logic. In this paper we identify a call-by-value variant of the system and prove confluence, strong normalization, and standardization. In the end, we show that the cbn and cbv variants of the system simulate each other via mappings based on extensions of the "protecting-by-a-lambda" compilation technique.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.35/LIPIcs.CSL.2020.35.pdf
Generalized applications
Natural deduction
Strong normalization
Standardization
Call-by-name
Call-by-value
Protecting-by-a-lambda
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
36:1
36:17
10.4230/LIPIcs.CSL.2020.36
article
Dynamic Complexity Meets Parameterised Algorithms
Schmidt, Jonas
1
Schwentick, Thomas
1
Vortmeier, Nils
1
Zeume, Thomas
1
Kokkinis, Ioannis
1
TU Dortmund University, Dortmund, Germany
Dynamic Complexity studies the maintainability of queries with logical formulas in a setting where the underlying structure or database changes over time. Most often, these formulas are from first-order logic, giving rise to the dynamic complexity class DynFO. This paper investigates extensions of DynFO in the spirit of parameterised algorithms. In this setting structures come with a parameter k and the extensions allow additional "space" of size f(k) (in the form of an additional structure of this size) or additional time f(k) (in the form of iterations of formulas) or both. The resulting classes are compared with their non-dynamic counterparts and other classes. The main part of the paper explores the applicability of methods for parameterised algorithms to this setting through case studies for various well-known parameterised problems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.36/LIPIcs.CSL.2020.36.pdf
Dynamic complexity
parameterised complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-01-06
152
37:1
37:16
10.4230/LIPIcs.CSL.2020.37
article
Dynamic Complexity of Parity Exists Queries
Vortmeier, Nils
1
Zeume, Thomas
1
TU Dortmund University, Dortmund, Germany
Given a graph whose nodes may be coloured red, the parity of the number of red nodes can easily be maintained with first-order update rules in the dynamic complexity framework DynFO of Patnaik and Immerman. Can this be generalised to other or even all queries that are definable in first-order logic extended by parity quantifiers? We consider the query that asks whether the number of nodes that have an edge to a red node is odd. Already this simple query of quantifier structure parity-exists is a major roadblock for dynamically capturing extensions of first-order logic.
We show that this query cannot be maintained with quantifier-free first-order update rules, and that variants induce a hierarchy for such update rules with respect to the arity of the maintained auxiliary relations. Towards maintaining the query with full first-order update rules, it is shown that degree-restricted variants can be maintained.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol152-csl2020/LIPIcs.CSL.2020.37/LIPIcs.CSL.2020.37.pdf
Dynamic complexity
parity quantifier
arity hierarchy