Volume
LIPIcs, Volume 122
38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)
Event
FSTTCS 2018, December 11-13, 2018, Ahmedabad, IndiaEditors
Publication Details
- published at: 2018-12-05
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-093-4
- DBLP: db/conf/fsttcs/fsttcs2018
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 122, FSTTCS'18, Complete Volume
Abstract
LIPIcs, Volume 122, FSTTCS'18, Complete Volume
Cite as
38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Proceedings{ganguly_et_al:LIPIcs.FSTTCS.2018,
title = {{LIPIcs, Volume 122, FSTTCS'18, Complete Volume}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018},
URN = {urn:nbn:de:0030-drops-100240},
doi = {10.4230/LIPIcs.FSTTCS.2018},
annote = {Keywords: Theory of Computation}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ganguly_et_al:LIPIcs.FSTTCS.2018.0,
author = {Ganguly, Sumit and Pandya, Paritosh},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.0},
URN = {urn:nbn:de:0030-drops-98992},
doi = {10.4230/LIPIcs.FSTTCS.2018.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper)
Abstract
Random testing has proven to be an effective way to catch bugs in concurrent and distributed systems. This is surprising, as the space of executions is enormous and conventional formal methods intuition would suggest that bad behaviors would only be found by extremely unlikely coincidences.
Empirically, many bugs in distributed systems can be explained by interactions among only a small number of features. Thus, one can attempt to explain the effectiveness of random testing under various "small depth" hypotheses. In particular, it may be possible to test all interactions of k features for a small constant k by executing a family of tests that is exponentially or even doubly-exponentially smaller than the family of all tests. Moreover, under certain conditions, a randomly chosen small set of tests is sufficient to cover all k-wise interactions with high probability.
I will describe two concrete scenarios. First, I will describe bugs in distributed systems caused by network partition faults. In many practical instances, these bugs occur due to two or three key nodes, such as leaders or replicas, not being able to communicate, or because the leading node finds itself in a block of the partition without quorum. In this case, I will show using the probabilistic method that a small set of randomly chosen tests will cover all "small partition" scenarios with high probability.
Second, I will consider bugs that arise due to unexpected schedules (interleavings) of concurrent events. Again, many bugs depend only on the relative ordering of a small number of events (the "bug depth" of the bug). In this case, I will show a testing algorithm that prioritizes low depth interleavings and a randomized testing algorithm that bounds the probability of sampling any behavior of bug depth k for a fixed k. The testing algorithm is based on combinatorial insights from the theory of partial orders, such as the notion of dimension and its generalization to d-hitting families as well as results on online chain partitioning.
Beyond the potential for designing or explaining random testing procedures, the technical arguments show the potential of combining "Theory A" and "Theory B" results to the important domain of software testing.
This is joint work primarily with Filip Niksic [Filip Niksic, 2018], and with Dmitry Chistikov, Simin Oraee, Burcu Kulahcioglu Özkan, Mitra Tabaei Befrouei, and Georg Weissenbacher. This work was partially funded by an ERC Synergy Award (ImPACT).
Cite as
Rupak Majumdar. Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper). In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{majumdar:LIPIcs.FSTTCS.2018.1,
author = {Majumdar, Rupak},
title = {{Random Testing for Distributed Systems with Theoretical Guarantees}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.1},
URN = {urn:nbn:de:0030-drops-99000},
doi = {10.4230/LIPIcs.FSTTCS.2018.1},
annote = {Keywords: Random testing, Hitting families}
}
Document
Invited Paper
Model Checking Randomized Security Protocols (Invited Paper)
Abstract
The design of security protocols is extremely subtle and is prone to serious faults. Many tools for automatic analysis of such protocols have been developed. However, none of them have the ability to model protocols that use explicit randomization. Such randomized protocols are being increasingly used in systems to provide privacy and anonymity guarantees. In this talk we consider the problem of automatic verification of randomized security protocols. We consider verification of secrecy and indistinguishability properties under a powerful threat model of Dolev-Yao adversary. We present some complexity bounds on verification of these properties. We also describe practical algorithms for checking indistinguishability. These algorithms have been implemented in the tool SPAN and have been experimentally evaluated. The talk concludes with future challenges.
(Joint work with: Matt Bauer, Rohit Chadha and Mahesh Viswanathan)
Cite as
A. Prasad Sistla. Model Checking Randomized Security Protocols (Invited Paper). In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{sistla:LIPIcs.FSTTCS.2018.2,
author = {Sistla, A. Prasad},
title = {{Model Checking Randomized Security Protocols}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.2},
URN = {urn:nbn:de:0030-drops-99018},
doi = {10.4230/LIPIcs.FSTTCS.2018.2},
annote = {Keywords: Randomized Protocols, Verification}
}
Document
Invited Paper
Algorithms for the Asymmetric Traveling Salesman Problem (Invited Paper)
Abstract
The traveling salesman problem is one of the most fundamental optimization problems. Given n cities and pairwise distances, it is the problem of finding a tour of minimum total distance that visits each city once. In spite of significant research efforts, current techniques seem insufficient for settling the approximability of the traveling salesman problem. The gap in our understanding is especially large in the general asymmetric setting where the distance from city i to j is not assumed to equal the distance from j to i.
Indeed, until recently, it remained an open problem to design an algorithm with any constant approximation guarantee. This status is particularly intriguing as the standard linear programming relaxation is believed to give a constant-factor approximation algorithm, where the constant may in fact be as small as 2.
In this talk, we will give an overview of old and new approaches for settling this question. We shall, in particular, talk about our new approach that gives the first constant-factor approximation algorithm for the asymmetric traveling salesman problem. Our approximation guarantee is analyzed with respect to the standard LP relaxation, and thus our result confirms the conjectured constant integrality gap of that relaxation. The main idea of our approach is to first give a generic reduction to structured instances and on those instances we then solve an easier problem (but equivalent in terms of constant-factor approximation) obtained by relaxing the general connectivity requirements into local connectivity conditions.
This is based on joint work with Jakub Tarnawski and László A. Végh.
Cite as
Ola Svensson. Algorithms for the Asymmetric Traveling Salesman Problem (Invited Paper). In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{svensson:LIPIcs.FSTTCS.2018.3,
author = {Svensson, Ola},
title = {{Algorithms for the Asymmetric Traveling Salesman Problem}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.3},
URN = {urn:nbn:de:0030-drops-99024},
doi = {10.4230/LIPIcs.FSTTCS.2018.3},
annote = {Keywords: Approximation algorithms, combinatorial optimization, linear programming, traveling salesman problem}
}
Document
Invited Paper
Continuous Algorithms (Invited Paper)
Abstract
While the design of algorithms is traditionally a discrete endeavour, in recent years many advances have come from continuous perspectives. Typically, a continuous process, deterministic or randomized, is designed and shown to have desirable properties, such as approaching an optimal solution or a target distribution, and an algorithm is derived from this by appropriate discretization. We will discuss examples of this for optimization (gradient descent, interior-point method) and sampling (Brownian motion, Hamiltonian Monte Carlo), with applications to learning. In some interesting and rather general settings, the current fastest methods have been obtained via this approach.
Cite as
Santosh Vempala. Continuous Algorithms (Invited Paper). In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{vempala:LIPIcs.FSTTCS.2018.4,
author = {Vempala, Santosh},
title = {{Continuous Algorithms}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {4:1--4:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.4},
URN = {urn:nbn:de:0030-drops-99037},
doi = {10.4230/LIPIcs.FSTTCS.2018.4},
annote = {Keywords: Algorithms}
}
Document
On the Probabilistic Degree of OR over the Reals
Abstract
We study the probabilistic degree over R of the OR function on n variables. For epsilon in (0,1/3), the epsilon-error probabilistic degree of any Boolean function f:{0,1}^n -> {0,1} over R is the smallest non-negative integer d such that the following holds: there exists a distribution of polynomials Pol in R[x_1,...,x_n] entirely supported on polynomials of degree at most d such that for all z in {0,1}^n, we have Pr_{P ~ Pol}[P(z) = f(z)] >= 1- epsilon. It is known from the works of Tarui (Theoret. Comput. Sci. 1993) and Beigel, Reingold, and Spielman (Proc. 6th CCC 1991), that the epsilon-error probabilistic degree of the OR function is at most O(log n * log(1/epsilon)). Our first observation is that this can be improved to O{log (n atop <= log(1/epsilon))}, which is better for small values of epsilon.
In all known constructions of probabilistic polynomials for the OR function (including the above improvement), the polynomials P in the support of the distribution Pol have the following special structure: P(x_1,...,x_n) = 1 - prod_{i in [t]} (1- L_i(x_1,...,x_n)), where each L_i(x_1,..., x_n) is a linear form in the variables x_1,...,x_n, i.e., the polynomial 1-P(bar{x}) is a product of affine forms. We show that the epsilon-error probabilistic degree of OR when restricted to polynomials of the above form is Omega(log (n over <= log(1/epsilon))/log^2 (log (n over <= log(1/epsilon))})), thus matching the above upper bound (up to polylogarithmic factors).
Cite as
Siddharth Bhandari, Prahladh Harsha, Tulasimohan Molli, and Srikanth Srinivasan. On the Probabilistic Degree of OR over the Reals. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 5:1-5:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bhandari_et_al:LIPIcs.FSTTCS.2018.5,
author = {Bhandari, Siddharth and Harsha, Prahladh and Molli, Tulasimohan and Srinivasan, Srikanth},
title = {{On the Probabilistic Degree of OR over the Reals}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {5:1--5:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.5},
URN = {urn:nbn:de:0030-drops-99044},
doi = {10.4230/LIPIcs.FSTTCS.2018.5},
annote = {Keywords: Polynomials over reals, probabilistic polynomials, probabilistic degree, OR polynomial}
}
Document
Quasipolynomial Hitting Sets for Circuits with Restricted Parse Trees
Abstract
We study the class of non-commutative Unambiguous circuits or Unique-Parse-Tree (UPT) circuits, and a related model of Few-Parse-Trees (FewPT) circuits (which were recently introduced by Lagarde, Malod and Perifel [Guillaume Lagarde et al., 2016] and Lagarde, Limaye and Srinivasan [Guillaume Lagarde et al., 2017]) and give the following constructions:
- An explicit hitting set of quasipolynomial size for UPT circuits,
- An explicit hitting set of quasipolynomial size for FewPT circuits (circuits with constantly many parse tree shapes),
- An explicit hitting set of polynomial size for UPT circuits (of known parse tree shape), when a parameter of preimage-width is bounded by a constant.
The above three results are extensions of the results of [Manindra Agrawal et al., 2015], [Rohit Gurjar et al., 2015] and [Rohit Gurjar et al., 2016] to the setting of UPT circuits, and hence also generalize their results in the commutative world from read-once oblivious algebraic branching programs (ROABPs) to UPT-set-multilinear circuits.
The main idea is to study shufflings of non-commutative polynomials, which can then be used to prove suitable depth reduction results for UPT circuits and thereby allow a careful translation of the ideas in [Manindra Agrawal et al., 2015], [Rohit Gurjar et al., 2015] and [Rohit Gurjar et al., 2016].
Cite as
Ramprasad Saptharishi and Anamay Tengse. Quasipolynomial Hitting Sets for Circuits with Restricted Parse Trees. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{saptharishi_et_al:LIPIcs.FSTTCS.2018.6,
author = {Saptharishi, Ramprasad and Tengse, Anamay},
title = {{Quasipolynomial Hitting Sets for Circuits with Restricted Parse Trees}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {6:1--6:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.6},
URN = {urn:nbn:de:0030-drops-99050},
doi = {10.4230/LIPIcs.FSTTCS.2018.6},
annote = {Keywords: Unambiguous Circuits, Read-once Oblivious ABPs, Polynomial Identity Testing, Lower Bounds, Algebraic Circuit Complexity}
}
Document
Univariate Ideal Membership Parameterized by Rank, Degree, and Number of Generators
Abstract
Let F[X] be the polynomial ring over the variables X={x_1,x_2, ..., x_n}. An ideal I= <p_1(x_1), ..., p_n(x_n)> generated by univariate polynomials {p_i(x_i)}_{i=1}^n is a univariate ideal. We study the ideal membership problem for the univariate ideals and show the following results.
- Let f(X) in F[l_1, ..., l_r] be a (low rank) polynomial given by an arithmetic circuit where l_i : 1 <= i <= r are linear forms, and I=<p_1(x_1), ..., p_n(x_n)> be a univariate ideal. Given alpha in F^n, the (unique) remainder f(X) mod I can be evaluated at alpha in deterministic time d^{O(r)} * poly(n), where d=max {deg(f),deg(p_1)...,deg(p_n)}. This yields a randomized n^{O(r)} algorithm for minimum vertex cover in graphs with rank-r adjacency matrices. It also yields an n^{O(r)} algorithm for evaluating the permanent of a n x n matrix of rank r, over any field F. Over Q, an algorithm of similar run time for low rank permanent is due to Barvinok [Barvinok, 1996] via a different technique.
- Let f(X)in F[X] be given by an arithmetic circuit of degree k (k treated as fixed parameter) and I=<p_1(x_1), ..., p_n(x_n)>. We show that in the special case when I=<x_1^{e_1}, ..., x_n^{e_n}>, we obtain a randomized O^*(4.08^k) algorithm that uses poly(n,k) space.
- Given f(X)in F[X] by an arithmetic circuit and I=<p_1(x_1), ..., p_k(x_k)>, membership testing is W[1]-hard, parameterized by k. The problem is MINI[1]-hard in the special case when I=<x_1^{e_1}, ..., x_k^{e_k}>.
Cite as
V. Arvind, Abhranil Chatterjee, Rajit Datta, and Partha Mukhopadhyay. Univariate Ideal Membership Parameterized by Rank, Degree, and Number of Generators. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{arvind_et_al:LIPIcs.FSTTCS.2018.7,
author = {Arvind, V. and Chatterjee, Abhranil and Datta, Rajit and Mukhopadhyay, Partha},
title = {{Univariate Ideal Membership Parameterized by Rank, Degree, and Number of Generators}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.7},
URN = {urn:nbn:de:0030-drops-99068},
doi = {10.4230/LIPIcs.FSTTCS.2018.7},
annote = {Keywords: Combinatorial Nullstellensatz, Ideal Membership, Parametric Hardness, Low Rank Permanent}
}
Document
Verification of Timed Asynchronous Programs
Abstract
In this paper, we address the verification problem for timed asynchronous programs. We associate to each task, a deadline for its execution. We first show that the control state reachability problem for such class of systems is decidable while the configuration reachability problem is undecidable. Then, we consider the subclass of timed asynchronous programs where tasks are always being executed from the same state. For this subclass, we show that the control state reachability problem is PSPACE-complete. Furthermore, we show the decidability for the configuration reachability problem for the subclass.
Cite as
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna, and Shaan Vaidya. Verification of Timed Asynchronous Programs. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2018.8,
author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Krishna, Shankara Narayanan and Vaidya, Shaan},
title = {{Verification of Timed Asynchronous Programs}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {8:1--8:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.8},
URN = {urn:nbn:de:0030-drops-99076},
doi = {10.4230/LIPIcs.FSTTCS.2018.8},
annote = {Keywords: Reachability, Timed Automata, Asynchronous programs}
}
Document
The Cayley-Graph of the Queue Monoid: Logic and Decidability
Abstract
We investigate the decidability of logical aspects of graphs that arise as Cayley-graphs of the so-called queue monoids. These monoids model the behavior of the classical (reliable) fifo-queues. We answer a question raised by Huschenbett, Kuske, and Zetzsche and prove the decidability of the first-order theory of these graphs with the help of an - at least for the authors - new combination of the well-known method from Ferrante and Rackoff and an automata-based approach. On the other hand, we prove that the monadic second-order of the queue monoid's Cayley-graph is undecidable.
Cite as
Faried Abu Zaid and Chris Köcher. The Cayley-Graph of the Queue Monoid: Logic and Decidability. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{abuzaid_et_al:LIPIcs.FSTTCS.2018.9,
author = {Abu Zaid, Faried and K\"{o}cher, Chris},
title = {{The Cayley-Graph of the Queue Monoid: Logic and Decidability}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {9:1--9:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.9},
URN = {urn:nbn:de:0030-drops-99088},
doi = {10.4230/LIPIcs.FSTTCS.2018.9},
annote = {Keywords: Queues, Transformation Monoid, Cayley-Graph, Logic, First-Order Theory, MSO Theory, Model Checking}
}
Document
Uniformly Automatic Classes of Finite Structures
Abstract
We investigate the recently introduced concept of uniformly tree-automatic classes in the realm of parameterized complexity theory. Roughly speaking, a class of finite structures is uniformly tree-automatic if it can be presented by a set of finite trees and a tuple of automata. A tree t encodes a structure and an element of this structure is encoded by a labeling of t. The automata are used to present the relations of the structure. We use this formalism to obtain algorithmic meta-theorems for first-order logic and in some cases also monadic second-order logic on classes of finite Boolean algebras, finite groups, and graphs of bounded tree-depth. Our main concern is the efficiency of this approach with respect to the hidden parameter dependence (size of the formula). We develop a method to analyze the complexity of uniformly tree-automatic presentations, which allows us to give upper bounds for the runtime of the automata-based model checking algorithm on the presented class. It turns out that the parameter dependence is elementary for all the above mentioned classes. Additionally we show that one can lift the FPT results, which are obtained by our method, from a class C to the closure of C under direct products with only a singly exponential blow-up in the parameter dependence.
Cite as
Faried Abu Zaid. Uniformly Automatic Classes of Finite Structures. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{abuzaid:LIPIcs.FSTTCS.2018.10,
author = {Abu Zaid, Faried},
title = {{Uniformly Automatic Classes of Finite Structures}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {10:1--10:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.10},
URN = {urn:nbn:de:0030-drops-99095},
doi = {10.4230/LIPIcs.FSTTCS.2018.10},
annote = {Keywords: Automatic Structures, Model Checking, Fixed-Parameter Tractability, Algorithmic Meta Theorems}
}
Document
Towards a General Direct Product Testing Theorem
Abstract
The Direct Product encoding of a string a in {0,1}^n on an underlying domain V subseteq ([n] choose k), is a function DP_V(a) which gets as input a set S in V and outputs a restricted to S. In the Direct Product Testing Problem, we are given a function F:V -> {0,1}^k, and our goal is to test whether F is close to a direct product encoding, i.e., whether there exists some a in {0,1}^n such that on most sets S, we have F(S)=DP_V(a)(S). A natural test is as follows: select a pair (S,S')in V according to some underlying distribution over V x V, query F on this pair, and check for consistency on their intersection. Note that the above distribution may be viewed as a weighted graph over the vertex set V and is referred to as a test graph.
The testability of direct products was studied over various domains and test graphs: Dinur and Steurer (CCC '14) analyzed it when V equals the k-th slice of the Boolean hypercube and the test graph is a member of the Johnson graph family. Dinur and Kaufman (FOCS '17) analyzed it for the case where V is the set of faces of a Ramanujan complex, where in this case V=O_k(n). In this paper, we study the testability of direct products in a general setting, addressing the question: what properties of the domain and the test graph allow one to prove a direct product testing theorem?
Towards this goal we introduce the notion of coordinate expansion of a test graph. Roughly speaking a test graph is a coordinate expander if it has global and local expansion, and has certain nice intersection properties on sampling. We show that whenever the test graph has coordinate expansion then it admits a direct product testing theorem. Additionally, for every k and n we provide a direct product domain V subseteq (n choose k) of size n, called the Sliding Window domain for which we prove direct product testability.
Cite as
Elazar Goldenberg and Karthik C. S.. Towards a General Direct Product Testing Theorem. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{goldenberg_et_al:LIPIcs.FSTTCS.2018.11,
author = {Goldenberg, Elazar and C. S., Karthik},
title = {{Towards a General Direct Product Testing Theorem}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {11:1--11:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.11},
URN = {urn:nbn:de:0030-drops-99105},
doi = {10.4230/LIPIcs.FSTTCS.2018.11},
annote = {Keywords: Property Testing, Direct Product, PCP, Johnson graph, Ramanujan Complex, Derandomization}
}
Document
Space Complexity of Two Adaptive Bitprobe Schemes Storing Three Elements
Abstract
We consider the following set membership problem in the bitprobe model - that of storing subsets of size at most three from a universe of size m, and answering membership queries using two adaptive bitprobes. Baig and Kesh [Mirza Galib Anwarul Husain Baig and Deepanjan Kesh, 2018] proposed a scheme for the problem which takes O(m^{2/3}) space. In this paper, we present a proof which shows that any scheme for the problem requires Omega(m^{2/3}) amount of space. These two results together settle the space complexity issue for this particular problem.
Cite as
Deepanjan Kesh. Space Complexity of Two Adaptive Bitprobe Schemes Storing Three Elements. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 12:1-12:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kesh:LIPIcs.FSTTCS.2018.12,
author = {Kesh, Deepanjan},
title = {{Space Complexity of Two Adaptive Bitprobe Schemes Storing Three Elements}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {12:1--12:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.12},
URN = {urn:nbn:de:0030-drops-99110},
doi = {10.4230/LIPIcs.FSTTCS.2018.12},
annote = {Keywords: Data structures, set membership problem, bitprobe model, lower bound}
}
Document
New Constructions with Quadratic Separation between Sensitivity and Block Sensitivity
Abstract
Nisan and Szegedy [Nisan and Szegedy, 1994] conjectured that block sensitivity is at most polynomial in sensitivity for any Boolean function. There is a huge gap between the best known upper bound on block sensitivity in terms of sensitivity - which is exponential, and the best known separating examples - which give only a quadratic separation between block sensitivity and sensitivity.
In this paper we give various new constructions of families of Boolean functions that exhibit quadratic separation between sensitivity and block sensitivity. Our constructions have several novel aspects. For example, we give the first direct constructions of families of Boolean functions that have both 0-block sensitivity and 1-block sensitivity quadratically larger than sensitivity.
Cite as
Siddhesh Chaubal and Anna Gál. New Constructions with Quadratic Separation between Sensitivity and Block Sensitivity. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{chaubal_et_al:LIPIcs.FSTTCS.2018.13,
author = {Chaubal, Siddhesh and G\'{a}l, Anna},
title = {{New Constructions with Quadratic Separation between Sensitivity and Block Sensitivity}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {13:1--13:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.13},
URN = {urn:nbn:de:0030-drops-99129},
doi = {10.4230/LIPIcs.FSTTCS.2018.13},
annote = {Keywords: Sensitivity Conjecture, Boolean Functions, Complexity Measures}
}
Document
Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered
Abstract
Asada and Kobayashi [ICALP 2017] conjectured a higher-order version of Kruskal's tree theorem, and proved a pumping lemma for higher-order languages modulo the conjecture. The conjecture has been proved up to order-2, which implies that Asada and Kobayashi's pumping lemma holds for order-2 tree languages, but remains open for order-3 or higher. In this paper, we prove a variation of the conjecture for order-3. This is sufficient for proving that a variation of the pumping lemma holds for order-3 tree languages (equivalently, for order-4 word languages).
Cite as
Kazuyuki Asada and Naoki Kobayashi. Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{asada_et_al:LIPIcs.FSTTCS.2018.14,
author = {Asada, Kazuyuki and Kobayashi, Naoki},
title = {{Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {14:1--14:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.14},
URN = {urn:nbn:de:0030-drops-99138},
doi = {10.4230/LIPIcs.FSTTCS.2018.14},
annote = {Keywords: higher-order grammar, pumping lemma, Kruskal's tree theorem, well-quasi-ordering, simply-typed lambda calculus}
}
Document
A Hypersequent Calculus with Clusters for Tense Logic over Ordinals
Abstract
Prior's tense logic forms the core of linear temporal logic, with both past- and future-looking modalities. We present a sound and complete proof system for tense logic over ordinals. Technically, this is a hypersequent system, enriched with an ordering, clusters, and annotations. The system is designed with proof search algorithms in mind, and yields an optimal coNP complexity for the validity problem. It entails a small model property for tense logic over ordinals: every satisfiable formula has a model of order type at most omega^2. It also allows to answer the validity problem for ordinals below or exactly equal to a given one.
Cite as
David Baelde, Anthony Lick, and Sylvain Schmitz. A Hypersequent Calculus with Clusters for Tense Logic over Ordinals. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{baelde_et_al:LIPIcs.FSTTCS.2018.15,
author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain},
title = {{A Hypersequent Calculus with Clusters for Tense Logic over Ordinals}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {15:1--15:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.15},
URN = {urn:nbn:de:0030-drops-99143},
doi = {10.4230/LIPIcs.FSTTCS.2018.15},
annote = {Keywords: modal logic, proof system, hypersequent}
}
Document
Büchi Good-for-Games Automata Are Efficiently Recognizable
Abstract
Good-for-Games (GFG) automata offer a compromise between deterministic and nondeterministic automata. They can resolve nondeterministic choices in a step-by-step fashion, without needing any information about the remaining suffix of the word. These automata can be used to solve games with omega-regular conditions, and in particular were introduced as a tool to solve Church's synthesis problem. We focus here on the problem of recognizing Büchi GFG automata, that we call Büchi GFGness problem: given a nondeterministic Büchi automaton, is it GFG? We show that this problem can be decided in P, and more precisely in O(n^4m^2|Sigma|^2), where n is the number of states, m the number of transitions and |Sigma| is the size of the alphabet. We conjecture that a very similar algorithm solves the problem in polynomial time for any fixed parity acceptance condition.
Cite as
Marc Bagnol and Denis Kuperberg. Büchi Good-for-Games Automata Are Efficiently Recognizable. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 16:1-16:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bagnol_et_al:LIPIcs.FSTTCS.2018.16,
author = {Bagnol, Marc and Kuperberg, Denis},
title = {{B\"{u}chi Good-for-Games Automata Are Efficiently Recognizable}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {16:1--16:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.16},
URN = {urn:nbn:de:0030-drops-99157},
doi = {10.4230/LIPIcs.FSTTCS.2018.16},
annote = {Keywords: B\"{u}chi, automata, games, polynomial time, nondeterminism}
}
Document
Popular Matchings in Complete Graphs
Abstract
Our input is a complete graph G = (V,E) on n vertices where each vertex has a strict ranking of all other vertices in G. The goal is to construct a matching in G that is "globally stable" or popular. A matching M is popular if M does not lose a head-to-head election against any matching M': here each vertex casts a vote for the matching in {M,M'} where it gets a better assignment. Popular matchings need not exist in the given instance G and the popular matching problem is to decide whether one exists or not. The popular matching problem in G is easy to solve for odd n. Surprisingly, the problem becomes NP-hard for even n, as we show here.
Cite as
Ágnes Cseh and Telikepalli Kavitha. Popular Matchings in Complete Graphs. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{cseh_et_al:LIPIcs.FSTTCS.2018.17,
author = {Cseh, \'{A}gnes and Kavitha, Telikepalli},
title = {{Popular Matchings in Complete Graphs}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {17:1--17:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.17},
URN = {urn:nbn:de:0030-drops-99164},
doi = {10.4230/LIPIcs.FSTTCS.2018.17},
annote = {Keywords: popular matching, complete graph, complexity, linear programming}
}
Document
Graph Pattern Polynomials
Abstract
Given a host graph G and a pattern graph H, the induced subgraph isomorphism problem is to decide whether G contains an induced subgraph that is isomorphic to H. We study the time complexity of induced subgraph isomorphism problems when the pattern graph is fixed. Nesetril and Poljak gave an O(n^{k omega}) time algorithm that decides the induced subgraph isomorphism problem for any 3k vertex pattern graph (the universal algorithm), where omega is the matrix multiplication exponent. Improvements are not known for any infinite pattern family.
Algorithms faster than the universal algorithm are known only for a finite number of pattern graphs. In this paper, we show that there exists infinitely many pattern graphs for which the induced subgraph isomorphism problem has algorithms faster than the universal algorithm.
Our algorithm works by reducing the pattern detection problem into a multilinear term detection problem on special classes of polynomials called graph pattern polynomials. We show that many of the existing algorithms including the universal algorithm can also be described in terms of such a reduction. We formalize this class of algorithms by defining graph pattern polynomial families and defining a notion of reduction between these polynomial families. The reduction also allows us to argue about relative hardness of various graph pattern detection problems within this framework. We show that solving the induced subgraph isomorphism for any pattern graph that contains a k-clique is at least as hard detecting k-cliques. An equivalent theorem is not known in the general case.
In the full version of this paper, we obtain new algorithms for P_5 and C_5 that are optimal under reasonable hardness assumptions. We also use this method to derive new combinatorial algorithms - algorithms that do not use fast matrix multiplication - for paths and cycles. We also show why graph homomorphisms play a major role in algorithms for subgraph isomorphism problems. Using this, we show that the arithmetic circuit complexity of the graph homomorphism polynomial for K_k - e (The k-clique with an edge removed) is related to the complexity of many subgraph isomorphism problems. This generalizes and unifies many existing results.
Cite as
Markus Bläser, Balagopal Komarath, and Karteek Sreenivasaiah. Graph Pattern Polynomials. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 18:1-18:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{blaser_et_al:LIPIcs.FSTTCS.2018.18,
author = {Bl\"{a}ser, Markus and Komarath, Balagopal and Sreenivasaiah, Karteek},
title = {{Graph Pattern Polynomials}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {18:1--18:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.18},
URN = {urn:nbn:de:0030-drops-99172},
doi = {10.4230/LIPIcs.FSTTCS.2018.18},
annote = {Keywords: algorithms, induced subgraph detection, algebraic framework}
}
Document
Shortest k-Disjoint Paths via Determinants
Abstract
The well-known k-disjoint path problem (k-DPP) asks for pairwise vertex-disjoint paths between k specified pairs of vertices (s_i, t_i) in a given graph, if they exist. The decision version of the shortest k-DPP asks for the length of the shortest (in terms of total length) such paths. Similarly, the search and counting versions ask for one such and the number of such shortest set of paths, respectively.
We restrict attention to the shortest k-DPP instances on undirected planar graphs where all sources and sinks lie on a single face or on a pair of faces. We provide efficient sequential and parallel algorithms for the search versions of the problem answering one of the main open questions raised by Colin de Verdière and Schrijver [Éric Colin de Verdière and Alexander Schrijver, 2011] for the general one-face problem. We do so by providing a randomised NC^2 algorithm along with an O(n^{omega/2}) time randomised sequential algorithm, for any fixed k. We also obtain deterministic algorithms with similar resource bounds for the counting and search versions. In contrast, previously, only the sequential complexity of decision and search versions of the "well-ordered" case has been studied. For the one-face case, sequential versions of our routines have better running times for constantly many terminals.
The algorithms are based on a bijection between a shortest k-tuple of disjoint paths in the given graph and cycle covers in a related digraph. This allows us to non-trivially modify established techniques relating counting cycle covers to the determinant. We further need to do a controlled inclusion-exclusion to produce a polynomial sum of determinants such that all "bad" cycle covers cancel out in the sum allowing us to count "pure" cycle covers.
Cite as
Samir Datta, Siddharth Iyer, Raghav Kulkarni, and Anish Mukherjee. Shortest k-Disjoint Paths via Determinants. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{datta_et_al:LIPIcs.FSTTCS.2018.19,
author = {Datta, Samir and Iyer, Siddharth and Kulkarni, Raghav and Mukherjee, Anish},
title = {{Shortest k-Disjoint Paths via Determinants}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {19:1--19:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.19},
URN = {urn:nbn:de:0030-drops-99183},
doi = {10.4230/LIPIcs.FSTTCS.2018.19},
annote = {Keywords: disjoint paths, planar graph, parallel algorithm, cycle cover, determinant, inclusion-exclusion}
}
Document
Hyper Partial Order Logic
Abstract
We define HyPOL, a local hyper logic for partial order models, expressing properties of sets of runs. These properties depict shapes of causal dependencies in sets of partially ordered executions, with similarity relations defined as isomorphisms of past observations. Unsurprisingly, since comparison of projections are included, satisfiability of this logic is undecidable. We then address model checking of HyPOL and show that, already for safe Petri nets, the problem is undecidable. Fortunately, sensible restrictions of observations and nets allow us to bring back model checking of HyPOL to a decidable problem, namely model checking of MSO on graphs of bounded treewidth.
Cite as
Béatrice Bérard, Stefan Haar, and Loic Hélouët. Hyper Partial Order Logic. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{berard_et_al:LIPIcs.FSTTCS.2018.20,
author = {B\'{e}rard, B\'{e}atrice and Haar, Stefan and H\'{e}lou\"{e}t, Loic},
title = {{Hyper Partial Order Logic}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {20:1--20:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.20},
URN = {urn:nbn:de:0030-drops-99190},
doi = {10.4230/LIPIcs.FSTTCS.2018.20},
annote = {Keywords: Partial orders, logic, hyper-logic}
}
Document
On the Way to Alternating Weak Automata
Abstract
Different types of automata over words and trees offer different trade-offs between expressivity, conciseness, and the complexity of decision procedures. Alternating weak automata enjoy simple algorithms for emptiness and membership checks, which makes transformations into automata of this type particularly interesting. For instance, an algorithm for solving two-player infinite games can be viewed as a special case of such a transformation. However, our understanding of the worst-case size blow-up that these transformations can incur is rather poor. This paper establishes two new results, one on word automata and one on tree automata. We show that:
- Alternating parity word automata can be turned into alternating weak automata of quasi-polynomial (rather than exponential) size.
- Universal co-Büchi tree automata, a special case of alternating parity tree automata, can be exponentially more concise than alternating weak automata.
Along the way, we present a family of game languages, strict for the levels of the weak hierarchy of tree automata, which corresponds to a weak version of the canonical game languages known to be strict for the Mostowski - Rabin index hierarchy.
Cite as
Udi Boker and Karoliina Lehtinen. On the Way to Alternating Weak Automata. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{boker_et_al:LIPIcs.FSTTCS.2018.21,
author = {Boker, Udi and Lehtinen, Karoliina},
title = {{On the Way to Alternating Weak Automata}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {21:1--21:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.21},
URN = {urn:nbn:de:0030-drops-99200},
doi = {10.4230/LIPIcs.FSTTCS.2018.21},
annote = {Keywords: Alternating automata, Parity games, Parity automata, Weak automata}
}
Document
Origin-Equivalence of Two-Way Word Transducers Is in PSPACE
Abstract
We consider equivalence and containment problems for word transductions. These problems are known to be undecidable when the transductions are relations between words realized by non-deterministic transducers, and become decidable when restricting to functions from words to words. Here we prove that decidability can be equally recovered the origin semantics, that was introduced by Bojanczyk in 2014. We prove that the equivalence and containment problems for two-way word transducers in the origin semantics are PSPACE-complete. We also consider a variant of the containment problem where two-way transducers are compared under the origin semantics, but in a more relaxed way, by allowing distortions of the origins. The possible distortions are described by means of a resynchronization relation. We propose MSO-definable resynchronizers and show that they preserve the decidability of the containment problem under resynchronizations.
{}
Cite as
Sougata Bose, Anca Muscholl, Vincent Penelle, and Gabriele Puppis. Origin-Equivalence of Two-Way Word Transducers Is in PSPACE. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bose_et_al:LIPIcs.FSTTCS.2018.22,
author = {Bose, Sougata and Muscholl, Anca and Penelle, Vincent and Puppis, Gabriele},
title = {{Origin-Equivalence of Two-Way Word Transducers Is in PSPACE}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {22:1--22:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.22},
URN = {urn:nbn:de:0030-drops-99213},
doi = {10.4230/LIPIcs.FSTTCS.2018.22},
annote = {Keywords: Transducers, origin semantics, equivalence}
}
Document
Constant Factor Approximation Algorithm for Uniform Hard Capacitated Knapsack Median Problem
Abstract
In this paper, we give the first constant factor approximation algorithm for capacitated knapsack median problem (CKnM) for hard uniform capacities, violating the budget by a factor of 1+epsilon and capacities by a 2+epsilon factor. To the best of our knowledge, no constant factor approximation is known for the problem even with capacity/budget/both violations. Even for the uncapacitated variant of the problem, the natural LP is known to have an unbounded integrality gap even after adding the covering inequalities to strengthen the LP. Our techniques for CKnM provide two types of results for the capacitated k-facility location problem. We present an O(1/epsilon^2) factor approximation for the problem, violating capacities by (2+epsilon). Another result is an O(1/epsilon) factor approximation, violating the capacities by a factor of at most (1 + epsilon) using at most 2k facilities for a fixed epsilon>0. As a by-product, a constant factor approximation algorithm for capacitated facility location problem with uniform capacities is presented, violating the capacities by (1 + epsilon) factor. Though constant factor results are known for the problem without violating the capacities, the result is interesting as it is obtained by rounding the solution to the natural LP, which is known to have an unbounded integrality gap without violating the capacities. Thus, we achieve the best possible from the natural LP for the problem. The result shows that the natural LP is not too bad.
Cite as
Sapna Grover, Neelima Gupta, Samir Khuller, and Aditya Pancholi. Constant Factor Approximation Algorithm for Uniform Hard Capacitated Knapsack Median Problem. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 23:1-23:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{grover_et_al:LIPIcs.FSTTCS.2018.23,
author = {Grover, Sapna and Gupta, Neelima and Khuller, Samir and Pancholi, Aditya},
title = {{Constant Factor Approximation Algorithm for Uniform Hard Capacitated Knapsack Median Problem}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {23:1--23:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.23},
URN = {urn:nbn:de:0030-drops-99224},
doi = {10.4230/LIPIcs.FSTTCS.2018.23},
annote = {Keywords: Capacitated Knapsack Median, Capacitated k -Facility Location}
}
Document
A 5-Approximation for Universal Facility Location
Abstract
In this paper, we propose and analyze a local search algorithm for the Universal facility location problem. Our algorithm improves the approximation ratio of this problem from 5.83, given by Angel et al., to 5. A second major contribution of the paper is that it gets rid of the expensive multi operation that was a mainstay of all previous local search algorithms for capacitated facility location and universal facility location problem. The only operations that we require to prove the 5-approximation are add, open, and close. A multi operation is basically a combination of the open and close operations. The 5-approximation algorithm for the capacitated facility location problem, given by Bansal et al., also uses the multi operation. However, on careful observation, it turned out that add, open, and close operations are sufficient to prove a 5-factor for the problem. This resulted into an improved algorithm for the universal facility location problem, with an improved factor.
Cite as
Manisha Bansal, Naveen Garg, and Neelima Gupta. A 5-Approximation for Universal Facility Location. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 24:1-24:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bansal_et_al:LIPIcs.FSTTCS.2018.24,
author = {Bansal, Manisha and Garg, Naveen and Gupta, Neelima},
title = {{A 5-Approximation for Universal Facility Location}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {24:1--24:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.24},
URN = {urn:nbn:de:0030-drops-99239},
doi = {10.4230/LIPIcs.FSTTCS.2018.24},
annote = {Keywords: Facility location, Approximation Algorithms, Local Search}
}
Document
On Fair Division for Indivisible Items
Abstract
We consider the task of assigning indivisible goods to a set of agents in a fair manner. Our notion of fairness is Nash social welfare, i.e., the goal is to maximize the geometric mean of the utilities of the agents. Each good comes in multiple items or copies, and the utility of an agent diminishes as it receives more items of the same good. The utility of a bundle of items for an agent is the sum of the utilities of the items in the bundle. Each agent has a utility cap beyond which he does not value additional items. We give a polynomial time approximation algorithm that maximizes Nash social welfare up to a factor of e^{1/{e}} ~~ 1.445. The computed allocation is Pareto-optimal and approximates envy-freeness up to one item up to a factor of 2 + epsilon.
Cite as
Bhaskar Ray Chaudhury, Yun Kuen Cheung, Jugal Garg, Naveen Garg, Martin Hoefer, and Kurt Mehlhorn. On Fair Division for Indivisible Items. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{chaudhury_et_al:LIPIcs.FSTTCS.2018.25,
author = {Chaudhury, Bhaskar Ray and Cheung, Yun Kuen and Garg, Jugal and Garg, Naveen and Hoefer, Martin and Mehlhorn, Kurt},
title = {{On Fair Division for Indivisible Items}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {25:1--25:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.25},
URN = {urn:nbn:de:0030-drops-99242},
doi = {10.4230/LIPIcs.FSTTCS.2018.25},
annote = {Keywords: Fair Division, Indivisible Goods, Envy-Free}
}
Document
Combinatorial Algorithms for General Linear Arrow-Debreu Markets
Abstract
We present a combinatorial algorithm for determining the market clearing prices of a general linear Arrow-Debreu market, where every agent can own multiple goods. The existing combinatorial algorithms for linear Arrow-Debreu markets consider the case where each agent can own all of one good only. We present an O~((n+m)^7 log^3(UW)) algorithm where n, m, U and W refer to the number of agents, the number of goods, the maximal integral utility and the maximum quantity of any good in the market respectively. The algorithm refines the iterative algorithm of Duan, Garg and Mehlhorn using several new ideas. We also identify the hard instances for existing combinatorial algorithms for linear Arrow-Debreu markets. In particular we find instances where the ratio of the maximum to the minimum equilibrium price of a good is U^{Omega(n)} and the number of iterations required by the existing iterative combinatorial algorithms of Duan, and Mehlhorn and Duan, Garg, and Mehlhorn are high. Our instances also separate the two algorithms.
Cite as
Bhaskar Ray Chaudhury and Kurt Mehlhorn. Combinatorial Algorithms for General Linear Arrow-Debreu Markets. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{chaudhury_et_al:LIPIcs.FSTTCS.2018.26,
author = {Chaudhury, Bhaskar Ray and Mehlhorn, Kurt},
title = {{Combinatorial Algorithms for General Linear Arrow-Debreu Markets}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {26:1--26:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.26},
URN = {urn:nbn:de:0030-drops-99255},
doi = {10.4230/LIPIcs.FSTTCS.2018.26},
annote = {Keywords: Linear Exchange Markets, Equilibrium, Combinatorial Algorithms}
}
Document
On the Welfare of Cardinal Voting Mechanisms
Abstract
A voting mechanism is a method for preference aggregation that takes as input preferences over alternatives from voters, and selects an alternative, or a distribution over alternatives. While preferences of voters are generally assumed to be cardinal utility functions that map each alternative to a real value, mechanisms typically studied assume coarser inputs, such as rankings of the alternatives (called ordinal mechanisms). We study cardinal mechanisms, that take as input the cardinal utilities of the voters, with the objective of minimizing the distortion - the worst-case ratio of the best social welfare to that obtained by the mechanism.
For truthful cardinal mechanisms with m alternatives and n voters, we show bounds of Theta(mn), Omega(m), and Omega(sqrt{m}) for deterministic, unanimous, and randomized mechanisms respectively. This shows, somewhat surprisingly, that even mechanisms that allow cardinal inputs have large distortion. There exist ordinal (and hence, cardinal) mechanisms with distortion O(sqrt{m log m}), and hence our lower bound for randomized mechanisms is nearly tight. In an effort to close this gap, we give a class of truthful cardinal mechanisms that we call randomized hyperspherical mechanisms that have O(sqrt{m log m}) distortion. These are interesting because they violate two properties - localization and non-perversity - that characterize truthful ordinal mechanisms, demonstrating non-trivial mechanisms that differ significantly from ordinal mechanisms.
Given the strong lower bounds for truthful mechanisms, we then consider approximately truthful mechanisms. We give a mechanism that is delta-truthful given delta in (0,1), and has distortion close to 1. Finally, we consider the simple mechanism that selects the alternative that maximizes social welfare. This mechanism is not truthful, and we study the distortion at equilibria for the voters (equivalent to the Price of Anarchy, or PoA). While in general, the PoA is unbounded, we show that for equilibria obtained from natural dynamics, the PoA is close to 1. Thus relaxing the notion of truthfulness in both cases allows us to obtain near-optimal distortion.
Cite as
Umang Bhaskar and Abheek Ghosh. On the Welfare of Cardinal Voting Mechanisms. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 27:1-27:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bhaskar_et_al:LIPIcs.FSTTCS.2018.27,
author = {Bhaskar, Umang and Ghosh, Abheek},
title = {{On the Welfare of Cardinal Voting Mechanisms}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {27:1--27:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.27},
URN = {urn:nbn:de:0030-drops-99260},
doi = {10.4230/LIPIcs.FSTTCS.2018.27},
annote = {Keywords: computational social choice, voting rules, cardinal mechanisms, price of anarchy, distortion}
}
Document
Symbolic Approximation of Weighted Timed Games
Abstract
Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the accumulated weight while reaching a target. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. For non-negative weights, the largest class that can be analysed has been introduced by Bouyer, Jaziri and Markey in 2015. Though the value problem is undecidable, the authors show how to approximate the value by considering regions with a refined granularity. In this work, we extend this class to incorporate negative weights, allowing one to model energy for instance, and prove that the value can still be approximated, with the same complexity. In addition, we show that a symbolic algorithm, relying on the paradigm of value iteration, can be used as an approximation schema on this class.
Cite as
Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Symbolic Approximation of Weighted Timed Games. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{busattogaston_et_al:LIPIcs.FSTTCS.2018.28,
author = {Busatto-Gaston, Damien and Monmege, Benjamin and Reynier, Pierre-Alain},
title = {{Symbolic Approximation of Weighted Timed Games}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {28:1--28:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.28},
URN = {urn:nbn:de:0030-drops-99277},
doi = {10.4230/LIPIcs.FSTTCS.2018.28},
annote = {Keywords: Weighted timed games, Real-time systems, Game theory, Approximation}
}
Document
A Symbolic Framework to Analyse Physical Proximity in Security Protocols
Abstract
For many modern applications like e.g., contactless payment, and keyless systems, ensuring physical proximity is a security goal of paramount importance. Formal methods have proved their usefulness when analysing standard security protocols. However, existing results and tools do not apply to e.g., distance bounding protocols that aims to ensure physical proximity between two entities. This is due in particular to the fact that existing models do not represent in a faithful way the locations of the participants, and the fact that transmission of messages takes time.
In this paper, we propose several reduction results: when looking for an attack, it is actually sufficient to consider a simple scenario involving at most four participants located at some specific locations. These reduction results allow one to use verification tools (e.g. ProVerif, Tamarin) developed for analysing more classical security properties. As an application, we analyse several distance bounding protocols, as well as a contactless payment protocol.
Cite as
Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling. A Symbolic Framework to Analyse Physical Proximity in Security Protocols. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{debant_et_al:LIPIcs.FSTTCS.2018.29,
author = {Debant, Alexandre and Delaune, St\'{e}phanie and Wiedling, Cyrille},
title = {{A Symbolic Framework to Analyse Physical Proximity in Security Protocols}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {29:1--29:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.29},
URN = {urn:nbn:de:0030-drops-99288},
doi = {10.4230/LIPIcs.FSTTCS.2018.29},
annote = {Keywords: cryptographic protocols, verification, formal methods, process algebra, Dolev-Yao model}
}
Document
On Canonical Models for Rational Functions over Infinite Words
Abstract
This paper investigates canonical transducers for rational functions over infinite words, i.e., functions of infinite words defined by finite transducers. We first consider sequential functions, defined by finite transducers with a deterministic underlying automaton. We provide a Myhill-Nerode-like characterization, in the vein of Choffrut's result over finite words, from which we derive an algorithm that computes a transducer realizing the function which is minimal and unique (up to the automaton for the domain).
The main contribution of the paper is the notion of a canonical transducer for rational functions over infinite words, extending the notion of canonical bimachine due to Reutenauer and Schützenberger from finite to infinite words. As an application, we show that the canonical transducer is aperiodic whenever the function is definable by some aperiodic transducer, or equivalently, by a first-order transduction. This allows to decide whether a rational function of infinite words is first-order definable.
Cite as
Emmanuel Filiot, Olivier Gauwin, Nathan Lhote, and Anca Muscholl. On Canonical Models for Rational Functions over Infinite Words. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{filiot_et_al:LIPIcs.FSTTCS.2018.30,
author = {Filiot, Emmanuel and Gauwin, Olivier and Lhote, Nathan and Muscholl, Anca},
title = {{On Canonical Models for Rational Functions over Infinite Words}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {30:1--30:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.30},
URN = {urn:nbn:de:0030-drops-99295},
doi = {10.4230/LIPIcs.FSTTCS.2018.30},
annote = {Keywords: transducers, infinite words, minimization, aperiodicty, first-order logic}
}
Document
Reachability for Two-Counter Machines with One Test and One Reset
Abstract
We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.
Cite as
Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for Two-Counter Machines with One Test and One Reset. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{finkel_et_al:LIPIcs.FSTTCS.2018.31,
author = {Finkel, Alain and Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
title = {{Reachability for Two-Counter Machines with One Test and One Reset}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {31:1--31:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.31},
URN = {urn:nbn:de:0030-drops-99305},
doi = {10.4230/LIPIcs.FSTTCS.2018.31},
annote = {Keywords: Counter machine, Vector addition system, Reachability problem, Formal verification, Presburger arithmetic, Infinite-state system}
}
Document
The Parikh Property for Weighted Context-Free Grammars
Abstract
Parikh's Theorem states that every context-free grammar (CFG) is equivalent to some regular CFG when the ordering of symbols in the words is ignored. The same is not true for the so-called weighted CFGs, which additionally assign a weight to each grammar rule. If the result holds for a given weighted CFG G, we say that G satisfies the Parikh property. We prove constructively that the Parikh property holds for every weighted nonexpansive CFG. We also give a decision procedure for the property when the weights are over the rationals.
Cite as
Pierre Ganty and Elena Gutiérrez. The Parikh Property for Weighted Context-Free Grammars. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{ganty_et_al:LIPIcs.FSTTCS.2018.32,
author = {Ganty, Pierre and Guti\'{e}rrez, Elena},
title = {{The Parikh Property for Weighted Context-Free Grammars}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {32:1--32:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.32},
URN = {urn:nbn:de:0030-drops-99315},
doi = {10.4230/LIPIcs.FSTTCS.2018.32},
annote = {Keywords: Weighted Context-Free Grammars, Algebraic Language Theory, Parikh Image}
}
Document
Characterizing Demand Graphs for (Fixed-Parameter) Shallow-Light Steiner Network
Abstract
We consider the Shallow-Light Steiner Network problem from a fixed-parameter perspective. Given a graph G, a distance bound L, and p pairs of vertices (s_1,t_1),...,(s_p,t_p), the objective is to find a minimum-cost subgraph G' such that s_i and t_i have distance at most L in G' (for every i in [p]). Our main result is on the fixed-parameter tractability of this problem for parameter p. We exactly characterize the demand structures that make the problem "easy", and give FPT algorithms for those cases. In all other cases, we show that the problem is W[1]-hard. We also extend our results to handle general edge lengths and costs, precisely characterizing which demands allow for good FPT approximation algorithms and which demands remain W[1]-hard even to approximate.
Cite as
Amy Babay, Michael Dinitz, and Zeyu Zhang. Characterizing Demand Graphs for (Fixed-Parameter) Shallow-Light Steiner Network. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 33:1-33:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{babay_et_al:LIPIcs.FSTTCS.2018.33,
author = {Babay, Amy and Dinitz, Michael and Zhang, Zeyu},
title = {{Characterizing Demand Graphs for (Fixed-Parameter) Shallow-Light Steiner Network}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {33:1--33:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.33},
URN = {urn:nbn:de:0030-drops-99329},
doi = {10.4230/LIPIcs.FSTTCS.2018.33},
annote = {Keywords: fixed-parameter tractable, network design, shallow-light steiner network, demand graphs}
}
Document
On the Parameterized Complexity of [1,j]-Domination Problems
Abstract
For a graph G, a set D subseteq V(G) is called a [1,j]-dominating set if every vertex in V(G) setminus D has at least one and at most j neighbors in D. A set D subseteq V(G) is called a [1,j]-total dominating set if every vertex in V(G) has at least one and at most j neighbors in D. In the [1,j]-(Total) Dominating Set problem we are given a graph G and a positive integer k. The objective is to test whether there exists a [1,j]-(total) dominating set of size at most k. The [1,j]-Dominating Set problem is known to be NP-complete, even for restricted classes of graphs such as chordal and planar graphs, but polynomial-time solvable on split graphs. The [1,2]-Total Dominating Set problem is known to be NP-complete, even for bipartite graphs. As both problems generalize the Dominating Set problem, both are W[1]-hard when parameterized by solution size. In this work, we study [1,j]-Dominating Set on sparse graph classes from the perspective of parameterized complexity and prove the following results when the problem is parameterized by solution size:
- [1,j]-Dominating Set is W[1]-hard on d-degenerate graphs for d = j + 1;
- [1,j]-Dominating Set is FPT on nowhere dense graphs.
We also prove that the known algorithm for [1,j]-Dominating Set on split graphs is optimal under the Strong Exponential Time Hypothesis (SETH). Finally, assuming SETH, we provide a lower bound for the running time of any algorithm solving the [1,2]-Total Dominating Set problem parameterized by pathwidth.
Cite as
Mohsen Alambardar Meybodi, Fedor Fomin, Amer E. Mouawad, and Fahad Panolan. On the Parameterized Complexity of [1,j]-Domination Problems. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 34:1-34:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{alambardarmeybodi_et_al:LIPIcs.FSTTCS.2018.34,
author = {Alambardar Meybodi, Mohsen and Fomin, Fedor and Mouawad, Amer E. and Panolan, Fahad},
title = {{On the Parameterized Complexity of \lbrack1,j\rbrack-Domination Problems}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {34:1--34:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.34},
URN = {urn:nbn:de:0030-drops-99330},
doi = {10.4230/LIPIcs.FSTTCS.2018.34},
annote = {Keywords: \lbrack1, j\rbrack-dominating set, parameterized complexity, sparse graphs}
}
Document
Sub-Exponential Time Parameterized Algorithms for Graph Layout Problems on Digraphs with Bounded Independence Number
Abstract
Fradkin and Seymour [Journal of Combinatorial Graph Theory, Series B, 2015] defined the class of digraphs of bounded independence number as a generalization of the class of tournaments. They argued that the class of digraphs of bounded independence number is structured enough to be exploited algorithmically. In this paper, we further strengthen this belief by showing that several cut problems that admit sub-exponential time parameterized algorithms (a trait uncommon to parameterized algorithms) on tournaments, including Directed Feedback Arc Set, Directed Cutwidth and Optimal Linear Arrangement, also admit such algorithms on digraphs of bounded independence number. Towards this, we rely on the generic approach of Fomin and Pilipczuk [ESA, 2013], where to get the desired algorithms, it is enough to bound the number of k-cuts in digraphs of bounded independence number by a sub-exponential FPT function (Fomin and Pilipczuk bounded the number of k-cuts in transitive tournaments). Specifically, our main technical contribution is that the yes-instances of the problems above have a sub-exponential number of k-cuts. We prove this bound by using a combination of chromatic coding, an inductive argument and structural properties of the digraphs.
Cite as
Pranabendu Misra, Saket Saurabh, Roohani Sharma, and Meirav Zehavi. Sub-Exponential Time Parameterized Algorithms for Graph Layout Problems on Digraphs with Bounded Independence Number. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{misra_et_al:LIPIcs.FSTTCS.2018.35,
author = {Misra, Pranabendu and Saurabh, Saket and Sharma, Roohani and Zehavi, Meirav},
title = {{Sub-Exponential Time Parameterized Algorithms for Graph Layout Problems on Digraphs with Bounded Independence Number}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {35:1--35:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.35},
URN = {urn:nbn:de:0030-drops-99341},
doi = {10.4230/LIPIcs.FSTTCS.2018.35},
annote = {Keywords: sub-exponential fixed-parameter tractable algorithms, directed feedback arc set, directed cutwidth, optimal linear arrangement, bounded independence number digraph}
}
Document
Safe and Optimal Scheduling for Hard and Soft Tasks
Abstract
We consider a stochastic scheduling problem with both hard and soft tasks on a single machine. Each task is described by a discrete probability distribution over possible execution times, and possible inter-arrival times of the job, and a fixed deadline. Soft tasks also carry a penalty cost to be paid when they miss a deadline. We ask to compute an online and non-clairvoyant scheduler (i.e. one that must take decisions without knowing the future evolution of the system) that is safe and efficient. Safety imposes that deadline of hard tasks are never violated while efficient means that we want to minimise the mean cost of missing deadlines by soft tasks.
First, we show that the dynamics of such a system can be modelled as a finite Markov Decision Process (MDP). Second, we show that our scheduling problem is PP-hard and in EXPTime. Third, we report on a prototype tool that solves our scheduling problem by relying on the Storm tool to analyse the corresponding MDP. We show how antichain techniques can be used as a potential heuristic.
Cite as
Gilles Geeraerts, Shibashis Guha, and Jean-François Raskin. Safe and Optimal Scheduling for Hard and Soft Tasks. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{geeraerts_et_al:LIPIcs.FSTTCS.2018.36,
author = {Geeraerts, Gilles and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
title = {{Safe and Optimal Scheduling for Hard and Soft Tasks}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {36:1--36:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.36},
URN = {urn:nbn:de:0030-drops-99352},
doi = {10.4230/LIPIcs.FSTTCS.2018.36},
annote = {Keywords: Non-clairvoyant scheduling, hard and soft tasks, automatic synthesis, Markov decision processes}
}
Document
The Delta-Framework
Abstract
We introduce the Delta-framework, LF_Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong proof-functional connectives take into account the shape of logical proofs, thus reflecting polymorphic features of proofs in formulae. This is in contrast to classical or intuitionistic connectives where the meaning of a compound formula depends only on the truth value or the provability of its subformulae. Our framework encompasses a wide range of type disciplines. Moreover, since relevant implication permits to express subtyping, LF_Delta subsumes also Pfenning's refinement types. We discuss the design decisions which have led us to the formulation of LF_Delta, study its metatheory, and provide various examples of applications. Our strong proof-functional type theory can be plugged in existing common proof assistants.
Cite as
Furio Honsell, Luigi Liquori, Claude Stolze, and Ivan Scagnetto. The Delta-Framework. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{honsell_et_al:LIPIcs.FSTTCS.2018.37,
author = {Honsell, Furio and Liquori, Luigi and Stolze, Claude and Scagnetto, Ivan},
title = {{The Delta-Framework}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {37:1--37:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.37},
URN = {urn:nbn:de:0030-drops-99367},
doi = {10.4230/LIPIcs.FSTTCS.2018.37},
annote = {Keywords: Logic of programs, type theory, lambda-calculus}
}
Document
Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions
Abstract
We study finite-memory (FM) determinacy in games on finite graphs, a central question for applications in controller synthesis, as FM strategies correspond to implementable controllers. We establish general conditions under which FM strategies suffice to play optimally, even in a broad multi-objective setting. We show that our framework encompasses important classes of games from the literature, and permits to go further, using a unified approach. While such an approach cannot match ad-hoc proofs with regard to tightness of memory bounds, it has two advantages: first, it gives a widely-applicable criterion for FM determinacy; second, it helps to understand the cornerstones of FM determinacy, which are often hidden but common in proofs for specific (combinations of) winning conditions.
Cite as
Stéphane Le Roux, Arno Pauly, and Mickael Randour. Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{leroux_et_al:LIPIcs.FSTTCS.2018.38,
author = {Le Roux, St\'{e}phane and Pauly, Arno and Randour, Mickael},
title = {{Extending Finite-Memory Determinacy by Boolean Combination of Winning Conditions}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {38:1--38:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.38},
URN = {urn:nbn:de:0030-drops-99373},
doi = {10.4230/LIPIcs.FSTTCS.2018.38},
annote = {Keywords: games on graphs, finite-memory determinacy, multiple objectives}
}
Document
Deterministic Algorithms for Maximum Matching on General Graphs in the Semi-Streaming Model
Abstract
We present an improved deterministic algorithm for Maximum Cardinality Matching on general graphs in the Semi-Streaming Model. In the Semi-Streaming Model, a graph is presented as a sequence of edges, and an algorithm must access the edges in the given sequence. It can only use O(n polylog n) space to perform computations, where n is the number of vertices of the graph. If the algorithm goes over the stream k times, it is called a k-pass algorithm. In this model, McGregor [McGregor, 2005] gave the currently best known randomized (1+epsilon)-approximation algorithm for maximum cardinality matching on general graphs, that uses (1/epsilon)^{O(1/epsilon)} passes. Ahn and Guha [Ahn and Guha, 2013] later gave the currently best known deterministic (1+epsilon)-approximation algorithms for maximum cardinality matching: one on bipartite graphs that uses O(log log(1/epsilon)/epsilon^2) passes, and the other on general graphs that uses O(log n *poly(1/epsilon)) passes (note that, for general graphs, the number of passes is dependent on the size of the input). We present the first deterministic algorithm that achieves a (1+epsilon)-approximation on general graphs in only a constant number ((1/epsilon)^{O(1/epsilon)}) of passes.
Cite as
Sumedh Tirodkar. Deterministic Algorithms for Maximum Matching on General Graphs in the Semi-Streaming Model. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 39:1-39:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{tirodkar:LIPIcs.FSTTCS.2018.39,
author = {Tirodkar, Sumedh},
title = {{Deterministic Algorithms for Maximum Matching on General Graphs in the Semi-Streaming Model}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {39:1--39:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.39},
URN = {urn:nbn:de:0030-drops-99383},
doi = {10.4230/LIPIcs.FSTTCS.2018.39},
annote = {Keywords: Semi Streaming, Maximum Matching}
}
Document
Sketching, Streaming, and Fine-Grained Complexity of (Weighted) LCS
Abstract
We study sketching and streaming algorithms for the Longest Common Subsequence problem (LCS) on strings of small alphabet size |Sigma|. For the problem of deciding whether the LCS of strings x,y has length at least L, we obtain a sketch size and streaming space usage of O(L^{|Sigma| - 1} log L). We also prove matching unconditional lower bounds.
As an application, we study a variant of LCS where each alphabet symbol is equipped with a weight that is given as input, and the task is to compute a common subsequence of maximum total weight. Using our sketching algorithm, we obtain an O(min{nm, n + m^{|Sigma|}})-time algorithm for this problem, on strings x,y of length n,m, with n >= m. We prove optimality of this running time up to lower order factors, assuming the Strong Exponential Time Hypothesis.
Cite as
Karl Bringmann and Bhaskar Ray Chaudhury. Sketching, Streaming, and Fine-Grained Complexity of (Weighted) LCS. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 40:1-40:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bringmann_et_al:LIPIcs.FSTTCS.2018.40,
author = {Bringmann, Karl and Chaudhury, Bhaskar Ray},
title = {{Sketching, Streaming, and Fine-Grained Complexity of (Weighted) LCS}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {40:1--40:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.40},
URN = {urn:nbn:de:0030-drops-99390},
doi = {10.4230/LIPIcs.FSTTCS.2018.40},
annote = {Keywords: algorithms, SETH, communication complexity, run-length encoding}
}
Document
On the Inner Product Predicate and a Generalization of Matching Vector Families
Abstract
Motivated by cryptographic applications such as predicate encryption, we consider the problem of representing an arbitrary predicate as the inner product predicate on two vectors. Concretely, fix a Boolean function P and some modulus q. We are interested in encoding x to x_vector and y to y_vector so that P(x,y) = 1 <=> <x_vector,y_vector> = 0 mod q, where the vectors should be as short as possible. This problem can also be viewed as a generalization of matching vector families, which corresponds to the equality predicate. Matching vector families have been used in the constructions of Ramsey graphs, private information retrieval (PIR) protocols, and more recently, secret sharing.
Our main result is a simple lower bound that allows us to show that known encodings for many predicates considered in the cryptographic literature such as greater than and threshold are essentially optimal for prime modulus q. Using this approach, we also prove lower bounds on encodings for composite q, and then show tight upper bounds for such predicates as greater than, index and disjointness.
Cite as
Balthazar Bauer, Jevgenijs Vihrovs, and Hoeteck Wee. On the Inner Product Predicate and a Generalization of Matching Vector Families. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 41:1-41:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bauer_et_al:LIPIcs.FSTTCS.2018.41,
author = {Bauer, Balthazar and Vihrovs, Jevgenijs and Wee, Hoeteck},
title = {{On the Inner Product Predicate and a Generalization of Matching Vector Families}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {41:1--41:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.41},
URN = {urn:nbn:de:0030-drops-99400},
doi = {10.4230/LIPIcs.FSTTCS.2018.41},
annote = {Keywords: Predicate Encryption, Inner Product Encoding, Matching Vector Families}
}
Document
Extending Propositional Separation Logic for Robustness Properties
Abstract
We study an extension of propositional separation logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard. As separating implication, reachability predicates (under some syntactical restrictions) and a unique quantified variable are allowed, this logic subsumes several PSpace-complete separation logics considered in previous works.
Cite as
Alessio Mansutti. Extending Propositional Separation Logic for Robustness Properties. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{mansutti:LIPIcs.FSTTCS.2018.42,
author = {Mansutti, Alessio},
title = {{Extending Propositional Separation Logic for Robustness Properties}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {42:1--42:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.42},
URN = {urn:nbn:de:0030-drops-99418},
doi = {10.4230/LIPIcs.FSTTCS.2018.42},
annote = {Keywords: Separation logic, decision problems, reachability, logics on trees, interval temporal logic, adjuncts and quantifiers elimination}
}
Document
Bundled Fragments of First-Order Modal Logic: (Un)Decidability
Abstract
Quantified modal logic is notorious for being undecidable, with very few known decidable fragments such as the monodic ones. For instance, even the two-variable fragment over unary predicates is undecidable. In this paper, we study a particular fragment, namely the bundled fragment, where a first-order quantifier is always followed by a modality when occurring in the formula, inspired by the proposal of [Yanjing Wang, 2017] in the context of non-standard epistemic logics of know-what, know-how, know-why, and so on.
As always with quantified modal logics, it makes a significant difference whether the domain stays the same across possible worlds. In particular, we show that the predicate logic with the bundle "forall Box" alone is undecidable over constant domain interpretations, even with only monadic predicates, whereas having the "exists Box" bundle instead gives us a decidable logic. On the other hand, over increasing domain interpretations, we get decidability with both "forall Box" and "exists Box" bundles with unrestricted predicates, where we obtain tableau based procedures that run in PSPACE. We further show that the "exists Box" bundle cannot distinguish between constant domain and variable domain interpretations.
Cite as
Anantha Padmanabha, R Ramanujam, and Yanjing Wang. Bundled Fragments of First-Order Modal Logic: (Un)Decidability. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 43:1-43:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{padmanabha_et_al:LIPIcs.FSTTCS.2018.43,
author = {Padmanabha, Anantha and Ramanujam, R and Wang, Yanjing},
title = {{Bundled Fragments of First-Order Modal Logic: (Un)Decidability}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {43:1--43:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.43},
URN = {urn:nbn:de:0030-drops-99424},
doi = {10.4230/LIPIcs.FSTTCS.2018.43},
annote = {Keywords: First-order modal logic, decidability, bundled fragments}
}
Document
On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems
Abstract
Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later extended to a general class of models, well-structured transition systems, and, more recently, to pushdown VASS. In this paper, we extend pushdown VASS to higher-order pushdown VASS (called HOPVASS), and we investigate whether an approach à la Karp and Miller can still be used to solve termination and boundedness. We provide a decidable characterisation of runs that can be iterated arbitrarily many times, which is the main ingredient of Karp and Miller's approach. However, the resulting Karp and Miller procedure only gives a semi-algorithm for HOPVASS. In fact, we show that coverability, termination and boundedness are all undecidable for HOPVASS, even in the restricted subcase of one counter and an order 2 stack. On the bright side, we prove that this semi-algorithm is in fact an algorithm for higher-order pushdown automata.
Cite as
Vincent Penelle, Sylvain Salvati, and Grégoire Sutre. On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 44:1-44:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{penelle_et_al:LIPIcs.FSTTCS.2018.44,
author = {Penelle, Vincent and Salvati, Sylvain and Sutre, Gr\'{e}goire},
title = {{On the Boundedness Problem for Higher-Order Pushdown Vector Addition Systems}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {44:1--44:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.44},
URN = {urn:nbn:de:0030-drops-99432},
doi = {10.4230/LIPIcs.FSTTCS.2018.44},
annote = {Keywords: Higher-order pushdown automata, Vector addition systems, Boundedness problem, Termination problem, Coverability problem}
}
Document
Stronger Tradeoffs for Orthogonal Range Querying in the Semigroup Model
Abstract
In this paper, we focus on lower bounds for data structures supporting orthogonal range querying on m points in n-dimensions in the semigroup model. Such a data structure usually maintains a family of "canonical subsets" of the given set of points and on a range query, it outputs a disjoint union of the appropriate subsets. Fredman showed that in order to prove lower bounds in the semigroup model, it suffices to prove a lower bound on a certain combinatorial tradeoff between two parameters: (a) the total sizes of the canonical subsets, and (b) the total number of canonical subsets required to cover all query ranges. In particular, he showed that the arithmetic mean of these two parameters is Omega(m log^n m). We strengthen this tradeoff by showing that the geometric mean of the same two parameters is Omega(m log^n m).
Our second result is an alternate proof of Fredman's tradeoff in the one dimensional setting. The problem of answering range queries using canonical subsets can be formulated as factoring a specific boolean matrix as a product of two boolean matrices, one representing the canonical sets and the other capturing the appropriate disjoint unions of the former to output all possible range queries. In this formulation, we can ask what is an optimal data structure, i.e., a data structure that minimizes the sum of the two parameters mentioned above, and how does the balanced binary search tree compare with this optimal data structure in the two parameters? The problem of finding an optimal data structure is a non-linear optimization problem. In one dimension, Fredman's result implies that the minimum value of the objective function is Omega(m log m), which means that at least one of the parameters has to be Omega(m log m). We show that both the parameters in an optimal solution have to be Omega(m log m). This implies that balanced binary search trees are near optimal data structures for range querying in one dimension. We derive intermediate results on factoring matrices, not necessarily boolean, while trying to minimize the norms of the factors, that may be of independent interest.
Cite as
Swaroop N. Prabhakar and Vikram Sharma. Stronger Tradeoffs for Orthogonal Range Querying in the Semigroup Model. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 45:1-45:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{n.prabhakar_et_al:LIPIcs.FSTTCS.2018.45,
author = {N. Prabhakar, Swaroop and Sharma, Vikram},
title = {{Stronger Tradeoffs for Orthogonal Range Querying in the Semigroup Model}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {45:1--45:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.45},
URN = {urn:nbn:de:0030-drops-99440},
doi = {10.4230/LIPIcs.FSTTCS.2018.45},
annote = {Keywords: range querying, lower bounds, matrix factorization, Lagrange dual function}
}
Document
Parameterized Dynamic Cluster Editing
Abstract
We introduce a dynamic version of the NP-hard Cluster Editing problem. The essential point here is to take into account dynamically evolving input graphs: Having a cluster graph (that is, a disjoint union of cliques) that represents a solution for a first input graph, can we cost-efficiently transform it into a "similar" cluster graph that is a solution for a second ("subsequent") input graph? This model is motivated by several application scenarios, including incremental clustering, the search for compromise clusterings, or also local search in graph-based data clustering. We thoroughly study six problem variants (edge editing, edge deletion, edge insertion; each combined with two distance measures between cluster graphs). We obtain both fixed-parameter tractability as well as parameterized hardness results, thus (except for two open questions) providing a fairly complete picture of the parameterized computational complexity landscape under the perhaps two most natural parameterizations: the distance of the new "similar" cluster graph to (i) the second input graph and to (ii) the input cluster graph.
Cite as
Junjie Luo, Hendrik Molter, André Nichterlein, and Rolf Niedermeier. Parameterized Dynamic Cluster Editing. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 46:1-46:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{luo_et_al:LIPIcs.FSTTCS.2018.46,
author = {Luo, Junjie and Molter, Hendrik and Nichterlein, Andr\'{e} and Niedermeier, Rolf},
title = {{Parameterized Dynamic Cluster Editing}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {46:1--46:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.46},
URN = {urn:nbn:de:0030-drops-99450},
doi = {10.4230/LIPIcs.FSTTCS.2018.46},
annote = {Keywords: graph-based data clustering, goal-oriented clustering, compromise clustering, NP-hard problems, fixed-parameter tractability, parameterized hardness}
}
Document
The Complexity of Separation for Levels in Concatenation Hierarchies
Abstract
We investigate the complexity of the separation problem associated to classes of regular languages. For a class C, C-separation takes two regular languages as input and asks whether there exists a third language in C which includes the first and is disjoint from the second. First, in contrast with the situation for the classical membership problem, we prove that for most classes C, the complexity of C-separation does not depend on how the input languages are represented: it is the same for nondeterministic finite automata and monoid morphisms. Then, we investigate specific classes belonging to finitely based concatenation hierarchies. It was recently proved that the problem is always decidable for levels 1/2 and 1 of any such hierarchy (with inefficient algorithms). Here, we build on these results to show that when the alphabet is fixed, there are polynomial time algorithms for both levels. Finally, we investigate levels 3/2 and 2 of the famous Straubing-Thérien hierarchy. We show that separation is PSpace-complete for level 3/2 and between PSpace-hard and EXPTime for level 2.
Cite as
Thomas Place and Marc Zeitoun. The Complexity of Separation for Levels in Concatenation Hierarchies. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 47:1-47:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{place_et_al:LIPIcs.FSTTCS.2018.47,
author = {Place, Thomas and Zeitoun, Marc},
title = {{The Complexity of Separation for Levels in Concatenation Hierarchies}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {47:1--47:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.47},
URN = {urn:nbn:de:0030-drops-99463},
doi = {10.4230/LIPIcs.FSTTCS.2018.47},
annote = {Keywords: Regular languages, separation, concatenation hierarchies, complexity}
}
Document
Reducing Transducer Equivalence to Register Automata Problems Solved by "Hilbert Method"
Abstract
In the past decades, classical results from algebra, including Hilbert's Basis Theorem, had various applications in formal languages, including a proof of the Ehrenfeucht Conjecture, decidability of HDT0L sequence equivalence, and decidability of the equivalence problem for functional tree-to-string transducers.
In this paper, we study the scope of the algebraic methods mentioned above, particularily as applied to the functionality problem for register automata, and equivalence for functional register automata. We provide two results, one positive, one negative. The positive result is that functionality and equivalence are decidable for MSO transformations on unordered forests. The negative result comes from a try to extend this method to decide functionality and equivalence on macro tree transducers. We reduce macro tree transducers equivalence to an equivalence problem for some class of register automata naturally relevant to our method. We then prove this latter problem to be undecidable.
Cite as
Adrien Boiret, Radoslaw Piórkowski, and Janusz Schmude. Reducing Transducer Equivalence to Register Automata Problems Solved by "Hilbert Method". In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 48:1-48:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{boiret_et_al:LIPIcs.FSTTCS.2018.48,
author = {Boiret, Adrien and Pi\'{o}rkowski, Radoslaw and Schmude, Janusz},
title = {{Reducing Transducer Equivalence to Register Automata Problems Solved by "Hilbert Method"}},
booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
pages = {48:1--48:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-093-4},
ISSN = {1868-8969},
year = {2018},
volume = {122},
editor = {Ganguly, Sumit and Pandya, Paritosh},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.48},
URN = {urn:nbn:de:0030-drops-99479},
doi = {10.4230/LIPIcs.FSTTCS.2018.48},
annote = {Keywords: formal language, Hilbert's basis theorem, transducers, register automata, equivalence problem, unordered trees, MSO transformations}
}