Volume
LIPIcs, Volume 182
40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)
Event
FSTTCS 2020, December 14-18, 2020, BITS Pilani, K K Birla Goa Campus, Goa, India (Virtual Conference)Editors
Publication Details
- published at: 2020-12-04
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-174-0
- DBLP: db/conf/fsttcs/fsttcs2020
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 182, FSTTCS 2020, Complete Volume
Abstract
LIPIcs, Volume 182, FSTTCS 2020, Complete Volume
Cite as
40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 1-912, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Proceedings{saxena_et_al:LIPIcs.FSTTCS.2020,
title = {{LIPIcs, Volume 182, FSTTCS 2020, Complete Volume}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {1--912},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020},
URN = {urn:nbn:de:0030-drops-132401},
doi = {10.4230/LIPIcs.FSTTCS.2020},
annote = {Keywords: LIPIcs, Volume 182, FSTTCS 2020, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{saxena_et_al:LIPIcs.FSTTCS.2020.0,
author = {Saxena, Nitin and Simon, Sunil},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {0:i--0:xvi},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.0},
URN = {urn:nbn:de:0030-drops-132413},
doi = {10.4230/LIPIcs.FSTTCS.2020.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
The Quest for Mathematical Understanding of Deep Learning (Invited Talk)
Abstract
Deep learning has transformed Machine Learning and Artificial Intelligence in the past decade. It raises fundamental questions for mathematics and theory of computer science, since it relies upon solving large-scale nonconvex problems via gradient descent and its variants. This talk will be an introduction to mathematical questions raised by deep learning, and some partial understanding obtained in recent years.
Cite as
Sanjeev Arora. The Quest for Mathematical Understanding of Deep Learning (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{arora:LIPIcs.FSTTCS.2020.1,
author = {Arora, Sanjeev},
title = {{The Quest for Mathematical Understanding of Deep Learning}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.1},
URN = {urn:nbn:de:0030-drops-132427},
doi = {10.4230/LIPIcs.FSTTCS.2020.1},
annote = {Keywords: machine learning, artificial intelligence, deep learning, gradient descent, optimization}
}
Document
Invited Talk
Proofs of Soundness and Proof Search (Invited Talk)
Abstract
Let P be a sound proof system for propositional logic. For each CNF formula F, let SAT(F) be a CNF formula whose satisfying assignments are in 1-to-1 correspondence with those of F (e.g., F itself). For each integer s, let REF(F,s) be a CNF formula whose satisfying assignments are in 1-to-1 correspondence with the P-refutations of F of length s. Since P is sound, it is obvious that the conjunction formula SAT(F) & REF(F,s) is unsatisfiable for any choice of F and s. It has been long known that, for many natural proof systems P and for the most natural formalizations of the formulas SAT and REF, the unsatisfiability of SAT(F) & REF(F,s) can be established by a short refutation. In addition, for many P, these short refutations live in the proof system P itself. This is the case for all Frege proof systems. In contrast it was known since the early 2000’s that Resolution proofs of Resolution’s soundness statements must have superpolynomial length. In this talk I will explain how the soundness formulas for a proof system P relate to the computational complexity of the proof search problem for P. In particular, I will explain how such formulas are used in the recent proof that the problem of approximating the minimum proof-length for Resolution is NP-hard (Atserias-Müller 2019). Besides playing a key role in this hardness of approximation result, the renewed interest in the soundness formulas led to a complete answer to the question whether Resolution has subexponential-length proofs of its own soundness statements (Garlík 2019).
Cite as
Albert Atserias. Proofs of Soundness and Proof Search (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{atserias:LIPIcs.FSTTCS.2020.2,
author = {Atserias, Albert},
title = {{Proofs of Soundness and Proof Search}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.2},
URN = {urn:nbn:de:0030-drops-132439},
doi = {10.4230/LIPIcs.FSTTCS.2020.2},
annote = {Keywords: Proof complexity, automatability, Resolution, proof search, consistency statements, lower bounds, reflection principle, satisfiability}
}
Document
Invited Talk
Convex Optimization and Dynamic Data Structure (Invited Talk)
Abstract
In the last three years, there are many breakthroughs in optimization such as nearly quadratic time algorithms for bipartite matching, linear programming algorithms that are as fast as Ax = b. All of these algorithms are based on a careful combination of optimization techniques and dynamic data structures. In this talk, we will explain the framework underlying all the recent breakthroughs.
Joint work with Jan van den Brand, Michael B. Cohen, Sally Dong, Haotian Jiang, Tarun Kathuria, Danupon Nanongkai, Swati Padmanabhan, Richard Peng, Thatchaphol Saranurak, Aaron Sidford, Zhao Song, Di Wang, Sam Chiu-wai Wong, Guanghao Ye, Qiuyi Zhang.
Cite as
Yin Tat Lee. Convex Optimization and Dynamic Data Structure (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{lee:LIPIcs.FSTTCS.2020.3,
author = {Lee, Yin Tat},
title = {{Convex Optimization and Dynamic Data Structure}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.3},
URN = {urn:nbn:de:0030-drops-132440},
doi = {10.4230/LIPIcs.FSTTCS.2020.3},
annote = {Keywords: Convex Optimization, Dynamic Data Structure}
}
Document
Invited Talk
Holonomic Techniques, Periods, and Decision Problems (Invited Talk)
Abstract
Holonomic techniques have deep roots going back to Wallis, Euler, and Gauss, and have evolved in modern times as an important subfield of computer algebra, thanks in large part to the work of Zeilberger and others over the past three decades. In this talk, I will give an overview of the area, and in particular will present a select survey of known and original results on decision problems for holonomic sequences and functions. (Holonomic sequences satisfy linear recurrence relations with polynomial coefficients, and holonomic functions satisfy linear differential equations with polynomial coefficients.) I will also discuss some surprising connections to the theory of periods and exponential periods, which are classical objects of study in algebraic geometry and number theory; in particular, I will relate the decidability of certain decision problems for holonomic sequences to deep conjectures about periods and exponential periods, notably those due to Kontsevich and Zagier.
Cite as
Joël Ouaknine. Holonomic Techniques, Periods, and Decision Problems (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{ouaknine:LIPIcs.FSTTCS.2020.4,
author = {Ouaknine, Jo\"{e}l},
title = {{Holonomic Techniques, Periods, and Decision Problems}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {4:1--4:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.4},
URN = {urn:nbn:de:0030-drops-132451},
doi = {10.4230/LIPIcs.FSTTCS.2020.4},
annote = {Keywords: holonomic techniques, decision problems, recurrence sequences, minimal solutions, Positivity Problem, continued fractions, special functions, periods, exponential periods}
}
Document
Invited Talk
Algorithmic Improvisation for Dependable Intelligent Autonomy (Invited Talk)
Abstract
Algorithmic Improvisation, also called control improvisation or controlled improvisation, is a new framework for automatically synthesizing systems with specified random but controllable behavior. In this talk, I will present the theory of algorithmic improvisation and show how it can be used in a wide variety of applications where randomness can provide variety, robustness, or unpredictability while guaranteeing safety or other properties. Applications demonstrated to date include robotic surveillance, software fuzz testing, music improvisation, human modeling, generating test cases for simulating cyber-physical systems, and generation of synthetic data sets to train and test machine learning algorithms. In this talk, I will particularly focus on applications to the design of intelligent autonomous systems, presenting work on randomized planning for robotics and a domain-specific probabilistic programming language for the design and analysis of learning-based autonomous systems.
Cite as
Sanjit A. Seshia. Algorithmic Improvisation for Dependable Intelligent Autonomy (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{seshia:LIPIcs.FSTTCS.2020.5,
author = {Seshia, Sanjit A.},
title = {{Algorithmic Improvisation for Dependable Intelligent Autonomy}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {5:1--5:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.5},
URN = {urn:nbn:de:0030-drops-132465},
doi = {10.4230/LIPIcs.FSTTCS.2020.5},
annote = {Keywords: Formal methods, synthesis, verification, randomized algorithms, formal specification, testing, machine learning, synthetic data generation, planning}
}
Document
Invited Talk
On Some Recent Advances in Algebraic Complexity (Invited Talk)
Abstract
Algebraic complexity is the field studying the intrinsic difficulty of algebraic problems in an algebraic model of computation, most notably arithmetic circuits. It is a very natural model of computation that attracted a large amount of research in the last few decades, partially due to its simplicity and elegance, but mostly because of its importance. Being a more structured model than Boolean circuits, one could hope that the fundamental problems of theoretical computer science, such as separating P from NP, deciding whether P = BPP and more, will be easier to solve for arithmetic circuits.
In this talk I will give the basic definitions, explain the main questions and how they relate to their Boolean counterparts, and discuss what I view as promising approaches to tackling the most fundamental problems in the field.
Cite as
Amir Shpilka. On Some Recent Advances in Algebraic Complexity (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, p. 6:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{shpilka:LIPIcs.FSTTCS.2020.6,
author = {Shpilka, Amir},
title = {{On Some Recent Advances in Algebraic Complexity}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {6:1--6:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.6},
URN = {urn:nbn:de:0030-drops-132472},
doi = {10.4230/LIPIcs.FSTTCS.2020.6},
annote = {Keywords: Algebraic Complexity, Arithmetic Circuits, Polynomial Identity Testing}
}
Document
Faster Property Testers in a Variation of the Bounded Degree Model
Abstract
Property testing algorithms are highly efficient algorithms, that come with probabilistic accuracy guarantees. For a property P, the goal is to distinguish inputs that have P from those that are far from having P with high probability correctly, by querying only a small number of local parts of the input. In property testing on graphs, the distance is measured by the number of edge modifications (additions or deletions), that are necessary to transform a graph into one with property P. Much research has focussed on the query complexity of such algorithms, i. e. the number of queries the algorithm makes to the input, but in view of applications, the running time of the algorithm is equally relevant.
In (Adler, Harwath STACS 2018), a natural extension of the bounded degree graph model of property testing to relational databases of bounded degree was introduced, and it was shown that on databases of bounded degree and bounded tree-width, every property that is expressible in monadic second-order logic with counting (CMSO) is testable with constant query complexity and sublinear running time. It remains open whether this can be improved to constant running time.
In this paper we introduce a new model, which is based on the bounded degree model, but the distance measure allows both edge (tuple) modifications and vertex (element) modifications. Our main theorem shows that on databases of bounded degree and bounded tree-width, every property that is expressible in CMSO is testable with constant query complexity and constant running time in the new model. We also show that every property that is testable in the classical model is testable in our model with the same query complexity and running time, but the converse is not true.
We argue that our model is natural and our meta-theorem showing constant-time CMSO testability supports this.
Cite as
Isolde Adler and Polly Fahey. Faster Property Testers in a Variation of the Bounded Degree Model. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{adler_et_al:LIPIcs.FSTTCS.2020.7,
author = {Adler, Isolde and Fahey, Polly},
title = {{Faster Property Testers in a Variation of the Bounded Degree Model}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {7:1--7:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.7},
URN = {urn:nbn:de:0030-drops-132482},
doi = {10.4230/LIPIcs.FSTTCS.2020.7},
annote = {Keywords: Constant Time Algorithms, Logic and Databases, Property Testing, Bounded Degree Model}
}
Document
Clustering Under Perturbation Stability in Near-Linear Time
Abstract
We consider the problem of center-based clustering in low-dimensional Euclidean spaces under the perturbation stability assumption. An instance is α-stable if the underlying optimal clustering continues to remain optimal even when all pairwise distances are arbitrarily perturbed by a factor of at most α. Our main contribution is in presenting efficient exact algorithms for α-stable clustering instances whose running times depend near-linearly on the size of the data set when α ≥ 2 + √3. For k-center and k-means problems, our algorithms also achieve polynomial dependence on the number of clusters, k, when α ≥ 2 + √3 + ε for any constant ε > 0 in any fixed dimension. For k-median, our algorithms have polynomial dependence on k for α > 5 in any fixed dimension; and for α ≥ 2 + √3 in two dimensions. Our algorithms are simple, and only require applying techniques such as local search or dynamic programming to a suitably modified metric space, combined with careful choice of data structures.
Cite as
Pankaj K. Agarwal, Hsien-Chih Chang, Kamesh Munagala, Erin Taylor, and Emo Welzl. Clustering Under Perturbation Stability in Near-Linear Time. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{agarwal_et_al:LIPIcs.FSTTCS.2020.8,
author = {Agarwal, Pankaj K. and Chang, Hsien-Chih and Munagala, Kamesh and Taylor, Erin and Welzl, Emo},
title = {{Clustering Under Perturbation Stability in Near-Linear Time}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {8:1--8:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.8},
URN = {urn:nbn:de:0030-drops-132492},
doi = {10.4230/LIPIcs.FSTTCS.2020.8},
annote = {Keywords: clustering, stability, local search, dynamic programming, coreset, polyhedral metric, trapezoid decomposition, range query}
}
Document
Width Notions for Ordering-Related Problems
Abstract
We are studying a weighted version of a linear extension problem, given some finite partial order ρ, called Completion of an Ordering. While this problem is NP-complete, we show that it lies in FPT when parameterized by the interval width of ρ. This ordering problem can be used to model several ordering problems stemming from diverse application areas, such as graph drawing, computational social choice, or computer memory management. Each application yields a special ρ. We also relate the interval width of ρ to parameterizations such as maximum range that have been introduced earlier in these applications, sometimes improving on parameterized algorithms that have been developed for these parameterizations before. This approach also gives some practical sub-exponential time algorithms for ordering problems.
Cite as
Emmanuel Arrighi, Henning Fernau, Mateus de Oliveira Oliveira, and Petra Wolf. Width Notions for Ordering-Related Problems. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{arrighi_et_al:LIPIcs.FSTTCS.2020.9,
author = {Arrighi, Emmanuel and Fernau, Henning and de Oliveira Oliveira, Mateus and Wolf, Petra},
title = {{Width Notions for Ordering-Related Problems}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.9},
URN = {urn:nbn:de:0030-drops-132505},
doi = {10.4230/LIPIcs.FSTTCS.2020.9},
annote = {Keywords: Parameterized algorithms, interval width, linear extension, one-sided crossing minimization, Kemeny rank aggregation, grouping by swapping}
}
Document
Optimal Output Sensitive Fault Tolerant Cuts
Abstract
In this paper we consider two classic cut-problems, Global Min-Cut and Min k-Cut, via the lens of fault tolerant network design. In particular, given a graph G on n vertices, and a positive integer f, our objective is to compute an upper bound on the size of the sparsest subgraph H of G that preserves edge connectivity of G (denoted by λ(G)) in the case of Global Min-Cut, and λ(G,k) (denotes the minimum number of edges whose removal would partition the graph into at least k connected components) in the case of Min k-Cut, upon failure of any f edges of G. The subgraph H corresponding to Global Min-Cut and Min k-Cut is called f-FTCS and f-FT-k-CS, respectively. We obtain the following results about the sizes of f-FTCS and f-FT-k-CS.
- There exists an f-FTCS with (n-1)(f+λ(G)) edges. We complement this upper bound with a matching lower bound, by constructing an infinite family of graphs where any f-FTCS must have at least ((n-λ(G)-1)(λ(G)+f-1))/2+(n-λ(G)-1)+/λ(G)(λ(G)+1))/2 edges.
- There exists an f-FT-k-CS with min{(2f+λ(G,k)-(k-1))(n-1), (f+λ(G,k))(n-k)+𝓁} edges. We complement this upper bound with a lower bound, by constructing an infinite family of graphs where any f-FT-k-CS must have at least ((n-λ(G,k)-1)(λ(G,k)+f-k+1))/2)+n-λ(G,k)+k-3+((λ(G,k)-k+3)(λ(G,k)-k+2))/2 edges. Our upper bounds exploit the structural properties of k-connectivity certificates. On the other hand, for our lower bounds we construct an infinite family of graphs, such that for any graph in the family any f-FTCS (or f-FT-k-CS) must contain all its edges. We also add that our upper bounds are constructive. That is, there exist polynomial time algorithms that construct H with the aforementioned number of edges.
Cite as
Niranka Banerjee, Venkatesh Raman, and Saket Saurabh. Optimal Output Sensitive Fault Tolerant Cuts. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{banerjee_et_al:LIPIcs.FSTTCS.2020.10,
author = {Banerjee, Niranka and Raman, Venkatesh and Saurabh, Saket},
title = {{Optimal Output Sensitive Fault Tolerant Cuts}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.10},
URN = {urn:nbn:de:0030-drops-132515},
doi = {10.4230/LIPIcs.FSTTCS.2020.10},
annote = {Keywords: Fault tolerant, minimum cuts, upper bound, lower bound}
}
Document
Online Matching with Recourse: Random Edge Arrivals
Abstract
The matching problem in the online setting models the following situation: we are given a set of servers in advance, the clients arrive one at a time, and each client has edges to some of the servers. Each client must be matched to some incident server upon arrival (or left unmatched) and the algorithm is not allowed to reverse its decisions. Due to this no-reversal restriction, we are not able to guarantee an exact maximum matching in this model, only an approximate one.
Therefore, it is natural to study a different setting, where the top priority is to match as many clients as possible, and changes to the matching are possible but expensive. Formally, the goal is to always maintain a maximum matching while minimizing the number of changes made to the matching (denoted the recourse). This model is called the online model with recourse, and has been studied extensively over the past few years. For the specific problem of matching, the focus has been on vertex-arrival model, where clients arrive one at a time with all their edges. A recent result of Bernstein et al. [Bernstein et al., 2019] gives an upper bound of O (nlog² n) recourse for the case of general bipartite graphs. For trees the best known bound is O(nlog n) recourse, due to Bosek et al. [Bosek et al., 2018]. These are nearly tight, as a lower bound of Ω(nlog n) is known.
In this paper, we consider the more general model where all the vertices are known in advance, but the edges of the graph are revealed one at a time. Even for the simple case where the graph is a path, there is a lower bound of Ω(n²). Therefore, we instead consider the natural relaxation where the graph is worst-case, but the edges are revealed in a random order. This relaxation is motivated by the fact that in many related models, such as the streaming setting or the standard online setting without recourse, faster algorithms have been obtained for the matching problem when the input comes in a random order. Our results are as follows:
- Our main result is that for the case of general (non-bipartite) graphs, the problem with random edge arrivals is almost as hard as in the adversarial setting: we show a family of graphs for which the expected recourse is Ω(n²/log n).
- We show that for some special cases of graphs, random arrival is significantly easier. For the case of trees, we get an upper bound of O(nlog²n) on the expected recourse. For the case of paths, this upper bound is O(nlog n). We also show that the latter bound is tight, i.e. that the expected recourse is at least Ω(nlog n).
Cite as
Aaron Bernstein and Aditi Dudeja. Online Matching with Recourse: Random Edge Arrivals. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bernstein_et_al:LIPIcs.FSTTCS.2020.11,
author = {Bernstein, Aaron and Dudeja, Aditi},
title = {{Online Matching with Recourse: Random Edge Arrivals}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {11:1--11:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.11},
URN = {urn:nbn:de:0030-drops-132521},
doi = {10.4230/LIPIcs.FSTTCS.2020.11},
annote = {Keywords: matchings, edge-arrival, online model}
}
Document
Hard QBFs for Merge Resolution
Abstract
We prove the first proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together with information on countermodels, which are syntactically stored in the proofs as merge maps. As demonstrated in [Olaf Beyersdorff et al., 2020], this makes MRes quite powerful: it has strategy extraction by design and allows short proofs for formulas which are hard for classical QBF resolution systems.
Here we show the first exponential lower bounds for MRes, thereby uncovering limitations of MRes. Technically, the results are either transferred from bounds from circuit complexity (for restricted versions of MRes) or directly obtained by combinatorial arguments (for full MRes). Our results imply that the MRes approach is largely orthogonal to other QBF resolution models such as the QCDCL resolution systems QRes and QURes and the expansion systems ∀Exp+Res and IR.
Cite as
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, and Gaurav Sood. Hard QBFs for Merge Resolution. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2020.12,
author = {Beyersdorff, Olaf and Blinkhorn, Joshua and Mahajan, Meena and Peitl, Tom\'{a}\v{s} and Sood, Gaurav},
title = {{Hard QBFs for Merge Resolution}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {12:1--12:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.12},
URN = {urn:nbn:de:0030-drops-132530},
doi = {10.4230/LIPIcs.FSTTCS.2020.12},
annote = {Keywords: QBF, resolution, proof complexity, lower bounds}
}
Document
On Sampling Based Algorithms for k-Means
Abstract
We generalise the results of Bhattacharya et al. [Bhattacharya et al., 2018] for the list-k-means problem defined as - for a (unknown) partition X₁, ..., X_k of the dataset X ⊆ ℝ^d, find a list of k-center-sets (each element in the list is a set of k centers) such that at least one of k-center-sets {c₁, ..., c_k} in the list gives an (1+ε)-approximation with respect to the cost function min_{permutation π} [∑_{i = 1}^{k} ∑_{x ∈ X_i} ||x - c_{π(i)}||²]. The list-k-means problem is important for the constrained k-means problem since algorithms for the former can be converted to {PTAS} for various versions of the latter. The algorithm for the list-k-means problem by Bhattacharya et al. is a D²-sampling based algorithm that runs in k iterations. Making use of a constant factor solution for the (classical or unconstrained) k-means problem, we generalise the algorithm of Bhattacharya et al. in two ways - (i) for any fixed set X_{j₁}, ..., X_{j_t} of t ≤ k clusters, the algorithm produces a list of (k/(ε))^{O(t/(ε))} t-center sets such that (w.h.p.) at least one of them is good for X_{j₁}, ..., X_{j_t}, and (ii) the algorithm runs in a single iteration. Following are the consequences of our generalisations:
1) Faster PTAS under stability and a parameterised reduction: Property (i) of our generalisation is useful in scenarios where finding good centers becomes easier once good centers for a few "bad" clusters have been chosen. One such case is clustering under stability of Awasthi et al. [Awasthi et al., 2010] where the number of such bad clusters is a constant. Using property (i), we significantly improve the running time of their algorithm from O(dn³) (k log{n})^{poly(1/(β), 1/(ε))} to O (dn³ (k/(ε)) ^{O(1/βε²)}). Another application is a parameterised reduction from the outlier version of k-means to the classical one where the bad clusters are the outliers.
2) Streaming algorithms: The sampling algorithm running in a single iteration (i.e., property (ii)) allows us to design a constant-pass, logspace streaming algorithm for the list-k-means problem. This can be converted to a constant-pass, logspace streaming PTAS for various constrained versions of the k-means problem. In particular, this gives a 3-pass, polylog-space streaming PTAS for the constrained binary k-means problem which in turn gives a 4-pass, polylog-space streaming PTAS for the generalised binary 𝓁₀-rank-r approximation problem. This is the first constant pass, polylog-space streaming algorithm for either of the two problems. Coreset based techniques, which is another approach for designing streaming algorithms in general, is not known to work for the constrained binary k-means problem to the best of our knowledge.
Cite as
Anup Bhattacharya, Dishant Goyal, Ragesh Jaiswal, and Amit Kumar. On Sampling Based Algorithms for k-Means. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bhattacharya_et_al:LIPIcs.FSTTCS.2020.13,
author = {Bhattacharya, Anup and Goyal, Dishant and Jaiswal, Ragesh and Kumar, Amit},
title = {{On Sampling Based Algorithms for k-Means}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.13},
URN = {urn:nbn:de:0030-drops-132549},
doi = {10.4230/LIPIcs.FSTTCS.2020.13},
annote = {Keywords: k-means, low rank approximation}
}
Document
String Indexing for Top-k Close Consecutive Occurrences
Abstract
The classic string indexing problem is to preprocess a string S into a compact data structure that supports efficient subsequent pattern matching queries, that is, given a pattern string P, report all occurrences of P within S. In this paper, we study a basic and natural extension of string indexing called the string indexing for top-k close consecutive occurrences problem (Sitcco). Here, a consecutive occurrence is a pair (i,j), i < j, such that P occurs at positions i and j in S and there is no occurrence of P between i and j, and their distance is defined as j-i. Given a pattern P and a parameter k, the goal is to report the top-k consecutive occurrences of P in S of minimal distance. The challenge is to compactly represent S while supporting queries in time close to the length of P and k. We give two time-space trade-offs for the problem. Let n be the length of S, m the length of P, and ε ∈ (0,1]. Our first result achieves O(nlog n) space and optimal query time of O(m+k), and our second result achieves linear space and query time O(m+k^{1+ε}). Along the way, we develop several techniques of independent interest, including a new translation of the problem into a line segment intersection problem and a new recursive clustering technique for trees.
Cite as
Philip Bille, Inge Li Gørtz, Max Rishøj Pedersen, Eva Rotenberg, and Teresa Anna Steiner. String Indexing for Top-k Close Consecutive Occurrences. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bille_et_al:LIPIcs.FSTTCS.2020.14,
author = {Bille, Philip and G{\o}rtz, Inge Li and Pedersen, Max Rish{\o}j and Rotenberg, Eva and Steiner, Teresa Anna},
title = {{String Indexing for Top-k Close Consecutive Occurrences}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {14:1--14:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.14},
URN = {urn:nbn:de:0030-drops-132558},
doi = {10.4230/LIPIcs.FSTTCS.2020.14},
annote = {Keywords: String indexing, pattern matching, consecutive occurrences}
}
Document
Fair Tree Connection Games with Topology-Dependent Edge Cost
Abstract
How do rational agents self-organize when trying to connect to a common target? We study this question with a simple tree formation game which is related to the well-known fair single-source connection game by Anshelevich et al. (FOCS'04) and selfish spanning tree games by Gourvès and Monnot (WINE'08). In our game agents correspond to nodes in a network that activate a single outgoing edge to connect to the common target node (possibly via other nodes). Agents pay for their path to the common target, and edge costs are shared fairly among all agents using an edge. The main novelty of our model is dynamic edge costs that depend on the in-degree of the respective endpoint. This reflects that connecting to popular nodes that have increased internal coordination costs is more expensive since they can charge higher prices for their routing service.
In contrast to related models, we show that equilibria are not guaranteed to exist, but we prove the existence for infinitely many numbers of agents. Moreover, we analyze the structure of equilibrium trees and employ these insights to prove a constant upper bound on the Price of Anarchy as well as non-trivial lower bounds on both the Price of Anarchy and the Price of Stability. We also show that in comparison with the social optimum tree the overall cost of an equilibrium tree is more fairly shared among the agents. Thus, we prove that self-organization of rational agents yields on average only slightly higher cost per agent compared to the centralized optimum, and at the same time, it induces a more fair cost distribution. Moreover, equilibrium trees achieve a beneficial trade-off between a low height and low maximum degree, and hence these trees might be of independent interest from a combinatorics point-of-view. We conclude with a discussion of promising extensions of our model.
Cite as
Davide Bilò, Tobias Friedrich, Pascal Lenzner, Anna Melnichenko, and Louise Molitor. Fair Tree Connection Games with Topology-Dependent Edge Cost. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bilo_et_al:LIPIcs.FSTTCS.2020.15,
author = {Bil\`{o}, Davide and Friedrich, Tobias and Lenzner, Pascal and Melnichenko, Anna and Molitor, Louise},
title = {{Fair Tree Connection Games with Topology-Dependent Edge Cost}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {15:1--15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.15},
URN = {urn:nbn:de:0030-drops-132562},
doi = {10.4230/LIPIcs.FSTTCS.2020.15},
annote = {Keywords: Network Design Games, Spanning Tree Games, Fair Cost Sharing, Price of Anarchy, Nash Equilibrium, Algorithmic Game Theory, Combinatorics}
}
Document
Locally Decodable/Correctable Codes for Insertions and Deletions
Abstract
Recent efforts in coding theory have focused on building codes for insertions and deletions, called insdel codes, with optimal trade-offs between their redundancy and their error-correction capabilities, as well as efficient encoding and decoding algorithms.
In many applications, polynomial running time may still be prohibitively expensive, which has motivated the study of codes with super-efficient decoding algorithms. These have led to the well-studied notions of Locally Decodable Codes (LDCs) and Locally Correctable Codes (LCCs). Inspired by these notions, Ostrovsky and Paskin-Cherniavsky (Information Theoretic Security, 2015) generalized Hamming LDCs to insertions and deletions. To the best of our knowledge, these are the only known results that study the analogues of Hamming LDCs in channels performing insertions and deletions.
Here we continue the study of insdel codes that admit local algorithms. Specifically, we reprove the results of Ostrovsky and Paskin-Cherniavsky for insdel LDCs using a different set of techniques. We also observe that the techniques extend to constructions of LCCs. Specifically, we obtain insdel LDCs and LCCs from their Hamming LDCs and LCCs analogues, respectively. The rate and error-correction capability blow up only by a constant factor, while the query complexity blows up by a poly log factor in the block length.
Since insdel locally decodable/correctble codes are scarcely studied in the literature, we believe our results and techniques may lead to further research. In particular, we conjecture that constant-query insdel LDCs/LCCs do not exist.
Cite as
Alexander R. Block, Jeremiah Blocki, Elena Grigorescu, Shubhang Kulkarni, and Minshen Zhu. Locally Decodable/Correctable Codes for Insertions and Deletions. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{block_et_al:LIPIcs.FSTTCS.2020.16,
author = {Block, Alexander R. and Blocki, Jeremiah and Grigorescu, Elena and Kulkarni, Shubhang and Zhu, Minshen},
title = {{Locally Decodable/Correctable Codes for Insertions and Deletions}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {16:1--16:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.16},
URN = {urn:nbn:de:0030-drops-132577},
doi = {10.4230/LIPIcs.FSTTCS.2020.16},
annote = {Keywords: Locally decodable/correctable codes, insert-delete channel}
}
Document
Maximum Clique in Disk-Like Intersection Graphs
Abstract
We study the complexity of Maximum Clique in intersection graphs of convex objects in the plane. On the algorithmic side, we extend the polynomial-time algorithm for unit disks [Clark '90, Raghavan and Spinrad '03] to translates of any fixed convex set. We also generalize the efficient polynomial-time approximation scheme (EPTAS) and subexponential algorithm for disks [Bonnet et al. '18, Bonamy et al. '18] to homothets of a fixed centrally symmetric convex set.
The main open question on that topic is the complexity of Maximum Clique in disk graphs. It is not known whether this problem is NP-hard. We observe that, so far, all the hardness proofs for Maximum Clique in intersection graph classes I follow the same road. They show that, for every graph G of a large-enough class C, the complement of an even subdivision of G belongs to the intersection class I. Then they conclude by invoking the hardness of Maximum Independent Set on the class C, and the fact that the even subdivision preserves that hardness. However there is a strong evidence that this approach cannot work for disk graphs [Bonnet et al. '18]. We suggest a new approach, based on a problem that we dub Max Interval Permutation Avoidance, which we prove unlikely to have a subexponential-time approximation scheme. We transfer that hardness to Maximum Clique in intersection graphs of objects which can be either half-planes (or unit disks) or axis-parallel rectangles. That problem is not amenable to the previous approach. We hope that a scaled down (merely NP-hard) variant of Max Interval Permutation Avoidance could help making progress on the disk case, for instance by showing the NP-hardness for (convex) pseudo-disks.
Cite as
Édouard Bonnet, Nicolas Grelier, and Tillmann Miltzow. Maximum Clique in Disk-Like Intersection Graphs. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bonnet_et_al:LIPIcs.FSTTCS.2020.17,
author = {Bonnet, \'{E}douard and Grelier, Nicolas and Miltzow, Tillmann},
title = {{Maximum Clique in Disk-Like Intersection Graphs}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {17:1--17:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.17},
URN = {urn:nbn:de:0030-drops-132587},
doi = {10.4230/LIPIcs.FSTTCS.2020.17},
annote = {Keywords: Disk Graphs, Intersection Graphs, Maximum Clique, Algorithms, NP-hardness, APX-hardness}
}
Document
Parameterized Complexity of Feedback Vertex Sets on Hypergraphs
Abstract
A feedback vertex set in a hypergraph H is a set of vertices S such that deleting S from H results in an acyclic hypergraph. Here, deleting a vertex means removing the vertex and all incident hyperedges, and a hypergraph is acyclic if its vertex-edge incidence graph is acyclic. We study the (parameterized complexity of) the Hypergraph Feedback Vertex Set (HFVS) problem: given as input a hypergraph H and an integer k, determine whether H has a feedback vertex set of size at most k. It is easy to see that this problem generalizes the classic Feedback Vertex Set (FVS) problem on graphs. Remarkably, despite the central role of FVS in parameterized algorithms and complexity, the parameterized complexity of a generalization of FVS to hypergraphs has not been studied previously. In this paper, we fill this void. Our main results are as follows
- HFVS is W[2]-hard (as opposed to FVS, which is fixed parameter tractable).
- If the input hypergraph is restricted to a linear hypergraph (no two hyperedges intersect in more than one vertex), HFVS admits a randomized algorithm with running time 2^{𝒪(k³log k)}n^{𝒪(1)}.
- If the input hypergraph is restricted to a d-hypergraph (hyperedges have cardinality at most d), then HFVS admits a deterministic algorithm with running time d^{𝒪(k)}n^{𝒪(1)}. The algorithm for linear hypergraphs combines ideas from the randomized algorithm for FVS by Becker et al. [J. Artif. Intell. Res., 2000] with the branching algorithm for Point Line Cover by Langerman and Morin [Discrete & Computational Geometry, 2005].
Cite as
Pratibha Choudhary, Lawqueen Kanesh, Daniel Lokshtanov, Fahad Panolan, and Saket Saurabh. Parameterized Complexity of Feedback Vertex Sets on Hypergraphs. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{choudhary_et_al:LIPIcs.FSTTCS.2020.18,
author = {Choudhary, Pratibha and Kanesh, Lawqueen and Lokshtanov, Daniel and Panolan, Fahad and Saurabh, Saket},
title = {{Parameterized Complexity of Feedback Vertex Sets on Hypergraphs}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {18:1--18:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.18},
URN = {urn:nbn:de:0030-drops-132596},
doi = {10.4230/LIPIcs.FSTTCS.2020.18},
annote = {Keywords: feedback vertex sets, hypergraphs, FPT, randomized algorithms}
}
Document
Size Bounds on Low Depth Circuits for Promise Majority
Abstract
We give two results on the size of AC0 circuits computing promise majority. ε-promise majority is majority promised that either at most an ε fraction of the input bits are 1 or at most ε are 0.
- First, we show super-quadratic size lower bounds on both monotone and general depth-3 circuits for promise majority.
- For any ε ∈ (0, 1/2), monotone depth-3 AC0 circuits for ε-promise majority have size Ω̃(ε³ n^{2 + (ln(1 - ε))/(ln(ε))}).
- For any ε ∈ (0, 1/2), general depth-3 AC0 circuits for ε-promise majority have size Ω̃(ε³ n^{2 + (ln(1 - ε²))/(2ln(ε))}). These are the first quadratic size lower bounds for depth-3 ε-promise majority circuits for ε < 0.49.
- Second, we give both uniform and non-uniform sub-quadratic size constant-depth circuits for promise majority.
- For integer k ≥ 1 and constant ε ∈ (0, 1/2), there exists monotone non uniform AC0 circuits of depth-(2 + 2 k) computing ε-promise majority with size Õ(n^{1/(1 - 2^{-k})}).
- For integer k ≥ 1 and constant ε ∈ (0, 1/2), there exists monotone uniform AC0 circuit of depth-(2 + 2 k) computing ε-promise majority with size n^{1/(1 - (2/3) ^k) + o(1)}. These circuits are based on incremental improvements to existing depth-3 circuits for promise majority given by Ajtai [Miklós Ajtai, 1983] and Viola [Emanuele Viola, 2009] combined with a divide and conquer strategy.
Cite as
Joshua Cook. Size Bounds on Low Depth Circuits for Promise Majority. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{cook:LIPIcs.FSTTCS.2020.19,
author = {Cook, Joshua},
title = {{Size Bounds on Low Depth Circuits for Promise Majority}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {19:1--19:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.19},
URN = {urn:nbn:de:0030-drops-132609},
doi = {10.4230/LIPIcs.FSTTCS.2020.19},
annote = {Keywords: AC0, Approximate Counting, Approximate Majority, Promise Majority, Depth 3 Circuits, Circuit Lower Bound}
}
Document
Lower Bounds for Semi-adaptive Data Structures via Corruption
Abstract
In a dynamic data structure problem we wish to maintain an encoding of some data in memory, in such a way that we may efficiently carry out a sequence of queries and updates to the data. A long-standing open problem in this area is to prove an unconditional polynomial lower bound of a trade-off between the update time and the query time of an adaptive dynamic data structure computing some explicit function. Ko and Weinstein provided such lower bound for a restricted class of semi-adaptive data structures, which compute the Disjointness function. There, the data are subsets x₁,… ,x_k and y of {1,… ,n}, the updates can modify y (by inserting and removing elements), and the queries are an index i ∈ {1,… ,k} (query i should answer whether x_i and y are disjoint, i.e., it should compute the Disjointness function applied to (x_i, y)). The semi-adaptiveness places a restriction in how the data structure can be accessed in order to answer a query. We generalize the lower bound of Ko and Weinstein to work not just for the Disjointness, but for any function having high complexity under the smooth corruption bound.
Cite as
Pavel Dvořák and Bruno Loff. Lower Bounds for Semi-adaptive Data Structures via Corruption. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{dvorak_et_al:LIPIcs.FSTTCS.2020.20,
author = {Dvo\v{r}\'{a}k, Pavel and Loff, Bruno},
title = {{Lower Bounds for Semi-adaptive Data Structures via Corruption}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {20:1--20:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.20},
URN = {urn:nbn:de:0030-drops-132617},
doi = {10.4230/LIPIcs.FSTTCS.2020.20},
annote = {Keywords: semi-adaptive dynamic data structure, polynomial lower bound, corruption bound, information theory}
}
Document
Stability-Preserving, Time-Efficient Mechanisms for School Choice in Two Rounds
Abstract
We address the following dynamic version of the school choice question: a city, named City, admits students in two temporally-separated rounds, denoted R₁ and R₂. In round R₁, the capacity of each school is fixed and mechanism M₁ finds a student optimal stable matching. In round R₂, certain parameters change, e.g., new students move into the City or the City is happy to allocate extra seats to specific schools. We study a number of Settings of this kind and give polynomial time algorithms for obtaining a stable matching for the new situations.
It is well established that switching the school of a student midway, unsynchronized with her classmates, can cause traumatic effects. This fact guides us to two types of results: the first simply disallows any re-allocations in round R₂, and the second asks for a stable matching that minimizes the number of re-allocations. For the latter, we prove that the stable matchings which minimize the number of re-allocations form a sublattice of the lattice of stable matchings. Observations about incentive compatibility are woven into these results. We also give a third type of results, namely proofs of NP-hardness for a mechanism for round R₂ under certain settings.
Cite as
Karthik Gajulapalli, James A. Liu, Tung Mai, and Vijay V. Vazirani. Stability-Preserving, Time-Efficient Mechanisms for School Choice in Two Rounds. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 21:1-21:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{gajulapalli_et_al:LIPIcs.FSTTCS.2020.21,
author = {Gajulapalli, Karthik and Liu, James A. and Mai, Tung and Vazirani, Vijay V.},
title = {{Stability-Preserving, Time-Efficient Mechanisms for School Choice in Two Rounds}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {21:1--21:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.21},
URN = {urn:nbn:de:0030-drops-132626},
doi = {10.4230/LIPIcs.FSTTCS.2020.21},
annote = {Keywords: stable matching, mechanism design, NP-Hardness}
}
Document
New Verification Schemes for Frequency-Based Functions on Data Streams
Abstract
We study the general problem of computing frequency-based functions, i.e., the sum of any given function of data stream frequencies. Special cases include fundamental data stream problems such as computing the number of distinct elements (F₀), frequency moments (F_k), and heavy-hitters. It can also be applied to calculate the maximum frequency of an element (F_{∞}).
Given that exact computation of most of these special cases provably do not admit any sublinear space algorithm, a natural approach is to consider them in an enhanced data streaming model, where we have a computationally unbounded but untrusted prover that can send proofs or help messages to ease the computation. Think of a memory-restricted client delegating the computation to a powerful cloud service. The client does not blindly trust the cloud, and with its limited memory, it wants to verify the proof that the cloud sends. Chakrabarti et al. (ICALP '09) introduced this model as the annotated data streaming model and showed that multiple problems including exact computation of frequency-based functions - that have no sublinear algorithms in basic streaming - do have algorithms, also called schemes, in the annotated streaming model with both space and proof-length sublinear in the input size.
We give a general scheme for computing any frequency-based function with both space usage and proof-size of O(n^{2/3}log n) bits, where n is the size of the universe. This improves upon the best known bound of O(n^{2/3}log^{4/3} n) given by the seminal paper of Chakrabarti et al. and as a result, also improves upon the best known bounds for the important special cases of computing F₀ and F_{∞}. We emphasize that while being quantitatively better, our scheme is also qualitatively better in the sense that it is simpler than the previously best scheme that uses intricate data structures and elaborate subroutines. Our scheme uses a simple technique tailored for this model: the verifier solves the problem partially by running an algorithm known to be helpful for it in the basic (sans prover) streaming model and then takes the prover’s help to solve the remaining part.
Cite as
Prantar Ghosh. New Verification Schemes for Frequency-Based Functions on Data Streams. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 22:1-22:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{ghosh:LIPIcs.FSTTCS.2020.22,
author = {Ghosh, Prantar},
title = {{New Verification Schemes for Frequency-Based Functions on Data Streams}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {22:1--22:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.22},
URN = {urn:nbn:de:0030-drops-132631},
doi = {10.4230/LIPIcs.FSTTCS.2020.22},
annote = {Keywords: data streams, interactive proofs, Arthur-Merlin}
}
Document
Online Carpooling Using Expander Decompositions
Abstract
We consider the online carpooling problem: given n vertices, a sequence of edges arrive over time. When an edge e_t = (u_t, v_t) arrives at time step t, the algorithm must orient the edge either as v_t → u_t or u_t → v_t, with the objective of minimizing the maximum discrepancy of any vertex, i.e., the absolute difference between its in-degree and out-degree. Edges correspond to pairs of persons wanting to ride together, and orienting denotes designating the driver. The discrepancy objective then corresponds to every person driving close to their fair share of rides they participate in.
In this paper, we design efficient algorithms which can maintain polylog(n,T) maximum discrepancy (w.h.p) over any sequence of T arrivals, when the arriving edges are sampled independently and uniformly from any given graph G. This provides the first polylogarithmic bounds for the online (stochastic) carpooling problem. Prior to this work, the best known bounds were O(√{n log n})-discrepancy for any adversarial sequence of arrivals, or O(log log n)-discrepancy bounds for the stochastic arrivals when G is the complete graph.
The technical crux of our paper is in showing that the simple greedy algorithm, which has provably good discrepancy bounds when the arriving edges are drawn uniformly at random from the complete graph, also has polylog discrepancy when G is an expander graph. We then combine this with known expander-decomposition results to design our overall algorithm.
Cite as
Anupam Gupta, Ravishankar Krishnaswamy, Amit Kumar, and Sahil Singla. Online Carpooling Using Expander Decompositions. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 23:1-23:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{gupta_et_al:LIPIcs.FSTTCS.2020.23,
author = {Gupta, Anupam and Krishnaswamy, Ravishankar and Kumar, Amit and Singla, Sahil},
title = {{Online Carpooling Using Expander Decompositions}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {23:1--23:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.23},
URN = {urn:nbn:de:0030-drops-132647},
doi = {10.4230/LIPIcs.FSTTCS.2020.23},
annote = {Keywords: Online Algorithms, Discrepancy Minimization, Carpooling}
}
Document
On the (Parameterized) Complexity of Almost Stable Marriage
Abstract
In the Stable Marriage problem, when the preference lists are complete, all agents of the smaller side can be matched. However, this need not be true when preference lists are incomplete. In most real-life situations, where agents participate in the matching market voluntarily and submit their preferences, it is natural to assume that each agent wants to be matched to someone in his/her preference list as opposed to being unmatched. In light of the Rural Hospital Theorem, we have to relax the "no blocking pair" condition for stable matchings in order to match more agents. In this paper, we study the question of matching more agents with fewest possible blocking edges. In particular, the goal is to find a matching whose size exceeds that of a stable matching in the graph by at least t and has at most k blocking edges. We study this question in the realm of parameterized complexity with respect to several natural parameters, k,t,d, where d is the maximum length of a preference list. Unfortunately, the problem remains intractable even for the combined parameter k+t+d. Thus, we extend our study to the local search variant of this problem, in which we search for a matching that not only fulfills each of the above conditions but is "closest", in terms of its symmetric difference to the given stable matching, and obtain an FPT algorithm.
Cite as
Sushmita Gupta, Pallavi Jain, Sanjukta Roy, Saket Saurabh, and Meirav Zehavi. On the (Parameterized) Complexity of Almost Stable Marriage. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{gupta_et_al:LIPIcs.FSTTCS.2020.24,
author = {Gupta, Sushmita and Jain, Pallavi and Roy, Sanjukta and Saurabh, Saket and Zehavi, Meirav},
title = {{On the (Parameterized) Complexity of Almost Stable Marriage}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {24:1--24:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.24},
URN = {urn:nbn:de:0030-drops-132655},
doi = {10.4230/LIPIcs.FSTTCS.2020.24},
annote = {Keywords: Stable Matching, Parameterized Complexity, Local Search}
}
Document
Min-Cost Popular Matchings
Abstract
Let G = (A ∪ B, E) be a bipartite graph on n vertices where every vertex ranks its neighbors in a strict order of preference. A matching M in G is popular if there is no matching N such that vertices that prefer N to M outnumber those that prefer M to N. Popular matchings always exist in G since every stable matching is popular. Thus it is easy to find a popular matching in G - however it is NP-hard to compute a min-cost popular matching in G when there is a cost function on the edge set; moreover it is NP-hard to approximate this to any multiplicative factor. An O^*(2ⁿ) algorithm to compute a min-cost popular matching in G follows from known results. Here we show:
- an algorithm with running time O^*(2^{n/4}) ≈ O^*(1.19ⁿ) to compute a min-cost popular matching;
- assume all edge costs are non-negative - then given ε > 0, a randomized algorithm with running time poly(n,1/(ε)) to compute a matching M such that cost(M) is at most twice the optimal cost and with high probability, the fraction of all matchings more popular than M is at most 1/2+ε.
Cite as
Telikepalli Kavitha. Min-Cost Popular Matchings. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kavitha:LIPIcs.FSTTCS.2020.25,
author = {Kavitha, Telikepalli},
title = {{Min-Cost Popular Matchings}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {25:1--25:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.25},
URN = {urn:nbn:de:0030-drops-132668},
doi = {10.4230/LIPIcs.FSTTCS.2020.25},
annote = {Keywords: Bipartite graphs, Stable matchings, Dual certificates}
}
Document
Constructing Large Matchings via Query Access to a Maximal Matching Oracle
Abstract
Multi-pass streaming algorithm for Maximum Matching have been studied since more than 15 years and various algorithmic results are known today, including 2-pass streaming algorithms that break the 1/2-approximation barrier, and (1-ε)-approximation streaming algorithms that run in O(poly 1/ε) passes in bipartite graphs and in O((1/ε)^(1/ε)) or O(poly (1/ε) ⋅ log n) passes in general graphs, where n is the number of vertices of the input graph. However, proving impossibility results for such algorithms has so far been elusive, and, for example, even the existence of 2-pass small space streaming algorithms with approximation factor 0.999 has not yet been ruled out.
The key building block of all multi-pass streaming algorithms for Maximum Matching is the Greedy matching algorithm. Our aim is to understand the limitations of this approach: How many passes are required if the algorithm solely relies on the invocation of the Greedy algorithm?
In this paper, we initiate the study of lower bounds for restricted families of multi-pass streaming algorithms for Maximum Matching. We focus on the simple yet powerful class of algorithms that in each pass run Greedy on a vertex-induced subgraph of the input graph. In bipartite graphs, we show that 3 passes are necessary and sufficient to improve on the trivial approximation factor of 1/2: We give a lower bound of 0.6 on the approximation ratio of such algorithms, which is optimal. We further show that Ω(1/ε) passes are required for computing a (1-ε)-approximation, even in bipartite graphs. Last, the considered class of algorithms is not well-suited to general graphs: We show that Ω(n) passes are required in order to improve on the trivial approximation factor of 1/2.
Cite as
Lidiya Khalidah binti Khalil and Christian Konrad. Constructing Large Matchings via Query Access to a Maximal Matching Oracle. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 26:1-26:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{khalil_et_al:LIPIcs.FSTTCS.2020.26,
author = {Khalil, Lidiya Khalidah binti and Konrad, Christian},
title = {{Constructing Large Matchings via Query Access to a Maximal Matching Oracle}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {26:1--26:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.26},
URN = {urn:nbn:de:0030-drops-132673},
doi = {10.4230/LIPIcs.FSTTCS.2020.26},
annote = {Keywords: Maximum matching approximation, Query model, Streaming algorithms}
}
Document
Planted Models for the Densest k-Subgraph Problem
Abstract
Given an undirected graph G, the Densest k-subgraph problem (DkS) asks to compute a set S ⊂ V of cardinality |S| ≤ k such that the weight of edges inside S is maximized. This is a fundamental NP-hard problem whose approximability, inspite of many decades of research, is yet to be settled. The current best known approximation algorithm due to Bhaskara et al. (2010) computes a 𝒪(n^{1/4 + ε}) approximation in time n^{𝒪(1/ε)}, for any ε > 0.
We ask what are some "easier" instances of this problem? We propose some natural semi-random models of instances with a planted dense subgraph, and study approximation algorithms for computing the densest subgraph in them. These models are inspired by the semi-random models of instances studied for various other graph problems such as the independent set problem, graph partitioning problems etc. For a large range of parameters of these models, we get significantly better approximation factors for the Densest k-subgraph problem. Moreover, our algorithm recovers a large part of the planted solution.
Cite as
Yash Khanna and Anand Louis. Planted Models for the Densest k-Subgraph Problem. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{khanna_et_al:LIPIcs.FSTTCS.2020.27,
author = {Khanna, Yash and Louis, Anand},
title = {{Planted Models for the Densest k-Subgraph Problem}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.27},
URN = {urn:nbn:de:0030-drops-132682},
doi = {10.4230/LIPIcs.FSTTCS.2020.27},
annote = {Keywords: Densest k-Subgraph, Semi-Random models, Planted Models, Semidefinite Programming, Approximation Algorithms, Beyond Worst Case Analysis}
}
Document
Sample-And-Gather: Fast Ruling Set Algorithms in the Low-Memory MPC Model
Abstract
Motivated by recent progress on symmetry breaking problems such as maximal independent set (MIS) and maximal matching in the low-memory Massively Parallel Computation (MPC) model (e.g., Behnezhad et al. PODC 2019; Ghaffari-Uitto SODA 2019), we investigate the complexity of ruling set problems in this model. The MPC model has become very popular as a model for large-scale distributed computing and it comes with the constraint that the memory-per-machine is strongly sublinear in the input size. For graph problems, extremely fast MPC algorithms have been designed assuming Ω̃(n) memory-per-machine, where n is the number of nodes in the graph (e.g., the O(log log n) MIS algorithm of Ghaffari et al., PODC 2018). However, it has proven much more difficult to design fast MPC algorithms for graph problems in the low-memory MPC model, where the memory-per-machine is restricted to being strongly sublinear in the number of nodes, i.e., O(n^ε) for constant 0 < ε < 1.
In this paper, we present an algorithm for the 2-ruling set problem, running in Õ(log^{1/6} Δ) rounds whp, in the low-memory MPC model. Here Δ is the maximum degree of the graph. We then extend this result to β-ruling sets for any integer β > 1. Specifically, we show that a β-ruling set can be computed in the low-memory MPC model with O(n^ε) memory-per-machine in Õ(β ⋅ log^{1/(2^{β+1}-2)} Δ) rounds, whp. From this it immediately follows that a β-ruling set for β = Ω(log log log Δ)-ruling set can be computed in in just O(β log log n) rounds whp. The above results assume a total memory of Õ(m + n^{1+ε}). We also present algorithms for β-ruling sets in the low-memory MPC model assuming that the total memory over all machines is restricted to Õ(m). For β > 1, these algorithms are all substantially faster than the Ghaffari-Uitto Õ(√{log Δ})-round MIS algorithm in the low-memory MPC model.
All our results follow from a Sample-and-Gather Simulation Theorem that shows how random-sampling-based Congest algorithms can be efficiently simulated in the low-memory MPC model. We expect this simulation theorem to be of independent interest beyond the ruling set algorithms derived here.
Cite as
Kishore Kothapalli, Shreyas Pai, and Sriram V. Pemmaraju. Sample-And-Gather: Fast Ruling Set Algorithms in the Low-Memory MPC Model. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kothapalli_et_al:LIPIcs.FSTTCS.2020.28,
author = {Kothapalli, Kishore and Pai, Shreyas and Pemmaraju, Sriram V.},
title = {{Sample-And-Gather: Fast Ruling Set Algorithms in the Low-Memory MPC Model}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.28},
URN = {urn:nbn:de:0030-drops-132690},
doi = {10.4230/LIPIcs.FSTTCS.2020.28},
annote = {Keywords: Massively Parallel Computation, Ruling Set, Simulation Theorems}
}
Document
On Parity Decision Trees for Fourier-Sparse Boolean Functions
Abstract
We study parity decision trees for Boolean functions. The motivation of our study is the log-rank conjecture for XOR functions and its connection to Fourier analysis and parity decision tree complexity. Our contributions are as follows. Let f : 𝔽₂ⁿ → {-1, 1} be a Boolean function with Fourier support 𝒮 and Fourier sparsity k.
- We prove via the probabilistic method that there exists a parity decision tree of depth O(√k) that computes f. This matches the best known upper bound on the parity decision tree complexity of Boolean functions (Tsang, Wong, Xie, and Zhang, FOCS 2013). Moreover, while previous constructions (Tsang et al., FOCS 2013, Shpilka, Tal, and Volk, Comput. Complex. 2017) build the trees by carefully choosing the parities to be queried in each step, our proof shows that a naive sampling of the parities suffices.
- We generalize the above result by showing that if the Fourier spectra of Boolean functions satisfy a natural "folding property", then the above proof can be adapted to establish existence of a tree of complexity polynomially smaller than O(√ k). More concretely, the folding property we consider is that for most distinct γ, δ in 𝒮, there are at least a polynomial (in k) number of pairs (α, β) of parities in 𝒮 such that α+β = γ+δ. We make a conjecture in this regard which, if true, implies that the communication complexity of an XOR function is bounded above by the fourth root of the rank of its communication matrix, improving upon the previously known upper bound of square root of rank (Tsang et al., FOCS 2013, Lovett, J. ACM. 2016).
- Motivated by the above, we present some structural results about the Fourier spectra of Boolean functions. It can be shown by elementary techniques that for any Boolean function f and all (α, β) in binom(𝒮,2), there exists another pair (γ, δ) in binom(𝒮,2) such that α + β = γ + δ. One can view this as a "trivial" folding property that all Boolean functions satisfy. Prior to our work, it was conceivable that for all (α, β) ∈ binom(𝒮,2), there exists exactly one other pair (γ, δ) ∈ binom(𝒮,2) with α + β = γ + δ. We show, among other results, that there must exist several γ ∈ 𝔽₂ⁿ such that there are at least three pairs of parities (α₁, α₂) ∈ binom(𝒮,2) with α₁+α₂ = γ. This, in particular, rules out the possibility stated earlier.
Cite as
Nikhil S. Mande and Swagato Sanyal. On Parity Decision Trees for Fourier-Sparse Boolean Functions. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{mande_et_al:LIPIcs.FSTTCS.2020.29,
author = {Mande, Nikhil S. and Sanyal, Swagato},
title = {{On Parity Decision Trees for Fourier-Sparse Boolean Functions}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {29:1--29:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.29},
URN = {urn:nbn:de:0030-drops-132703},
doi = {10.4230/LIPIcs.FSTTCS.2020.29},
annote = {Keywords: Parity decision trees, log-rank conjecture, analysis of Boolean functions, communication complexity}
}
Document
Colored Cut Games
Abstract
In a graph G = (V,E) with an edge coloring 𝓁:E → C and two distinguished vertices s and t, a colored (s,t)-cut is a set C̃ ⊆ C such that deleting all edges with some color c ∈ C̃ from G disconnects s and t. Motivated by applications in the design of robust networks, we introduce a family of problems called colored cut games. In these games, an attacker and a defender choose colors to delete and to protect, respectively, in an alternating fashion. It is the goal of the attacker to achieve a colored (s,t)-cut and the goal of the defender to prevent this. First, we show that for an unbounded number of alternations, colored cut games are PSPACE-complete. We then show that, even on subcubic graphs, colored cut games with a constant number i of alternations are complete for classes in the polynomial hierarchy whose level depends on i. To complete the dichotomy, we show that all colored cut games are polynomial-time solvable on graphs with degree at most two. Finally, we show that all colored cut games admit a polynomial kernel for the parameter k+κ_r where k denotes the total attacker budget and, for any constant r, κ_r is the number of vertex deletions that are necessary to transform G into a graph where the longest path has length at most r. In the case of r = 1, κ₁ is the vertex cover number vc of the input graph and we obtain a kernel with 𝒪(vc²k²) edges. Moreover, we introduce an algorithm solving the most basic colored cut game, Colored (s,t)-Cut, in 2^{vc + k}n^{𝒪(1)} time.
Cite as
Nils Morawietz, Niels Grüttemeier, Christian Komusiewicz, and Frank Sommer. Colored Cut Games. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{morawietz_et_al:LIPIcs.FSTTCS.2020.30,
author = {Morawietz, Nils and Gr\"{u}ttemeier, Niels and Komusiewicz, Christian and Sommer, Frank},
title = {{Colored Cut Games}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {30:1--30:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.30},
URN = {urn:nbn:de:0030-drops-132719},
doi = {10.4230/LIPIcs.FSTTCS.2020.30},
annote = {Keywords: Labeled Cut, Labeled Path, Network Robustness, Kernelization, PSPACE, Polynomial Hierarchy}
}
Document
Randomness Efficient Noise Stability and Generalized Small Bias Sets
Abstract
We present a randomness efficient version of the linear noise operator T_ρ from boolean function analysis by constructing a sparse linear operator on the space of boolean functions {0,1}ⁿ → {0,1} with similar eigenvalue profile to T_ρ. The linear operator we construct is a direct consequence of a generalization of ε-biased sets to the product distribution 𝒟_p on {0,1}ⁿ where the marginal of each coordinate is p = 1/2-1/2ρ. Such a generalization is a small support distribution that fools linear tests when the input of the test comes from 𝒟_p instead of the uniform distribution. We give an explicit construction of such a distribution that requires log n + O_{p}(log log n + log1/(ε)) bits of uniform randomness to sample from, where the p subscript hides O(log² 1/p) factors. When p and ε are constant, this yields a support size nearly linear in n, whereas previous best known constructions only guarantee a size of poly(n). Furthermore, our construction implies an explicitly constructible "sparse" noisy hypercube graph that is a small set expander.
Cite as
Dana Moshkovitz, Justin Oh, and David Zuckerman. Randomness Efficient Noise Stability and Generalized Small Bias Sets. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{moshkovitz_et_al:LIPIcs.FSTTCS.2020.31,
author = {Moshkovitz, Dana and Oh, Justin and Zuckerman, David},
title = {{Randomness Efficient Noise Stability and Generalized Small Bias Sets}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {31:1--31:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.31},
URN = {urn:nbn:de:0030-drops-132721},
doi = {10.4230/LIPIcs.FSTTCS.2020.31},
annote = {Keywords: pseudorandomness, derandomization, epsilon biased sets, noise stability}
}
Document
Connectivity Lower Bounds in Broadcast Congested Clique
Abstract
We prove three new lower bounds for graph connectivity in the 1-bit broadcast congested clique model, BCC(1). First, in the KT-0 version of BCC(1), in which nodes are aware of neighbors only through port numbers, we show an Ω(log n) round lower bound for Connectivity even for constant-error randomized Monte Carlo algorithms. The deterministic version of this result can be obtained via the well-known "edge-crossing" argument, but, the randomized version of this result requires establishing new combinatorial results regarding the indistinguishability graph induced by inputs. In our second result, we show that the Ω(log n) lower bound result extends to the KT-1 version of the BCC(1) model, in which nodes are aware of IDs of all neighbors, though our proof works only for deterministic algorithms. This result substantially improves upon the existing Ω(log^* n) deterministic lower bound (Jurdziński et el., SIROCCO 2018) for this problem. Since nodes know IDs of their neighbors in the KT-1 model, it is no longer possible to play "edge-crossing" tricks; instead we present a reduction from the 2-party communication complexity problem Partition in which Alice and Bob are given two set partitions on [n] and are required to determine if the join of these two set partitions equals the trivial one-part set partition. While our KT-1 Connectivity lower bound holds only for deterministic algorithms, in our third result we extend this Ω(log n) KT-1 lower bound to constant-error Monte Carlo algorithms for the closely related ConnectedComponents problem. We use information-theoretic techniques to obtain this result. All our results hold for the seemingly easy special case of Connectivity in which an algorithm has to distinguish an instance with one cycle from an instance with multiple cycles. Our results showcase three rather different lower bound techniques and lay the groundwork for further improvements in lower bounds for Connectivity in the BCC(1) model.
Cite as
Shreyas Pai and Sriram V. Pemmaraju. Connectivity Lower Bounds in Broadcast Congested Clique. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{pai_et_al:LIPIcs.FSTTCS.2020.32,
author = {Pai, Shreyas and Pemmaraju, Sriram V.},
title = {{Connectivity Lower Bounds in Broadcast Congested Clique}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {32:1--32:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.32},
URN = {urn:nbn:de:0030-drops-132732},
doi = {10.4230/LIPIcs.FSTTCS.2020.32},
annote = {Keywords: Distributed Algorithms, Broadcast Congested Clique, Connectivity, Lower Bounds, Indistinguishability, Communication Complexity, Information Theory}
}
Document
Fully Dynamic Sequential and Distributed Algorithms for MAX-CUT
Abstract
This paper initiates the study of the MAX-CUT problem in fully dynamic graphs. Given a graph G = (V,E), we present deterministic fully dynamic distributed and sequential algorithms to maintain a cut on G which always contains at least |E|/2 edges in sublinear update time under edge insertions and deletions to G. Our results include the following deterministic algorithms: i) an O(Δ) worst-case update time sequential algorithm, where Δ denotes the maximum degree of G, ii) the first fully dynamic distributed algorithm taking O(1) rounds and O(Δ) total bits of communication per update in the Massively Parallel Computation (MPC) model with n machines and O(n) words of memory per machine. The aforementioned algorithms require at most one adjustment, that is, a move of one vertex from one side of the cut to the other.
We also give the following fully dynamic sequential algorithms: i) a deterministic O(m^{1/2}) amortized update time algorithm where m denotes the maximum number of edges in G during any sequence of updates and, ii) a randomized algorithm which takes Õ(n^{2/3}) worst-case update time when edge updates come from an oblivious adversary.
Cite as
Omer Wasim and Valerie King. Fully Dynamic Sequential and Distributed Algorithms for MAX-CUT. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{wasim_et_al:LIPIcs.FSTTCS.2020.33,
author = {Wasim, Omer and King, Valerie},
title = {{Fully Dynamic Sequential and Distributed Algorithms for MAX-CUT}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {33:1--33:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.33},
URN = {urn:nbn:de:0030-drops-132746},
doi = {10.4230/LIPIcs.FSTTCS.2020.33},
annote = {Keywords: data structures, dynamic graph algorithms, approximate maximum cut, distributed computing, parallel computing}
}
Document
Weighted Tiling Systems for Graphs: Evaluation Complexity
Abstract
We consider weighted tiling systems to represent functions from graphs to a commutative semiring such as the Natural semiring or the Tropical semiring. The system labels the nodes of a graph by its states, and checks if the neighbourhood of every node belongs to a set of permissible tiles, and assigns a weight accordingly. The weight of a labeling is the semiring-product of the weights assigned to the nodes, and the weight of the graph is the semiring-sum of the weights of labelings. We show that we can model interesting algorithmic questions using this formalism - like computing the clique number of a graph or computing the permanent of a matrix. The evaluation problem is, given a weighted tiling system and a graph, to compute the weight of the graph. We study the complexity of the evaluation problem and give tight upper and lower bounds for several commutative semirings. Further we provide an efficient evaluation algorithm if the input graph is of bounded tree-width.
Cite as
C. Aiswarya and Paul Gastin. Weighted Tiling Systems for Graphs: Evaluation Complexity. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{aiswarya_et_al:LIPIcs.FSTTCS.2020.34,
author = {Aiswarya, C. and Gastin, Paul},
title = {{Weighted Tiling Systems for Graphs: Evaluation Complexity}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {34:1--34:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.34},
URN = {urn:nbn:de:0030-drops-132753},
doi = {10.4230/LIPIcs.FSTTCS.2020.34},
annote = {Keywords: Weighted graph tiling, tiling automata, Evaluation, Complexity, Tree-width}
}
Document
Process Symmetry in Probabilistic Transducers
Abstract
Model checking is the process of deciding whether a system satisfies a given specification. Often, when the setting comprises multiple processes, the specifications are over sets of input and output signals that correspond to individual processes. Then, many of the properties one wishes to specify are symmetric with respect to the processes identities. In this work, we consider the problem of deciding whether the given system exhibits symmetry with respect to the processes' identities. When the system is symmetric, this gives insight into the behaviour of the system, as well as allows the designer to use only representative specifications, instead of iterating over all possible process identities.
Specifically, we consider probabilistic systems, and we propose several variants of symmetry. We start with precise symmetry, in which, given a permutation π, the system maintains the exact distribution of permuted outputs, given a permuted inputs. We proceed to study approximate versions of symmetry, including symmetry induced by small L_∞ norm, variants of Parikh-image based symmetry, and qualitative symmetry. For each type of symmetry, we consider the problem of deciding whether a given system exhibits this type of symmetry.
Cite as
Shaull Almagor. Process Symmetry in Probabilistic Transducers. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 35:1-35:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{almagor:LIPIcs.FSTTCS.2020.35,
author = {Almagor, Shaull},
title = {{Process Symmetry in Probabilistic Transducers}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {35:1--35:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.35},
URN = {urn:nbn:de:0030-drops-132764},
doi = {10.4230/LIPIcs.FSTTCS.2020.35},
annote = {Keywords: Symmetry, Probabilistic Transducers, Model Checking, Permutations}
}
Document
Reachability in Dynamical Systems with Rounding
Abstract
We consider reachability in dynamical systems with discrete linear updates, but with fixed digital precision, i.e., such that values of the system are rounded at each step. Given a matrix M ∈ ℚ^{d × d}, an initial vector x ∈ ℚ^{d}, a granularity g ∈ ℚ_+ and a rounding operation [⋅] projecting a vector of ℚ^{d} onto another vector whose every entry is a multiple of g, we are interested in the behaviour of the orbit 𝒪 = ⟨[x], [M[x]],[M[M[x]]],… ⟩, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability - whether a given target y ∈ ℚ^{d} belongs to 𝒪 - is PSPACE-complete for hyperbolic systems (when no eigenvalue of M has modulus one). We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions.
Cite as
Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, and Markus A. Whiteland. Reachability in Dynamical Systems with Rounding. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{baier_et_al:LIPIcs.FSTTCS.2020.36,
author = {Baier, Christel and Funke, Florian and Jantsch, Simon and Karimov, Toghrul and Lefaucheux, Engel and Ouaknine, Jo\"{e}l and Pouly, Amaury and Purser, David and Whiteland, Markus A.},
title = {{Reachability in Dynamical Systems with Rounding}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {36:1--36:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.36},
URN = {urn:nbn:de:0030-drops-132778},
doi = {10.4230/LIPIcs.FSTTCS.2020.36},
annote = {Keywords: dynamical systems, rounding, reachability}
}
Document
Parameterized Complexity of Safety of Threshold Automata
Abstract
Threshold automata are a formalism for modeling fault-tolerant distributed algorithms. In this paper, we study the parameterized complexity of reachability of threshold automata. As a first result, we show that the problem becomes W[1]-hard even when parameterized by parameters which are quite small in practice. We then consider two restricted cases which arise in practice and provide fixed-parameter tractable algorithms for both these cases. Finally, we report on experimental results conducted on some protocols taken from the literature.
Cite as
A. R. Balasubramanian. Parameterized Complexity of Safety of Threshold Automata. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 37:1-37:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{balasubramanian:LIPIcs.FSTTCS.2020.37,
author = {Balasubramanian, A. R.},
title = {{Parameterized Complexity of Safety of Threshold Automata}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {37:1--37:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.37},
URN = {urn:nbn:de:0030-drops-132787},
doi = {10.4230/LIPIcs.FSTTCS.2020.37},
annote = {Keywords: Threshold automata, distributed algorithms, parameterized complexity}
}
Document
Uncertainty Reasoning for Probabilistic Petri Nets via Bayesian Networks
Abstract
This paper exploits extended Bayesian networks for uncertainty reasoning on Petri nets, where firing of transitions is probabilistic. In particular, Bayesian networks are used as symbolic representations of probability distributions, modelling the observer’s knowledge about the tokens in the net. The observer can study the net by monitoring successful and failed steps.
An update mechanism for Bayesian nets is enabled by relaxing some of their restrictions, leading to modular Bayesian nets that can conveniently be represented and modified. As for every symbolic representation, the question is how to derive information - in this case marginal probability distributions - from a modular Bayesian net. We show how to do this by generalizing the known method of variable elimination. The approach is illustrated by examples about the spreading of diseases (SIR model) and information diffusion in social networks. We have implemented our approach and provide runtime results.
Cite as
Rebecca Bernemann, Benjamin Cabrera, Reiko Heckel, and Barbara König. Uncertainty Reasoning for Probabilistic Petri Nets via Bayesian Networks. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bernemann_et_al:LIPIcs.FSTTCS.2020.38,
author = {Bernemann, Rebecca and Cabrera, Benjamin and Heckel, Reiko and K\"{o}nig, Barbara},
title = {{Uncertainty Reasoning for Probabilistic Petri Nets via Bayesian Networks}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {38:1--38:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.38},
URN = {urn:nbn:de:0030-drops-132794},
doi = {10.4230/LIPIcs.FSTTCS.2020.38},
annote = {Keywords: uncertainty reasoning, probabilistic knowledge, Petri nets, Bayesian networks}
}
Document
Synthesizing Safe Coalition Strategies
Abstract
Concurrent games with a fixed number of agents have been thoroughly studied, with various solution concepts and objectives for the agents. In this paper, we consider concurrent games with an arbitrary number of agents, and study the problem of synthesizing a coalition strategy to achieve a global safety objective. The problem is non-trivial since the agents do not know a priori how many they are when they start the game. We prove that the existence of a safe arbitrary-large coalition strategy for safety objectives is a PSPACE-hard problem that can be decided in exponential space.
Cite as
Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Synthesizing Safe Coalition Strategies. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2020.39,
author = {Bertrand, Nathalie and Bouyer, Patricia and Majumdar, Anirban},
title = {{Synthesizing Safe Coalition Strategies}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {39:1--39:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.39},
URN = {urn:nbn:de:0030-drops-132807},
doi = {10.4230/LIPIcs.FSTTCS.2020.39},
annote = {Keywords: concurrent games, parameterized verification, strategy synthesis}
}
Document
Dynamic Network Congestion Games
Abstract
Congestion games are a classical type of games studied in game theory, in which n players choose a resource, and their individual cost increases with the number of other players choosing the same resource. In network congestion games (NCGs), the resources correspond to simple paths in a graph, e.g. representing routing options from a source to a target. In this paper, we introduce a variant of NCGs, referred to as dynamic NCGs: in this setting, players take transitions synchronously, they select their next transitions dynamically, and they are charged a cost that depends on the number of players simultaneously using the same transition.
We study, from a complexity perspective, standard concepts of game theory in dynamic NCGs: social optima, Nash equilibria, and subgame perfect equilibria. Our contributions are the following: the existence of a strategy profile with social cost bounded by a constant is in PSPACE and NP-hard. (Pure) Nash equilibria always exist in dynamic NCGs; the existence of a Nash equilibrium with bounded cost can be decided in EXPSPACE, and computing a witnessing strategy profile can be done in doubly-exponential time. The existence of a subgame perfect equilibrium with bounded cost can be decided in 2EXPSPACE, and a witnessing strategy profile can be computed in triply-exponential time.
Cite as
Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur. Dynamic Network Congestion Games. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 40:1-40:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2020.40,
author = {Bertrand, Nathalie and Markey, Nicolas and Sadhukhan, Suman and Sankur, Ocan},
title = {{Dynamic Network Congestion Games}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {40:1--40:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.40},
URN = {urn:nbn:de:0030-drops-132811},
doi = {10.4230/LIPIcs.FSTTCS.2020.40},
annote = {Keywords: Congestion games, Nash equilibria, Subgame perfect equilibria, Complexity}
}
Document
On the Succinctness of Alternating Parity Good-For-Games Automata
Abstract
We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read.
We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we present a single exponential determinisation procedure and an Exptime upper bound to the problem of recognising whether an alternating automaton is GFG.
We also study the complexity of deciding "half-GFGness", a property specific to alternating automata that only requires nondeterministic choices to be resolved in an online manner. We show that this problem is PSpace-hard already for alternating automata on finite words.
Cite as
Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak. On the Succinctness of Alternating Parity Good-For-Games Automata. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 41:1-41:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{boker_et_al:LIPIcs.FSTTCS.2020.41,
author = {Boker, Udi and Kuperberg, Denis and Lehtinen, Karoliina and Skrzypczak, Micha{\l}},
title = {{On the Succinctness of Alternating Parity Good-For-Games Automata}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {41:1--41:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.41},
URN = {urn:nbn:de:0030-drops-132825},
doi = {10.4230/LIPIcs.FSTTCS.2020.41},
annote = {Keywords: Good for games, history-determinism, alternation}
}
Document
A Framework for Consistency Algorithms
Abstract
We present a framework that provides deterministic consistency algorithms for given memory models. Such an algorithm checks whether the executions of a shared-memory concurrent program are consistent under the axioms defined by a model. For memory models like SC and TSO, checking consistency is NP-complete. Our framework shows, that despite the hardness, fast deterministic consistency algorithms can be obtained by employing tools from fine-grained complexity.
The framework is based on a universal consistency problem which can be instantiated by different memory models. We construct an algorithm for the problem running in time 𝒪^*(2^k), where k is the number of write accesses in the execution that is checked for consistency. Each instance of the framework then admits an 𝒪^*(2^k)-time consistency algorithm. By applying the framework, we obtain corresponding consistency algorithms for SC, TSO, PSO, and RMO. Moreover, we show that the obtained algorithms for SC, TSO, and PSO are optimal in the fine-grained sense: there is no consistency algorithm for these running in time 2^{o(k)} unless the exponential time hypothesis fails.
Cite as
Peter Chini and Prakash Saivasan. A Framework for Consistency Algorithms. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{chini_et_al:LIPIcs.FSTTCS.2020.42,
author = {Chini, Peter and Saivasan, Prakash},
title = {{A Framework for Consistency Algorithms}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {42:1--42:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.42},
URN = {urn:nbn:de:0030-drops-132833},
doi = {10.4230/LIPIcs.FSTTCS.2020.42},
annote = {Keywords: Consistency, Weak Memory, Fine-Grained Complexity}
}
Document
Equivalence of Hidden Markov Models with Continuous Observations
Abstract
We consider Hidden Markov Models that emit sequences of observations that are drawn from continuous distributions. For example, such a model may emit a sequence of numbers, each of which is drawn from a uniform distribution, but the support of the uniform distribution depends on the state of the Hidden Markov Model. Such models generalise the more common version where each observation is drawn from a finite alphabet. We prove that one can determine in polynomial time whether two Hidden Markov Models with continuous observations are equivalent.
Cite as
Oscar Darwin and Stefan Kiefer. Equivalence of Hidden Markov Models with Continuous Observations. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 43:1-43:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{darwin_et_al:LIPIcs.FSTTCS.2020.43,
author = {Darwin, Oscar and Kiefer, Stefan},
title = {{Equivalence of Hidden Markov Models with Continuous Observations}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {43:1--43:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.43},
URN = {urn:nbn:de:0030-drops-132845},
doi = {10.4230/LIPIcs.FSTTCS.2020.43},
annote = {Keywords: Markov chains, equivalence, probabilistic systems, verification}
}
Document
Nivat-Theorem and Logic for Weighted Pushdown Automata on Infinite Words
Abstract
Recently, weighted ω-pushdown automata have been introduced by Droste, Ésik, Kuich. This new type of automaton has access to a stack and models quantitative aspects of infinite words. Here, we consider a simple version of those automata. The simple ω-pushdown automata do not use ε-transitions and have a very restricted stack access. In previous work, we could show this automaton model to be expressively equivalent to context-free ω-languages in the unweighted case. Furthermore, semiring-weighted simple ω-pushdown automata recognize all ω-algebraic series.
Here, we consider ω-valuation monoids as weight structures. As a first result, we prove that for this weight structure and for simple ω-pushdown automata, Büchi-acceptance and Muller-acceptance are expressively equivalent. In our second result, we derive a Nivat theorem for these automata stating that the behaviors of weighted ω-pushdown automata are precisely the projections of very simple ω-series restricted to ω-context-free languages. The third result is a weighted logic with the same expressive power as the new automaton model. To prove the equivalence, we use a similar result for weighted nested ω-word automata and apply our present result of expressive equivalence of Muller and Büchi acceptance.
Cite as
Manfred Droste, Sven Dziadek, and Werner Kuich. Nivat-Theorem and Logic for Weighted Pushdown Automata on Infinite Words. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 44:1-44:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{droste_et_al:LIPIcs.FSTTCS.2020.44,
author = {Droste, Manfred and Dziadek, Sven and Kuich, Werner},
title = {{Nivat-Theorem and Logic for Weighted Pushdown Automata on Infinite Words}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {44:1--44:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.44},
URN = {urn:nbn:de:0030-drops-132850},
doi = {10.4230/LIPIcs.FSTTCS.2020.44},
annote = {Keywords: Weighted automata, Pushdown automata, Infinite words, Weighted logic}
}
Document
Synchronization of Deterministic Visibly Push-Down Automata
Abstract
We generalize the concept of synchronizing words for finite automata, which map all states of the automata to the same state, to deterministic visibly push-down automata. Here, a synchronizing word w does not only map all states to the same state but also fulfills some conditions on the stack content of each run after reading w. We consider three types of these stack constraints: after reading w, the stack (1) is empty in each run, (2) contains the same sequence of stack symbols in each run, or (3) contains an arbitrary sequence which is independent of the other runs. We show that in contrast to general deterministic push-down automata, it is decidable for deterministic visibly push-down automata whether there exists a synchronizing word with each of these stack constraints, more precisely, the problems are in EXPTIME. Under the constraint (1), the problem is even in P. For the sub-classes of deterministic very visibly push-down automata, the problem is in P for all three types of constraints. We further study variants of the synchronization problem where the number of turns in the stack height behavior caused by a synchronizing word is restricted, as well as the problem of synchronizing a variant of a sequential transducer, which shows some visibly behavior, by a word that synchronizes the states and produces the same output on all runs.
Cite as
Henning Fernau and Petra Wolf. Synchronization of Deterministic Visibly Push-Down Automata. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 45:1-45:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{fernau_et_al:LIPIcs.FSTTCS.2020.45,
author = {Fernau, Henning and Wolf, Petra},
title = {{Synchronization of Deterministic Visibly Push-Down Automata}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {45:1--45:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.45},
URN = {urn:nbn:de:0030-drops-132861},
doi = {10.4230/LIPIcs.FSTTCS.2020.45},
annote = {Keywords: Synchronizing word, Deterministic visibly push-down automata, Deterministc finite atuomata, Finite-turn push-down automata, Sequential transducer, Computational complexity}
}
Document
Synthesis from Weighted Specifications with Partial Domains over Finite Words
Abstract
In this paper, we investigate the synthesis problem of terminating reactive systems from quantitative specifications. Such systems are modeled as finite transducers whose executions are represented as finite words in (I × O)^*, where I, O are finite sets of input and output symbols, respectively. A weighted specification S assigns a rational value (or -∞) to words in (I × O)^*, and we consider three kinds of objectives for synthesis, namely threshold objectives where the system’s executions are required to be above some given threshold, best-value and approximate objectives where the system is required to perform as best as it can by providing output symbols that yield the best value and ε-best value respectively w.r.t. S. We establish a landscape of decidability results for these three objectives and weighted specifications with partial domain over finite words given by deterministic weighted automata equipped with sum, discounted-sum and average measures. The resulting objectives are not regular in general and we develop an infinite game framework to solve the corresponding synthesis problems, namely the class of (weighted) critical prefix games.
Cite as
Emmanuel Filiot, Christof Löding, and Sarah Winter. Synthesis from Weighted Specifications with Partial Domains over Finite Words. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{filiot_et_al:LIPIcs.FSTTCS.2020.46,
author = {Filiot, Emmanuel and L\"{o}ding, Christof and Winter, Sarah},
title = {{Synthesis from Weighted Specifications with Partial Domains over Finite Words}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {46:1--46:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.46},
URN = {urn:nbn:de:0030-drops-132874},
doi = {10.4230/LIPIcs.FSTTCS.2020.46},
annote = {Keywords: synthesis, weighted games, weighted automata on finite words}
}
Document
Reachability for Updatable Timed Automata Made Faster and More Effective
Abstract
Updatable timed automata (UTA) are extensions of classical timed automata that allow special updates to clock variables, like x: = x - 1, x : = y + 2, etc., on transitions. Reachability for UTA is undecidable in general. Various subclasses with decidable reachability have been studied. A generic approach to UTA reachability consists of two phases: first, a static analysis of the automaton is performed to compute a set of clock constraints at each state; in the second phase, reachable sets of configurations, called zones, are enumerated. In this work, we improve the algorithm for the static analysis. Compared to the existing algorithm, our method computes smaller sets of constraints and guarantees termination for more UTA, making reachability faster and more effective. As the main application, we get an alternate proof of decidability and a more efficient algorithm for timed automata with bounded subtraction, a class of UTA widely used for modelling scheduling problems. We have implemented our procedure in the tool TChecker and conducted experiments that validate the benefits of our approach.
Cite as
Paul Gastin, Sayan Mukherjee, and B Srivathsan. Reachability for Updatable Timed Automata Made Faster and More Effective. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 47:1-47:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{gastin_et_al:LIPIcs.FSTTCS.2020.47,
author = {Gastin, Paul and Mukherjee, Sayan and Srivathsan, B},
title = {{Reachability for Updatable Timed Automata Made Faster and More Effective}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {47:1--47:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.47},
URN = {urn:nbn:de:0030-drops-132881},
doi = {10.4230/LIPIcs.FSTTCS.2020.47},
annote = {Keywords: Updatable timed automata, Reachability, Zones, Simulations, Static analysis}
}
Document
Active Prediction for Discrete Event Systems
Abstract
A central task in partially observed controllable system is to detect or prevent the occurrence of certain events called faults. Systems for which one can design a controller avoiding the faults are called actively safe. Otherwise, one may require that a fault is eventually detected, which is the task of diagnosis. Systems for which one can design a controller detecting the faults are called actively diagnosable. An intermediate requirement is prediction, which consists in determining that a fault will occur whatever the future behaviour of the system. When a system is not predictable, one may be interested in designing a controller to make it so. Here we study the latter problem, called active prediction, and its associated property, active predictability. In other words, we investigate how to determine whether or not a system enjoys the active predictability property, i.e., there exists an active predictor for the system.
Our contributions are threefold. From a semantical point of view, we refine the notion of predictability by adding two quantitative requirements: the minimal and maximal delay before the occurence of the fault, and we characterize the requirements fulfilled by a controller that performs predictions. Then we show that active predictability is EXPTIME-complete where the upper bound is obtained via a game-based approach. Finally we establish that active predictability is equivalent to active safety when the maximal delay is beyond a threshold depending on the size of the system, and we show that this threshold is accurate by exhibiting a family of systems fulfilling active predictability but not active safety.
Cite as
Stefan Haar, Serge Haddad, Stefan Schwoon, and Lina Ye. Active Prediction for Discrete Event Systems. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 48:1-48:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{haar_et_al:LIPIcs.FSTTCS.2020.48,
author = {Haar, Stefan and Haddad, Serge and Schwoon, Stefan and Ye, Lina},
title = {{Active Prediction for Discrete Event Systems}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {48:1--48:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.48},
URN = {urn:nbn:de:0030-drops-132898},
doi = {10.4230/LIPIcs.FSTTCS.2020.48},
annote = {Keywords: Automata Theory, Partially observed systems, Diagnosability, Predictability}
}
Document
Comparing Labelled Markov Decision Processes
Abstract
A labelled Markov decision process is a labelled Markov chain with nondeterminism, i.e., together with a strategy a labelled MDP induces a labelled Markov chain. The model is related to interval Markov chains. Motivated by applications of equivalence checking for the verification of anonymity, we study the algorithmic comparison of two labelled MDPs, in particular, whether there exist strategies such that the MDPs become equivalent/inequivalent, both in terms of trace equivalence and in terms of probabilistic bisimilarity. We provide the first polynomial-time algorithms for computing memoryless strategies to make the two labelled MDPs inequivalent if such strategies exist. We also study the computational complexity of qualitative problems about making the total variation distance and the probabilistic bisimilarity distance less than one or equal to one.
Cite as
Stefan Kiefer and Qiyi Tang. Comparing Labelled Markov Decision Processes. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 49:1-49:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kiefer_et_al:LIPIcs.FSTTCS.2020.49,
author = {Kiefer, Stefan and Tang, Qiyi},
title = {{Comparing Labelled Markov Decision Processes}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {49:1--49:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.49},
URN = {urn:nbn:de:0030-drops-132903},
doi = {10.4230/LIPIcs.FSTTCS.2020.49},
annote = {Keywords: Markov decision processes, Markov chains, Behavioural metrics}
}
Document
Computable Analysis for Verified Exact Real Computation
Abstract
We use ideas from computable analysis to formalize exact real number computation in the Coq proof assistant. Our formalization is built on top of the Incone library, a Coq library for computable analysis. We use the theoretical framework that computable analysis provides to systematically generate target specifications for real number algorithms. First we give very simple algorithms that fulfill these specifications based on rational approximations. To provide more efficient algorithms, we develop alternate representations that utilize an existing formalization of floating-point algorithms and interval arithmetic in combination with methods used by software packages for exact real arithmetic that focus on execution speed. We also define a general framework to define real number algorithms independently of their concrete encoding and to prove them correct. Algorithms verified in our framework can be extracted to Haskell programs for efficient computation. The performance of the extracted code is comparable to programs produced using non-verified software packages. This is without the need to optimize the extracted code by hand.
As an example, we formalize an algorithm for the square root function based on the Heron method. The algorithm is parametric in the implementation of the real number datatype, not referring to any details of its implementation. Thus the same verified algorithm can be used with different real number representations. Since Boolean valued comparisons of real numbers are not decidable, our algorithms use basic operations that take values in the Kleeneans and Sierpinski space. We develop some of the theory of these spaces. To capture the semantics of non-sequential operations, such as the "parallel or", we use multivalued functions.
Cite as
Michal Konečný, Florian Steinberg, and Holger Thies. Computable Analysis for Verified Exact Real Computation. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 50:1-50:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{konecny_et_al:LIPIcs.FSTTCS.2020.50,
author = {Kone\v{c}n\'{y}, Michal and Steinberg, Florian and Thies, Holger},
title = {{Computable Analysis for Verified Exact Real Computation}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {50:1--50:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.50},
URN = {urn:nbn:de:0030-drops-132914},
doi = {10.4230/LIPIcs.FSTTCS.2020.50},
annote = {Keywords: Computable Analysis, exact real computation, formal proofs, proof assistant, Coq}
}
Document
Perspective Games with Notifications
Abstract
A reactive system has to satisfy its specification in all environments. Accordingly, design of correct reactive systems corresponds to the synthesis of winning strategies in games that model the interaction between the system and its environment. The game is played on a graph whose vertices are partitioned among the players. The players jointly generate a path in the graph, with each player deciding the successor vertex whenever the path reaches a vertex she owns. The objective of the system player is to force the computation induced by the generated infinite path to satisfy a given specification. The traditional way of modelling uncertainty in such games is observation-based. There, uncertainty is longitudinal: the players partially observe all vertices in the history. Recently, researchers introduced perspective games, where uncertainty is transverse: players fully observe the vertices they own and have no information about the behavior of the computation between visits in such vertices. We introduce and study perspective games with notifications: uncertainty is still transverse, yet a player may be notified about events that happen between visits in vertices she owns. We distinguish between structural notifications, for example about visits in some vertices, and behavioral notifications, for example about the computation exhibiting a certain behavior. We study the theoretic properties of perspective games with notifications, and the problem of deciding whether a player has a winning perspective strategy. Such a strategy depends only on the visible history, which consists of both visits in vertices the player owns and notifications during visits in other vertices. We show that the problem is EXPTIME-complete for objectives given by a deterministic or universal parity automaton over an alphabet that labels the vertices of the game, and notifications given by a deterministic satellite, and is 2EXPTIME-complete for LTL objectives. In all cases, the complexity in the size of the graph and the satellite is polynomial - exponentially easier than games with observation-based partial visibility. We also analyze the complexity of the problem for richer types of satellites.
Cite as
Orna Kupferman and Noam Shenwald. Perspective Games with Notifications. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 51:1-51:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kupferman_et_al:LIPIcs.FSTTCS.2020.51,
author = {Kupferman, Orna and Shenwald, Noam},
title = {{Perspective Games with Notifications}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {51:1--51:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.51},
URN = {urn:nbn:de:0030-drops-132928},
doi = {10.4230/LIPIcs.FSTTCS.2020.51},
annote = {Keywords: Games, Incomplete Information, Automata}
}
Document
On the Complexity of Multi-Pushdown Games
Abstract
We study the influence of parameters like the number of contexts, phases, and stacks on the complexity of solving parity games over concurrent recursive programs. Our first result shows that k-context games are b-EXPTIME-complete, where b = max{k-2, 1}. This means up to three contexts do not increase the complexity over an analysis for the sequential case. Our second result shows that for ordered k-stack as well as k-phase games the complexity jumps to k-EXPTIME-complete.
Cite as
Roland Meyer and Sören van der Wall. On the Complexity of Multi-Pushdown Games. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 52:1-52:35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{meyer_et_al:LIPIcs.FSTTCS.2020.52,
author = {Meyer, Roland and van der Wall, S\"{o}ren},
title = {{On the Complexity of Multi-Pushdown Games}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {52:1--52:35},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.52},
URN = {urn:nbn:de:0030-drops-132930},
doi = {10.4230/LIPIcs.FSTTCS.2020.52},
annote = {Keywords: concurrency, complexity, games, infinite state, multi-pushdown}
}
Document
Higher-Order Nonemptiness Step by Step
Abstract
We show a new simple algorithm that checks whether a given higher-order grammar generates a nonempty language of trees. The algorithm amounts to a procedure that transforms a grammar of order n to a grammar of order n-1, preserving nonemptiness, and increasing the size only exponentially. After repeating the procedure n times, we obtain a grammar of order 0, whose nonemptiness can be easily checked. Since the size grows exponentially at each step, the overall complexity is n-EXPTIME, which is known to be optimal. More precisely, the transformation (and hence the whole algorithm) is linear in the size of the grammar, assuming that the arity of employed nonterminals is bounded by a constant. The same algorithm allows to check whether an infinite tree generated by a higher-order recursion scheme is accepted by an alternating safety (or reachability) automaton, because this question can be reduced to the nonemptiness problem by taking a product of the recursion scheme with the automaton.
A proof of correctness of the algorithm is formalised in the proof assistant Coq. Our transformation is motivated by a similar transformation of Asada and Kobayashi (2020) changing a word grammar of order n to a tree grammar of order n-1. The step-by-step approach can be opposed to previous algorithms solving the nonemptiness problem "in one step", being compulsorily more complicated.
Cite as
Paweł Parys. Higher-Order Nonemptiness Step by Step. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 53:1-53:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{parys:LIPIcs.FSTTCS.2020.53,
author = {Parys, Pawe{\l}},
title = {{Higher-Order Nonemptiness Step by Step}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {53:1--53:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.53},
URN = {urn:nbn:de:0030-drops-132941},
doi = {10.4230/LIPIcs.FSTTCS.2020.53},
annote = {Keywords: Higher-order grammars, Nonemptiness, Model-checking, Transformation, Order reduction}
}
Document
The Degree of a Finite Set of Words
Abstract
We generalize the notions of the degree and composition from uniquely decipherable codes to arbitrary finite sets of words. We prove that if X = Y∘Z is a composition of finite sets of words with Y complete, then d(X) = d(Y) ⋅ d(Z), where d(T) is the degree of T. We also show that a finite set is synchronizing if and only if its degree equals one.
This is done by considering, for an arbitrary finite set X of words, the transition monoid of an automaton recognizing X^* with multiplicities. We prove a number of results for such monoids, which generalize corresponding results for unambiguous monoids of relations.
Cite as
Dominique Perrin and Andrew Ryzhikov. The Degree of a Finite Set of Words. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 54:1-54:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{perrin_et_al:LIPIcs.FSTTCS.2020.54,
author = {Perrin, Dominique and Ryzhikov, Andrew},
title = {{The Degree of a Finite Set of Words}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {54:1--54:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.54},
URN = {urn:nbn:de:0030-drops-132952},
doi = {10.4230/LIPIcs.FSTTCS.2020.54},
annote = {Keywords: synchronizing set, degree of a set, group of a set, monoid of relations}
}
Document
What You Must Remember When Transforming Datawords
Abstract
Streaming Data String Transducers (SDSTs) were introduced to model a class of imperative and a class of functional programs, manipulating lists of data items. These can be used to write commonly used routines such as insert, delete and reverse. SDSTs can handle data values from a potentially infinite data domain. The model of Streaming String Transducers (SSTs) is the fragment of SDSTs where the infinite data domain is dropped and only finite alphabets are considered. SSTs have been much studied from a language theoretical point of view. We introduce data back into SSTs, just like data was introduced to finite state automata to get register automata. The result is Streaming String Register Transducers (SSRTs), which is a subclass of SDSTs.
We use origin semantics for SSRTs and give a machine independent characterization, along the lines of Myhill-Nerode theorem. Machine independent characterizations for similar models are the basis of learning algorithms and enable us to understand fragments of the models. Origin semantics of transducers track which positions of the output originate from which positions of the input. Although a restriction, using origin semantics is well justified and is known to simplify many problems related to transducers. We use origin semantics as a technical building block, in addition to characterizations of deterministic register automata. However, we need to build more on top of these to overcome some challenges unique to SSRTs.
Cite as
M. Praveen. What You Must Remember When Transforming Datawords. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 55:1-55:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{praveen:LIPIcs.FSTTCS.2020.55,
author = {Praveen, M.},
title = {{What You Must Remember When Transforming Datawords}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {55:1--55:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.55},
URN = {urn:nbn:de:0030-drops-132967},
doi = {10.4230/LIPIcs.FSTTCS.2020.55},
annote = {Keywords: Streaming String Transducers, Data words, Machine independent characterization}
}
Document
Minimising Good-For-Games Automata Is NP-Complete
Abstract
This paper discusses the hardness of finding minimal good-for-games (GFG) Büchi, Co-Büchi, and parity automata with state based acceptance. The problem appears to sit between finding small deterministic and finding small nondeterministic automata, where minimality is NP-complete and PSPACE-complete, respectively. However, recent work of Radi and Kupferman has shown that minimising Co-Büchi automata with transition based acceptance is tractable, which suggests that the complexity of minimising GFG automata might be cheaper than minimising deterministic automata.
We show for the standard state based acceptance that the minimality of a GFG automaton is NP-complete for Büchi, Co-Büchi, and parity GFG automata. The proofs are a surprisingly straight forward generalisation of the proofs from deterministic Büchi automata: they use a similar reductions, and the same hard class of languages.
Cite as
Sven Schewe. Minimising Good-For-Games Automata Is NP-Complete. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 56:1-56:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{schewe:LIPIcs.FSTTCS.2020.56,
author = {Schewe, Sven},
title = {{Minimising Good-For-Games Automata Is NP-Complete}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {56:1--56:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.56},
URN = {urn:nbn:de:0030-drops-132973},
doi = {10.4230/LIPIcs.FSTTCS.2020.56},
annote = {Keywords: Good-for-Games Automata, Automata Minimisation}
}
Document
Static Race Detection for RTOS Applications
Abstract
We present a static analysis technique for detecting data races in Real-Time Operating System (RTOS) applications. These applications are often employed in safety-critical tasks and the presence of races may lead to erroneous behaviour with serious consequences. Analyzing these applications is challenging due to the variety of non-standard synchronization mechanisms they use. We propose a technique based on the notion of an "occurs-in-between" relation between statements. This notion enables us to capture the interplay of various synchronization mechanisms. We use a pre-analysis and a small set of not-occurs-in-between patterns to detect whether two statements may race with each other. Our experimental evaluation shows that the technique is efficient and effective in identifying races with high precision.
Cite as
Rishi Tulsyan, Rekha Pai, and Deepak D'Souza. Static Race Detection for RTOS Applications. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 57:1-57:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{tulsyan_et_al:LIPIcs.FSTTCS.2020.57,
author = {Tulsyan, Rishi and Pai, Rekha and D'Souza, Deepak},
title = {{Static Race Detection for RTOS Applications}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {57:1--57:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.57},
URN = {urn:nbn:de:0030-drops-132983},
doi = {10.4230/LIPIcs.FSTTCS.2020.57},
annote = {Keywords: Static analysis, concurrency, data-race detection, RTOS}
}
Document
Synchronization Under Dynamic Constraints
Abstract
We introduce a new natural variant of the synchronization problem. Our aim is to model different constraints on the order in which a potential synchronizing word might traverse through the states. We discuss how a word can induce a state-order and examine the computational complexity of different variants of the problem whether an automaton can be synchronized with a word of which the induced order agrees with a given relation. While most of the problems are PSPACE-complete we also observe NP-complete variants and variants solvable in polynomial time. One of them is the careful synchronization problem for partial weakly acyclic automata (which are partial automata whose states can be ordered such that no transition leads to a smaller state), which is shown to be solvable in time 𝒪(k² n²) where n is the size of the state set and k is the alphabet-size. The algorithm even computes a synchronizing word as a witness. This is quite surprising as the careful synchronization problem uses to be a hard problem for most classes of automata. We will also observe a drop in the complexity if we track the orders of states on several paths simultaneously instead of tracking the set of active states. Further, we give upper bounds on the length of a synchronizing word depending on the size of the input relation and show that (despite the partiality) the bound of the Černý conjecture also holds for partial weakly acyclic automata.
Cite as
Petra Wolf. Synchronization Under Dynamic Constraints. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 58:1-58:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{wolf:LIPIcs.FSTTCS.2020.58,
author = {Wolf, Petra},
title = {{Synchronization Under Dynamic Constraints}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {58:1--58:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-174-0},
ISSN = {1868-8969},
year = {2020},
volume = {182},
editor = {Saxena, Nitin and Simon, Sunil},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.58},
URN = {urn:nbn:de:0030-drops-132998},
doi = {10.4230/LIPIcs.FSTTCS.2020.58},
annote = {Keywords: Synchronizing automaton, \v{C}ern\'{y} conjecture, Reset sequence, Dynamic constraints, Computational complexity}
}