Volume
LIPIcs, Volume 65
36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)
Event
FSTTCS 2016, December 13-15, 2016, Chennai, IndiaEditors
Publication Details
- published at: 2016-12-10
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-027-9
- DBLP: db/conf/fsttcs/fsttcs2016
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 65, FSTTCS'16, Complete Volume
Abstract
LIPICs, Volume 65, FSTTCS'16, Complete Volume
Cite as
36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@Proceedings{lal_et_al:LIPIcs.FSTTCS.2016,
title = {{LIPICs, Volume 65, FSTTCS'16, Complete Volume}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016},
URN = {urn:nbn:de:0030-drops-69074},
doi = {10.4230/LIPIcs.FSTTCS.2016},
annote = {Keywords: Software/Program Verification, Models of Computation, Modes of Computation, Complexity Measures and Classes, Nonnumerical Algorithms and Problems Specifying and Verifying and Reasoning about Programs, Mathematical Logic, Formal Languages}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers
Abstract
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers
Cite as
36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{lal_et_al:LIPIcs.FSTTCS.2016.0,
author = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
title = {{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.0},
URN = {urn:nbn:de:0030-drops-68412},
doi = {10.4230/LIPIcs.FSTTCS.2016.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}
}
Document
Invited Talk
Fast and Powerful Hashing Using Tabulation (Invited Talk)
Abstract
Randomized algorithms are often enjoyed for their simplicity, but the hash functions employed to yield the desired probabilistic guarantees are often too complicated to be practical. Here we survey recent results on how simple hashing schemes based on tabulation provide unexpectedly strong guarantees.
Simple tabulation hashing dates back to Zobrist [1970]. Keys are viewed as consisting of c characters and we have precomputed character tables h_1, ... , h_q mapping characters to random hash values. A key x = (x_1 , ..., x_c) is hashed to h_1[x_1] + h_2[x_2] ... + h_c[x_c]. This scheme is very fast with character tables in cache. While simple tabulation is not even 4-independent, it does
provide many of the guarantees that are normally obtained via higher independence, e.g., linear probing and Cuckoo hashing.
Next we consider twisted tabulation where one character is "twisted" with some simple operations. The resulting hash function has powerful distributional properties: Chernoff-Hoeffding type tail bounds and a very small bias for min-wise hashing.
Finally, we consider double tabulation where we compose two simple tabulation functions, applying one to the output of the other, and show that this yields very high independence in the classic framework of Carter and Wegman [1977]. In fact, w.h.p., for a given set of size
proportional to that of the space consumed, double tabulation gives fully-random hashing.
While these tabulation schemes are all easy to implement and use, their analysis is not.
Cite as
Mikkel Thorup. Fast and Powerful Hashing Using Tabulation (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{thorup:LIPIcs.FSTTCS.2016.1,
author = {Thorup, Mikkel},
title = {{Fast and Powerful Hashing Using Tabulation}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.1},
URN = {urn:nbn:de:0030-drops-68869},
doi = {10.4230/LIPIcs.FSTTCS.2016.1},
annote = {Keywords: Hashing, Randomized Algorithms}
}
Document
Invited Talk
Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk)
Abstract
Safety of a distributed protocol means that the protocol never reaches a bad state, e.g., a state where two nodes become leaders in a leader-election protocol. Proving safety is obviously undecidable since such protocols are run by an unbounded number of nodes, and their safety needs to be established for any number of nodes. I will describe a deductive approach for proving safety, based on the concept of universally quantified inductive invariants—an adaptation of the mathematical concept of induction to the domain of programs. In the deductive approach, the programmer specifies a candidate inductive invariant and the system automatically checks if it is inductive. By restricting the invariants to be universally quantified, this approach can be effectively implemented with a SAT solver.
This is a joint work with Ken McMillan (Microsoft Research), Oded Padon (Tel Aviv University), Aurojit Panda (UC Berkeley), and Sharon Shoham (Tel Aviv University) and was integrated into the IVY system. The work is inspired by Shachar Itzhaky's thesis.
Cite as
Mooly Sagiv. Simple Invariants for Proving the Safety of Distributed Protocols (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{sagiv:LIPIcs.FSTTCS.2016.2,
author = {Sagiv, Mooly},
title = {{Simple Invariants for Proving the Safety of Distributed Protocols}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.2},
URN = {urn:nbn:de:0030-drops-68877},
doi = {10.4230/LIPIcs.FSTTCS.2016.2},
annote = {Keywords: Program verification, Distributed protocols, Deductive reasoning}
}
Document
Invited Talk
My O Is Bigger Than Yours (Invited Talk)
Abstract
This invited talk starts off with a review of probabilistic safety assessment (PSA) methods currently exercised across the nuclear power plant domain worldwide. It then elaborates on crucial aspects of the Fukushima Dai-ichi accident which are not considered properly in contemporary PSA studies. New kinds of PSA are needed so as to take into account external hazards, dynamic aspects of accident progression, and partial information. All of these come with obvious increases in algorithmic analysis complexity. This motivates our ongoing work to gradually tackle the resulting modelling and analysis problems. They revolve around static and dynamic fault trees, open interpretations of compositional Markov models and advances in their effective numerical analysis.
Cite as
Holger Hermanns. My O Is Bigger Than Yours (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{hermanns:LIPIcs.FSTTCS.2016.3,
author = {Hermanns, Holger},
title = {{My O Is Bigger Than Yours}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {3:1--3:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.3},
URN = {urn:nbn:de:0030-drops-68881},
doi = {10.4230/LIPIcs.FSTTCS.2016.3},
annote = {Keywords: Probabilistic Safety Analysis, Fault Trees, Compositionality, Markov Models, Model Checking}
}
Document
Invited Talk
Continuous Optimization: The “Right” Language for Graph Algorithms? (Invited Talk)
Abstract
Traditionally, we view graphs as purely combinatorial objects and tend to design our graph algorithms to be combinatorial as well. In fact, in the context of algorithms, "combinatorial" became a synonym of "fast".
Recent work, however, shows that a number of such "inherently combinatorial" graph problems can be solved much faster using methods that are very "non-combinatorial". Specifically, by approaching these problems with tools and notions borrowed from linear algebra and, more broadly, from continuous optimization. A notable examples here are the recent lines of work on the maximum flow problem, the bipartite matching problem, and the shortest path problem in graphs with negative-length arcs.
This raises an intriguing question: Is continuous optimization a more suitable and principled optics for fast graph algorithms than the classic combinatorial view? In this talk, I will discuss this question as well as the developments that motivated it.
Cite as
Aleksander Madry. Continuous Optimization: The “Right” Language for Graph Algorithms? (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{madry:LIPIcs.FSTTCS.2016.4,
author = {Madry, Aleksander},
title = {{Continuous Optimization: The “Right” Language for Graph Algorithms?}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {4:1--4:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.4},
URN = {urn:nbn:de:0030-drops-68890},
doi = {10.4230/LIPIcs.FSTTCS.2016.4},
annote = {Keywords: maximum flow problem, bipartite matchings, interior-point methods, gradient decent method, Laplacian linear systems}
}
Document
Invited Talk
Graph Decompositions and Algorithms (Invited Talk)
Abstract
We overview the recent progress in solving intractable optimization problems on planar graphs as well as other classes of sparse graphs. In particular, we discuss how tools from Graph Minors theory can be used to obtain:
* subexponential parameterized algorithms
* approximation algorithms, and
* preprocessing and kernelization algorithms
on these classes of graphs.
Cite as
Fedor V. Fomin. Graph Decompositions and Algorithms (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{fomin:LIPIcs.FSTTCS.2016.5,
author = {Fomin, Fedor V.},
title = {{Graph Decompositions and Algorithms}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {5:1--5:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.5},
URN = {urn:nbn:de:0030-drops-68903},
doi = {10.4230/LIPIcs.FSTTCS.2016.5},
annote = {Keywords: Algorithms, logic, graph minor}
}
Document
Invited Talk
Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution (Invited Talk)
Abstract
A crucial problem in software security is the detection of side-channels. Information gained by observing non-functional properties of program executions (such as execution time or memory usage) can enable attackers to infer secret information (such as a password). In this
talk, I will discuss how symbolic execution, combined with a model counting constraint solver, can be used for quantifying side-channel leakage in Java programs. In addition to computing information leakage for a single run of a program, I will also discuss computation of information leakage for multiple runs for a type of side channels called segmented oracles. In segmented oracles, the attacker is able to explore each segment of a secret (for example each character of a password) independently. For segmented oracles, it is possible to compute information leakage for multiple runs using only the path constraints generated from a single run symbolic execution. These results have been implemented as an extension to the symbolic execution tool Symbolic Path Finder (SPF) using the SMT solver Z3 and two model counting constraint solvers LattE and ABC.
Cite as
Tevfik Bultan. Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 6:1-6:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bultan:LIPIcs.FSTTCS.2016.6,
author = {Bultan, Tevfik},
title = {{Side Channel Analysis Using a Model Counting Constraint Solver and Symbolic Execution}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {6:1--6:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.6},
URN = {urn:nbn:de:0030-drops-68914},
doi = {10.4230/LIPIcs.FSTTCS.2016.6},
annote = {Keywords: Side-channels, quantitative information flow, symbolic execution, model counting, constraint solvers}
}
Document
Mixed-Criticality Scheduling to Minimize Makespan
Abstract
In the mixed-criticality job model, each job is characterized by two execution time parameters, representing a smaller (less conservative) estimate and a larger (more conservative) estimate on its actual, unknown, execution time. Each job is further classified as being either less critical or more critical. The desired execution semantics are that all jobs should execute correctly provided all jobs complete upon being allowed to execute for up to the smaller of their execution time estimates, whereas if some jobs need to execute beyond their smaller execution time estimates (but not beyond their larger execution time estimates), then only the jobs classified as being more critical are required to execute correctly. The scheduling of collections of such mixed-criticality jobs upon identical multiprocessor platforms in order to minimize the makespan is considered here.
Cite as
Sanjoy Baruah, Arvind Easwaran, and Zhishan Guo. Mixed-Criticality Scheduling to Minimize Makespan. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 7:1-7:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{baruah_et_al:LIPIcs.FSTTCS.2016.7,
author = {Baruah, Sanjoy and Easwaran, Arvind and Guo, Zhishan},
title = {{Mixed-Criticality Scheduling to Minimize Makespan}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {7:1--7:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.7},
URN = {urn:nbn:de:0030-drops-68429},
doi = {10.4230/LIPIcs.FSTTCS.2016.7},
annote = {Keywords: Scheduling, Mixed criticality, Identical parallel machines, Makespan minimization, Approximation algorithm.}
}
Document
Capacitated k-Center Problem with Vertex Weights
Abstract
We study the capacitated k-center problem with vertex weights. It is a generalization of the well known k-center problem. In this variant each vertex has a weight and a capacity. The assignment cost of a vertex to a center is given by the product of the weight of the vertex and its distance to
the center. The distances are assumed to form a metric. Each center can only serve as many vertices as its capacity. We show an n^{1-epsilon}-approximation hardness for this problem, for any epsilon > 0, where n is the number of vertices in the input. Both the capacitated and the weighted versions of the k-center problem individually can be approximated within a constant factor. Yet the common extension of both the generalizations cannot be approximated efficiently within a constant factor, unless P = NP. This problem, to the best of our knowledge, is the first facility location problem with metric distances known to have a super-constant inapproximability result. The hardness result easily generalizes to versions of the problem that consider the p-norm of the assignment costs (weighted distances) as the objective function. We give n^{1- 1/p - epsilon}-approximation hardness for this problem, for p>1.
We complement the hardness result by showing a simple n-approximation algorithm for this problem. We also give a bi-criteria constant factor approximation algorithm, for the case of uniform capacities, which opens at most 2k centers.
Cite as
Aounon Kumar. Capacitated k-Center Problem with Vertex Weights. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 8:1-8:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{kumar:LIPIcs.FSTTCS.2016.8,
author = {Kumar, Aounon},
title = {{Capacitated k-Center Problem with Vertex Weights}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {8:1--8:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.8},
URN = {urn:nbn:de:0030-drops-68438},
doi = {10.4230/LIPIcs.FSTTCS.2016.8},
annote = {Keywords: approximation hardness, k-center, gadget reduction}
}
Document
Improved Pseudo-Polynomial-Time Approximation for Strip Packing
Abstract
We study the strip packing problem, a classical packing problem which generalizes both bin packing and makespan minimization. Here we are given a set of axis-parallel rectangles in the two-dimensional plane and the goal is to pack them in a vertical strip of fixed width such that the height of the obtained packing is minimized. The packing must be non-overlapping and the rectangles cannot be rotated.
A reduction from the partition problem shows that no approximation better than 3/2 is possible for strip packing in polynomial time (assuming P!=NP). Nadiradze and Wiese [SODA16] overcame this barrier by presenting a (7/5+epsilon)-approximation algorithm in pseudo-polynomial-time (PPT). As the problem is strongly NP-hard, it does not admit an exact PPT algorithm (though a PPT approximation scheme might exist).
In this paper we make further progress on the PPT approximability of strip packing, by presenting a (4/3+epsilon)-approximation algorithm. Our result is based on a non-trivial repacking of some rectangles in the "empty space" left by the construction by Nadiradze and Wiese, and in some sense pushes their approach to its limit.
Our PPT algorithm can be adapted to the case where we are allowed to rotate the rectangles by 90 degrees, achieving the same approximation factor and breaking the polynomial-time approximation barrier of 3/2 for the case with rotations as well.
Cite as
Waldo Gálvez, Fabrizio Grandoni, Salvatore Ingala, and Arindam Khan. Improved Pseudo-Polynomial-Time Approximation for Strip Packing. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{galvez_et_al:LIPIcs.FSTTCS.2016.9,
author = {G\'{a}lvez, Waldo and Grandoni, Fabrizio and Ingala, Salvatore and Khan, Arindam},
title = {{Improved Pseudo-Polynomial-Time Approximation for Strip Packing}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {9:1--9:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.9},
URN = {urn:nbn:de:0030-drops-68445},
doi = {10.4230/LIPIcs.FSTTCS.2016.9},
annote = {Keywords: approximation algorithms, strip packing, rectangle packing, cutting-stock problem}
}
Document
Embedding Approximately Low-Dimensional l_2^2 Metrics into l_1
Abstract
Goemans showed that any n points x_1,..., x_n in d-dimensions satisfying l_2^2 triangle inequalities can be embedded into l_{1}, with worst-case distortion at most sqrt{d}. We consider an extension of this theorem to the case when the points are approximately low-dimensional as opposed to exactly low-dimensional, and prove the following analogous theorem, albeit with average distortion guarantees: There exists an l_{2}^{2}-to-l_{1} embedding with average distortion at most the stable rank, sr(M), of the matrix M consisting of columns {x_i-x_j}_{i<j}. Average distortion embedding suffices for applications such as the SPARSEST CUT problem. Our embedding gives an approximation algorithm for the SPARSEST CUT problem on low threshold-rank graphs, where earlier work was inspired by Lasserre SDP hierarchy, and improves on a previous result of the first and third author [Deshpande and Venkat, in Proc. 17th APPROX, 2014]. Our ideas give a new perspective on l_{2}^{2} metric, an alternate proof of Goemans' theorem, and a simpler proof for average distortion sqrt{d}.
Cite as
Amit Deshpande, Prahladh Harsha, and Rakesh Venkat. Embedding Approximately Low-Dimensional l_2^2 Metrics into l_1. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 10:1-10:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{deshpande_et_al:LIPIcs.FSTTCS.2016.10,
author = {Deshpande, Amit and Harsha, Prahladh and Venkat, Rakesh},
title = {{Embedding Approximately Low-Dimensional l\underline2^2 Metrics into l\underline1}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {10:1--10:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.10},
URN = {urn:nbn:de:0030-drops-68456},
doi = {10.4230/LIPIcs.FSTTCS.2016.10},
annote = {Keywords: Metric Embeddings, Sparsest Cut, Negative type metrics, Approximation Algorithms}
}
Document
Relational Logic with Framing and Hypotheses
Abstract
Relational properties arise in many settings: relating two versions of a program that use different data representations, noninterference properties for security, etc. The main ingredient of relational verification, relating aligned pairs of intermediate steps, has been used in numerous guises, but existing relational program logics are narrow in scope. This paper introduces a logic based on novel syntax that weaves together product programs to express alignment of control flow points at which relational formulas are asserted. Correctness judgments feature hypotheses with relational specifications, discharged by a rule for the linking of procedure implementations. The logic supports reasoning about program-pairs containing both similar and dissimilar control and data structures. Reasoning about dynamically allocated objects is supported by a frame rule based on frame conditions amenable to SMT provers. We prove soundness and sketch how the logic can be used for data abstraction, loop optimizations, and secure information flow.
Cite as
Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. Relational Logic with Framing and Hypotheses. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{banerjee_et_al:LIPIcs.FSTTCS.2016.11,
author = {Banerjee, Anindya and Naumann, David A. and Nikouei, Mohammad},
title = {{Relational Logic with Framing and Hypotheses}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {11:1--11:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.11},
URN = {urn:nbn:de:0030-drops-68465},
doi = {10.4230/LIPIcs.FSTTCS.2016.11},
annote = {Keywords: Relational Hoare logic, program equivalence, product programs, frame conditions, region logic}
}
Document
FO-Definable Transformations of Infinite Strings
Abstract
The theory of regular and aperiodic transformations of finite strings has recently received a lot of interest. These classes can be equivalently defined using logic (Monadic second-order logic and first-order logic), two-way machines (regular two-way and aperiodic two-way transducers), and one-way register machines (regular streaming string and aperiodic streaming string transducers). These classes are known to be closed under operations such as sequential composition and regular (star-free) choice; and problems such as functional equivalence and type checking, are decidable for these classes. On the other hand, for infinite strings these results are only known for regular transformations: Alur, Filiot, and Trivedi studied transformations of infinite strings and introduced an extension of streaming string transducers over infinte strings and showed that they capture monadic second-order definable transformations for infinite strings. In this paper we extend their work to recover connection for infinite strings among first-order logic definable transformations, aperiodic two-way transducers, and aperiodic streaming string transducers.
Cite as
Vrunda Dave, Shankara Narayanan Krishna, and Ashutosh Trivedi. FO-Definable Transformations of Infinite Strings. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 12:1-12:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{dave_et_al:LIPIcs.FSTTCS.2016.12,
author = {Dave, Vrunda and Krishna, Shankara Narayanan and Trivedi, Ashutosh},
title = {{FO-Definable Transformations of Infinite Strings}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {12:1--12:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.12},
URN = {urn:nbn:de:0030-drops-68476},
doi = {10.4230/LIPIcs.FSTTCS.2016.12},
annote = {Keywords: Transducers, FO-definability, Infinite Strings}
}
Document
Aperiodicity of Rational Functions Is PSPACE-Complete
Abstract
It is known that a language of finite words is definable in monadic second-order logic - MSO - (resp. first-order logic - FO -) iff it is recognized by some finite automaton (resp. some aperiodic finite automaton). Deciding whether an automaton A is equivalent to an aperiodic one is known to be PSPACE-complete. This problem has an important application in logic: it allows one to decide whether a given MSO formula is equivalent to some FO formula. In this paper, we address the aperiodicity problem for functions from finite words to finite words (transductions), defined by finite transducers, or equivalently by bimachines, a transducer model studied by Schützenberger and Reutenauer. Precisely, we show that the problem of deciding whether a given bimachine is equivalent to some aperiodic one is PSPACE-complete.
Cite as
Emmanuel Filiot, Olivier Gauwin, and Nathan Lhote. Aperiodicity of Rational Functions Is PSPACE-Complete. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{filiot_et_al:LIPIcs.FSTTCS.2016.13,
author = {Filiot, Emmanuel and Gauwin, Olivier and Lhote, Nathan},
title = {{Aperiodicity of Rational Functions Is PSPACE-Complete}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {13:1--13:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.13},
URN = {urn:nbn:de:0030-drops-68482},
doi = {10.4230/LIPIcs.FSTTCS.2016.13},
annote = {Keywords: Rational word transductions, decision problem, aperiodicity, bimachines}
}
Document
Homomorphism Problems for First-Order Definable Structures
Abstract
We investigate several variants of the homomorphism problem: given two relational structures, is there a homomorphism from one to the other? The input structures are possibly infinite, but definable by first-order interpretations in a fixed structure. Their signatures can be either finite or infinite but definable. The homomorphisms can be either arbitrary, or definable with parameters, or definable without parameters. For each of these variants, we determine its decidability status.
Cite as
Bartek Klin, Slawomir Lasota, Joanna Ochremiak, and Szymon Torunczyk. Homomorphism Problems for First-Order Definable Structures. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{klin_et_al:LIPIcs.FSTTCS.2016.14,
author = {Klin, Bartek and Lasota, Slawomir and Ochremiak, Joanna and Torunczyk, Szymon},
title = {{Homomorphism Problems for First-Order Definable Structures}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {14:1--14:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.14},
URN = {urn:nbn:de:0030-drops-68498},
doi = {10.4230/LIPIcs.FSTTCS.2016.14},
annote = {Keywords: Sets with atoms, first-order interpretations, homomorphism problem}
}
Document
On the Sensitivity Conjecture for Disjunctive Normal Forms
Abstract
The sensitivity conjecture of Nisan and Szegedy [CC'94] asks whether for any Boolean function f, the maximum sensitivity s(f), is polynomially related to its block sensitivity bs(f), and hence to other major complexity measures. Despite major advances in the analysis of Boolean functions over the last decade, the problem remains widely open.
In this paper, we consider a restriction on the class of Boolean functions through a model of computation (DNF), and refer to the functions adhering to this restriction as admitting the Normalized Block property. We prove that for any function f admitting the Normalized Block property, bs(f) <= 4 * s(f)^2. We note that (almost) all the functions mentioned in literature that achieve a quadratic separation between sensitivity and block sensitivity admit the Normalized Block property.
Recently, Gopalan et al. [ITCS'16] showed that every Boolean function f is uniquely specified by its values on a Hamming ball of radius at most 2 * s(f). We extend this result and also construct examples of Boolean functions which provide the matching lower bounds.
Cite as
Karthik C. S. and Sébastien Tavenas. On the Sensitivity Conjecture for Disjunctive Normal Forms. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{s._et_al:LIPIcs.FSTTCS.2016.15,
author = {S., Karthik C. and Tavenas, S\'{e}bastien},
title = {{On the Sensitivity Conjecture for Disjunctive Normal Forms}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {15:1--15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.15},
URN = {urn:nbn:de:0030-drops-68504},
doi = {10.4230/LIPIcs.FSTTCS.2016.15},
annote = {Keywords: Boolean function, Sensitivity, Block sensitivity, DNF}
}
Document
The Zero-Error Randomized Query Complexity of the Pointer Function
Abstract
The pointer function of Goos, Pitassi and Watson and its variants have recently been used to prove separation results among various measures of complexity such as deterministic, randomized and quantum query complexity, exact and approximate polynomial degree, etc. In particular, Ambainis et al. (STOC 2016) obtained the widest possible (quadratic) separations between deterministic and zero-error randomized query complexity, as well as between bounded-error and zero-error randomized query complexity by considering variants of this pointer function.
However, as Ambainis et al. pointed out in their work, the precise zero-error complexity of the original pointer function was
not known. We show a lower bound of ~Omega(n^{3/4}) on the zero-error randomized query complexity of the pointer function on Theta(n * log(n)) bits; since an ~O(n^{3/4}) upper bound was already shown by Mukhopadhyay and Sanyal (FSTTCS 2015), our lower bound is optimal up to polylog factors. We, in fact, consider a generalization of the original function and obtain lower bounds for it that are optimal up to polylog factors.
Cite as
Jaikumar Radhakrishnan and Swagato Sanyal. The Zero-Error Randomized Query Complexity of the Pointer Function. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 16:1-16:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{radhakrishnan_et_al:LIPIcs.FSTTCS.2016.16,
author = {Radhakrishnan, Jaikumar and Sanyal, Swagato},
title = {{The Zero-Error Randomized Query Complexity of the Pointer Function}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {16:1--16:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.16},
URN = {urn:nbn:de:0030-drops-68514},
doi = {10.4230/LIPIcs.FSTTCS.2016.16},
annote = {Keywords: Deterministic Decision Tree, Randomized Decision Tree, Query Complexity, Models of Computation.}
}
Document
Robust Multiplication-Based Tests for Reed-Muller Codes
Abstract
We consider the following multiplication-based tests to check if a given function f: F^n_q -> F_q is the evaluation of a degree-d polynomial over F_q for q prime.
Test_{e,k}: Pick P_1,...,P_k independent random degree-e polynomials and accept iff the function f P_1 ... P_k is the evaluation of a degree-(d + ek) polynomial.
We prove the robust soundness of the above tests for large values of e, answering a question of Dinur and Guruswami (FOCS 2013). Previous soundness analyses of these tests were known only for the case when either e = 1 or k = 1. Even for the case k = 1 and e > 1, earlier soundness analyses were not robust.
We also analyze a derandomized version of this test, where (for example) the polynomials P_1 ,... , P_k can be the same random polynomial P. This generalizes a result of Guruswami et al. (STOC 2014).
One of the key ingredients that go into the proof of this robust soundness is an extension of the standard Schwartz-Zippel lemma over general finite fields F_q, which may be of independent interest.
Cite as
Prahladh Harsha and Srikanth Srinivasan. Robust Multiplication-Based Tests for Reed-Muller Codes. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{harsha_et_al:LIPIcs.FSTTCS.2016.17,
author = {Harsha, Prahladh and Srinivasan, Srikanth},
title = {{Robust Multiplication-Based Tests for Reed-Muller Codes}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {17:1--17:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.17},
URN = {urn:nbn:de:0030-drops-68524},
doi = {10.4230/LIPIcs.FSTTCS.2016.17},
annote = {Keywords: Polynomials over finite fields, Schwartz-Zippel lemma, Low degree testing, Low degree long code}
}
Document
Querying Regular Languages over Sliding Windows
Abstract
We study the space complexity of querying regular languages over data streams in the sliding window model. The algorithm has to answer at any point of time whether the content of the sliding window belongs to a fixed regular language. A trichotomy is shown: For every regular language the optimal space requirement is either in Theta(n), Theta(log(n)), or constant, where $n$ is the size of the sliding window.
Cite as
Moses Ganardi, Danny Hucke, and Markus Lohrey. Querying Regular Languages over Sliding Windows. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{ganardi_et_al:LIPIcs.FSTTCS.2016.18,
author = {Ganardi, Moses and Hucke, Danny and Lohrey, Markus},
title = {{Querying Regular Languages over Sliding Windows}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {18:1--18:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.18},
URN = {urn:nbn:de:0030-drops-68539},
doi = {10.4230/LIPIcs.FSTTCS.2016.18},
annote = {Keywords: streaming algorithms, regular languages, space complexity}
}
Document
Decidability and Complexity of Tree Share Formulas
Abstract
Fractional share models are used to reason about how multiple actors share ownership of resources. We examine the decidability and complexity of reasoning over the "tree share" model of Dockins et al. using first-order logic, or fragments thereof. We pinpoint a connection between the basic operations on trees union, intersection, and complement and countable atomless Boolean algebras, allowing us to obtain decidability with the precise complexity of both first-order and existential theories over the tree share model with the aforementioned operations. We establish a connection between the multiplication operation on trees and the theory of word equations, allowing us to derive the decidability of its existential theory and the undecidability of its full first-order theory. We prove that the full first-order theory over the model with both the Boolean operations and the restricted multiplication operation (with constants on the right hand side) is decidable via an embedding to tree-automatic structures.
Cite as
Xuan Bach Le, Aquinas Hobor, and Anthony W. Lin. Decidability and Complexity of Tree Share Formulas. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{le_et_al:LIPIcs.FSTTCS.2016.19,
author = {Le, Xuan Bach and Hobor, Aquinas and Lin, Anthony W.},
title = {{Decidability and Complexity of Tree Share Formulas}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {19:1--19:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.19},
URN = {urn:nbn:de:0030-drops-68544},
doi = {10.4230/LIPIcs.FSTTCS.2016.19},
annote = {Keywords: Fractional Share Models, Resource Accounting, Countable Atomless Boolean Algebras, Word Equations, Tree Automatic Structures}
}
Document
One-Counter Automata with Counter Observability
Abstract
In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: Whenever the automaton produces a letter, it outputs the current counter value along with it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are PSPACE-complete, thus no harder than the corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are effectively determinizable and closed under all boolean operations. Moreover, it turns out that they are expressively equivalent to strong automata, in which transitions are guarded by MSO formulas over the natural numbers with successor.
Cite as
Benedikt Bollig. One-Counter Automata with Counter Observability. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 20:1-20:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bollig:LIPIcs.FSTTCS.2016.20,
author = {Bollig, Benedikt},
title = {{One-Counter Automata with Counter Observability}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {20:1--20:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.20},
URN = {urn:nbn:de:0030-drops-68554},
doi = {10.4230/LIPIcs.FSTTCS.2016.20},
annote = {Keywords: One-counter automata, inclusion checking, observability, visibly one- counter automata, strong automata}
}
Document
Strong Parameterized Deletion: Bipartite Graphs
Abstract
The purpose of this article is two fold: (a) to formally introduce a stronger version of graph deletion problems; and (b) to study this version in the context of bipartite graphs. Given a family of graphs F, a typical instance of parameterized graph deletion problem consists of an undirected graph G and a positive integer k and the objective is to check whether we can delete at most k vertices (or k edges) such that the resulting graph belongs to F. Another version that has been recently studied is the one where the input contains two integers k and l and the objective is to check whether we can delete at most k vertices and l edges such that the resulting graph belongs to F. In this paper, we propose and initiate the study of a more general version which we call strong deletion. In this problem, given an undirected graph G and positive integers k and l, the objective is to check whether there exists a vertex subset S of size at most k such that each connected component of G-S can be transformed into a graph in F by deleting at most l edges. In this paper we study this stronger version of deletion problems for the class of bipartite graphs. In particular, we study Strong Bipartite Deletion, where given an undirected graph G and positive integers k and l, the objective is to check whether there exists a vertex subset S of size at most k such that each connected component of G-S can be made bipartite by deleting at most l edges. While fixed-parameter tractability when parameterizing by k or l alone is unlikely, we show that this problem is fixed-parameter tractable (FPT) when parameterized by both k and l.
Cite as
Ashutosh Rai and M. S. Ramanujan. Strong Parameterized Deletion: Bipartite Graphs. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 21:1-21:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{rai_et_al:LIPIcs.FSTTCS.2016.21,
author = {Rai, Ashutosh and Ramanujan, M. S.},
title = {{Strong Parameterized Deletion: Bipartite Graphs}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {21:1--21:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.21},
URN = {urn:nbn:de:0030-drops-68561},
doi = {10.4230/LIPIcs.FSTTCS.2016.21},
annote = {Keywords: fixed parameter tractable, bipartite-editing, recursive understanding}
}
Document
Parameterized Algorithms for List K-Cycle
Abstract
The classic K-Cycle problem asks if a graph G, with vertex set V(G), has a simple cycle containing all vertices of a given set K subseteq V(G). In terms of colored graphs, it can be rephrased as follows: Given a graph G, a set K subset of V(G) and an injective coloring c from K to {1,2,...,|K|}, decide if G has a simple cycle containing each color in {1,2,...,|K|} (once). Another problem widely known since the introduction of color coding is {Colorful Cycle}. Given a graph G and a coloring c from V(G) to {1,2,...,k} for some natural number k, it asks if G has a simple cycle of length k containing each color in {1,2,...,k} (once). We study a generalization of these problems: Given a graph G, a set K subset of V(G), a list-coloring L from K to 2^{{1,2,...,k^*}} for some natural number k^* and a parameter k, List K-Cycle asks if one can assign a color to each vertex in K so that G would have a simple cycle (of arbitrary length) containing exactly k vertices from K with distinct colors.
We design a randomized algorithm for List K-Cycle running in time 2^kn^{O(1)} on an -vertex graph, matching the best known running times of algorithms for both K-Cycle and Colorful Cycle. Moreover, unless the Set Cover Conjecture is false, our algorithm is essentially optimal. We also study a variant of List K-Cycle that generalizes the classic Hamiltonicity problem, where one specifies the size of a solution. Our results integrate three related algebraic approaches, introduced by Bjorklund, Husfeldt and Taslaman (SODA'12), Bjorklund, Kaski and Kowalik (STACS'13), and Bjorklund (FOCS'10).
Cite as
Fahad Panolan and Meirav Zehavi. Parameterized Algorithms for List K-Cycle. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 22:1-22:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{panolan_et_al:LIPIcs.FSTTCS.2016.22,
author = {Panolan, Fahad and Zehavi, Meirav},
title = {{Parameterized Algorithms for List K-Cycle}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {22:1--22:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.22},
URN = {urn:nbn:de:0030-drops-68571},
doi = {10.4230/LIPIcs.FSTTCS.2016.22},
annote = {Keywords: Parameterized Complexity, K-Cycle, Colorful Path, k-Path}
}
Document
Lossy Kernels for Graph Contraction Problems
Abstract
We study some well-known graph contraction problems in the recently introduced framework of lossy kernelization. In classical kernelization, given an instance (I,k) of a parameterized problem, we are interested in obtaining (in polynomial time) an equivalent instance (I',k') of the same problem whose size is bounded by a function in k. This notion however has a major limitation. Given an approximate solution to the instance (I',k'), we can say nothing about the original instance (I,k). To handle this issue, among others, the framework of lossy kernelization was introduced. In this framework, for a constant alpha, given an instance (I,k) we obtain an instance (I',k') of the same problem such that, for every c>1, any c-approximate solution to (I',k') can be turned into a (c*alpha)-approximate solution to the original instance (I, k) in polynomial time. Naturally, we are interested in a polynomial time algorithm for this task, and further require that |I'| + k' = k^{O(1)}. Akin to the notion of polynomial time approximation schemes in approximation algorithms, a parameterized problem is said to admit a polynomial size approximate kernelization scheme (PSAKS) if it admits a polynomial size alpha-approximate kernel for every approximation parameter alpha > 1. In this work, we design PSAKSs for Tree Contraction, Star Contraction, Out-Tree Contraction and Cactus Contraction problems. These problems do not admit polynomial kernels, and we show that each of them admit a PSAKS with running time k^{f(alpha)}|I|^{O(1)} that returns an instance of size k^{g(alpha)} where f(alpha) and g(alpha) are constants depending on alpha.
Cite as
R. Krithika, Pranabendu Misra, Ashutosh Rai, and Prafullkumar Tale. Lossy Kernels for Graph Contraction Problems. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 23:1-23:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{krithika_et_al:LIPIcs.FSTTCS.2016.23,
author = {Krithika, R. and Misra, Pranabendu and Rai, Ashutosh and Tale, Prafullkumar},
title = {{Lossy Kernels for Graph Contraction Problems}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {23:1--23:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.23},
URN = {urn:nbn:de:0030-drops-68587},
doi = {10.4230/LIPIcs.FSTTCS.2016.23},
annote = {Keywords: parameterized complexity, lossy kernelization, graph theory, edge contraction problems}
}
Document
Faster Exact and Parameterized Algorithm for Feedback Vertex Set in Bipartite Tournaments
Abstract
A bipartite tournament is a directed graph T:=(A cup B, E) such that every pair of vertices (a,b), a in A, b in B are connected by an arc, and no arc connects two vertices of A or two vertices of B. A feedback vertex set is a set S of vertices in T such that T - S is acyclic. In this article we consider the Feedback Vertex Set problem in bipartite tournaments. Here the input is a bipartite tournament T on n vertices together with an integer k, and the task is to determine whether T has a feedback vertex set of size at most k. We give a new algorithm for Feedback Vertex Set in Bipartite Tournaments. The running time of our algorithm is upper-bounded by O(1.6181^k + n^{O(1)}), improving over the previously best known algorithm with running time (2^k)k^{O(1)} + n^{O(1)} [Hsiao, ISAAC 2011]. As a by-product, we also obtain the fastest currently known exact exponential-time algorithm for the problem, with running time O(1.3820^n).
Cite as
Mithilesh Kumar and Daniel Lokshtanov. Faster Exact and Parameterized Algorithm for Feedback Vertex Set in Bipartite Tournaments. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{kumar_et_al:LIPIcs.FSTTCS.2016.24,
author = {Kumar, Mithilesh and Lokshtanov, Daniel},
title = {{Faster Exact and Parameterized Algorithm for Feedback Vertex Set in Bipartite Tournaments}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {24:1--24:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.24},
URN = {urn:nbn:de:0030-drops-68591},
doi = {10.4230/LIPIcs.FSTTCS.2016.24},
annote = {Keywords: Parameterized algorithms, Exact algorithms, Feedback vertex set, Tour- naments, Bipartite tournaments}
}
Document
Probabilistic Mu-Calculus: Decidability and Complete Axiomatization
Abstract
We introduce a version of the probabilistic mu-calculus (PMC) built on top of a probabilistic modal logic that allows encoding n-ary inequational conditions on transition probabilities. PMC extends previously studied calculi and we prove that, despite its expressiveness, it enjoys a series of good meta-properties. Firstly, we prove the decidability of satisfiability checking by establishing the small model property. An algorithm for deciding the satisfiability problem is developed. As a second major result, we provide a complete axiomatization for the alternation-free fragment of PMC. The completeness proof is innovative in many aspects combining various techniques from topology and model theory.
Cite as
Kim G. Larsen, Radu Mardare, and Bingtian Xue. Probabilistic Mu-Calculus: Decidability and Complete Axiomatization. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{larsen_et_al:LIPIcs.FSTTCS.2016.25,
author = {Larsen, Kim G. and Mardare, Radu and Xue, Bingtian},
title = {{Probabilistic Mu-Calculus: Decidability and Complete Axiomatization}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {25:1--25:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.25},
URN = {urn:nbn:de:0030-drops-68607},
doi = {10.4230/LIPIcs.FSTTCS.2016.25},
annote = {Keywords: Markov process, probabilistic modal mu-calculus, n-ary (in-)equational modalities, satisfiability, axiomatization}
}
Document
Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
Abstract
Model checking is a powerful method widely explored in formal verification to check the (state-transition) model of a system against desired properties of its behaviour. Classically, properties are expressed by formulas of a temporal logic, such as LTL, CTL, and CTL*. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. On the contrary, Halpern and Shoham's interval temporal logic (HS) is "interval-wise" interpreted, thus allowing one to naturally express properties of computation stretches, spanning a sequence of states, or properties involving temporal aggregations, which are inherently "interval-based".
In this paper, we study the expressiveness of HS in model checking, in comparison with that of the standard logics LTL, CTL, and CTL*. To this end, we consider HS endowed with three semantic variants: the state-based semantics, introduced by Montanari et al., which allows branching in the past and in the future, the linear-past semantics, allowing branching only in the future, and the linear semantics, disallowing branching. These variants are compared, as for their expressiveness, among themselves and to standard temporal logics, getting a complete picture. In particular, HS with linear (resp., linear-past) semantics is proved to be equivalent to LTL (resp., finitary CTL*).
Cite as
Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala. Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 26:1-26:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bozzelli_et_al:LIPIcs.FSTTCS.2016.26,
author = {Bozzelli, Laura and Molinari, Alberto and Montanari, Angelo and Peron, Adriano and Sala, Pietro},
title = {{Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {26:1--26:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.26},
URN = {urn:nbn:de:0030-drops-68615},
doi = {10.4230/LIPIcs.FSTTCS.2016.26},
annote = {Keywords: Interval Temporal Logics, Expressiveness, Model Checking}
}
Document
Model Checking Population Protocols
Abstract
Population protocols are a model for parameterized systems in which a set of identical, anonymous, finite-state processes interact pairwise through rendezvous synchronization. In each step, the pair of interacting processes is chosen by a random scheduler. Angluin et al. (PODC 2004) studied population protocols as a distributed computation model. They characterized the computational power in the limit (semi-linear predicates) of a subclass of protocols (the well-specified ones). However, the modeling power of protocols go beyond computation of semi-linear predicates and they can be used to study a wide range of distributed protocols, such as asynchronous leader election or consensus, stochastic evolutionary processes, or chemical reaction networks. Correspondingly, one is interested in checking specifications on these protocols that go beyond the well-specified computation of predicates.
In this paper, we characterize the decidability frontier for the model checking problem for population protocols against probabilistic linear-time specifications. We show that the model checking problem is decidable for qualitative objectives, but as hard as the reachability problem for Petri nets - a well-known hard problem without known elementary algorithms. On the other hand, model checking is undecidable for quantitative properties.
Cite as
Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Model Checking Population Protocols. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{esparza_et_al:LIPIcs.FSTTCS.2016.27,
author = {Esparza, Javier and Ganty, Pierre and Leroux, J\'{e}r\^{o}me and Majumdar, Rupak},
title = {{Model Checking Population Protocols}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {27:1--27:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.27},
URN = {urn:nbn:de:0030-drops-68628},
doi = {10.4230/LIPIcs.FSTTCS.2016.27},
annote = {Keywords: parameterized systems, population protocols, probabilistic model checking, probabilistic linear-time specifications, decidability}
}
Document
Visibly Linear Dynamic Logic
Abstract
We introduce Visibly Linear Dynamic Logic (VLDL), which extends Linear Temporal Logic (LTL) by temporal operators that are guarded by visibly pushdown languages over finite words. In VLDL one can, e.g., express that a function resets a variable to its original value after its execution, even in the presence of an unbounded number of intermediate recursive calls. We prove that VLDL describes exactly the omega-visibly pushdown languages. Thus it is strictly more expressive than LTL and able to express recursive properties of programs with unbounded call stacks.
The main technical contribution of this work is a translation of VLDL into omega-visibly pushdown automata of exponential size via one-way alternating jumping automata. This translation yields exponential-time algorithms for satisfiability, validity, and model checking. We also show that visibly pushdown games with VLDL winning conditions are solvable in triply-exponential time.We prove all these problems to be complete for their respective complexity classes.
Cite as
Alexander Weinert and Martin Zimmermann. Visibly Linear Dynamic Logic. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 28:1-28:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{weinert_et_al:LIPIcs.FSTTCS.2016.28,
author = {Weinert, Alexander and Zimmermann, Martin},
title = {{Visibly Linear Dynamic Logic}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {28:1--28:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.28},
URN = {urn:nbn:de:0030-drops-68639},
doi = {10.4230/LIPIcs.FSTTCS.2016.28},
annote = {Keywords: Temporal Logic, Visibly Pushdown Languages, Satisfiability, Model Checking, Infinite Games}
}
Document
Stable Matching Games: Manipulation via Subgraph Isomorphism
Abstract
In this paper we consider a problem that arises from a strategic issue in the stable matching model (with complete preference lists) from the viewpoint of exact-exponential time algorithms. Specifically, we study the Stable Extension of Partial Matching (SEOPM) problem, where the input consists of the complete preference lists of men, and a partial matching. The objective is to find (if one exists) a set of preference lists of women, such that the men-optimal Gale Shapley algorithm outputs a perfect matching that contains the given partial matching. Kobayashi and Matsui [Algorithmica, 2010] proved this problem is NP-complete. In this article, we give an exact-exponential algorithm for SEOPM running in time 2^{O(n)}, where n denotes the number of men/women. We complement our algorithmic finding by showing that unless Exponential Time Hypothesis (ETH) fails, our algorithm is asymptotically optimal. That is, unless ETH fails, there is no algorithm for SEOPM running in time 2^{o(n)}. Our algorithm is a non-trivial combination of a parameterized algorithm for Subgraph Isomorphism, a relationship between stable matching and finding an out-branching in an appropriate graph and enumerating non-isomorphic out-branchings.
Cite as
Sushmita Gupta and Sanjukta Roy. Stable Matching Games: Manipulation via Subgraph Isomorphism. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 29:1-29:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{gupta_et_al:LIPIcs.FSTTCS.2016.29,
author = {Gupta, Sushmita and Roy, Sanjukta},
title = {{Stable Matching Games: Manipulation via Subgraph Isomorphism}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {29:1--29:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.29},
URN = {urn:nbn:de:0030-drops-68642},
doi = {10.4230/LIPIcs.FSTTCS.2016.29},
annote = {Keywords: stable matching, Gale-Shapley algorithm, suitor graph, subgraph iso- morphism, exact-exponential time algorithms}
}
Document
The Adwords Problem with Strict Capacity Constraints
Abstract
We study an online assignment problem where the offline servers have capacities, and the objective is to obtain a maximum-weight assignment of requests that arrive online. The weight of edges incident to any server can be at most the server capacity. Our problem is related to the adwords problem, where the assignment to a server is allowed to exceed its capacity. In many applications, however, server capacities are strict and partially-served requests are of no use, motivating the problem we study.
While no deterministic algorithm can be competitive in general for this problem, we give an algorithm with competitive ratio that depends on the ratio of maximum weight of any edge to the capacity of the server it is incident to. If this ratio is 1/2, our algorithm is tight. Further, we give a randomized algorithm that is 6-competitive in expectation for the general problem. Most previous work on the problem and its variants assumes that the edge weights are much smaller than server capacities. Our guarantee, in contrast, does not require any assumptions about job weights. We also give improved lower bounds for both deterministic and randomized algorithms. For the special case of parallel servers, we show that a load-balancing algorithm is tight and near-optimal.
Cite as
Umang Bhaskar, Ajil Jalal, and Rahul Vaze. The Adwords Problem with Strict Capacity Constraints. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 30:1-30:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bhaskar_et_al:LIPIcs.FSTTCS.2016.30,
author = {Bhaskar, Umang and Jalal, Ajil and Vaze, Rahul},
title = {{The Adwords Problem with Strict Capacity Constraints}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {30:1--30:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.30},
URN = {urn:nbn:de:0030-drops-68651},
doi = {10.4230/LIPIcs.FSTTCS.2016.30},
annote = {Keywords: Online Algorithms, Adwords, Budgeted Matching, Greedy Algorithms}
}
Document
Most Likely Voronoi Diagrams in Higher Dimensions
Abstract
The Most Likely Voronoi Diagram is a generalization of the well known Voronoi Diagrams to a stochastic setting, where a stochastic point is a point associated with a given probability of existence, and the cell for such a point is the set of points which would classify the given point as its most likely nearest neighbor. We investigate the complexity of this subdivision of space in d dimensions. We show that in the general case, the complexity of such a subdivision is Omega(n^{2d}) where n is the number of points. This settles an open question raised in a recent (ISAAC 2014) paper of Suri and Verbeek, which first defined the Most Likely Voronoi Diagram. We also show that when the probabilities are assigned using a random permutation of a fixed set of values, in expectation the complexity is only ~O(n^{ceil{d/2}}) where the ~O(*) means that logarithmic factors are suppressed. In the worst case, this bound is tight up to polylog factors.
Cite as
Nirman Kumar, Benjamin Raichel, Subhash Suri, and Kevin Verbeek. Most Likely Voronoi Diagrams in Higher Dimensions. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{kumar_et_al:LIPIcs.FSTTCS.2016.31,
author = {Kumar, Nirman and Raichel, Benjamin and Suri, Subhash and Verbeek, Kevin},
title = {{Most Likely Voronoi Diagrams in Higher Dimensions}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {31:1--31:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.31},
URN = {urn:nbn:de:0030-drops-68667},
doi = {10.4230/LIPIcs.FSTTCS.2016.31},
annote = {Keywords: Uncertainty, Lower bounds, Voronoi Diagrams, Stochastic}
}
Document
Fréchet Distance Between a Line and Avatar Point Set
Abstract
Frechet distance is an important geometric measure that captures the distance between two curves or more generally point sets. In this paper, we consider a natural variant of Frechet distance problem with multiple choice, provide an approximation algorithm and address its parameterized and kernelization complexity. A multiple choice problem consists of a set of color classes Q={Q_1,Q_2,...,Q_n}, where each class Q_i consists of a pair of points Q_i = {q_i, bar{q_i}}. We call a subset A subset {q_i , bar{q_i}:1 <= i <= n} conflict free if A contains at most one point from each color class. The standard objective in multiple choice problem is to select a conflict free subset that optimizes a given function.
Given a line segment l and set Q of a pair of points in R^2, our objective is to find a conflict free subset that minimizes the Frechet distance between l and the point set, where the minimum is taken over all possible conflict free subsets. We first show that this problem is NP-hard, and provide a 3-approximation algorithm. Then we develop a simple randomized FPT algorithm which is later derandomized using universal family of sets. We believe that this technique can be of independent interest, and can be used to solve other parameterized multiple choice problems. The randomized algorithm runs in O(2^k * n * log^2(n)) time, and the derandomized deterministic algorithm runs in O(2^k * k^{O(log(k))} * n * log^2(n)) time, where k, the parameter, is the number of elements in the conflict free subset solution. Finally we present a simple branching algorithm for the problem running in O(2^k * n^{2} *log(n)) time. We also show that the problem is unlikely to have a polynomial sized kernel under standard complexity theoretic assumption.
Cite as
Aritra Banik, Fahad Panolan, Venkatesh Raman, and Vibha Sahlot. Fréchet Distance Between a Line and Avatar Point Set. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 32:1-32:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{banik_et_al:LIPIcs.FSTTCS.2016.32,
author = {Banik, Aritra and Panolan, Fahad and Raman, Venkatesh and Sahlot, Vibha},
title = {{Fr\'{e}chet Distance Between a Line and Avatar Point Set}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {32:1--32:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.32},
URN = {urn:nbn:de:0030-drops-68676},
doi = {10.4230/LIPIcs.FSTTCS.2016.32},
annote = {Keywords: Frechet Distance, Avatar Problems, Multiple Choice, FPT}
}
Document
Greed is Good for Deterministic Scale-Free Networks
Abstract
Large real-world networks typically follow a power-law degree distribution. To study such networks, numerous random graph models have been proposed. However, real-world networks are not drawn at random. In fact, the behavior of real-world networks and random graph models can be the complete opposite of one another, depending on the considered property. Brach, Cygan, Lacki, and Sankowski [SODA 2016] introduced two natural deterministic conditions: (1) a power-law upper bound on the degree distribution (PLB-U) and (2) power-law neighborhoods, that is, the degree distribution of neighbors of each vertex is also upper bounded by a power law (PLB-N). They showed that many real-world networks satisfy both deterministic properties and exploit them to design faster algorithms for a number of classical graph problems like transitive closure, maximum matching, determinant, PageRank, matrix inverse, counting triangles and maximum clique.
We complement the work of Brach et al. by showing that some well-studied random graph models exhibit both the mentioned PLB properties and additionally also a power-law lower bound on the degree distribution (PLB-L). All three properties hold with high probability for Chung-Lu Random Graphs and Geometric Inhomogeneous Random Graphs and almost surely for Hyperbolic Random Graphs. As a consequence, all results of Brach et al. also hold with high probability for Chung-Lu Random Graphs and Geometric Inhomogeneous Random Graphs and almost surely for Hyperbolic Random Graphs.
In the second part of this work we study three classical NP-hard combinatorial optimization problems on PLB networks. It is known that on general graphs, a greedy algorithm, which chooses nodes in the order of their degree, only achieves an approximation factor of asymptotically at least logarithmic in the maximum degree for Minimum Vertex Cover and Minimum Dominating Set, and an approximation factor of asymptotically at least the maximum degree for Maximum Independent Set. We prove that the PLB-U property suffices such that the greedy approach achieves a constant-factor approximation for all three problems. We also show that all three combinatorial optimization problems are APX-complete, even if all PLB-properties hold. Hence, a PTAS cannot be expected, unless P=NP.
Cite as
Ankit Chauhan, Tobias Friedrich, and Ralf Rothenberger. Greed is Good for Deterministic Scale-Free Networks. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{chauhan_et_al:LIPIcs.FSTTCS.2016.33,
author = {Chauhan, Ankit and Friedrich, Tobias and Rothenberger, Ralf},
title = {{Greed is Good for Deterministic Scale-Free Networks}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {33:1--33:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.33},
URN = {urn:nbn:de:0030-drops-68682},
doi = {10.4230/LIPIcs.FSTTCS.2016.33},
annote = {Keywords: random graphs, power-law degree distribution, scale-free networks, PLB networks, approximation algorithms, vertex cover, dominating set, independent s}
}
Document
Independent-Set Reconfiguration Thresholds of Hereditary Graph Classes
Abstract
Traditionally, reconfiguration problems ask the question whether a given solution of an optimization problem can be transformed to a target solution in a sequence of small steps that preserve feasibility of the intermediate solutions. In this paper, rather than asking this question from an algorithmic perspective, we analyze the combinatorial structure behind it. We consider the problem of reconfiguring one independent set into another, using two different processes: (1) exchanging exactly k vertices in each step, or (2) removing or adding one vertex in each step while ensuring the intermediate sets contain at most k fewer vertices than the initial solution. We are interested in determining the minimum value of k for which this reconfiguration is possible, and bound these threshold values in terms of several structural graph parameters. For hereditary graph classes we identify structures that cause the reconfiguration threshold to be large.
Cite as
Mark de Berg, Bart M. P. Jansen, and Debankur Mukherjee. Independent-Set Reconfiguration Thresholds of Hereditary Graph Classes. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{deberg_et_al:LIPIcs.FSTTCS.2016.34,
author = {de Berg, Mark and Jansen, Bart M. P. and Mukherjee, Debankur},
title = {{Independent-Set Reconfiguration Thresholds of Hereditary Graph Classes}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {34:1--34:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.34},
URN = {urn:nbn:de:0030-drops-68694},
doi = {10.4230/LIPIcs.FSTTCS.2016.34},
annote = {Keywords: Reconfiguration, Independent set, Token Addition Removal, Token Sliding}
}
Document
LZ77 Factorisation of Trees
Abstract
We generalise the fundamental concept of LZ77 factorisation from strings to trees. A tree is represented as a collection of edge-disjoint fragments that either consist of one node or has already occurred earlier (in the BFS order). Similarly as for strings, such a collection uniquely determines the tree, so by minimising the number of fragments we obtain a compressed representation of the tree. We show that our generalisation has several useful properties of the standard LZ77 factorisation: it can be computed in polynomial time and its simpler variant in linear time; its size is not larger than the smallest grammar for a tree; it can be transformed (in linear time) into a tree grammar of size O(rg log(n/(rg))), where n is the size of the tree, g the size of the smallest grammar for this tree and r the maximal arity of the nodes in the tree, which matches a recent bound of Jez and Lohrey [STACS 2014], but with a simpler and more modular proof.
Cite as
Pawel Gawrychowski and Artur Jez. LZ77 Factorisation of Trees. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 35:1-35:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{gawrychowski_et_al:LIPIcs.FSTTCS.2016.35,
author = {Gawrychowski, Pawel and Jez, Artur},
title = {{LZ77 Factorisation of Trees}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {35:1--35:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.35},
URN = {urn:nbn:de:0030-drops-68700},
doi = {10.4230/LIPIcs.FSTTCS.2016.35},
annote = {Keywords: Tree grammars, Grammar compression, LZ77, SLP, Tree compression}
}
Document
Finger Search in Grammar-Compressed Strings
Abstract
Grammar-based compression, where one replaces a long string by a small context-free grammar that generates the string, is a simple and powerful paradigm that captures many popular compression schemes. Given a grammar, the random access problem is to compactly represent the grammar while supporting random access, that is, given a position in the original uncompressed string report the character at that position. In this paper we study the random access problem with the finger search property, that is, the time for a random access query should depend on the distance between a specified index f, called the finger, and the query index i. We consider both a static variant, where we first place a finger and subsequently access indices near the finger efficiently, and a dynamic variant where also moving the finger such that the time depends on the distance moved is supported.
Let n be the size the grammar, and let N be the size of the string. For the static variant we give a linear space representation that supports placing the finger in O(log(N)) time and subsequently accessing in O(log(D)) time, where D is the distance between the finger and the accessed index. For the dynamic variant we give a linear space representation that supports placing the finger in O(log(N)) time and accessing and moving the finger in O(log(D) + log(log(N))) time. Compared to the best linear space solution to random access, we improve a O(log(N)) query bound to O(log(D)) for the static variant and to O(log(D) + log(log(N))) for the dynamic variant, while maintaining linear space. As an application of our results we obtain an improved solution to the longest common extension problem in grammar compressed strings. To obtain our results, we introduce several new techniques of independent interest, including a novel van Emde Boas style decomposition of grammars.
Cite as
Philip Bille, Anders Roy Christiansen, Patrick Hagge Cording, and Inge Li Gortz. Finger Search in Grammar-Compressed Strings. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bille_et_al:LIPIcs.FSTTCS.2016.36,
author = {Bille, Philip and Christiansen, Anders Roy and Cording, Patrick Hagge and Gortz, Inge Li},
title = {{Finger Search in Grammar-Compressed Strings}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {36:1--36:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.36},
URN = {urn:nbn:de:0030-drops-68717},
doi = {10.4230/LIPIcs.FSTTCS.2016.36},
annote = {Keywords: Compression, Grammars, Finger search, Algorithms}
}
Document
Characterization and Lower Bounds for Branching Program Size Using Projective Dimension
Abstract
We study projective dimension, a graph parameter (denoted by pd(G) for a graph G), introduced by Pudlak and Rodl (1992). For a Boolean function f(on n bits), Pudlak and Rodl associated a bipartite graph G_f and showed that size of the optimal branching program computing f (denoted by bpsize(f)) is at least pd(G_f) (also denoted by pd(f)). Hence, proving lower bounds for pd(f) imply lower bounds for bpsize(f). Despite several attempts (Pudlak and Rodl (1992), Ronyai et.al, (2000)), proving super-linear lower bounds for projective dimension of explicit families of graphs has remained elusive.
We observe that there exist a Boolean function f for which the gap between the pd(f) and bpsize(f) is 2^{Omega(n)}. Motivated by the argument in Pudlak and Rodl (1992), we define two variants of projective dimension - projective dimension with intersection dimension 1 (denoted by upd(f)) and {bitwise decomposable projective dimension} (denoted by bpdim(f)). We show the following results:
(a) We observe that there exist a Boolean function f for which the gap between upd(f) and bpsize(f) is 2^{Omega(n)}. In contrast, we also show that the bitwise decomposable projective dimension characterizes size of the branching program up to a polynomial factor. That is, there exists a large constant c>0 and for any function f, bpdim(f)/6 <= bpsize(f) <= (bpdim(f))^c.
(b) We introduce a new candidate function family f for showing super-polynomial lower bounds for bpdim(f). As our main result, we demonstrate gaps between pd(f) and the above two new measures for f: pd(f) = O(sqrt{n}), upd(f) = Omega(n), bpdim(f) = Omega({n^{1.5}}/{log(n)}).
(c) Although not related to branching program lower bounds, we derive exponential lower bounds for two restricted variants of pd(f) and upd(f) respectively by observing that they are exactly equal to well-studied graph parameters - bipartite clique cover number and bipartite partition number respectively.
Cite as
Krishnamoorthy Dinesh, Sajin Koroth, and Jayalal Sarma. Characterization and Lower Bounds for Branching Program Size Using Projective Dimension. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 37:1-37:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{dinesh_et_al:LIPIcs.FSTTCS.2016.37,
author = {Dinesh, Krishnamoorthy and Koroth, Sajin and Sarma, Jayalal},
title = {{Characterization and Lower Bounds for Branching Program Size Using Projective Dimension}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {37:1--37:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.37},
URN = {urn:nbn:de:0030-drops-68722},
doi = {10.4230/LIPIcs.FSTTCS.2016.37},
annote = {Keywords: Projective Dimension, Lower Bounds, Branching Program Size}
}
Document
Finer Separations Between Shallow Arithmetic Circuits
Abstract
In this paper, we show that there is a family of polynomials P_n, where P_n is a polynomial in n variables of degree at most d = O(log^2(n)), such that
* P_n can be computed by linear sized homogeneous depth-5 arithmetic circuits,
* P_n can be computed by poly(n) sized non-homogeneous depth-3 arithmetic circuits.
* Any homogeneous depth-4 arithmetic circuit computing P_n must have size at least n^{Omega(sqrt(d))}.
This shows that the parameters for the depth reduction results of [Agrawal-Vinay 08, Koiran 12, Tavenas 13] are tight for extremely restricted classes of arithmetic circuits, for instance homogeneous depth-5 circuits and non-homogeneous depth-3 circuits, and over an appropriate range of parameters, qualitatively improve a result of [Kumar-Saraf 14], which showed that the parameters of depth reductions are optimal for algebraic branching programs.
As an added advantage, our proofs are much shorter and simpler than the two known proofs of n^{Omega(sqrt(d))} lower bound for homogeneous depth-4 circuits [Kayal-Limaye-Saha-Srinivasan 14, Kumar-Saraf 14], albeit our proofs only work when d = O(log^2(n)).
Cite as
Mrinal Kumar and Ramprasad Saptharishi. Finer Separations Between Shallow Arithmetic Circuits. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 38:1-38:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{kumar_et_al:LIPIcs.FSTTCS.2016.38,
author = {Kumar, Mrinal and Saptharishi, Ramprasad},
title = {{Finer Separations Between Shallow Arithmetic Circuits}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {38:1--38:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.38},
URN = {urn:nbn:de:0030-drops-68730},
doi = {10.4230/LIPIcs.FSTTCS.2016.38},
annote = {Keywords: arithmetic circuits, lower bounds, separations, depth reduction}
}
Document
Sum of Products of Read-Once Formulas
Abstract
We study limitations of polynomials computed by depth two circuits built over read-once formulas (ROFs). In particular,
1. We prove an exponential lower bound for the sum of ROFs computing the 2n-variate polynomial in VP defined by Raz and Yehudayoff [CC,2009].
2. We obtain an exponential lower bound on the size of arithmetic circuits computing sum of products of restricted ROFs of unbounded depth computing the permanent of an n by n matrix. The restriction is on the number of variables with + gates as a parent in a proper sub formula of the ROF to be bounded by sqrt(n). Additionally, we restrict the product fan in to be bounded by a sub linear function. This proves an exponential lower bound for a subclass of possibly non-multilinear formulas of unbounded depth computing the permanent polynomial.
3. We also show an exponential lower bound for the above model against a polynomial in VP.
4. Finally we observe that the techniques developed yield an exponential lower bound on the size of sums of products of syntactically multilinear arithmetic circuits computing a product of variable disjoint linear forms where the bottom sum gate and product gates at the second level have fan in bounded by a sub linear function.
Our proof techniques are built on the measure developed by Kumar et al.[ICALP 2013] and are based on a non-trivial analysis of ROFs under random partitions. Further, our results exhibit strengths and provide more insight into the lower bound techniques introduced by Raz [STOC 2004].
Cite as
Ramya C. and B. V. Raghavendra Rao. Sum of Products of Read-Once Formulas. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 39:1-39:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{c._et_al:LIPIcs.FSTTCS.2016.39,
author = {C., Ramya and Rao, B. V. Raghavendra},
title = {{Sum of Products of Read-Once Formulas}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {39:1--39:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.39},
URN = {urn:nbn:de:0030-drops-68741},
doi = {10.4230/LIPIcs.FSTTCS.2016.39},
annote = {Keywords: Arithmetic Circuits, Permanent, Computational Complexity, Algebraic Complexity Theory}
}
Document
Understanding Cutting Planes for QBFs
Abstract
We define a cutting planes system CP+ForallRed for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while CP+ForallRed is again weaker than QBF Frege and stronger than the CDCL-based QBF resolution systems Q-Res and QU-Res, it turns out to be incomparable to even the weakest expansion-based QBF resolution system ForallExp+Res.
Technically, our results establish the effectiveness of two lower bound techniques for CP+ForallRed: via strategy extraction and via monotone feasible interpolation.
Cite as
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding Cutting Planes for QBFs. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2016.40,
author = {Beyersdorff, Olaf and Chew, Leroy and Mahajan, Meena and Shukla, Anil},
title = {{Understanding Cutting Planes for QBFs}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {40:1--40:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.40},
URN = {urn:nbn:de:0030-drops-68758},
doi = {10.4230/LIPIcs.FSTTCS.2016.40},
annote = {Keywords: proof complexity, QBF, cutting planes, resolution, simulations}
}
Document
Summaries for Context-Free Games
Abstract
We study two-player games played on the infinite graph of sentential forms induced by a context-free grammar (that comes with an ownership partitioning of the non-terminals). The winning condition is inclusion of the derived terminal word in the language of a finite automaton. Our contribution is a new algorithm to decide the winning player and to compute her strategy. It is based on a novel representation of all plays starting in a non-terminal. The representation uses the domain of Boolean formulas over the transition monoid of the target automaton. The elements of the monoid are essentially procedure summaries, and our approach can be seen as the first summary-based algorithm for the synthesis of recursive programs. We show that our algorithm has optimal (doubly exponential) time complexity, that it is compatible with recent antichain optimizations, and that it admits a lazy evaluation strategy. Our preliminary experiments indeed show encouraging results, indicating a speed up of three orders of magnitude over a competitor.
Cite as
Lukás Holík, Roland Meyer, and Sebastian Muskalla. Summaries for Context-Free Games. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 41:1-41:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{holik_et_al:LIPIcs.FSTTCS.2016.41,
author = {Hol{\'\i}k, Luk\'{a}s and Meyer, Roland and Muskalla, Sebastian},
title = {{Summaries for Context-Free Games}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {41:1--41:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.41},
URN = {urn:nbn:de:0030-drops-68763},
doi = {10.4230/LIPIcs.FSTTCS.2016.41},
annote = {Keywords: summaries, context-free games, Kleene iteration, transition monoid, strategy synthesis}
}
Document
Admissibility in Quantitative Graph Games
Abstract
Admissibility has been studied for games of infinite duration with Boolean objectives. We extend here this study to games of infinite duration with quantitative objectives. First, we show that, under the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the notion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide relevant verification and synthesis problems.
Cite as
Romain Brenguier, Guillermo A. Pérez, Jean-Francois Raskin, and Ocan Sankur. Admissibility in Quantitative Graph Games. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 42:1-42:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{brenguier_et_al:LIPIcs.FSTTCS.2016.42,
author = {Brenguier, Romain and P\'{e}rez, Guillermo A. and Raskin, Jean-Francois and Sankur, Ocan},
title = {{Admissibility in Quantitative Graph Games}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {42:1--42:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.42},
URN = {urn:nbn:de:0030-drops-68772},
doi = {10.4230/LIPIcs.FSTTCS.2016.42},
annote = {Keywords: Quantitative games, Verification, Reactive synthesis, Admissibility}
}
Document
Prompt Delay
Abstract
Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. Recently, such games with quantitative winning conditions in weak MSO with the unbounding quantifier were studied, but their properties turned out to be unsatisfactory. In particular, unbounded lookahead is in general necessary.
Here, we study delay games with winning conditions given by Prompt-LTL, Linear Temporal Logic equipped with a parameterized eventually operator whose scope is bounded. Our main result shows that solving Prompt-LTL delay games is complete for triply-exponential time. Furthermore, we give tight triply-exponential bounds on the necessary lookahead and on the scope of the parameterized eventually operator. Thus, we identify Prompt-LTL as the first known class of well-behaved quantitative winning conditions for delay games.
Finally, we show that applying our techniques to delay games with omega-regular winning conditions answers open questions in the cases where the winning conditions are given by non-deterministic, universal, or alternating automata.
Cite as
Felix Klein and Martin Zimmermann. Prompt Delay. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 43:1-43:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{klein_et_al:LIPIcs.FSTTCS.2016.43,
author = {Klein, Felix and Zimmermann, Martin},
title = {{Prompt Delay}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {43:1--43:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.43},
URN = {urn:nbn:de:0030-drops-68786},
doi = {10.4230/LIPIcs.FSTTCS.2016.43},
annote = {Keywords: Infinite Games, Delay Games, Prompt-LTL, LTL}
}
Document
Mean-Payoff Games on Timed Automata
Abstract
Mean-payoff games on timed automata are played on the infinite weighted graph of configurations of priced timed automata between two players - Player Min and Player Max - by moving a token along the states of the graph to form an infinite run. The goal of Player Min is to minimize the limit average weight of the run, while the goal of the Player Max is the opposite. Brenguier, Cassez, and Raskin recently studied a variation of these games and showed that mean-payoff games are undecidable for timed automata with five or more clocks. We refine this result by proving the undecidability of mean-payoff games with three clocks. On a positive side, we show the decidability of mean-payoff games on one-clock timed automata with binary price-rates. A key contribution of this paper is the application of dynamic programming based proof techniques applied in the context of average reward optimization on an uncountable state and action space.
Cite as
Shibashis Guha, Marcin Jurdzinski, Shankara Narayanan Krishna, and Ashutosh Trivedi. Mean-Payoff Games on Timed Automata. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 44:1-44:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{guha_et_al:LIPIcs.FSTTCS.2016.44,
author = {Guha, Shibashis and Jurdzinski, Marcin and Krishna, Shankara Narayanan and Trivedi, Ashutosh},
title = {{Mean-Payoff Games on Timed Automata}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {44:1--44:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.44},
URN = {urn:nbn:de:0030-drops-68797},
doi = {10.4230/LIPIcs.FSTTCS.2016.44},
annote = {Keywords: Timed Automata, Mean-Payoff Games, Controller-Synthesis}
}
Document
The Power and Limitations of Uniform Samples in Testing Properties of Figures
Abstract
We investigate testing of properties of 2-dimensional figures that consist of a black object on a white background. Given a parameter epsilon in (0,1/2), a tester for a specified property has to accept with probability at least 2/3 if the input figure satisfies the property and reject with probability at least 2/3 if it does not. In general, property testers can query the color of any point in the input figure.
We study the power of testers that get access only to uniform samples from the input figure. We show that for the property of being a half-plane, the uniform testers are as powerful as general testers: they require only O(1/epsilon) samples. In contrast, we prove that convexity can be tested with O(1/epsilon) queries by testers that can make queries of their choice while uniform testers for this property require Omega(1/epsilon^{5/4}) samples. Previously, the fastest known tester for convexity needed Theta(1/epsilon^{4/3}) queries.
Cite as
Piotr Berman, Meiram Murzabulatov, and Sofya Raskhodnikova. The Power and Limitations of Uniform Samples in Testing Properties of Figures. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 45:1-45:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{berman_et_al:LIPIcs.FSTTCS.2016.45,
author = {Berman, Piotr and Murzabulatov, Meiram and Raskhodnikova, Sofya},
title = {{The Power and Limitations of Uniform Samples in Testing Properties of Figures}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {45:1--45:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.45},
URN = {urn:nbn:de:0030-drops-68803},
doi = {10.4230/LIPIcs.FSTTCS.2016.45},
annote = {Keywords: Property testing, randomized algorithms, being a half-plane, convexity}
}
Document
Local Testing for Membership in Lattices
Abstract
Testing membership in lattices is of practical relevance, with applications to integer programming, error detection in lattice-based communication and cryptography. In this work, we initiate a systematic study of local testing for membership in lattices, complementing and building upon the extensive body of work on locally testable codes. In particular, we formally define the notion of local tests for lattices and present the following:
1. We show that in order to achieve low query complexity, it is sufficient to design one-sided non-adaptive canonical tests. This result is akin to, and based on an analogous result for error-correcting codes due to Ben-Sasson et al. (SIAM J. Computing, 35(1):1-21).
2. We demonstrate upper and lower bounds on the query complexity of local testing for membership in code formula lattices. We instantiate our results for code formula lattices constructed from Reed-Muller codes to obtain nearly-matching upper and lower bounds on the query complexity of testing such lattices.
3. We contrast lattice testing from code testing by showing lower bounds on the query complexity of testing low-dimensional lattices. This illustrates large lower bounds on the query complexity of testing membership in knapsack lattices. On the other hand, we show that knapsack lattices with bounded coefficients have low-query testers if the inputs are promised to lie in the span of the lattice.
Cite as
Karthekeyan Chandrasekaran, Mahdi Cheraghchi, Venkata Gandikota, and Elena Grigorescu. Local Testing for Membership in Lattices. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 46:1-46:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{chandrasekaran_et_al:LIPIcs.FSTTCS.2016.46,
author = {Chandrasekaran, Karthekeyan and Cheraghchi, Mahdi and Gandikota, Venkata and Grigorescu, Elena},
title = {{Local Testing for Membership in Lattices}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {46:1--46:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.46},
URN = {urn:nbn:de:0030-drops-68818},
doi = {10.4230/LIPIcs.FSTTCS.2016.46},
annote = {Keywords: Lattices, Property Testing, Locally Testable Codes, Complexity Theory}
}
Document
Super-Fast MST Algorithms in the Congested Clique Using o(m) Messages
Abstract
In a sequence of recent results (PODC 2015 and PODC 2016), the running time of the fastest algorithm for the minimum spanning tree (MST) problem in the Congested Clique model was first improved to O(log(log(log(n)))) from O(log(log(n))) (Hegeman et al., PODC 2015) and then to O(log^*(n)) (Ghaffari and Parter, PODC 2016). All of these algorithms use Theta(n^2) messages independent of the number of edges in the input graph.
This paper positively answers a question raised in Hegeman et al., and presents the first "super-fast" MST algorithm with o(m) message complexity for input graphs with m edges. Specifically, we present an algorithm running in O(log^*(n)) rounds, with message complexity ~O(sqrt{m * n}) and then build on this algorithm to derive a family of algorithms, containing for any epsilon, 0 < epsilon <= 1, an algorithm running in O(log^*(n)/epsilon) rounds, using ~O(n^{1 + epsilon}/epsilon) messages. Setting epsilon = log(log(n))/log(n) leads to the first sub-logarithmic round Congested Clique MST algorithm that uses only ~O(n) messages.
Our primary tools in achieving these results are
(i) a component-wise bound on the number of candidates for MST edges, extending the sampling lemma of Karger, Klein, and Tarjan (Karger, Klein, and Tarjan, JACM 1995) and
(ii) Theta(log(n))-wise-independent linear graph sketches (Cormode and Firmani, Dist. Par. Databases, 2014) for generating MST candidate edges.
Cite as
Sriram V. Pemmaraju and Vivek B. Sardeshmukh. Super-Fast MST Algorithms in the Congested Clique Using o(m) Messages. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 47:1-47:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{pemmaraju_et_al:LIPIcs.FSTTCS.2016.47,
author = {Pemmaraju, Sriram V. and Sardeshmukh, Vivek B.},
title = {{Super-Fast MST Algorithms in the Congested Clique Using o(m) Messages}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {47:1--47:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.47},
URN = {urn:nbn:de:0030-drops-68827},
doi = {10.4230/LIPIcs.FSTTCS.2016.47},
annote = {Keywords: Congested Clique, Minimum Spanning Tree, Linear Graph Sketches, Message Complexity, Sampling}
}
Document
Why Liveness for Timed Automata Is Hard, and What We Can Do About It
Abstract
The liveness problem for timed automata asks if a given automaton has a run passing infinitely often through an accepting state. We show that unless P=NP, the liveness problem is more difficult than the reachability problem; more precisely, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is NP-hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it with the existing solutions.
Cite as
Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz. Why Liveness for Timed Automata Is Hard, and What We Can Do About It. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 48:1-48:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{herbreteau_et_al:LIPIcs.FSTTCS.2016.48,
author = {Herbreteau, Fr\'{e}d\'{e}ric and Srivathsan, B. and Tran, Thanh-Tung and Walukiewicz, Igor},
title = {{Why Liveness for Timed Automata Is Hard, and What We Can Do About It}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {48:1--48:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.48},
URN = {urn:nbn:de:0030-drops-68831},
doi = {10.4230/LIPIcs.FSTTCS.2016.48},
annote = {Keywords: Timed automata, model-checking, liveness invariant, state subsumption}
}
Document
Verified Analysis of List Update Algorithms
Abstract
This paper presents a machine-verified analysis of a number of classical algorithms for the list update problem: 2-competitiveness of move-to-front, the lower bound of 2 for the competitiveness of deterministic list update algorithms and 1.6-competitiveness of the randomized COMB algorithm, the best randomized list update algorithm known to date. The analysis is verified with help of the theorem prover Isabelle; some low-level proofs could be automated.
Cite as
Maximilian P. L. Haslbeck and Tobias Nipkow. Verified Analysis of List Update Algorithms. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{haslbeck_et_al:LIPIcs.FSTTCS.2016.49,
author = {Haslbeck, Maximilian P. L. and Nipkow, Tobias},
title = {{Verified Analysis of List Update Algorithms}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {49:1--49:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.49},
URN = {urn:nbn:de:0030-drops-68849},
doi = {10.4230/LIPIcs.FSTTCS.2016.49},
annote = {Keywords: Program Verification, Algorithm Analysis, Online Algorithms}
}
Document
Tunable Online MUS/MSS Enumeration
Abstract
In various areas of computer science, the problem of dealing with a set of constraints arises. If the set of constraints is unsatisfiable, one may ask for a minimal description of the reason for this unsatisifiability. Minimal unsatisfiable subsets (MUSes) and maximal satisfiable subsets (MSSes) are two kinds of such minimal descriptions. The goal of this work is the enumeration of MUSes and MSSes for a given constraint system. As such full enumeration may be intractable in general, we focus on building an online algorithm, which produces MUSes/MSSes in an on-the-fly manner as soon as they are discovered. The problem has been studied before even in its online version. However, our algorithm uses a novel approach that is able to outperform the current state-of-the art algorithms for online MUS/MSS enumeration. Moreover, the performance of our algorithm can be adjusted using tunable parameters. We evaluate the algorithm on a set of benchmarks.
Cite as
Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jirí Barnat. Tunable Online MUS/MSS Enumeration. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 50:1-50:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
Copy BibTex To Clipboard
@InProceedings{bendik_et_al:LIPIcs.FSTTCS.2016.50,
author = {Bend{\'\i}k, Jaroslav and Benes, Nikola and Cern\'{a}, Ivana and Barnat, Jir{\'\i}},
title = {{Tunable Online MUS/MSS Enumeration}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {50:1--50:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.50},
URN = {urn:nbn:de:0030-drops-68855},
doi = {10.4230/LIPIcs.FSTTCS.2016.50},
annote = {Keywords: Minimal unsatisfiable subsets, Maximal satisfiable subsets, Unsatisfiab- ility analysis, Infeasibility analysis}
}