Volume
LIPIcs, Volume 29
34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)
Event
FSTTCS 2014, December 15-17, 2014, New Delhi, IndiaEditors
Publication Details
- published at: 2014-12-12
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-77-4
- DBLP: db/conf/fsttcs/fsttcs2014
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 29, FSTTCS'14, Complete Volume
Abstract
LIPIcs, Volume 29, FSTTCS'14, Complete Volume
Cite as
34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@Proceedings{raman_et_al:LIPIcs.FSTTCS.2014,
title = {{LIPIcs, Volume 29, FSTTCS'14, Complete Volume}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014},
URN = {urn:nbn:de:0030-drops-48795},
doi = {10.4230/LIPIcs.FSTTCS.2014},
annote = {Keywords: Software/Program Verification, Models of Computation, Modes of Computation, Complexity Measures and Classes, Nonnumerical Algorithms and Problems, Specifying and Verifying and Reasoning about Programs, Mathematical Logic, Formal Languages}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{raman_et_al:LIPIcs.FSTTCS.2014.i,
author = {Raman, Venkatesh and Suresh, S. P.},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {i--xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.i},
URN = {urn:nbn:de:0030-drops-48258},
doi = {10.4230/LIPIcs.FSTTCS.2014.i},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
New Developments in Iterated Rounding (Invited Talk)
Abstract
Iterated rounding is a relatively recent technique in algorithm design, that despite its simplicity has led to several remarkable new results and also simpler proofs of many previous results. We will briefly survey some applications of the method, including some recent developments and giving a high level overview of the ideas.
Cite as
Nikhil Bansal. New Developments in Iterated Rounding (Invited Talk). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{bansal:LIPIcs.FSTTCS.2014.1,
author = {Bansal, Nikhil},
title = {{New Developments in Iterated Rounding}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {1--10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.1},
URN = {urn:nbn:de:0030-drops-48275},
doi = {10.4230/LIPIcs.FSTTCS.2014.1},
annote = {Keywords: Algorithms, Approximation, Rounding}
}
Document
Invited Talk
Reasoning About Distributed Systems: WYSIWYG (Invited Talk)
Abstract
There are two schools of thought on reasoning about distributed systems: one following interleaving based semantics, and one following partial-order/graph based semantics. This paper compares these two approaches and argues in favour of the latter. An introductory treatment of the split-width technique is also provided.
Cite as
Aiswarya Cyriac and Paul Gastin. Reasoning About Distributed Systems: WYSIWYG (Invited Talk). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 11-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{cyriac_et_al:LIPIcs.FSTTCS.2014.11,
author = {Cyriac, Aiswarya and Gastin, Paul},
title = {{Reasoning About Distributed Systems: WYSIWYG}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {11--30},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.11},
URN = {urn:nbn:de:0030-drops-48283},
doi = {10.4230/LIPIcs.FSTTCS.2014.11},
annote = {Keywords: Verification of distributed systems, Communicating recursive programs, Partial order/graph semantics, Split-width and tree interpretation}
}
Document
Invited Talk
Colour Refinement: A Simple Partitioning Algorithm with Applications From Graph Isomorphism Testing to Machine Learning (Invited Talk)
Abstract
Colour refinement is a simple algorithm that partitions the vertices
of a graph according their "iterated degree sequence." It has very efficient implementations, running in quasilinear time, and a surprisingly wide range of applications. The algorithm has been designed in the context of graph isomorphism testing, and it is used an important subroutine in almost all practical graph isomorphism tools. Somewhat surprisingly, other applications in machine learning, probabilistic inference, and linear programming have surfaced recently.
In the first part of my talk, I will introduce the basic algorithm as well as higher dimensional extensions known as the k-dimensional Weisfeiler-Lehman algorithm. I will also discuss an unexpected connection between colour refinement and a natural linear programming approach to graph isomorphism testing. In the second part of my talk, I will discuss various applications of colour refinement.
Cite as
Martin Grohe. Colour Refinement: A Simple Partitioning Algorithm with Applications From Graph Isomorphism Testing to Machine Learning (Invited Talk). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, p. 31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{grohe:LIPIcs.FSTTCS.2014.31,
author = {Grohe, Martin},
title = {{Colour Refinement: A Simple Partitioning Algorithm with Applications From Graph Isomorphism Testing to Machine Learning}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {31--31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.31},
URN = {urn:nbn:de:0030-drops-48290},
doi = {10.4230/LIPIcs.FSTTCS.2014.31},
annote = {Keywords: Color Refinement, Graph Isomorphism, Machine Learning}
}
Document
Invited Talk
Properties and Utilization of Capacitated Automata (Invited Talk)
Abstract
We study capacitated automata(CAs), where transitions correspond to resources and may have bounded capacities. Each transition in a CA is associated with a (possibly infinite) bound on the number of times it may be traversed. We study CAs from two points of view. The first is that of traditional automata theory, where we view CAs as recognizers of formal languages and examine their expressive power, succinctness, and determinization. The second is that of resource-allocation theory, where we view CAs as a rich description of a flow network and study their utilization.
Cite as
Orna Kupferman and Tami Tamir. Properties and Utilization of Capacitated Automata (Invited Talk). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 33-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{kupferman_et_al:LIPIcs.FSTTCS.2014.33,
author = {Kupferman, Orna and Tamir, Tami},
title = {{Properties and Utilization of Capacitated Automata}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {33--44},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.33},
URN = {urn:nbn:de:0030-drops-48306},
doi = {10.4230/LIPIcs.FSTTCS.2014.33},
annote = {Keywords: Automata, Capacitated transitions, Determinization, Maximum utilization}
}
Document
Invited Talk
Algorithms, Games, and Evolution (Invited Talk)
Abstract
Even the most seasoned students of evolution, starting with Darwin himself, have occasionally expressed amazement at the fact that the mechanism of natural selection has produced the whole of Life as we see it around us. From a computational perspective, it is natural to marvel at evolution's solution to the problems of robotics, vision and theorem proving! What, then, is the complexity of evolution, viewed as an algorithm? One answer to this question is 10^{12}, roughly the number of sequential steps or generations from the earliest single celled creatures to today's Homo Sapiens. To put this into perspective, the processor of a modern cell phone can perform 10^{12} steps in less than an hour. Another answer is 10^30, the degree of parallelism, roughly the maximum number of organisms living on the Earth at any time. Perhaps the answer should be the product of the two numbers, roughly 10^42, to reflect the total work done by evolution, viewed as a parallel algorithm.
Here we argue, interpreting our recently published paper, that none of the above answers is really correct. Viewing evolution as an algorithm poses an additional challenge: recombination. Even if evolution succeeds in producing a particularly good solution (a highly fit individual), its offspring would only inherit half its genes, and therefore appear unlikely to be a good solution. This is the core of the problem of explaining the role of sex in evolution, known as the "queen of problems in evolutionary biology".
The starting point is the diffusion-equation-based approach of theoretical population geneticists, who analyze the changing allele frequencies (over the generations) in the gene pool, consisting of the aggregate of the genetic variants (or "alleles") over all genes (or "loci") and over all individuals in a species. Taking this viewpoint to its logical conclusion, rather than acting on individuals or species or genes, evolution acts on this gene pool, or genetic soup, by making it more "potent", in the sense that it increases the expected fitness of genotype drawn randomly from this soup. Moreover, for much genetic variation, this soup may be assumed to be in the regime of weak selection, a regime where the probability of occurrence of a certain genotype involving various alleles at different loci is simply the product of the probabilities of each of its alleles. In this regime, we show that evolution in the regime of weak selection can be formulated as a game, where the recombining loci are the players, the alleles in those loci are possible moves or actions of each player, and the expected payoff of each player-locus is precisely the organism's expected fitness across the genotypes that are present in the population. Moreover, the dynamics specified by the diffusion equations of theoretical population geneticists is closely approximated by the dynamics of multiplicative weight updates (MWUA).
The algorithmic connection to MWUA brings with it new insights for evolutionary biology, specifically, into the question of how genetic diversity is maintained in the presence of natural selection. For this it is useful to consider a dual view of MWUA, which expresses "what each gene is optimizing" as it plays the game. Remarkably this turns out to be a particular convex combination of the entropy of its distribution over alleles and cumulative expected fitness. This sheds new light on the maintenance of diversity in evolution.
All of this suggests that the complexity of evolution should indeed be viewed as 10^12, but for a subtle reason. It is the number of steps of multiplicative weight updates carried out on allele frequencies in the genetic soup. A closer examination of this reveals further that the accurate tracking of allele frequencies over the generations requires the simulation of a quadratic dynamical system (two parents for each offspring). Moreover the simulation of even simple quadratic dynamical systems is known to be PSPACE-hard. This suggests that the tracking of allele frequencies might require large population sizes for each species, putting into perspective the number 10^30. Finally, it is worth noting that in this view there is a primacy to recombination or sex, which serve to provide robustness to the mechanism of evolution, as well as the framework within which MWUA operates.
Cite as
Erick Chastain, Adi Livnat, Christos H. Papadimitriou, and Umesh V. Vazirani. Algorithms, Games, and Evolution (Invited Talk). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 45-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{chastain_et_al:LIPIcs.FSTTCS.2014.45,
author = {Chastain, Erick and Livnat, Adi and Papadimitriou, Christos H. and Vazirani, Umesh V.},
title = {{Algorithms, Games, and Evolution}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {45--46},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.45},
URN = {urn:nbn:de:0030-drops-48310},
doi = {10.4230/LIPIcs.FSTTCS.2014.45},
annote = {Keywords: evolution, recombination, coordination games, multiplicative weight updates}
}
Document
Invited Talk
The Polynomial Method in Circuit Complexity Applied to Algorithm Design (Invited Talk)
Abstract
In circuit complexity, the polynomial method is a general approach to proving circuit lower bounds in restricted settings. One shows that functions computed by sufficiently restricted circuits are "correlated" in some way with a low-complexity polynomial, where complexity may be measured by the degree of the polynomial or the number of monomials. Then, results limiting the capabilities of low-complexity polynomials are extended to the restricted circuits.
Old theorems proved by this method have recently found interesting applications to the design of algorithms for basic problems in the theory of computing. This paper surveys some of these applications, and gives a few new ones.
Cite as
Richard Ryan Williams. The Polynomial Method in Circuit Complexity Applied to Algorithm Design (Invited Talk). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 47-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{williams:LIPIcs.FSTTCS.2014.47,
author = {Williams, Richard Ryan},
title = {{The Polynomial Method in Circuit Complexity Applied to Algorithm Design}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {47--60},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.47},
URN = {urn:nbn:de:0030-drops-48328},
doi = {10.4230/LIPIcs.FSTTCS.2014.47},
annote = {Keywords: algorithm design, circuit complexity, polynomial method}
}
Document
Vertex Exponential Algorithms for Connected f-Factors
Abstract
Given a graph G and a function f:V(G) -> [V(G)], an f-factor is a subgraph H of G such that deg_H(v)=f(v) for every vertex v in V(G); we say that H is a connected f-factor if, in addition, the subgraph H is connected. Tutte (1954) showed that one can check whether a given graph has a specified f-factor in polynomial time. However, detecting a connected f-factor is NP-complete, even when f is a constant function - a foremost example is the problem of checking whether a graph has a Hamiltonian cycle; here f is a function which maps every vertex to 2. The current best algorithm for this latter problem is due to Björklund (FOCS 2010), and runs in randomized O^*(1.657^n) time (the O^*() notation hides polynomial factors). This was the first superpolynomial improvement, in nearly fifty years, over the previous best algorithm of Bellman, Held and Karp (1962) which checks for a Hamiltonian cycle in deterministic O(2^n*n^2) time.
In this paper we present the first vertex-exponential algorithms for the more general problem of finding a connected f-factor. Our first result is a randomized algorithm which, given a graph G on n vertices and a function f:V(G) -> [n], checks whether G has a connected f-factor in O^*(2^n) time. We then extend our result to the case when f is a mapping from V(G) to {0,1} and the degree of every vertex v in the subgraph H is required to be f(v)(mod 2). This generalizes the problem of checking whether a graph has an Eulerian subgraph; this is a connected subgraph whose degrees are all even (f(v) equiv 0). Furthermore, we show that the min-cost editing and edge-weighted versions of these problems can be solved in randomized O^*(2^n) time as long as the costs/weights are bounded polynomially in n.
Cite as
Geevarghese Philip and M. S. Ramanujan. Vertex Exponential Algorithms for Connected f-Factors. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 61-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{philip_et_al:LIPIcs.FSTTCS.2014.61,
author = {Philip, Geevarghese and Ramanujan, M. S.},
title = {{Vertex Exponential Algorithms for Connected f-Factors}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {61--71},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.61},
URN = {urn:nbn:de:0030-drops-48337},
doi = {10.4230/LIPIcs.FSTTCS.2014.61},
annote = {Keywords: Exact Exponential Time Algorithms, f-Factors}
}
Document
Connecting Vertices by Independent Trees
Abstract
We study the paramereteized complexity of the following connectivity problem. For a vertex subset U of a graph G, trees T_1,...,T_s of G are completely independent spanning trees of U if each of them contains U, and for every two distinct vertices u,v in U, the paths from u to v in T_1,...,T_s are pairwise vertex disjoint except for end-vertices u and v. Then for a given s >= 2 and a parameter k, the task is to decide if a given n-vertex graph G contains a set U of size at least k such that there are s completely independent spanning trees of U. The problem is known to be NP-complete already for s=2. We prove the following results: (*) For s=2 the problem is solvable in time 2^{O(k)}*n^{O(1)}. (*) For s=2 the problem does not admit a polynomial kernel unless NP subseteq coNP/poly. (*) For arbitrary s, we show that the problem is solvable in time f(s,k)n^{O(1)} for some function f of s and k only.
Cite as
Manu Basavaraju, Fedor V. Fomin, Petr A. Golovach, and Saket Saurabh. Connecting Vertices by Independent Trees. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 73-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{basavaraju_et_al:LIPIcs.FSTTCS.2014.73,
author = {Basavaraju, Manu and Fomin, Fedor V. and Golovach, Petr A. and Saurabh, Saket},
title = {{Connecting Vertices by Independent Trees}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {73--84},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.73},
URN = {urn:nbn:de:0030-drops-48340},
doi = {10.4230/LIPIcs.FSTTCS.2014.73},
annote = {Keywords: Parameterized complexity, FPT-algorithms, completely independent spanning trees}
}
Document
Tree Deletion Set Has a Polynomial Kernel (but no OPT^O(1) Approximation)
Abstract
In the Tree Deletion Set problem the input is a graph G together with an integer k. The objective is to determine whether there exists a set S of at most k vertices such that G \ S is a tree. The problem is NP-complete and even NP-hard to approximate within any factor of OPT^c for any constant c. In this paper we give an O(k^5) size kernel for the Tree Deletion Set problem. An appealing feature of our kernelization algorithm is a new reduction rule, based on system of linear equations, that we use to handle the instances on which Tree Deletion Set is hard to approximate.
Cite as
Archontia C. Giannopoulou, Daniel Lokshtanov, Saket Saurabh, and Ondrej Suchy. Tree Deletion Set Has a Polynomial Kernel (but no OPT^O(1) Approximation). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 85-96, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{giannopoulou_et_al:LIPIcs.FSTTCS.2014.85,
author = {Giannopoulou, Archontia C. and Lokshtanov, Daniel and Saurabh, Saket and Suchy, Ondrej},
title = {{Tree Deletion Set Has a Polynomial Kernel (but no OPT^O(1) Approximation)}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {85--96},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.85},
URN = {urn:nbn:de:0030-drops-48261},
doi = {10.4230/LIPIcs.FSTTCS.2014.85},
annote = {Keywords: Tree Deletion Set, Feedback Vertex Set, Kernelization, Linear Equations}
}
Document
Editing to Eulerian Graphs
Abstract
We investigate the problem of modifying a graph into a connected graph in which the degree of each vertex satisfies a prescribed parity constraint. Let ea, ed and vd denote the operations edge addition, edge deletion and vertex deletion respectively. For any S subseteq {ea,ed,vd}, we define Connected Degree Parity Editing (S) (CDPE(S)) to be the problem that takes as input a graph G, an integer k and a function delta: V(G) -> {0,1}, and asks whether G can be modified into a connected graph H with d_H(v) = delta(v)(mod 2) for each v in V(H), using at most k operations from S. We prove that (*) if S={ea} or S={ea,ed}, then CDPE(S) can be solved in polynomial time; (*) if {vd} subseteq S subseteq {ea,ed,vd}, then CDPE(S) is NP-complete and W-hard when parameterized by k, even if delta = 0.
Together with known results by Cai and Yang and by Cygan, Marx, Pilipczuk, Pilipczuk and Schlotter, our results completely classify the classical and parameterized complexity of the CDPE(S) problem for all S subseteq {ea,ed,vd}. We obtain the same classification for a natural variant of the cdpe(S) problem on directed graphs, where the target is a weakly connected digraph in which the difference between the in- and out-degree of every vertex equals a prescribed value.
As an important implication of our results, we obtain polynomial-time algorithms for Eulerian Editing problem and its directed variant. To the best of our knowledge, the only other natural non-trivial graph class H for which the H-Editing problem is known to be polynomial-time solvable is the class of split graphs.
Cite as
Konrad K. Dabrowski, Petr A. Golovach, Pim van 't Hof, and Daniel Paulusma. Editing to Eulerian Graphs. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 97-108, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{dabrowski_et_al:LIPIcs.FSTTCS.2014.97,
author = {Dabrowski, Konrad K. and Golovach, Petr A. and van 't Hof, Pim and Paulusma, Daniel},
title = {{Editing to Eulerian Graphs}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {97--108},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.97},
URN = {urn:nbn:de:0030-drops-48356},
doi = {10.4230/LIPIcs.FSTTCS.2014.97},
annote = {Keywords: Eulerian graphs, graph editing, polynomial algorithm}
}
Document
Parameterized Complexity of Fixed Variable Logics
Abstract
We study the complexity of model checking formulas in first-order logic parameterized by the number of distinct variables in the formula. This problem, which is not known to be fixed-parameter tractable, resisted to be properly classified in the context of parameterized complexity. We show that it is complete for a newly-defined complexity class that we propose as an analog of the classical class PSPACE in parameterized complexity. We support this intuition by the following findings: First, the proposed class admits a definition in terms of alternating Turing machines in a similar way as PSPACE can be defined in terms of polynomial-time alternating machines. Second, we show that parameterized versions of other PSPACE-complete problems, like winning certain pebble games and finding restricted resolution refutations, are complete for this class.
Cite as
Christoph Berkholz and Michael Elberfeld. Parameterized Complexity of Fixed Variable Logics. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 109-120, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{berkholz_et_al:LIPIcs.FSTTCS.2014.109,
author = {Berkholz, Christoph and Elberfeld, Michael},
title = {{Parameterized Complexity of Fixed Variable Logics}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {109--120},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.109},
URN = {urn:nbn:de:0030-drops-48367},
doi = {10.4230/LIPIcs.FSTTCS.2014.109},
annote = {Keywords: Parameterized complexity, polynomial space, first-order logic, pebble games, regular resolutions}
}
Document
Synchronizing Words for Weighted and Timed Automata
Abstract
The problem of synchronizing automata is concerned with the existence of a word that sends all states of the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete.
In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.
Cite as
Laurent Doyen, Line Juhl, Kim G. Larsen, Nicolas Markey, and Mahsa Shirmohammadi. Synchronizing Words for Weighted and Timed Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 121-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{doyen_et_al:LIPIcs.FSTTCS.2014.121,
author = {Doyen, Laurent and Juhl, Line and Larsen, Kim G. and Markey, Nicolas and Shirmohammadi, Mahsa},
title = {{Synchronizing Words for Weighted and Timed Automata}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {121--132},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.121},
URN = {urn:nbn:de:0030-drops-48370},
doi = {10.4230/LIPIcs.FSTTCS.2014.121},
annote = {Keywords: Synchronizing words, weighted automata, timed automata}
}
Document
Finite-Valued Weighted Automata
Abstract
Any weighted automaton (WA) defines a relation from finite words to values: given an input word, its set of values is obtained as the set of values computed by each accepting run on that word. A WA is k-valued if the relation it defines has degree at most k, i.e., every set of values associated with an input word has cardinality at most k. We investigate the class of quantitative languages defined by k-valued automata, for all parameters k. We consider several measures to associate values with runs: sum, discounted-sum, and more generally values in groups.
We define a general procedure which decides, given a bound k and a WA over a group, whether this automaton is k-valued. We also show that any k-valued WA over a group, under some general conditions, can be decomposed as a union of k unambiguous WA. While inclusion and equivalence are undecidable problems for arbitrary sum-automata, we show, based on this decomposition, that they are decidable for k-valued sum-automata, and k-valued discounted sum-automata over inverted integer discount factors. We finally show that the quantitative Church problem is undecidable for k-valued sum-automata, even given as finite unions of deterministic sum-automata.
Cite as
Emmanuel Filiot, Raffaella Gentilini, and Jean-Francois Raskin. Finite-Valued Weighted Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 133-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{filiot_et_al:LIPIcs.FSTTCS.2014.133,
author = {Filiot, Emmanuel and Gentilini, Raffaella and Raskin, Jean-Francois},
title = {{Finite-Valued Weighted Automata}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {133--145},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.133},
URN = {urn:nbn:de:0030-drops-48388},
doi = {10.4230/LIPIcs.FSTTCS.2014.133},
annote = {Keywords: Nested word, Transducer, Streaming}
}
Document
First-order Definable String Transformations
Abstract
The connection between languages defined by computational models and logic for languages is well-studied. Monadic second-order logic and finite automata are shown to closely correspond to each-other for the languages of strings, trees, and partial-orders. Similar connections are shown for first-order logic and finite automata with certain aperiodicity restriction. Courcelle in 1994 proposed a way to use logic to define functions over structures where the output structure is defined using logical formulas interpreted over the input structure. Engelfriet and Hoogeboom discovered the corresponding "automata connection" by showing that two-way generalised sequential machines capture the class of monadic-second order definable transformations. Alur and Cerny further refined the result by proposing a one-way deterministic transducer model with string variables - called the streaming string transducers - to capture the same class of transformations. In this paper we establish a transducer-logic correspondence for Courcelle's first-order definable string transformations. We propose a new notion of transition monoid for streaming string transducers that involves structural properties of both underlying input automata and variable dependencies. By putting an aperiodicity restriction on the transition monoids, we define a class of streaming string transducers that captures exactly the class of first-order definable transformations.
Cite as
Emmanuel Filiot, Shankara Narayanan Krishna, and Ashutosh Trivedi. First-order Definable String Transformations. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 147-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{filiot_et_al:LIPIcs.FSTTCS.2014.147,
author = {Filiot, Emmanuel and Krishna, Shankara Narayanan and Trivedi, Ashutosh},
title = {{First-order Definable String Transformations}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {147--159},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.147},
URN = {urn:nbn:de:0030-drops-48393},
doi = {10.4230/LIPIcs.FSTTCS.2014.147},
annote = {Keywords: First-order logic, streaming string transducers}
}
Document
Regular Sensing
Abstract
The size of deterministic automata required for recognizing regular and omega-regular languages is a well-studied measure for the complexity of languages. We introduce and study a new complexity measure, based on the sensing required for recognizing the language. Intuitively, the sensing cost quantifies the detail in which a random input word has to be read in order to decide its membership in the language. We show that for finite words, size and sensing are related, and minimal sensing is attained by minimal automata. Thus, a unique minimal-sensing deterministic automaton exists, and is based on the language's right-congruence relation. For infinite words, the minimal sensing may be attained only by an infinite sequence of automata. We show that the optimal limit cost of such sequences can be characterized by the language's right-congruence relation, which enables us to find the sensing cost of omega-regular languages in polynomial time.
Cite as
Shaull Almagor, Denis Kuperberg, and Orna Kupferman. Regular Sensing. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 161-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.FSTTCS.2014.161,
author = {Almagor, Shaull and Kuperberg, Denis and Kupferman, Orna},
title = {{Regular Sensing}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {161--173},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.161},
URN = {urn:nbn:de:0030-drops-48409},
doi = {10.4230/LIPIcs.FSTTCS.2014.161},
annote = {Keywords: Automata, regular languages, omega-regular languages, complexity, sensing, minimization}
}
Document
Symbolic Solving of Extended Regular Expression Inequalities
Abstract
This paper presents a new algorithm for the containment problem for extended regular expressions that contain intersection and complement operators and that range over infinite alphabets. The algorithm solves extended regular expressions inequalities symbolically by term rewriting and thus avoids the translation to an expression-equivalent automaton.
Our algorithm is based on Brzozowski's regular expression derivatives and on Antimirov's term-rewriting approach to check containment. To deal with large or infinite alphabets effectively, we generalize Brzozowski's derivative operator to work with respect to (potentially infinite) representable character sets.
Cite as
Matthias Keil and Peter Thiemann. Symbolic Solving of Extended Regular Expression Inequalities. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 175-186, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{keil_et_al:LIPIcs.FSTTCS.2014.175,
author = {Keil, Matthias and Thiemann, Peter},
title = {{Symbolic Solving of Extended Regular Expression Inequalities}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {175--186},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.175},
URN = {urn:nbn:de:0030-drops-48411},
doi = {10.4230/LIPIcs.FSTTCS.2014.175},
annote = {Keywords: Extended regular expression, containment, infinite alphabet, infinite character set, effective boolean algebra}
}
Document
Solving the Stable Set Problem in Terms of the Odd Cycle Packing Number
Abstract
The classic stable set problem asks to find a maximum cardinality set of pairwise non-adjacent vertices in an undirected graph G. This problem is NP-hard to approximate with factor n^{1-epsilon} for any constant epsilon>0 [Hastad/Acta Mathematica/1996; Zuckerman/STOC/2006], where n is the number of vertices, and therefore there is no hope for good approximations in the general case. We study the stable set problem when restricted to graphs with bounded odd cycle packing number ocp(G), possibly by a function of n. This is the largest number of vertex-disjoint odd cycles in G. Equivalently, it is the logarithm of the largest absolute value of a sub-determinant of the edge-node incidence matrix A_G of G. Hence, if A_G is totally unimodular, then ocp(G)=0. Therefore, ocp(G) is a natural distance measure of A_G to the set of totally unimodular matrices on a scale from 1 to n/3.
When ocp(G)=0, the graph is bipartite and it is well known that stable set can be solved in polynomial time. Our results imply that the odd cycle packing number indeed strongly influences the approximability of stable set. More precisely, we obtain a polynomial-time approximation scheme for graphs with ocp(G)=o(n/log(n)), and an alpha-approximation algorithm for any graph where alpha smoothly increases from a constant to n as ocp(G) grows from O(n/log(n)) to n/3. On the hardness side, we show that, assuming the exponential-time hypothesis, stable set cannot be solved in polynomial time if ocp(G)=Omega(log^{1+epsilon}(n)) for some epsilon>0. Finally, we generalize a theorem by Györi et al. [Györi et al./Discrete Mathematics/1997] and show that graphs without odd cycles of small weight can be made bipartite by removing a small number of vertices. This allows us to extend some of our above results to the weighted stable set problem.
Cite as
Adrian Bock, Yuri Faenza, Carsten Moldenhauer, and Andres Jacinto Ruiz-Vargas. Solving the Stable Set Problem in Terms of the Odd Cycle Packing Number. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 187-198, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{bock_et_al:LIPIcs.FSTTCS.2014.187,
author = {Bock, Adrian and Faenza, Yuri and Moldenhauer, Carsten and Ruiz-Vargas, Andres Jacinto},
title = {{Solving the Stable Set Problem in Terms of the Odd Cycle Packing Number}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {187--198},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.187},
URN = {urn:nbn:de:0030-drops-48422},
doi = {10.4230/LIPIcs.FSTTCS.2014.187},
annote = {Keywords: stable set problem, independent set problem, approximation algorithms, odd cycle packing number, maximum subdeterminants}
}
Document
Lift & Project Systems Performing on the Partial Vertex Cover Polytope
Abstract
We study integrality gap (IG) lower bounds on strong LP and SDP relaxations derived by the Sherali-Adams (SA), Lovász-Schrijver-SDP (LS_+), and Sherali-Adams-SDP (SA_+) lift-and-project (L&P) systems for the t-Partial-Vertex-Cover (t-PVC) problem, a variation of the classic Vertex-Cover problem in which only t edges need to be covered. t-PVC admits a 2-approximation using various algorithmic techniques, all relying on a natural LP relaxation. Starting from this LP relaxation, our main results assert that for every epsilon>0, level-Theta(n) LPs or SDPs derived by all known L&P systems that have been used for positive algorithmic results (but the Lasserre hierarchy) have IGs at least (1-epsilon)n/t, where n is the number of vertices of the input graph. Our lower bounds are nearly tight, in that level-n relaxations, even of the weakest systems, have integrality gap 1.
As lift-and-project systems have given the best algorithms known for numerous combinatorial optimization problems, our results show that restricted yet powerful models of computation derived by many L&P systems fail to witness c-approximate solutions to t-PVC for any constant c, and for t=O(n). This is one of the very few known examples of an intractable combinatorial optimization problem for which LP-based algorithms induce a constant approximation ratio, still lift-and-project LP and SDP tightenings of the same LP have unbounded IGs.
As further motivation for our results, we show that the SDP that has given the best algorithm known for t-PVC has integrality gap n/t on instances that can be solved by the level-1 LP relaxation derived by the LS system. This constitutes another rare phenomenon where (even in specific instances) a static LP outperforms an SDP that has been used for the best approximation guarantee for the problem at hand.
Finally, we believe our results are of independent interest as they are among the very few known integrality gap lower bounds for LP and SDP 0-1 relaxations in which not all variables possess the same semantics in the underlying combinatorial optimization problem. Most importantly, one of our main contributions is that we make explicit of a new and simple methodology of constructing solutions to LP relaxations that almost trivially satisfy constraints derived by all SDP L&P systems known to be useful for algorithmic positive results (except the La system). The latter sheds some light as to why La tightenings seem strictly stronger than LS_+ or SA_+ tightenings.
Cite as
Konstantinos Georgiou and Edward Lee. Lift & Project Systems Performing on the Partial Vertex Cover Polytope. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 199-211, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{georgiou_et_al:LIPIcs.FSTTCS.2014.199,
author = {Georgiou, Konstantinos and Lee, Edward},
title = {{Lift \& Project Systems Performing on the Partial Vertex Cover Polytope}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {199--211},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.199},
URN = {urn:nbn:de:0030-drops-48437},
doi = {10.4230/LIPIcs.FSTTCS.2014.199},
annote = {Keywords: Partial vertex cover, combinatorial optimization, linear programming, semidefinite programming, lift and project systems, integrality gaps}
}
Document
Replica Placement on Directed Acyclic Graphs
Abstract
The replica placement problem has been well studied on trees. In this paper, we study this problem on directed acyclic graphs. The replica placement problem on general DAGs generalizes the set cover problem. We present a constant factor approximation algorithm for the special case of DAGs having bounded degree and bounded tree-width (BDBT-DAGs). We also present a constant factor approximation algorithm for DAGs composed of local BDBT-DAGs connected in a tree like manner (TBDBT-DAGs). The latter class of DAGs generalizes trees as well; we improve upon the previously best known approximation ratio for the problem on trees. Our algorithms are based on the LP rounding technique; the core component of our algorithm exploits the structural properties of tree-decompositions to massage the LP solution into an integral solution.
Cite as
Sonika Arora, Venkatesan T. Chakaravarthy, Kanika Gupta, Neelima Gupta, and Yogish Sabharwal. Replica Placement on Directed Acyclic Graphs. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 213-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{arora_et_al:LIPIcs.FSTTCS.2014.213,
author = {Arora, Sonika and Chakaravarthy, Venkatesan T. and Gupta, Kanika and Gupta, Neelima and Sabharwal, Yogish},
title = {{Replica Placement on Directed Acyclic Graphs}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {213--225},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.213},
URN = {urn:nbn:de:0030-drops-48449},
doi = {10.4230/LIPIcs.FSTTCS.2014.213},
annote = {Keywords: Approximation Algorithms, LP Rounding}
}
Document
Maintaining Approximate Maximum Matching in an Incremental Bipartite Graph in Polylogarithmic Update Time
Abstract
A sparse subgraph G' of G is called a matching sparsifier if the size or weight of matching in G' is approximately equal to the size or weight of maximum matching in G. Recently, algorithms have been developed to find matching sparsifiers in a static bipartite graph. In this paper, we show that we can find matching sparsifier even in an incremental bipartite graph.
This observation leads to following results: 1. We design an algorithm that maintains a (1+epsilon) approximate matching in an incremental bipartite graph in O(log^2(n) / (epsilon^{4}) update time. 2. For weighted graphs, we design an algorithm that maintains (1+epsilon) approximate weighted matching in O((log(n)*log(n*N)) / (epsilon^4) update time where \maxweight is the maximum weight of any edge in the graph.
Cite as
Manoj Gupta. Maintaining Approximate Maximum Matching in an Incremental Bipartite Graph in Polylogarithmic Update Time. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 227-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{gupta:LIPIcs.FSTTCS.2014.227,
author = {Gupta, Manoj},
title = {{Maintaining Approximate Maximum Matching in an Incremental Bipartite Graph in Polylogarithmic Update Time}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {227--239},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.227},
URN = {urn:nbn:de:0030-drops-48453},
doi = {10.4230/LIPIcs.FSTTCS.2014.227},
annote = {Keywords: Graph Algorithm, Dynamic Graph}
}
Document
The Complexity of Counting Models of Linear-time Temporal Logic
Abstract
We determine the complexity of counting models of bounded size of specifications expressed in Linear-time Temporal Logic. Counting word-models is #P-complete, if the bound is given in unary, and as hard as counting accepting runs of nondeterministic polynomial space Turing machines, if the bound is given in binary. Counting tree-models is as hard as counting accepting runs of nondeterministic exponential time Turing machines, if the bound is given in unary. For a binary encoding of the bound, the problem is at least as hard as counting accepting runs of nondeterministic exponential space Turing machines. On the other hand, it is not harder than counting accepting runs of nondeterministic doubly-exponential time Turing machines.
Cite as
Hazem Torfah and Martin Zimmermann. The Complexity of Counting Models of Linear-time Temporal Logic. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 241-252, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{torfah_et_al:LIPIcs.FSTTCS.2014.241,
author = {Torfah, Hazem and Zimmermann, Martin},
title = {{The Complexity of Counting Models of Linear-time Temporal Logic}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {241--252},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.241},
URN = {urn:nbn:de:0030-drops-48463},
doi = {10.4230/LIPIcs.FSTTCS.2014.241},
annote = {Keywords: Model Counting, Temporal Logic, Model Checking, Counting Complexity}
}
Document
Extending Temporal Logics with Data Variable Quantifications
Abstract
Although data values are available in almost every computer system, reasoning about them is a challenging task due to the huge data size or even infinite data domains. Temporal logics are the well-known specification formalisms for reactive and concurrent systems. Various extensions of temporal logics have been proposed to reason about data values, mostly in the last decade. Among them, one natural idea is to extend temporal logics with variable quantifications ranging over an infinite data domain. In this paper, we focus on the variable extensions of two widely used temporal logics, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Grumberg, Kupferman and Sheinvald recently investigated the extension of LTL with variable quantifications. They defined the extension as formulas in the prenex normal form, that is, all the variable quantifications precede the LTL formulas. Our goal in this paper is to do a relatively complete investigation on this topic. For this purpose, we define the extensions of LTL and CTL by allowing arbitrary nestings of variable quantifications, Boolean and temporal operators (the resulting logics are called respectively variable-LTL, in brief VLTL, and variable-CTL, in brief VCTL), and identify the decidability frontiers of both the satisfiability and model checking problem. In particular, we obtain the following results: 1) Existential variable quantifiers or one single universal quantifier in the beginning already entails undecidability for the satisfiability problem of both VLTL and VCTL, 2) If only existential path quantifiers are used in VCTL, then the satisfiability problem is decidable, no matter which variable quantifiers are available. 3) For VLTL formulas with one single universal variable quantifier in the beginning, if the occurrences of the non-parameterized atomic propositions are guarded by the positive occurrences of the quantified variable, then its satisfiability problem becomes decidable. Based on these results of the satisfiability problem, we deduce the (un)decidability results of the model checking problem.
Cite as
Fu Song and Zhilin Wu. Extending Temporal Logics with Data Variable Quantifications. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 253-265, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{song_et_al:LIPIcs.FSTTCS.2014.253,
author = {Song, Fu and Wu, Zhilin},
title = {{Extending Temporal Logics with Data Variable Quantifications}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {253--265},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.253},
URN = {urn:nbn:de:0030-drops-48475},
doi = {10.4230/LIPIcs.FSTTCS.2014.253},
annote = {Keywords: Temporal logics with variable quantifications, satisfiability and model checking, alternating register automata, data automata}
}
Document
Generalized Data Automata and Fixpoint Logic
Abstract
Data omega-words are omega-words where each position is additionally labelled by a data value from an infinite alphabet. They can be seen as graphs equipped with two sorts of edges: "next position" and "next position with the same data value". Based on this view, an extension of Data Automata called Generalized Data Automata (GDA) is introduced. While the decidability of emptiness of GDA is open, the decidability for a subclass class called Büchi GDA is shown using Multicounter Automata. Next a natural fixpoint logic is defined on the graphs of data omega-words and it is shown that the mu-fragment as well as the alternation-free fragment is undecidable. But the fragment which is defined by limiting the number of alternations between future and past formulas is shown to be decidable, by first converting the formulas to equivalent alternating Büchi automata and then to Büchi GDA.
Cite as
Thomas Colcombet and Amaldev Manuel. Generalized Data Automata and Fixpoint Logic. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 267-278, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2014.267,
author = {Colcombet, Thomas and Manuel, Amaldev},
title = {{Generalized Data Automata and Fixpoint Logic}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {267--278},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.267},
URN = {urn:nbn:de:0030-drops-48483},
doi = {10.4230/LIPIcs.FSTTCS.2014.267},
annote = {Keywords: Data words, Data Automata, Decidability, Fixpoint Logic}
}
Document
Consistency of Injective Tree Patterns
Abstract
Testing if an incomplete description of an XML document is consistent, that is, if it describes a real document conforming to the imposed schema, amounts to deciding if a given tree pattern can be matched injectively into a tree accepted by a fixed automaton. This problem can be solved in polynomial time for patterns that use the child relation and the sibling order, but do not use the descendant relation. For general patterns the problem is in NP, but no lower bound has been known so far. We show that the problem is NP-complete already for patterns using only child and descendant relations. The source of hardness turns out to be the interplay between these relations: for patterns using only descendant we give a polynomial algorithm. We also show that the algorithm can be adapted to patterns using descendant and following-sibling, but combining descendant and next-sibling leads to intractability.
Cite as
Claire David, Nadime Francis, and Filip Murlak. Consistency of Injective Tree Patterns. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 279-290, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{david_et_al:LIPIcs.FSTTCS.2014.279,
author = {David, Claire and Francis, Nadime and Murlak, Filip},
title = {{Consistency of Injective Tree Patterns}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {279--290},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.279},
URN = {urn:nbn:de:0030-drops-48496},
doi = {10.4230/LIPIcs.FSTTCS.2014.279},
annote = {Keywords: XML, incomplete information, injective tree patterns, consistency}
}
Document
Asymptotically Optimal Encodings for Range Selection
Abstract
We consider the problem of preprocessing an array A[1..n] to answer range selection and range top-k queries. Given a query interval [i..j] and a value k, the former query asks for the position of the k-th largest value in A[i..j], whereas the latter asks for the positions of all the k largest values in A[i..j]. We consider the encoding} version of the problem, where A is not available at query time, and an upper bound kappa on k, the rank that is to be selected, is given at construction time. We obtain data structures with asymptotically optimal size and query time on a RAM model with word size Theta(lg(n)): our structures use O(n*lg(kappa)) bits and answer range selection queries in time O(1+lg(k) / lg(lg(n))) and range top-k queries in time O(k), for any k <= kappa.
Cite as
Gonzalo Navarro, Rajeev Raman, and Srinivasa Rao Satti. Asymptotically Optimal Encodings for Range Selection. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 291-301, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{navarro_et_al:LIPIcs.FSTTCS.2014.291,
author = {Navarro, Gonzalo and Raman, Rajeev and Satti, Srinivasa Rao},
title = {{Asymptotically Optimal Encodings for Range Selection}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {291--301},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.291},
URN = {urn:nbn:de:0030-drops-48502},
doi = {10.4230/LIPIcs.FSTTCS.2014.291},
annote = {Keywords: Data Structures, Order Statistics, Succinct Data Structures, Space-efficient Data Structures}
}
Document
Output-Sensitive Pattern Extraction in Sequences
Abstract
Genomic Analysis, Plagiarism Detection, Data Mining, Intrusion Detection, Spam Fighting and Time Series Analysis are just some examples of applications where extraction of recurring patterns in sequences of objects is one of the main computational challenges. Several notions of patterns exist, and many share the common idea of strictly specifying some parts of the pattern and to don't care about the remaining parts. Since the number of patterns can be exponential in the length of the sequences, pattern extraction focuses on statistically relevant patterns, where any attempt to further refine or extend them causes a loss of significant information (where the number of occurrences changes). Output-sensitive algorithms have been proposed to enumerate and list these patterns, taking polynomial time O(n^c) per pattern for constant c > 1, which is impractical for massive sequences of very large length n.
We address the problem of extracting maximal patterns with at most k don't care symbols and at least q occurrences. Our contribution is to give the first algorithm that attains a stronger notion of output-sensitivity, borrowed from the analysis of data structures: the cost is proportional to the actual number of occurrences of each pattern, which is at most n and practically much smaller than n in real applications, thus avoiding the aforementioned cost of O(n^c) per pattern.
Cite as
Roberto Grossi, Giulia Menconi, Nadia Pisanti, Roberto Trani, and Soren Vind. Output-Sensitive Pattern Extraction in Sequences. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 303-314, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{grossi_et_al:LIPIcs.FSTTCS.2014.303,
author = {Grossi, Roberto and Menconi, Giulia and Pisanti, Nadia and Trani, Roberto and Vind, Soren},
title = {{Output-Sensitive Pattern Extraction in Sequences}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {303--314},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.303},
URN = {urn:nbn:de:0030-drops-48513},
doi = {10.4230/LIPIcs.FSTTCS.2014.303},
annote = {Keywords: Pattern Extraction, Motif Detection, Pattern Discovery, Motif Trie}
}
Document
Robust Proximity Search for Balls Using Sublinear Space
Abstract
Given a set of n disjoint balls b_1, ..., b_n in R^d, we provide a data structure, of near linear size, that can answer (1 +- epsilon)-approximate k-th-nearest neighbor queries in O(log(n) + 1/epsilon^d) time, where k and epsilon are provided at query time. If k and epsilon are provided in advance, we provide a data structure to answer such queries, that requires (roughly) O(n/k) space; that is, the data structure has sublinear space requirement if k is sufficiently large.
Cite as
Sariel Har-Peled and Nirman Kumar. Robust Proximity Search for Balls Using Sublinear Space. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 315-326, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{harpeled_et_al:LIPIcs.FSTTCS.2014.315,
author = {Har-Peled, Sariel and Kumar, Nirman},
title = {{Robust Proximity Search for Balls Using Sublinear Space}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {315--326},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.315},
URN = {urn:nbn:de:0030-drops-48526},
doi = {10.4230/LIPIcs.FSTTCS.2014.315},
annote = {Keywords: Approximate Nearest neighbors, algorithms, data structures}
}
Document
The Benes Network is q*(q-1)/2n-Almost q-set-wise Independent
Abstract
A switching network of depth d is a layered graph with d layers and n vertices in each layer. The edges of the switching network do not cross between layers and in each layer the edges form a partial matching. A switching network defines a stochastic process over Sn that starts with the identity permutation and goes through the layers of the network from first to last, where for each layer and each pair (i,j) in the partial matching of the layer, it applies the transposition (i j) with probability half. A switching network is good if the final distribution is close to the uniform distribution over S_n.
A switching network is epsilon-almost q-permutation-wise independent if its action on any ordered set of size q is almost uniform, and is epsilon-almost q-set-wise independent if its action on any set of size q is almost uniform. Mixing of switching networks (even for q-permutation-wise and q-set-wise independence) has found several applications, mostly in cryptography. Some applications further require some additional properties from the network, e.g., the existence of an algorithm that given a permutation can set the switches such that the network generates the given permutation, a property that the Benes network has.
Morris, Rogaway and Stegers showed the Thorp shuffle (which corresponds to applying two or more butterflies one after the other) is q-permutation-wise independent, for q=n^gamma for gamma that depends on the number of sequential applications of the butterfly network. The techniques applied by Morris et al. do not seem to apply for the Benes network.
In this work we show the Benes network is almost q-set-wise independent for q up to about sqrt(n). Our technique is simple and completely new, and we believe carries hope for getting even better results in the future.
Cite as
Efraim Gelman and Amnon Ta-Shma. The Benes Network is q*(q-1)/2n-Almost q-set-wise Independent. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 327-338, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{gelman_et_al:LIPIcs.FSTTCS.2014.327,
author = {Gelman, Efraim and Ta-Shma, Amnon},
title = {{The Benes Network is q*(q-1)/2n-Almost q-set-wise Independent}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {327--338},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.327},
URN = {urn:nbn:de:0030-drops-48538},
doi = {10.4230/LIPIcs.FSTTCS.2014.327},
annote = {Keywords: switching network, mixing, Benes}
}
Document
Notes on Counting with Finite Machines
Abstract
We determine the descriptional complexity (smallest number of states, up to constant factors) of recognizing languages {1^n} and {1^{t n} : t = 0, 1, 2, ...} with state-based finite machines of various kinds. This task is understood as counting to n and modulo n, respectively, and was previously studied for classes of finite-state automata by Kupferman, Ta-Shma, and Vardi (2001). We show that for Turing machines it requires log(n)/log(log(n)) states in the worst case, and individual values are related to Kolmogorov complexity of the binary encoding of n. For deterministic pushdown and counter automata, the complexity is log(n) and sqrt(n), respectively; for alternating counter automata, we show an upper bound of log(n). For visibly pushdown automata, i.e., if the stack movements are determined by input symbols, we consider languages {a^n b^n} and {a^{t n} b^{t n} : n t = 0, 1, 2, ...} and determine their complexity, of sqrt(n) and min(n_1 + n_2), respectively, with minimum over all factorizations n = n_1 n_2.
Cite as
Dmitry Chistikov. Notes on Counting with Finite Machines. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 339-350, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{chistikov:LIPIcs.FSTTCS.2014.339,
author = {Chistikov, Dmitry},
title = {{Notes on Counting with Finite Machines}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {339--350},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.339},
URN = {urn:nbn:de:0030-drops-48547},
doi = {10.4230/LIPIcs.FSTTCS.2014.339},
annote = {Keywords: State complexity, Unary languages, Counting}
}
Document
Mixed Nash Equilibria in Concurrent Terminal-Reward Games
Abstract
We study mixed-strategy Nash equilibria in multiplayer deterministic concurrent games played on graphs, with terminal-reward payoffs (that is, absorbing states with a value for each player). We show undecidability of the existence of a constrained Nash equilibrium (the constraint requiring that one player should have maximal payoff), with only three players and 0/1-rewards (i.e., reachability objectives). This has to be compared with the undecidability result by Ummels and Wojtczak for turn-based games which requires 14 players and general rewards. Our proof has various interesting consequences: (i) the undecidability of the existence of a Nash equilibrium with a constraint on the social welfare; (ii) the undecidability of the existence of an (unconstrained) Nash equilibrium in concurrent games with terminal-reward payoffs.
Cite as
Patricia Bouyer, Nicolas Markey, and Daniel Stan. Mixed Nash Equilibria in Concurrent Terminal-Reward Games. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 351-363, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2014.351,
author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel},
title = {{Mixed Nash Equilibria in Concurrent Terminal-Reward Games}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {351--363},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.351},
URN = {urn:nbn:de:0030-drops-48550},
doi = {10.4230/LIPIcs.FSTTCS.2014.351},
annote = {Keywords: concurrent games, randomized strategy, Nash equilibria, undecidability}
}
Document
Quantitative Games with Interval Objectives
Abstract
Traditionally quantitative games such as mean-payoff games and discount sum games have two players - one trying to maximize the payoff, the other trying to minimize it. The associated decision problem, "Can Eve (the maximizer) achieve, for example, a positive payoff?" can be thought of as one player trying to attain a payoff in the interval (0,infinity). In this paper we consider the more general problem of determining if a player can attain a payoff in a finite union of arbitrary intervals for various payoff functions (liminf/limsup, mean-payoff, discount sum, total sum). In particular this includes the interesting exact-value problem, "Can Eve achieve a payoff of exactly (e.g.) 0?"
Cite as
Paul Hunter and Jean-Francois Raskin. Quantitative Games with Interval Objectives. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 365-377, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{hunter_et_al:LIPIcs.FSTTCS.2014.365,
author = {Hunter, Paul and Raskin, Jean-Francois},
title = {{Quantitative Games with Interval Objectives}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {365--377},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.365},
URN = {urn:nbn:de:0030-drops-48569},
doi = {10.4230/LIPIcs.FSTTCS.2014.365},
annote = {Keywords: Quantitative games, Mean-payoff games, Discount sum games}
}
Document
Playing Safe
Abstract
We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety conditions. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety condition is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety conditions without any regularity assumptions, and for all (finite or infinite) graphs of finite degree.
We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of positional strategies in games with counters.
Cite as
Thomas Colcombet, Nathanael Fijalkow, and Florian Horn. Playing Safe. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 379-390, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2014.379,
author = {Colcombet, Thomas and Fijalkow, Nathanael and Horn, Florian},
title = {{Playing Safe}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {379--390},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.379},
URN = {urn:nbn:de:0030-drops-48571},
doi = {10.4230/LIPIcs.FSTTCS.2014.379},
annote = {Keywords: Game Theory, Synthesis, Safety Specifications, Program Verification}
}
Document
Metaconfluence of Calculi with Explicit Substitutions at a Distance
Abstract
Confluence is a key property of rewriting calculi that guarantees uniqueness of normal-forms when they exist. Metaconfluence is even more general, and guarantees confluence on open/meta terms, i.e. terms with holes, called metavariables that can be filled up with other (open/meta) terms. The difficulty to deal with open terms comes from the fact that the structure of metaterms is only partially known, so that some reduction rules became blocked by the metavariables. In this work, we establish metaconfluence for a family of calculi with explicit substitutions (ES) that enjoy preservation of strong-normalization (PSN) and that act at a distance. For that, we first extend the notion of reduction on metaterms in such a way that explicit substitutions are never structurally moved, i.e. they also act at a distance on metaterms. The resulting reduction relations are still rewriting systems, i.e. they do not include equational axioms, thus providing for the first time an interesting family of lambda-calculi with explicit substitutions that enjoy both PSN and metaconfluence without requiring sophisticated notions of reduction modulo a set of equations.
Cite as
Flávio L. C. de Moura, Delia Kesner, and Mauricio Ayala-Rincón. Metaconfluence of Calculi with Explicit Substitutions at a Distance. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 391-402, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{demoura_et_al:LIPIcs.FSTTCS.2014.391,
author = {de Moura, Fl\'{a}vio L. C. and Kesner, Delia and Ayala-Rinc\'{o}n, Mauricio},
title = {{Metaconfluence of Calculi with Explicit Substitutions at a Distance}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {391--402},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.391},
URN = {urn:nbn:de:0030-drops-48588},
doi = {10.4230/LIPIcs.FSTTCS.2014.391},
annote = {Keywords: Confluence, Explicit Substitutions, Lambda Calculi}
}
Document
Behavioral Metrics via Functor Lifting
Abstract
We study behavioral metrics in an abstract coalgebraic setting. Given a coalgebra alpha : X -> FX in Set, where the functor F specifies the branching type, we define a framework for deriving pseudometrics on X which measure the behavioral distance of states.
A first crucial step is the lifting of the functor F on Set to a functor /F in the category PMet of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ.
Then a final coalgebra for F in Set can be endowed with a behavioral distance resulting as the smallest solution of a fixed-point equation, yielding the final /F-coalgebra in PMet. The same technique, applied to an arbitrary coalgebra alpha : X -> FX in Set, provides the behavioral distance on X. Under some constraints we can prove that two states are at distance 0 if and only if they are behaviorally equivalent.
Cite as
Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral Metrics via Functor Lifting. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 403-415, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{baldan_et_al:LIPIcs.FSTTCS.2014.403,
author = {Baldan, Paolo and Bonchi, Filippo and Kerstan, Henning and K\"{o}nig, Barbara},
title = {{Behavioral Metrics via Functor Lifting}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {403--415},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.403},
URN = {urn:nbn:de:0030-drops-48599},
doi = {10.4230/LIPIcs.FSTTCS.2014.403},
annote = {Keywords: behavioral metric, functor lifting, pseudometric, coalgebra}
}
Document
Foundation of Diagnosis and Predictability in Probabilistic Systems
Abstract
In discrete event systems prone to unobservable faults, a diagnoser must eventually detect fault occurrences. The diagnosability problem consists in deciding whether such a diagnoser exists. Here we investigate diagnosis for probabilistic systems modelled by partially observed Markov chains also called probabilistic labeled transition systems (pLTS). First we study different specifications of diagnosability and establish their relations both in finite and infinite pLTS. Then we analyze the complexity of the diagnosability problem for finite pLTS: we show that the polynomial time procedure earlier proposed is erroneous and that in fact for all considered specifications, the problem is PSPACE-complete. We also establish tight bounds for the size of diagnosers. Afterwards we consider the dual notion of predictability which consists in predicting that in a safe run, a fault will eventually occur. Predictability is an easier problem than diagnosability: it is NLOGSPACE-complete. Yet the predictor synthesis is as hard as the diagnoser synthesis. Finally we introduce and study the more flexible notion of prediagnosability that generalizes predictability and diagnosability.
Cite as
Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux. Foundation of Diagnosis and Predictability in Probabilistic Systems. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 417-429, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2014.417,
author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux, Engel},
title = {{Foundation of Diagnosis and Predictability in Probabilistic Systems}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {417--429},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.417},
URN = {urn:nbn:de:0030-drops-48605},
doi = {10.4230/LIPIcs.FSTTCS.2014.417},
annote = {Keywords: Partially observed systems, Diagnosis, Markov chains}
}
Document
Lipschitz Robustness of Finite-state Transducers
Abstract
We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation
using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using set-similarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers.
Cite as
Thomas A. Henzinger, Jan Otop, and Roopsha Samanta. Lipschitz Robustness of Finite-state Transducers. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 431-443, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{henzinger_et_al:LIPIcs.FSTTCS.2014.431,
author = {Henzinger, Thomas A. and Otop, Jan and Samanta, Roopsha},
title = {{Lipschitz Robustness of Finite-state Transducers}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {431--443},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.431},
URN = {urn:nbn:de:0030-drops-48614},
doi = {10.4230/LIPIcs.FSTTCS.2014.431},
annote = {Keywords: Robustness, Transducers, Weighted Automata}
}
Document
Separating Cook Completeness from Karp-Levin Completeness Under a Worst-Case Hardness Hypothesis
Abstract
We show that there is a language that is Turing complete for NP but not many-one complete for NP, under a worst-case hardness hypothesis. Our hypothesis asserts the existence of a non-deterministic, double-exponential time machine that runs in time O(2^2^n^c) (for some c > 1) accepting Sigma^* whose accepting computations cannot be computed by bounded-error, probabilistic machines running in time O(2^2^{beta * 2^n^c) (for some beta > 0). This is the first result that separates completeness notions for NP under a worst-case hardness hypothesis.
Cite as
Debasis Mandal, A. Pavan, and Rajeswari Venugopalan. Separating Cook Completeness from Karp-Levin Completeness Under a Worst-Case Hardness Hypothesis. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 445-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{mandal_et_al:LIPIcs.FSTTCS.2014.445,
author = {Mandal, Debasis and Pavan, A. and Venugopalan, Rajeswari},
title = {{Separating Cook Completeness from Karp-Levin Completeness Under a Worst-Case Hardness Hypothesis}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {445--456},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.445},
URN = {urn:nbn:de:0030-drops-48621},
doi = {10.4230/LIPIcs.FSTTCS.2014.445},
annote = {Keywords: Cook reduction, Karp reduction, NP-completeness, Turing completeness, many-one completeness}
}
Document
Constructing Small Tree Grammars and Small Circuits for Formulas
Abstract
It is shown that every tree of size n over a fixed set of sigma different ranked symbols can be decomposed into O(n/log_sigma(n)) = O((n * log(sigma))/ log(n)) many hierarchically defined pieces. Formally, such a hierarchical decomposition has the form of a straight-line linear context-free tree grammar of size O(n/log_sigma(n)), which can be used as a compressed representation of the input tree. This generalizes an analogous result for strings. Previous grammar-based tree compressors were not analyzed for the worst-case size of the computed grammar, except for the top dag of Bille et al., for which only the weaker upper bound of O(n/log^{0.19}(n)) for unranked and unlabelled trees has been derived. The main result is used to show that every arithmetical formula of size n, in which only m <= n different variables occur, can be transformed (in time O(n * log(n)) into an arithmetical circuit of size O((n * log(m))/log(n)) and depth O(log(n)). This refines a classical result of Brent, according to which an arithmetical formula of size n can be transformed into a logarithmic depth circuit of size O(n).
Cite as
Danny Hucke, Markus Lohrey, and Eric Noeth. Constructing Small Tree Grammars and Small Circuits for Formulas. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 457-468, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{hucke_et_al:LIPIcs.FSTTCS.2014.457,
author = {Hucke, Danny and Lohrey, Markus and Noeth, Eric},
title = {{Constructing Small Tree Grammars and Small Circuits for Formulas}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {457--468},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.457},
URN = {urn:nbn:de:0030-drops-48639},
doi = {10.4230/LIPIcs.FSTTCS.2014.457},
annote = {Keywords: grammar-based compression, tree compression, arithmetical circuits}
}
Document
One Time-traveling Bit is as Good as Logarithmically Many
Abstract
We consider computation in the presence of closed timelike curves (CTCs), as proposed by Deutsch. We focus on the case in which the CTCs carry classical bits (as opposed to qubits). Previously, Aaronson and Watrous showed that computation with polynomially many CTC bits is equivalent in power to PSPACE. On the other hand, Say and Yakaryilmaz showed that computation with just 1 classical CTC bit gives the power of "postselection", thereby upgrading classical randomized computation (BPP) to the complexity class BPP_path and standard quantum computation (BQP) to the complexity class PP. It is natural to ask whether increasing the number of CTC bits from 1 to 2 (or 3, 4, etc.) leads to increased computational power. We show that the answer is no: randomized computation with logarithmically many CTC bits (i.e., polynomially many CTC states) is equivalent to BPP_path. (Similarly, quantum computation augmented with logarithmically many classical CTC bits is equivalent to PP.) Spoilsports with no interest in time travel may view our results as concerning the robustness of the class BPP_path and the computational complexity of sampling from an implicitly defined Markov chain.
Cite as
Ryan O'Donnell and A. C. Cem Say. One Time-traveling Bit is as Good as Logarithmically Many. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 469-480, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{odonnell_et_al:LIPIcs.FSTTCS.2014.469,
author = {O'Donnell, Ryan and Cem Say, A. C.},
title = {{One Time-traveling Bit is as Good as Logarithmically Many}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {469--480},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.469},
URN = {urn:nbn:de:0030-drops-48646},
doi = {10.4230/LIPIcs.FSTTCS.2014.469},
annote = {Keywords: Time travel, postselection, Markov chains, randomized computation}
}
Document
New Bounds for the Garden-Hose Model
Abstract
We show new results about the garden-hose model. Our main results include improved lower bounds based on non-deterministic communication complexity (leading to the previously unknown Theta(n) bounds for Inner Product mod 2 and Disjointness), as well as an O(n * log^3(n) upper bound for the Distributed Majority function (previously conjectured to have quadratic complexity). We show an efficient simulation of formulae made of AND, OR, XOR gates in the garden-hose model, which implies that lower bounds on the garden-hose complexity GH(f) of the order Omega(n^{2+epsilon}) will be hard to obtain for explicit functions. Furthermore we study a time-bounded variant of the model, in which even modest savings in time can lead to exponential lower bounds on the size of garden-hose protocols.
Cite as
Hartmut Klauck and Supartha Podder. New Bounds for the Garden-Hose Model. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 481-492, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{klauck_et_al:LIPIcs.FSTTCS.2014.481,
author = {Klauck, Hartmut and Podder, Supartha},
title = {{New Bounds for the Garden-Hose Model}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {481--492},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.481},
URN = {urn:nbn:de:0030-drops-48657},
doi = {10.4230/LIPIcs.FSTTCS.2014.481},
annote = {Keywords: Space Complexity, Communication Complexity, Garden-Hose Model}
}
Document
Homomorphism Polynomials Complete for VP
Abstract
The VP versus VNP question, introduced by Valiant, is probably the most important open question in algebraic complexity theory. Thanks to completeness results, a variant of this question, VBP versus VNP, can be succinctly restated as asking whether the permanent of a generic matrix can be written as a determinant of a matrix of polynomially bounded size. Strikingly, this restatement does not mention any notion of computational model. To get a similar restatement for the original and more fundamental question, and also to better understand the class itself, we need a complete polynomial for VP. Ad hoc constructions yielding complete polynomials were known, but not natural examples in the vein of the determinant. We give here several variants of natural complete polynomials for VP, based on the notion of graph homomorphism polynomials.
Cite as
Arnaud Durand, Meena Mahajan, Guillaume Malod, Nicolas de Rugy-Altherre, and Nitin Saurabh. Homomorphism Polynomials Complete for VP. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 493-504, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{durand_et_al:LIPIcs.FSTTCS.2014.493,
author = {Durand, Arnaud and Mahajan, Meena and Malod, Guillaume and de Rugy-Altherre, Nicolas and Saurabh, Nitin},
title = {{Homomorphism Polynomials Complete for VP}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {493--504},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.493},
URN = {urn:nbn:de:0030-drops-48665},
doi = {10.4230/LIPIcs.FSTTCS.2014.493},
annote = {Keywords: algebraic complexity, graph homomorphism, polynomials, VP, VNP, completeness}
}
Document
Computing Information Flow Using Symbolic Model-Checking
Abstract
Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret inputs. We consider the problem of computing information leaked by a deterministic or probabilistic program when the measure of information is based on (a) min-entropy and (b) Shannon entropy. The key challenge in computing these measures is that we need the total number of possible outputs and, for each possible output, the number of inputs that lead to it. A direct computation of these quantities is infeasible because of the state-explosion problem. We therefore propose symbolic algorithms based on binary decision diagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easily implemented in any BDD-based model-checking tool that checks for reachability in deterministic non-recursive programs by computing program summaries. We demonstrate the validity of our approach by implementing these algorithms in a tool Moped-QLeak, which is built upon Moped, a model checker for Boolean programs. Finally, we show how this symbolic approach extends to probabilistic programs.
Cite as
Rohit Chadha, Umang Mathur, and Stefan Schwoon. Computing Information Flow Using Symbolic Model-Checking. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 505-516, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{chadha_et_al:LIPIcs.FSTTCS.2014.505,
author = {Chadha, Rohit and Mathur, Umang and Schwoon, Stefan},
title = {{Computing Information Flow Using Symbolic Model-Checking}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {505--516},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.505},
URN = {urn:nbn:de:0030-drops-48676},
doi = {10.4230/LIPIcs.FSTTCS.2014.505},
annote = {Keywords: Information leakage, Min Entropy, Shannon Entropy, Abstract decision diagrams, Program summaries}
}
Document
Information Leakage of Non-Terminating Processes
Abstract
In recent years, quantitative security techniques have been providing effective measures of the security of a system against an attacker. Such techniques usually assume that the system produces a finite amount of observations based on a finite amount of secret bits and terminates, and the attack is based on these observations. By modeling systems with Markov chains, we are able to measure the effectiveness of attacks on non-terminating systems. Such systems do not necessarily produce a finite amount of output and are not necessarily based on a finite amount of secret bits. We provide characterizations and algorithms to define meaningful measures of security for non-terminating systems, and to compute them when possible. We also study the bounded versions of the problems, and show examples of non-terminating programs and how their effectiveness in protecting their secret can be measured.
Cite as
Fabrizio Biondi, Axel Legay, Bo Friis Nielsen, Pasquale Malacaria, and Andrzej Wasowski. Information Leakage of Non-Terminating Processes. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 517-529, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{biondi_et_al:LIPIcs.FSTTCS.2014.517,
author = {Biondi, Fabrizio and Legay, Axel and Nielsen, Bo Friis and Malacaria, Pasquale and Wasowski, Andrzej},
title = {{Information Leakage of Non-Terminating Processes}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {517--529},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.517},
URN = {urn:nbn:de:0030-drops-48683},
doi = {10.4230/LIPIcs.FSTTCS.2014.517},
annote = {Keywords: Quantitative information flow, Markov chain, information leakage, infinite execution}
}
Document
Multiple-Environment Markov Decision Processes
Abstract
We introduce Multi-Environment Markov Decision Processes (MEMDPs) which are MDPs with a set of probabilistic transition functions. The goal in an MEMDP is to synthesize a single controller strategy with guaranteed performances against all environments even though the environment is unknown a priori. While MEMDPs can be seen as a special class of partially observable MDPs, we show that several verification problems that are undecidable for partially observable MDPs, are decidable for MEMDPs and sometimes have even efficient solutions.
Cite as
Jean-Francois Raskin and Ocan Sankur. Multiple-Environment Markov Decision Processes. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 531-543, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{raskin_et_al:LIPIcs.FSTTCS.2014.531,
author = {Raskin, Jean-Francois and Sankur, Ocan},
title = {{Multiple-Environment Markov Decision Processes}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {531--543},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.531},
URN = {urn:nbn:de:0030-drops-48692},
doi = {10.4230/LIPIcs.FSTTCS.2014.531},
annote = {Keywords: Markov decision processes, probabilistic systems, multiple objectives}
}
Document
Summary-Based Inter-Procedural Analysis via Modular Trace Refinement
Abstract
We propose a generalisation of trace refinement for the verification of inter-procedural programs. Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the main features of our approach and yields promising results.
Cite as
Franck Cassez, Christian Müller, and Karla Burnett. Summary-Based Inter-Procedural Analysis via Modular Trace Refinement. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 545-556, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{cassez_et_al:LIPIcs.FSTTCS.2014.545,
author = {Cassez, Franck and M\"{u}ller, Christian and Burnett, Karla},
title = {{Summary-Based Inter-Procedural Analysis via Modular Trace Refinement}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {545--556},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.545},
URN = {urn:nbn:de:0030-drops-48708},
doi = {10.4230/LIPIcs.FSTTCS.2014.545},
annote = {Keywords: Program verification, Hoare Logic, Refinement, Automata}
}
Document
A Two-Level Logic Approach to Reasoning About Typed Specification Languages
Abstract
The two-level logic approach (2LL) to reasoning about computational specifications, as implemented by the Abella theorem prover, represents derivations of a specification language as an inductive definition in a reasoning logic. This approach has traditionally been formulated with the specification and reasoning logics having the same type system, and only the formulas being translated. However, requiring identical type systems limits the approach in two important ways: (1) every change in the specification language's type system requires a corresponding change in that of the reasoning logic, and (2) the same reasoning logic cannot be used with two specification languages at once if they have incompatible type systems. We propose a technique based on adequate encodings of the types and judgements of a typed specification language in terms of a simply typed higher-order logic program, which is then used for reasoning about the specification language in the usual 2LL. Moreover, a single specification logic implementation can be used as a basis for a number of other specification languages just by varying the encoding. We illustrate our technique with an implementation of the LF dependent type theory as a new specification language for Abella, co-existing with its current simply typed higher-order hereditary Harrop specification logic, without modifying the type system of its reasoning logic.
Cite as
Mary Southern and Kaustuv Chaudhuri. A Two-Level Logic Approach to Reasoning About Typed Specification Languages. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 557-569, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{southern_et_al:LIPIcs.FSTTCS.2014.557,
author = {Southern, Mary and Chaudhuri, Kaustuv},
title = {{A Two-Level Logic Approach to Reasoning About Typed Specification Languages}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {557--569},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.557},
URN = {urn:nbn:de:0030-drops-48716},
doi = {10.4230/LIPIcs.FSTTCS.2014.557},
annote = {Keywords: Abella theorem prover, two-level logic, typed specification languages}
}
Document
On the Complexity of Computing Maximum Entropy for Markovian Models
Abstract
We investigate the complexity of computing entropy of various Markovian models including Markov Chains (MCs), Interval Markov Chains (IMCs) and Markov Decision Processes (MDPs). We consider both entropy and entropy rate for general MCs, and study two algorithmic questions, i.e., entropy approximation problem and entropy threshold problem. The former asks for an approximation of the entropy/entropy rate within a given precision, whereas the latter aims to decide whether they exceed a given threshold. We give polynomial-time algorithms for the approximation problem, and show the threshold problem is in P^CH_3 (hence in PSPACE) and in P assuming some number-theoretic conjectures. Furthermore, we study both questions for IMCs and MDPs where we aim to maximise the entropy/entropy rate among an infinite family of MCs associated with the given model. We give various conditional decidability results for the threshold problem, and show the approximation problem is solvable in polynomial-time via convex programming.
Cite as
Taolue Chen and Tingting Han. On the Complexity of Computing Maximum Entropy for Markovian Models. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 571-583, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.FSTTCS.2014.571,
author = {Chen, Taolue and Han, Tingting},
title = {{On the Complexity of Computing Maximum Entropy for Markovian Models}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {571--583},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.571},
URN = {urn:nbn:de:0030-drops-48725},
doi = {10.4230/LIPIcs.FSTTCS.2014.571},
annote = {Keywords: Markovian Models, Entropy, Complexity, Probabilistic Verification}
}
Document
New Time-Space Upperbounds for Directed Reachability in High-genus and H-minor-free Graphs
Abstract
We obtain the following new simultaneous time-space upper bounds for the directed reachability problem. (1) A polynomial-time, O(n^{2/3} * g^{1/3})-space algorithm for directed graphs embedded on orientable surfaces of genus g. (2) A polynomial-time, O(n^{2/3})-space algorithm for all H-minor-free graphs given the tree decomposition, and (3) for K_{3,3}-free and K_5-free graphs, a polynomial-time, O(n^{1/2 + epsilon})-space algorithm, for every epsilon > 0.
For the general directed reachability problem, the best known simultaneous time-space upper bound is the BBRS bound, due to Barnes, Buss, Ruzzo, and Schieber, which achieves a space bound of O(n/2^{k * sqrt(log(n))}) with polynomial running time, for any constant k. It is a significant open question to improve this bound for reachability over general directed graphs. Our algorithms beat the BBRS bound for graphs embedded on surfaces of genus n/2^{omega(sqrt(log(n))}, and for all H-minor-free graphs. This significantly broadens the class of directed graphs for which the BBRS bound can be improved.
Cite as
Diptarka Chakraborty, A. Pavan, Raghunath Tewari, N. V. Vinodchandran, and Lin Forrest Yang. New Time-Space Upperbounds for Directed Reachability in High-genus and H-minor-free Graphs. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 585-595, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{chakraborty_et_al:LIPIcs.FSTTCS.2014.585,
author = {Chakraborty, Diptarka and Pavan, A. and Tewari, Raghunath and Vinodchandran, N. V. and Yang, Lin Forrest},
title = {{New Time-Space Upperbounds for Directed Reachability in High-genus and H-minor-free Graphs}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {585--595},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.585},
URN = {urn:nbn:de:0030-drops-48730},
doi = {10.4230/LIPIcs.FSTTCS.2014.585},
annote = {Keywords: Reachability, Space complexity, Time-Space Efficient Algorithms, Graphs on Surfaces, Minor Free Graphs, Savitch's Algorithm, BBRS Bound}
}
Document
Polynomial Min/Max-weighted Reachability is in Unambiguous Log-space
Abstract
For a graph G(V,E) and a vertex s in V, a weighting scheme (w : E -> N) is called a min-unique (resp. max-unique) weighting scheme, if for any vertex v of the graph G, there is a unique path of minimum (resp. maximum) weight from s to v. Instead, if the number of paths of minimum (resp. maximum) weight is bounded by n^c for some constant c, then the weighting scheme is called a min-poly (resp. max-poly) weighting scheme.
In this paper, we propose an unambiguous non-deterministic log-space (UL) algorithm for the problem of testing reachability in layered directed acyclic graphs (DAGs) augmented with a min-poly weighting scheme. This improves the result due to Reinhardt and Allender [Reinhardt/Allender, SIAM J. Comp., 2000] where a UL algorithm was given for the case when the weighting scheme is min-unique.
Our main technique is a triple inductive counting, which generalizes the techniques of [Immermann, Siam J. Comp.,1988; Szelepcsényi, Acta Inf.,1988] and [Reinhardt/Allender, SIAM J. Comp., 2000], combined with a hashing technique due to [Fredman et al.,J. ACM, 1984] (also used in [Garvin et al., Comp. Compl.,2014]). We combine this with a complementary unambiguous verification method, to give the desired UL algorithm.
At the other end of the spectrum, we propose a UL algorithm for testing reachability in layered DAGs augmented with max-poly weighting schemes. To achieve this, we first reduce reachability in DAGs to the longest path problem for DAGs with a unique source, such that the reduction also preserves the max-poly property of the graph. Using our techniques, we generalize the double inductive counting method in [Limaye et al., CATS, 2009] where UL algorithms were given for the longest path problem on DAGs with a unique sink and augmented with a max-unique weighting scheme.
An important consequence of our results is that, to show NL = UL, it suffices to design log-space computable min-poly (or max-poly) weighting schemes for DAGs.
Cite as
Anant Dhayal, Jayalal Sarma, and Saurabh Sawlani. Polynomial Min/Max-weighted Reachability is in Unambiguous Log-space. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 597-609, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{dhayal_et_al:LIPIcs.FSTTCS.2014.597,
author = {Dhayal, Anant and Sarma, Jayalal and Sawlani, Saurabh},
title = {{Polynomial Min/Max-weighted Reachability is in Unambiguous Log-space}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {597--609},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.597},
URN = {urn:nbn:de:0030-drops-48744},
doi = {10.4230/LIPIcs.FSTTCS.2014.597},
annote = {Keywords: Reachability Problem, Space Complexity, Unambiguous Algorithms}
}
Document
On Bounded Reachability Analysis of Shared Memory Systems
Abstract
This paper addresses the reachability problem for pushdown systems communicating via shared memory. It is already known that this problem is undecidable. It turns out that undecidability holds even if the shared memory consists of a single boolean variable. We propose a restriction on the behaviours of such systems, called stage bound, towards decidability. A k stage bounded run can be split into a k stages, such that in each stage there is at most one process writing to the shared memory while any number of processes may read from it. We consider several versions of stage-bounded systems and establish decidability and complexity results.
Cite as
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. On Bounded Reachability Analysis of Shared Memory Systems. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 611-623, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{atig_et_al:LIPIcs.FSTTCS.2014.611,
author = {Atig, Mohamed Faouzi and Bouajjani, Ahmed and Narayan Kumar, K. and Saivasan, Prakash},
title = {{On Bounded Reachability Analysis of Shared Memory Systems}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {611--623},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.611},
URN = {urn:nbn:de:0030-drops-48754},
doi = {10.4230/LIPIcs.FSTTCS.2014.611},
annote = {Keywords: Reachability problem, Pushdown systems, Counter systems}
}
Document
Parameterized Communicating Automata: Complementation and Model Checking
Abstract
We study the language-theoretical aspects of parameterized communicating automata (PCAs), in which processes communicate via rendez-vous. A given PCA can be run on any topology of bounded degree such as pipelines, rings, ranked trees, and grids. We show that, under a context bound, which restricts the local behavior of each process, PCAs are effectively complementable. Complementability is considered a key aspect of robust automata models and can, in particular, be exploited for verification. In this paper, we use it to obtain a characterization of context-bounded PCAs in terms of monadic second-order (MSO) logic. As the emptiness problem for context-bounded PCAs is decidable for the classes of pipelines, rings, and trees, their model-checking problem wrt. MSO properties also becomes decidable. While previous work on model checking parameterized systems typically uses temporal logics without next operator, our MSO logic allows one to express several natural next modalities.
Cite as
Benedikt Bollig, Paul Gastin, and Akshay Kumar. Parameterized Communicating Automata: Complementation and Model Checking. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 625-637, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{bollig_et_al:LIPIcs.FSTTCS.2014.625,
author = {Bollig, Benedikt and Gastin, Paul and Kumar, Akshay},
title = {{Parameterized Communicating Automata: Complementation and Model Checking}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {625--637},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.625},
URN = {urn:nbn:de:0030-drops-48761},
doi = {10.4230/LIPIcs.FSTTCS.2014.625},
annote = {Keywords: parameterized verification, complementation, monadic second-order logic}
}
Document
Distributed Synthesis for Acyclic Architectures
Abstract
The distributed synthesis problem is about constructing correct distributed systems, i.e., systems that satisfy a given specification. We consider a slightly more general problem of distributed control, where the goal is to restrict the behavior of a given distributed system in order to satisfy the specification. Our systems are finite state machines that communicate via rendez-vous (Zielonka automata). We show decidability of the synthesis problem for all omega-regular local specifications, under the restriction that the communication graph of the system is acyclic. This result extends a previous decidability result for a restricted form of local reachability specifications.
Cite as
Anca Muscholl and Igor Walukiewicz. Distributed Synthesis for Acyclic Architectures. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 639-651, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{muscholl_et_al:LIPIcs.FSTTCS.2014.639,
author = {Muscholl, Anca and Walukiewicz, Igor},
title = {{Distributed Synthesis for Acyclic Architectures}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {639--651},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.639},
URN = {urn:nbn:de:0030-drops-48772},
doi = {10.4230/LIPIcs.FSTTCS.2014.639},
annote = {Keywords: Distributed synthesis, distributed control, causal memory}
}
Document
Verification of Dynamic Register Automata
Abstract
We consider the verification problem for Dynamic Register Automata (DRA). DRA extend classical register automata by process creation. In this setting, each process is equipped with a finite set of registers in which the process IDs of other processes can be stored. A process can communicate with processes whose IDs are stored in its registers and can send them the content of its registers. The state reachability problem asks whether a DRA reaches a configuration where at least one process is in an error state. We first show that this problem is in general undecidable. This result holds even when we restrict the analysis to configurations where the maximal length of the simple paths in their underlying (un)directed communication graphs are bounded by some constant. Then we introduce the model of degenerative DRA which allows non-deterministic reset of the registers. We prove that for every given DRA, its corresponding degenerative one has the same set of reachable states. While the state reachability of a degenerative DRA remains undecidable, we show that the problem becomes decidable with nonprimitive recursive complexity when we restrict the analysis to strongly bounded configurations, i.e. configurations whose underlying undirected graphs have bounded simple paths. Finally, we consider the class of strongly safe DRA, where all the reachable configurations are assumed to be strongly bounded. We show that for strongly safe DRA, the state reachability problem becomes decidable.
Cite as
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, and Othmane Rezine. Verification of Dynamic Register Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 653-665, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2014.653,
author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Kara, Ahmet and Rezine, Othmane},
title = {{Verification of Dynamic Register Automata}},
booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
pages = {653--665},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-77-4},
ISSN = {1868-8969},
year = {2014},
volume = {29},
editor = {Raman, Venkatesh and Suresh, S. P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.653},
URN = {urn:nbn:de:0030-drops-48787},
doi = {10.4230/LIPIcs.FSTTCS.2014.653},
annote = {Keywords: Verification, Reachability problem, Register automata}
}