Volume
LIPIcs, Volume 45
35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)
Event
FSTTCS 2015, December 16-18, 2015, Bangalore, IndiaEditors
Publication Details
- published at: 2015-12-14
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-97-2
- DBLP: db/conf/fsttcs/fsttcs2015
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 45, FSTTCS'15, Complete Volume
Abstract
LIPIcs, Volume 45, FSTTCS'15, Complete Volume
Cite as
35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@Proceedings{harsha_et_al:LIPIcs.FSTTCS.2015,
title = {{LIPIcs, Volume 45, FSTTCS'15, Complete Volume }},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015},
URN = {urn:nbn:de:0030-drops-56671},
doi = {10.4230/LIPIcs.FSTTCS.2015},
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
35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{harsha_et_al:LIPIcs.FSTTCS.2015.i,
author = {Harsha, Prahladh and Ramalingam, G.},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {i--xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.i},
URN = {urn:nbn:de:0030-drops-56174},
doi = {10.4230/LIPIcs.FSTTCS.2015.i},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Bypassing Worst Case Analysis: Tensor Decomposition and Clustering (Invited Talk)
Abstract
Typical worst case analysis of algorithms has led to a rich theory, but suffers from many pitfalls.
This has inspired several approaches to bypass worst case analysis.
In this talk, I will describe two vignettes from recent work in this realm.
In the first part of the talk, I will discuss tensor decomposition -- a natural higher dimensional analog of matrix decomposition.
Low rank tensor decompositions have proved to be a powerful tool for learning generative models, and uniqueness results give them a significant advantage over matrix decomposition methods. Yet, they pose significant challenges for algorithm design as most problems about tensors
are NP-hard. I will discuss a smoothed analysis framework for analyzing algorithms for tensor decomposition which models realistic instances of learning problems and allows us to overcome many of the usual limitations of using tensor methods.
In the second part of the talk, I will explore the phenomenon of convex relaxations returning integer solutions. Clearly this is not true in the worst case. I will discuss instances of discrete optimization problems where, for a suitable distribution on inputs, LP and SDP relaxations produce integer solutions with high probability. This has been studied in the context of LP decoding, sparse recovery, stochastic block models and so on. I will mention some recent results for clustering problems: when points are drawn from a distribution over k sufficiently separated clusters, the well known k-median relaxation and a (not so well known) SDP relaxation for k-means exactly recover the clusters.
Cite as
Moses S. Charikar. Bypassing Worst Case Analysis: Tensor Decomposition and Clustering (Invited Talk). In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{charikar:LIPIcs.FSTTCS.2015.1,
author = {Charikar, Moses S.},
title = {{Bypassing Worst Case Analysis: Tensor Decomposition and Clustering}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {1--1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.1},
URN = {urn:nbn:de:0030-drops-56647},
doi = {10.4230/LIPIcs.FSTTCS.2015.1},
annote = {Keywords: tensor decomposition, smoothed analysis, convex relaxations, integrality}
}
Document
Invited Talk
Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk)
Abstract
Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections including stacks and queues are vital to modern computer systems. Programming them is however error prone. To minimize synchronization overhead between concurrent object-method invocations, implementors avoid blocking operations like lock acquisition, allowing methods to execute concurrently. However, concurrency risks unintended inter-operation interference. Their correctness is captured by observational refinement which ensures conformance to atomic reference implementations. Formally, given two libraries L_1 and L_2 implementing the methods of some concurrent object, we say L_1 refines L_2 if and only if every computation of every program using L_1 would also be possible were L_2 used instead.
Linearizability, being an equivalent property, is the predominant proof technique for establishing observational refinement: one shows that each concurrent execution has a linearization which is a valid sequential execution according to a specification, given by an abstract data type or atomic reference implementation.
However, checking linearizability is intrinsically hard. Indeed, even in the case where method implementations are finite-state and object specifications are also finite-state, and when a fixed number of threads (invoking methods in parallel) is considered, the linearizability problem is EXPSPACE-complete, and it becomes undecidable when the number of threads is unbounded. These results show in particular that there is a complexity/decidability gap between the problem of checking linearizability and the problem of
checking reachability (i.e., the dual of checking safety/invariance properties), the latter being, PSPACE-complete and EXPSPACE-complete in the above considered cases, respectively.
We address here the issue of investigating cases where tractable reductions of the observational refinement/linearizability problem to the reachability problem, or dually to invariant checking, are possible. Our aim is (1) to develop algorithmic approaches that avoid a systematic exploration of all possible linearizations of all computations, (2) to exploit existing techniques and tools for
efficient invariant checking to check observational refinement, and (3) to establish decidability and complexity results for significant classes of concurrent objects and data structures.
We present two approaches that we have proposed recently. The first approach introduces a parameterized approximation schema for detecting observational refinement violations. This approach exploits a fundamental property of shared-memory library executions: their histories are interval orders, a special case of partial orders which admit canonical representations in which each operation o is mapped to a positive-integer-bounded interval I(o). Interval orders are equipped with a natural notion of length, which corresponds to the smallest integer constant for which an interval mapping exists. Then, we define a notion of bounded-interval-length analysis, and demonstrate its efficiency, in terms of complexity, coverage, and scalability, for detecting observational refinement bugs.
The second approach focuses on a specific class of abstract data types, including common concurrent objects and data structures such as stacks and queues. We show that for this class of objects, the linearizability problem is actually as hard as the control-state reachability problem. Indeed, we prove that in this case, the
existence of linearizability violations (i.e., finite computations that are not linearizable), can be captured completely by a finite number of finite-state automata, even when an unbounded number of parallel operations is allowed (assuming that libraries are data-independent).
Cite as
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk). In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 2-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bouajjani_et_al:LIPIcs.FSTTCS.2015.2,
author = {Bouajjani, Ahmed and Emmi, Michael and Enea, Constantin and Hamza, Jad},
title = {{Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {2--4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.2},
URN = {urn:nbn:de:0030-drops-56638},
doi = {10.4230/LIPIcs.FSTTCS.2015.2},
annote = {Keywords: Concurrent objects, linearizability, verification, bug detection}
}
Document
Invited Talk
Reachability Problems for Continuous Linear Dynamical Systems (Invited Talk)
Abstract
This talk is about reachability problems for continuous-time linear
dynamical systems. A central decision problem in the area is the
Continuous Skolem Problem. In particular, this problem lies at the heart of several reachability questions in continuous-time Markov chains and linear hybrid automata.
We describe some recent work, done in collaboration with Chonev and Ouaknine, that uses results in transcendence theory and real algebraic geometry to obtain decidability for certain variants of the problem. In particular, we consider a bounded version of the Continuous Skolem Problem, corresponding to time-bounded reachability. We prove decidability of the bounded problem assuming Schanuel's conjecture, a central conjecture in transcendence theory. We also describe some partial decidability results in the unbounded case in the case of functions satisfying differential equations of fixed low order.
Finally, we give evidence of significant mathematical obstacles to
proving decidability of the Continuous Skolem Problem in full
generality by exhibiting some number-theoretic consequences of the
existence of a decision procedure for this problem.
Cite as
James Worrell. Reachability Problems for Continuous Linear Dynamical Systems (Invited Talk). In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 5-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{worrell:LIPIcs.FSTTCS.2015.5,
author = {Worrell, James},
title = {{Reachability Problems for Continuous Linear Dynamical Systems}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {5--6},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.5},
URN = {urn:nbn:de:0030-drops-56410},
doi = {10.4230/LIPIcs.FSTTCS.2015.5},
annote = {Keywords: Linear Differential Equations, Continuous-Time Markov Chains, Hybrid Automata, Schanuel's Conjecture}
}
Document
Invited Talk
Convexity, Bayesianism, and the Quest Towards Optimal Algorithms (Invited Talk)
Abstract
In this high level and accessible talk I will describe a recent line of works aimed at trying to understand the intrinsic complexity of computational problems by finding optimal algorithms for large classes of such problems. In particular, I will talk about efforts centered on convex programming as a source for such candidate algorithms. As we will see, a byproduct of this effort is a computational analog of Bayesian probability that is of its own interest.
I will demonstrate the approach using the example of the planted clique (also known as hidden clique) problem - a central problem in average case complexity with connections to machine learning, community detection, compressed sensing, finding Nash equilibrium and more. While the complexity of the planted clique problem is still wide open, this line of works has led to interesting insights on it.
Cite as
Boaz Barak. Convexity, Bayesianism, and the Quest Towards Optimal Algorithms (Invited Talk). In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, p. 7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{barak:LIPIcs.FSTTCS.2015.7,
author = {Barak, Boaz},
title = {{Convexity, Bayesianism, and the Quest Towards Optimal Algorithms}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {7--7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.7},
URN = {urn:nbn:de:0030-drops-56626},
doi = {10.4230/LIPIcs.FSTTCS.2015.7},
annote = {Keywords: Convex programming, Bayesian probability, Average-case complexity, Planted clique}
}
Document
Invited Talk
Beyond Matrix Completion (Invited Talk)
Abstract
Here we study some of the statistical and algorithmic problems that arise in recommendation systems. We will be interested in what happens when we move beyond the matrix setting, to work with higher order objects — namely, tensors. To what extent does inference over more complex objects yield better predictions, but at the expense of the running time? We will explore the computational vs. statistical tradeoffs for some basic problems about recovering approximately low rank tensors from few observations, and will show that our algorithms are nearly optimal among all polynomial time algorithms, under natural complexity-theoretic assumptions.
This is based on joint work with Boaz Barak.
Cite as
Ankur Moitra. Beyond Matrix Completion (Invited Talk). In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, p. 8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{moitra:LIPIcs.FSTTCS.2015.8,
author = {Moitra, Ankur},
title = {{Beyond Matrix Completion}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {8--8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.8},
URN = {urn:nbn:de:0030-drops-56650},
doi = {10.4230/LIPIcs.FSTTCS.2015.8},
annote = {Keywords: matrix completion, recommendation systems, tensor prediction}
}
Document
Invited Talk
Relational Refinement Types for Higher-Order Shape Transformers (Invited Talk)
Abstract
Understanding, discovering, and proving useful properties of sophisticated data structures are central problems in program verification. A particularly challenging exercise for shape analyses
involves reasoning about sophisticated shape transformers that preserve the shape of a data structure (e.g., the data structure skeleton is always maintained as a balanced tree) or the relationship among values contained therein (e.g., the in-order relation of the elements of a tree or the parent-child relation of the elements of a heap) across program transformations.
In this talk, we consider the specification and verification of such transformers for ML programs. The structural properties preserved by transformers can often be naturally expressed as inductively-defined relations over the recursive structure evident in the definitions of the datatypes they manipulate. By carefully augmenting a refinement type system with support for reasoning about structural relations over algebraic datatypes, we realize an expressive yet decidable specification language, capable of capturing useful structural invariants, which can nonetheless be automatically verified using off-the-shelf type checkers and theorem provers. Notably, our technique generalizes to definitions of parametric relations for polymorphic data types which, in turn, lead to highly composable specifications over higher-order polymorphic shape transformers.
Cite as
Suresh Jagannathan. Relational Refinement Types for Higher-Order Shape Transformers (Invited Talk). In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, p. 9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{jagannathan:LIPIcs.FSTTCS.2015.9,
author = {Jagannathan, Suresh},
title = {{Relational Refinement Types for Higher-Order Shape Transformers}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {9--9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.9},
URN = {urn:nbn:de:0030-drops-56406},
doi = {10.4230/LIPIcs.FSTTCS.2015.9},
annote = {Keywords: Relational Specifications; Inductive and Parametric Relations; Refinement Types, Shape Analysis, Data Structure Verification\}}
}
Document
Robust Reoptimization of Steiner Trees
Abstract
In reoptimization problems, one is given an optimal solution to a problem instance and a local modification of the instance. The goal is to obtain a solution for the modified instance. The additional information about the instance provided by the given solution plays a central role: we aim to use that information in order to obtain better solutions than we are able to compute from scratch.
In this paper, we consider Steiner tree reoptimization and address the optimality requirement of the provided solution. Instead of assuming that we are provided an optimal solution, we relax the assumption to the more realistic scenario where we are given an approximate solution with an upper bound on its performance guarantee.
We show that for Steiner tree reoptimization there is a clear separation between local modifications where optimality is crucial for obtaining improved approximations and those instances where approximate solutions are acceptable starting points. For some of the local modifications that have been considered in previous research, we show that for every fixed epsilon > 0, approximating the reoptimization problem with respect to a given (1+epsilon)-approximation is as hard as approximating the Steiner tree problem itself (whereas with a given optimal solution to the original problem it is known that one can obtain considerably improved results). Furthermore, we provide a new algorithmic technique that, with some further insights, allows us to obtain improved performance guarantees for Steiner tree reoptimization with respect to all remaining local modifications that have been considered in the literature: a required node of degree more than one becomes a Steiner node; a Steiner node becomes a required node; the cost of one edge is increased.
Cite as
Keshav Goyal and Tobias Mömke. Robust Reoptimization of Steiner Trees. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 10-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{goyal_et_al:LIPIcs.FSTTCS.2015.10,
author = {Goyal, Keshav and M\"{o}mke, Tobias},
title = {{Robust Reoptimization of Steiner Trees}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {10--24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.10},
URN = {urn:nbn:de:0030-drops-56251},
doi = {10.4230/LIPIcs.FSTTCS.2015.10},
annote = {Keywords: reoptimization, approximation algorithms, Steiner tree problem, robustness}
}
Document
Minimizing Weighted lp-Norm of Flow-Time in the Rejection Model
Abstract
We consider the online scheduling problem to minimize the weighted ell_p-norm of flow-time of jobs. We study this problem under the rejection model introduced by Choudhury et al. (SODA 2015) - here the online algorithm is allowed to not serve an eps-fraction of the requests. We consider the restricted assignments setting where each job can go to a specified subset of machines. Our main result is an immediate dispatch non-migratory 1/eps^{O(1)}-competitive algorithm for this problem when one is allowed to reject at most eps-fraction of the total weight of jobs arriving. This is in contrast with the speed augmentation model under which no online algorithm for this problem can achieve a competitive ratio independent of p.
Cite as
Anamitra Roy Choudhury, Syamantak Das, and Amit Kumar. Minimizing Weighted lp-Norm of Flow-Time in the Rejection Model. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 25-37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{roychoudhury_et_al:LIPIcs.FSTTCS.2015.25,
author = {Roy Choudhury, Anamitra and Das, Syamantak and Kumar, Amit},
title = {{Minimizing Weighted lp-Norm of Flow-Time in the Rejection Model}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {25--37},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.25},
URN = {urn:nbn:de:0030-drops-56341},
doi = {10.4230/LIPIcs.FSTTCS.2015.25},
annote = {Keywords: online scheduling, flow-time, competitive analysis}
}
Document
On Correcting Inputs: Inverse Optimization for Online Structured Prediction
Abstract
Algorithm designers typically assume that the input data is correct, and then proceed to find "optimal" or "sub-optimal" solutions using this input data. However this assumption of correct data does not always hold in practice, especially in the context of online learning systems where the objective is to learn appropriate feature weights given some training samples. Such scenarios necessitate the study of inverse optimization problems where one is given an input instance as well as a desired output and the task is to adjust the input data so that the given output is indeed optimal. Motivated by learning structured prediction models, in this paper we consider inverse optimization with a margin, i.e., we require the given output to be better than all other feasible outputs by a desired margin. We consider such inverse optimization problems for maximum weight matroid basis, matroid intersection, perfect matchings, minimum cost maximum flows, and shortest paths and derive the first known results for such problems with a non-zero margin. The effectiveness of these algorithmic approaches to online learning for structured prediction is also discussed.
Cite as
Hal Daumé III, Samir Khuller, Manish Purohit, and Gregory Sanders. On Correcting Inputs: Inverse Optimization for Online Structured Prediction. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 38-51, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{daumeiii_et_al:LIPIcs.FSTTCS.2015.38,
author = {Daum\'{e} III, Hal and Khuller, Samir and Purohit, Manish and Sanders, Gregory},
title = {{On Correcting Inputs: Inverse Optimization for Online Structured Prediction}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {38--51},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.38},
URN = {urn:nbn:de:0030-drops-56375},
doi = {10.4230/LIPIcs.FSTTCS.2015.38},
annote = {Keywords: Inverse Optimization, Structured Prediction, Online Learning}
}
Document
Dynamic Sketching for Graph Optimization Problems with Applications to Cut-Preserving Sketches
Abstract
In this paper, we introduce a new model for sublinear algorithms called dynamic sketching. In this model, the underlying data is partitioned into a large static part and a small dynamic part and the goal is to compute a summary of the static part (i.e, a sketch) such that given any update for the dynamic part, one can combine it with the sketch to compute a given function. We say that a sketch is compact if its size is bounded by a polynomial function of the length of the dynamic data, (essentially) independent of the size of the static part.
A graph optimization problem P in this model is defined as follows. The input is a graph G(V,E) and a set T \subseteq V of k terminals; the edges between the terminals are the dynamic part and the other edges in G are the static part. The goal is to summarize the graph G into a compact sketch (of size poly(k)) such that given any set Q of edges between the terminals, one can answer the problem P for the graph obtained by inserting all edges in Q to G, using only the sketch.
We study the fundamental problem of computing a maximum matching and prove tight bounds on the sketch size. In particular, we show that there exists a (compact) dynamic sketch of size O(k^2) for the matching problem and any such sketch has to be of size \Omega(k^2). Our sketch for matchings can be further used to derive compact dynamic sketches for other fundamental graph problems involving cuts and connectivities. Interestingly, our sketch for matchings can also be used to give an elementary construction of a cut-preserving vertex sparsifier with space O(kC^2) for k-terminal graphs, which matches the best known upper bound; here C is the total capacity of the edges incident on the terminals. Additionally, we give an improved lower bound (in terms of C) of Omega(C/log{C}) on size of cut-preserving vertex sparsifiers, and establish that progress on dynamic sketching of the s-t max-flow problem (either upper bound or lower bound) immediately leads to better bounds for size of cut-preserving vertex sparsifiers.
Cite as
Sepehr Assadi, Sanjeev Khanna, Yang Li, and Val Tannen. Dynamic Sketching for Graph Optimization Problems with Applications to Cut-Preserving Sketches. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 52-68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{assadi_et_al:LIPIcs.FSTTCS.2015.52,
author = {Assadi, Sepehr and Khanna, Sanjeev and Li, Yang and Tannen, Val},
title = {{Dynamic Sketching for Graph Optimization Problems with Applications to Cut-Preserving Sketches}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {52--68},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.52},
URN = {urn:nbn:de:0030-drops-56361},
doi = {10.4230/LIPIcs.FSTTCS.2015.52},
annote = {Keywords: Small-space Algorithms, Maximum Matchings, Vertex Sparsifiers}
}
Document
Weighted Strategy Logic with Boolean Goals Over One-Counter Games
Abstract
Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in [Mogavero et al. Reasoning about strategies: On the model-checking problem. ACM ToCL 15(4),2014]. As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.
Cite as
Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Weighted Strategy Logic with Boolean Goals Over One-Counter Games. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 69-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2015.69,
author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {{Weighted Strategy Logic with Boolean Goals Over One-Counter Games}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {69--83},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.69},
URN = {urn:nbn:de:0030-drops-56537},
doi = {10.4230/LIPIcs.FSTTCS.2015.69},
annote = {Keywords: Temporal logics, multi-player games, strategy logic, quantitative games}
}
Document
Decidability in the Logic of Subsequences and Supersequences
Abstract
We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the Sigma_2 theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the FO^2 theory is decidable while the FO^3 theory is undecidable.
Cite as
Prateek Karandikar and Philippe Schnoebelen. Decidability in the Logic of Subsequences and Supersequences. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 84-97, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{karandikar_et_al:LIPIcs.FSTTCS.2015.84,
author = {Karandikar, Prateek and Schnoebelen, Philippe},
title = {{Decidability in the Logic of Subsequences and Supersequences}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {84--97},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.84},
URN = {urn:nbn:de:0030-drops-56428},
doi = {10.4230/LIPIcs.FSTTCS.2015.84},
annote = {Keywords: subsequence, subword, logic, first-order logic, decidability, piecewise- testability, Simon’s congruence}
}
Document
Fragments of Fixpoint Logic on Data Words
Abstract
We study fragments of a mu-calculus over data words whose primary modalities are 'go to next position' (X^g), 'go to previous position}' (Y^g), 'go to next position with the same data value' (X^c), 'go to previous position with the same data value (Y^c)'. Our focus is on two fragments that are called the bounded mode
alternation fragment (BMA) and the bounded reversal fragment (BR). BMA is the fragment of those formulas that whose unfoldings contain only a bounded number of alternations between global modalities (X^g, Y^g) and class modalities (X^c, Y^c). Similarly BR is the fragment of formulas whose unfoldings contain only a bounded number of alternations between left modalities (Y^g, Y^c) and right modalities (X^g, X^c). We show that these fragments are decidable (by inclusion in Data Automata), enjoy effective Boolean closure, and contain previously defined logics such as the two variable fragment of first-order logic and DataLTL. More precisely the definable language in each formalism obey the following inclusions that are effective.
FO^2 subsetneq DataLTL subsetneq BMA BR subsetneq nu subseteq Data Automata.
Our main contribution is a method to prove inexpressibility results on the fragment BMA by reducing them to inexpressibility results for combinatorial expressions. More precisely we prove the following hierarchy of definable languages,
emptyset=BMA^0 subsetneq BMA^1 subsetneq ... subsetneq BMA subsetneq BR , where BMA^k is the set of all formulas whose unfoldings contain at most k-1 alternations between global modalities (X^g, Y^g) and class modalities (X^c, Y^c). Since the class BMA is a generalization of FO^2 and DataLTL the inexpressibility results carry over to them as well.
Cite as
Thomas Colcombet and Amaldev Manuel. Fragments of Fixpoint Logic on Data Words. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 98-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2015.98,
author = {Colcombet, Thomas and Manuel, Amaldev},
title = {{Fragments of Fixpoint Logic on Data Words}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {98--111},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.98},
URN = {urn:nbn:de:0030-drops-56289},
doi = {10.4230/LIPIcs.FSTTCS.2015.98},
annote = {Keywords: Data words, Data automata, Fixpoint logic}
}
Document
Efficient Algorithms for Morphisms over Omega-Regular Languages
Abstract
Morphisms to finite semigroups can be used for recognizing omega-regular languages. The so-called strongly recognizing morphisms can be seen as a deterministic computation model which provides minimal objects (known as the syntactic morphism) and a trivial complementation procedure. We give a quadratic-time algorithm for computing the syntactic morphism from any given strongly recognizing morphism, thereby showing that minimization is easy as well. In addition, we give algorithms for efficiently solving various decision problems for weakly recognizing morphisms. Weakly recognizing morphism are often smaller than their strongly recognizing counterparts. Finally, we describe the language operations needed for converting formulas in monadic second-order logic (MSO) into strongly recognizing morphisms, and we give some experimental results.
Cite as
Lukas Fleischer and Manfred Kufleitner. Efficient Algorithms for Morphisms over Omega-Regular Languages. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 112-124, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fleischer_et_al:LIPIcs.FSTTCS.2015.112,
author = {Fleischer, Lukas and Kufleitner, Manfred},
title = {{Efficient Algorithms for Morphisms over Omega-Regular Languages}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {112--124},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.112},
URN = {urn:nbn:de:0030-drops-56200},
doi = {10.4230/LIPIcs.FSTTCS.2015.112},
annote = {Keywords: B\"{u}chi automata, omega-regular language, syntactic semigroup, recognizing morphism, MSO}
}
Document
Approximating the Regular Graphic TSP in Near Linear Time
Abstract
We present a randomized approximation algorithm for computing traveling salesperson tours in undirected regular graphs. Given an n-vertex, k-regular graph, the algorithm computes a tour of length at most (1+frac 4+ln 4+varepsilon ln k-O(1)n, with high probability, in O(nk log k) time. This improves upon the result by Vishnoi ([Vishnoi12],FOCS 2012) for the same problem, in terms of both approximation factor, and running time. Furthermore, our result is incomparable with the recent result by Feige, Ravi, and Singh ([FeigeRS14], IPCO 2014), since our algorithm runs in linear time, for any fixed k. The key ingredient of our algorithm is a technique that uses edge-coloring algorithms to sample a cycle cover with O(n/log k) cycles, with high probability, in near linear time.
Additionally, we also give a deterministic frac{3}{2}+O(frac{1}sqrt{k}) factor approximation algorithm for the TSP on n-vertex, k-regular graphs running in time O(nk).
Cite as
Ashish Chiplunkar and Sundar Vishwanathan. Approximating the Regular Graphic TSP in Near Linear Time. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 125-135, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{chiplunkar_et_al:LIPIcs.FSTTCS.2015.125,
author = {Chiplunkar, Ashish and Vishwanathan, Sundar},
title = {{Approximating the Regular Graphic TSP in Near Linear Time}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {125--135},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.125},
URN = {urn:nbn:de:0030-drops-56264},
doi = {10.4230/LIPIcs.FSTTCS.2015.125},
annote = {Keywords: traveling salesperson problem, approximation, linear time}
}
Document
On Weighted Bipartite Edge Coloring
Abstract
We study weighted bipartite edge coloring problem, which is a generalization of two classical problems: bin packing and edge coloring. This problem has been inspired from the study of Clos networks in multirate switching environment in communication networks. In weighted bipartite edge coloring problem, we are given an edge-weighted bipartite multi-graph G=(V,E) with weights
w:E\rightarrow [0,1]. The goal is to find a proper
weighted coloring of the edges with as few colors as possible. An
edge coloring of the weighted graph is called a proper
weighted coloring if the sum of the weights of the edges incident
to a vertex of any color is at most one. Chung and Ross conjectured 2m-1 colors are sufficient for a proper weighted coloring, where m denotes the minimum number of unit sized bins needed to pack the weights of all edges incident at any vertex. We give an algorithm that returns a coloring with at most \lceil 2.2223m \rceil colors improving on the previous result of \frac{9m}{4} by Feige and Singh.
Our algorithm is purely combinatorial and combines the König's theorem for edge coloring bipartite graphs and first-fit decreasing heuristic for bin packing. However, our analysis uses configuration linear program for the bin packing problem to give the improved result.
Cite as
Arindam Khan and Mohit Singh. On Weighted Bipartite Edge Coloring. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 136-150, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{khan_et_al:LIPIcs.FSTTCS.2015.136,
author = {Khan, Arindam and Singh, Mohit},
title = {{On Weighted Bipartite Edge Coloring}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {136--150},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.136},
URN = {urn:nbn:de:0030-drops-56437},
doi = {10.4230/LIPIcs.FSTTCS.2015.136},
annote = {Keywords: Edge coloring, Bin packing, Clos networks, Approximation algorithms, Graph algorithms}
}
Document
Deciding Orthogonality in Construction-A Lattices
Abstract
Lattices are discrete mathematical objects with widespread applications to integer programs as well as modern cryptography. A fundamental problem in both domains is the Closest Vector Problem (popularly known as CVP). It is well-known that CVP can be easily solved in lattices that have an orthogonal basis if the orthogonal basis is specified. This motivates the orthogonality decision problem: verify whether a given lattice has an orthogonal basis. Surprisingly, the orthogonality decision problem is not known to be either NP-complete or in P.
In this paper, we focus on the orthogonality decision problem for a well-known family of lattices, namely Construction-A lattices. These are lattices of the form C + qZ^n, where C is an error-correcting q-ary code, and are studied in communication settings. We provide a complete characterization of lattices obtained from binary and ternary codes using Construction- A that have an orthogonal basis. This characterization leads to an efficient algorithm solving the orthogonality decision problem, which also finds an orthogonal basis if one exists for this family of lattices. We believe that these results could provide a better understanding of the complexity of the orthogonality decision problem in general.
Cite as
Karthekeyan Chandrasekaran, Venkata Gandikota, and Elena Grigorescu. Deciding Orthogonality in Construction-A Lattices. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 151-162, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{chandrasekaran_et_al:LIPIcs.FSTTCS.2015.151,
author = {Chandrasekaran, Karthekeyan and Gandikota, Venkata and Grigorescu, Elena},
title = {{Deciding Orthogonality in Construction-A Lattices}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {151--162},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.151},
URN = {urn:nbn:de:0030-drops-56509},
doi = {10.4230/LIPIcs.FSTTCS.2015.151},
annote = {Keywords: Orthogonal Lattices, Construction-A, Orthogonal Decomposition, Lattice isomorphism}
}
Document
Ordered Tree-Pushdown Systems
Abstract
We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application, we show that our simple model can encode several formalisms generalizing pushdown systems, such as ordered multi-pushdown systems, annotated higher-order pushdown systems, the Krivine machine, and ordered annotated multi-pushdown systems. In each case, our procedure yields tight complexity.
Cite as
Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz. Ordered Tree-Pushdown Systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 163-177, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{clemente_et_al:LIPIcs.FSTTCS.2015.163,
author = {Clemente, Lorenzo and Parys, Pawel and Salvati, Sylvain and Walukiewicz, Igor},
title = {{Ordered Tree-Pushdown Systems}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {163--177},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.163},
URN = {urn:nbn:de:0030-drops-56470},
doi = {10.4230/LIPIcs.FSTTCS.2015.163},
annote = {Keywords: reachability analysis, saturation technique, pushdown automata, ordered pushdown automata, higher-order pushdown automata, higher-order recursive sche}
}
Document
One-way Definability of Sweeping Transducer
Abstract
Two-way finite-state transducers on words are strictly more expressive than one-way transducers. It has been shown recently how to decide if a two-way functional transducer has an equivalent one-way transducer, and the complexity of the algorithm is non-elementary. We propose an alternative and simpler characterization for sweeping functional transducers, namely, for transducers that can only reverse their head direction at the extremities of the input. Our algorithm works in 2EXPSPACE and, in the positive case, produces an equivalent one-way transducer of doubly exponential size. We also show that the bound on the size of the transducer is tight, and that the one-way definability problem is undecidable for (sweeping) non-functional transducers.
Cite as
Félix Baschenis, Olivier Gauwin, Anca Muscholl, and Gabriele Puppis. One-way Definability of Sweeping Transducer. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 178-191, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{baschenis_et_al:LIPIcs.FSTTCS.2015.178,
author = {Baschenis, F\'{e}lix and Gauwin, Olivier and Muscholl, Anca and Puppis, Gabriele},
title = {{One-way Definability of Sweeping Transducer}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {178--191},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.178},
URN = {urn:nbn:de:0030-drops-56297},
doi = {10.4230/LIPIcs.FSTTCS.2015.178},
annote = {Keywords: Regular word transductions, sweeping transducers, one-way definability}
}
Document
What's Decidable about Availability Languages?
Abstract
We study here the algorithmic analysis of systems modeled in terms of availability languages. Our first main result is a positive answer to the emptiness problem: it is decidable whether a given availability language contains a word. The key idea is an inductive construction that replaces availability languages with Parikh-equivalent regular languages. As a second contribution, we solve the intersection problem modulo bounded languages: given availability languages and a bounded language, it is decidable whether the intersection of the former contains a word from the bounded language. We show that the problem is NP-complete. The idea is to reduce to satisfiability of existential Presburger arithmetic. Since the (general) intersection problem for availability languages is known to be undecidable, our results characterize the decidability border for this model. Our last contribution is a study of the containment problem between regular and availability languages. We show that safety verification, i.e., checking containment of an availability language in a regular language, is decidable. The containment problem of regular languages in availability languages is proven undecidable.
Cite as
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi. What's Decidable about Availability Languages?. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 192-205, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2015.192,
author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Meyer, Roland and Seyed Salehi, Mehdi},
title = {{What's Decidable about Availability Languages?}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {192--205},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.192},
URN = {urn:nbn:de:0030-drops-56602},
doi = {10.4230/LIPIcs.FSTTCS.2015.192},
annote = {Keywords: Availability, formal languages, emptiness, decidability}
}
Document
Towards Better Separation between Deterministic and Randomized Query Complexity
Abstract
We show that there exists a Boolean function F which gives the following separations among deterministic query complexity (D(F)), randomized zero error query complexity (R_0(F)) and randomized one-sided error query complexity (R_1(F)): R_1(F) = ~O(sqrt{D(F)) and R_0(F)=~O(D(F))^3/4. This refutes the conjecture made by Saks and Wigderson that for any Boolean function f, R_0(f)=Omega(D(f))^0.753.. . This also shows widest separation between R_1(f) and D(f) for any Boolean function. The function F was defined by Göös, Pitassi and Watson who studied it for showing a separation between deterministic decision tree complexity and unambiguous non-deterministic decision tree complexity. Independently of us, Ambainis et al proved that different variants of the function F certify optimal (quadratic) separation between D(f) and R_0(f), and polynomial separation between R_0(f) and R_1(f). Viewed as separation results, our results are subsumed by those of Ambainis et al. However, while the functions considered in the work of Ambainis et al are different variants of F, in this work we show that the original function F itself is sufficient to refute the Saks-Wigderson conjecture and obtain widest possible separation between the deterministic and one-sided error randomized query complexity.
Cite as
Sagnik Mukhopadhyay and Swagato Sanyal. Towards Better Separation between Deterministic and Randomized Query Complexity. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 206-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{mukhopadhyay_et_al:LIPIcs.FSTTCS.2015.206,
author = {Mukhopadhyay, Sagnik and Sanyal, Swagato},
title = {{Towards Better Separation between Deterministic and Randomized Query Complexity}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {206--220},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.206},
URN = {urn:nbn:de:0030-drops-56467},
doi = {10.4230/LIPIcs.FSTTCS.2015.206},
annote = {Keywords: Deterministic Decision Tree, Randomized Decision Tree, Query Complexity, Models of Computation.}
}
Document
Dimension, Pseudorandomness and Extraction of Pseudorandomness
Abstract
In this paper we propose a quantification of distributions on a set of strings, in terms of how close to pseudorandom a distribution is. The quantification is an adaptation of the theory of dimension of sets of infinite sequences introduced by Lutz. Adapting Hitchcock's work, we also show that the logarithmic loss incurred by a predictor on a distribution is quantitatively equivalent to the notion of dimension we define. Roughly, this captures the equivalence between pseudorandomness defined via indistinguishability and via unpredictability. Later we show some natural properties of our notion of dimension. We also do a comparative study among our proposed notion of dimension and two well known notions of computational analogue of entropy, namely HILL-type pseudo min-entropy and next-bit pseudo Shannon entropy.
Further, we apply our quantification to the following problem. If we know that the dimension of a distribution on the set of n-length strings is s in (0,1], can we extract out O(sn) pseudorandom bits out of the distribution? We show that to construct such extractor, one need at least Omega(log n) bits of pure randomness. However, it is still open to do the same using O(log n) random bits. We show that deterministic extraction is possible in a special case - analogous to the bit-fixing sources introduced by Chor et al., which we term nonpseudorandom bit-fixing source. We adapt the techniques of Gabizon, Raz and Shaltiel to construct a deterministic pseudorandom extractor for this source.
By the end, we make a little progress towards P vs. BPP problem by showing that existence of optimal stretching function that stretches O(log n) input bits to produce n output bits such that output distribution has dimension s in (0,1], implies P=BPP.
Cite as
Manindra Agrawal, Diptarka Chakraborty, Debarati Das, and Satyadev Nandakumar. Dimension, Pseudorandomness and Extraction of Pseudorandomness. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 221-235, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{agrawal_et_al:LIPIcs.FSTTCS.2015.221,
author = {Agrawal, Manindra and Chakraborty, Diptarka and Das, Debarati and Nandakumar, Satyadev},
title = {{Dimension, Pseudorandomness and Extraction of Pseudorandomness}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {221--235},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.221},
URN = {urn:nbn:de:0030-drops-56184},
doi = {10.4230/LIPIcs.FSTTCS.2015.221},
annote = {Keywords: Pseudorandomness, Dimension, Martingale, Unpredictability, Pseudoentropy, Pseudorandom Extractor, Hard Function}
}
Document
On the NP-Completeness of the Minimum Circuit Size Problem
Abstract
We study the Minimum Circuit Size Problem (MCSP): given the
truth-table of a Boolean function f and a number k, does there
exist a Boolean circuit of size at most k computing f? This is a
fundamental NP problem that is not known to be NP-complete. Previous
work has studied consequences of the NP-completeness of MCSP. We
extend this work and consider whether MCSP may be complete for NP
under more powerful reductions. We also show that NP-completeness of
MCSP allows for amplification of circuit complexity.
We show the following results.
- If MCSP is NP-complete via many-one reductions, the following circuit complexity amplification result holds: If NP cap co-NP requires 2^n^{Omega(1)-size circuits, then E^NP requires 2^Omega(n)-size circuits.
- If MCSP is NP-complete under truth-table reductions, then
EXP neq NP cap SIZE(2^n^epsilon) for some epsilon> 0 and EXP neq ZPP. This result extends to polylog Turing reductions.
Cite as
John M. Hitchcock and A. Pavan. On the NP-Completeness of the Minimum Circuit Size Problem. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 236-245, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hitchcock_et_al:LIPIcs.FSTTCS.2015.236,
author = {Hitchcock, John M. and Pavan, A.},
title = {{On the NP-Completeness of the Minimum Circuit Size Problem}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {236--245},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.236},
URN = {urn:nbn:de:0030-drops-56613},
doi = {10.4230/LIPIcs.FSTTCS.2015.236},
annote = {Keywords: Minimum Circuit Size, NP-completeness, truth-table reductions, circuit complexity}
}
Document
Counting Euler Tours in Undirected Bounded Treewidth Graphs
Abstract
We show that counting Euler tours in undirected bounded tree-width graphs is tractable even in parallel - by proving a GapL upper bound. This is in stark contrast to #P-completeness of the same problem in general graphs.
Our main technical contribution is to show how (an instance of) dynamic programming on bounded clique-width graphs can be performed efficiently in parallel. Thus we show that the sequential result of Espelage, Gurski and Wanke for efficiently computing Hamiltonian paths in bounded clique-width graphs can be adapted in the parallel setting to count the number of Hamiltonian paths which in turn is a tool for counting the number of Euler tours in bounded tree-width graphs. Our technique also yields parallel algorithms for counting longest paths and bipartite perfect matchings in bounded-clique width graphs.
While establishing that counting Euler tours in bounded tree-width graphs can be computed by non-uniform monotone arithmetic circuits of polynomial degree (which characterize #SAC^1) is relatively easy, establishing a uniform #SAC^1 bound needs a careful use of polynomial interpolation.
Cite as
Nikhil Balaji, Samir Datta, and Venkatesh Ganesan. Counting Euler Tours in Undirected Bounded Treewidth Graphs. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 246-260, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{balaji_et_al:LIPIcs.FSTTCS.2015.246,
author = {Balaji, Nikhil and Datta, Samir and Ganesan, Venkatesh},
title = {{Counting Euler Tours in Undirected Bounded Treewidth Graphs}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {246--260},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.246},
URN = {urn:nbn:de:0030-drops-56493},
doi = {10.4230/LIPIcs.FSTTCS.2015.246},
annote = {Keywords: Euler Tours, Bounded Treewidth, Bounded clique-width, Hamiltonian cycles, Parallel algorithms}
}
Document
Revisiting Robustness in Priced Timed Games
Abstract
Priced timed games are optimal-cost reachability games played between
two players---the controller and the environment---by moving a token along the edges of infinite graphs of configurations of priced timed automata. The goal of the controller is to reach a given set of target locations as cheaply as possible, while the goal of the environment is the opposite. Priced timed games are known to be undecidable for timed automata with 3 or more clocks, while they are known to be decidable for automata with 1 clock. In an attempt to recover decidability for priced timed games Bouyer, Markey, and Sankur studied robust priced timed games where the environment has the power to slightly perturb delays proposed by the controller.
Unfortunately, however, they showed that the natural problem of deciding the existence of optimal limit-strategy---optimal strategy of the controller where the perturbations tend to vanish in the limit---is undecidable with 10 or more clocks. In this paper we revisit this problem and improve our understanding of the decidability of these games. We show that the limit-strategy problem is already undecidable for a subclass of robust priced timed games with 5 or more clocks. On a positive side, we show the decidability of the existence of almost optimal strategies for the same subclass of one-clock robust priced timed games by adapting a classical construction by Bouyer at al. for one-clock priced timed games.
Cite as
Shibashis Guha, Shankara Narayanan Krishna, Lakshmi Manasa, and Ashutosh Trivedi. Revisiting Robustness in Priced Timed Games. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 261-277, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{guha_et_al:LIPIcs.FSTTCS.2015.261,
author = {Guha, Shibashis and Krishna, Shankara Narayanan and Manasa, Lakshmi and Trivedi, Ashutosh},
title = {{Revisiting Robustness in Priced Timed Games}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {261--277},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.261},
URN = {urn:nbn:de:0030-drops-56440},
doi = {10.4230/LIPIcs.FSTTCS.2015.261},
annote = {Keywords: Priced Timed Games, Decidability, Optimal strategies, Robustness}
}
Document
Simple Priced Timed Games are not That Simple
Abstract
Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modeling the costs of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary (positive and negative) weights and show that, for an important subclass of theirs (the so-called simple priced timed games), one can compute, in exponential time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called reset-acyclic priced timed games (with arbitrary weights and one-clock).
Cite as
Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. Simple Priced Timed Games are not That Simple. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 278-292, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{brihaye_et_al:LIPIcs.FSTTCS.2015.278,
author = {Brihaye, Thomas and Geeraerts, Gilles and Haddad, Axel and Lefaucheux, Engel and Monmege, Benjamin},
title = {{Simple Priced Timed Games are not That Simple}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {278--292},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.278},
URN = {urn:nbn:de:0030-drops-56235},
doi = {10.4230/LIPIcs.FSTTCS.2015.278},
annote = {Keywords: Priced timed games, real-time systems, game theory}
}
Document
Quantitative Games under Failures
Abstract
We study a generalisation of sabotage games, a model of dynamic network games introduced by van Benthem. The original definition of the game is inherently finite and therefore does not allow one to model infinite processes. We propose an extension of the sabotage games in which the first player (Runner) traverses an arena with dynamic weights determined by the second player (Saboteur). In our model of quantitative sabotage games, Saboteur is now given a budget that he can distribute amongst the edges of the graph, whilst Runner attempts to minimise the quantity of budget witnessed while completing his task. We show that, on the one hand, for most of the classical cost functions considered in the literature, the problem of determining if Runner has a strategy to ensure a cost below some threshold is EXPTIME-complete. On the other hand, if the budget of Saboteur is fixed a priori, then the problem is in PTIME for most cost functions. Finally, we show that restricting the dynamics of the game also leads to better complexity.
Cite as
Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Benjamin Monmege, Guillermo A. Pérez, and Gabriel Renault. Quantitative Games under Failures. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 293-306, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{brihaye_et_al:LIPIcs.FSTTCS.2015.293,
author = {Brihaye, Thomas and Geeraerts, Gilles and Haddad, Axel and Monmege, Benjamin and P\'{e}rez, Guillermo A. and Renault, Gabriel},
title = {{Quantitative Games under Failures}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {293--306},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.293},
URN = {urn:nbn:de:0030-drops-56229},
doi = {10.4230/LIPIcs.FSTTCS.2015.293},
annote = {Keywords: Quantitative games, verification, synthesis, game theory}
}
Document
Games with Delays - A Frankenstein Approach
Abstract
We investigate infinite games on finite graphs where the information flow is perturbed by non- deterministic signalling delays. It is known that such perturbations make synthesis problems virtually unsolvable, in the general case. On the classical model where signals are attached to states, tractable cases are rare and difficult to identify.
In this paper, we propose a model where signals are detached from control states, and we identify a subclass on which equilibrium outcomes can be preserved, even if signals are delivered with a delay that is finitely bounded. To offset the perturbation, our solution procedure combines responses from a collection of virtual plays following an equilibrium strategy in the instant- signalling game to synthesise, in a Dr. Frankenstein manner, an equivalent equilibrium strategy for the delayed-signalling game.
Cite as
Dietmar Berwanger and Marie van den Bogaard. Games with Delays - A Frankenstein Approach. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 307-319, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{berwanger_et_al:LIPIcs.FSTTCS.2015.307,
author = {Berwanger, Dietmar and van den Bogaard, Marie},
title = {{Games with Delays - A Frankenstein Approach}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {307--319},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.307},
URN = {urn:nbn:de:0030-drops-56575},
doi = {10.4230/LIPIcs.FSTTCS.2015.307},
annote = {Keywords: infinite games on graphs, imperfect information, delayed monitoring, distributed synthesis}
}
Document
Forbidden Extension Queries
Abstract
Document retrieval is one of the most fundamental problem in information retrieval. The objective is to retrieve all documents from a document collection that are relevant to an input pattern.
Several variations of this problem such as ranked document retrieval, document listing with two patterns and forbidden patterns have been studied. We introduce the problem of document retrieval with forbidden extensions.
Let D={T_1,T_2,...,T_D} be a collection of D string documents of n characters in total, and P^+ and P^- be two query patterns, where P^+ is a proper prefix of P^-. We call P^- as the forbidden extension of the included pattern P^+. A forbidden extension query < P^+,P^- > asks to report all occ documents in D that contains P^+ as a substring, but does not contain P^- as one. A top-k forbidden extension query < P^+,P^-,k > asks to report those k documents among the occ documents that are most relevant to P^+. We present a linear index (in words) with an O(|P^-| + occ) query time for the document listing problem. For the top-k version of the problem, we achieve the following results, when the relevance of a document is based on PageRank:
- an O(n) space (in words) index with O(|P^-|log sigma+ k) query time, where sigma is the size of the alphabet from which characters in D are chosen. For constant alphabets, this yields an optimal query time of O(|P^-|+ k).
- for any constant epsilon > 0, a |CSA| + |CSA^*| + Dlog frac{n}{D} + O(n) bits index with O(search(P)+ k cdot tsa cdot log ^{2+epsilon} n) query time, where search(P) is the time to find the suffix range of a pattern P, tsa is the time to find suffix (or inverse suffix) array value, and |CSA^*| denotes the maximum of the space needed to store the compressed suffix array CSA of the concatenated text of all documents, or the total space needed to store the individual CSA of each document.
Cite as
Sudip Biswas, Arnab Ganguly, Rahul Shah, and Sharma V. Thankachan. Forbidden Extension Queries. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 320-335, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{biswas_et_al:LIPIcs.FSTTCS.2015.320,
author = {Biswas, Sudip and Ganguly, Arnab and Shah, Rahul and Thankachan, Sharma V.},
title = {{Forbidden Extension Queries}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {320--335},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.320},
URN = {urn:nbn:de:0030-drops-56522},
doi = {10.4230/LIPIcs.FSTTCS.2015.320},
annote = {Keywords: document retrieval, suffix trees, range queries, succinct data structure}
}
Document
On Density, Threshold and Emptiness Queries for Intervals in the Streaming Model
Abstract
In this paper, we study the maximum density, threshold and emptiness
queries for intervals in the streaming model. The input is a stream S
of n points in the real line R and a floating closed interval W of width alpha. The specific problems we consider in this paper are as follows.
- Maximum density: find a placement of W in R containing the
maximum number of points of S.
- Threshold query: find a placement of W in R, if it exists,
that contains at least Delta elements of S.
- Emptiness query: find, if possible, a placement of W within the extent of S so that the interior of W does not contain any element of S.
The stream S, being huge, does not fit into main memory and can be read sequentially at most a constant number of times, usually once.
The problems studied here in the geometric setting have relations to frequency estimation and heavy hitter identification in a stream of data. We provide lower bounds and results on trade-off between extra space and quality of solution. We also discuss generalizations for the higher dimensional variants for a few cases.
Cite as
Arijit Bishnu, Amit Chakrabarti, Subhas C. Nandy, and Sandeep Sen. On Density, Threshold and Emptiness Queries for Intervals in the Streaming Model. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 336-349, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{bishnu_et_al:LIPIcs.FSTTCS.2015.336,
author = {Bishnu, Arijit and Chakrabarti, Amit and Nandy, Subhas C. and Sen, Sandeep},
title = {{On Density, Threshold and Emptiness Queries for Intervals in the Streaming Model}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {336--349},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.336},
URN = {urn:nbn:de:0030-drops-56488},
doi = {10.4230/LIPIcs.FSTTCS.2015.336},
annote = {Keywords: Density, threshold, emptiness queries, interval queries, streaming model, heavy hitter, frequency estimation}
}
Document
Clustering on Sliding Windows in Polylogarithmic Space
Abstract
In PODS 2003, Babcock, Datar, Motwani and O'Callaghan gave the first streaming solution for the k-median problem on sliding windows using
O(frack k tau^4 W^2tau log^2 W) space, with a O(2^O(1/tau)) approximation factor, where W is the window size and tau in (0,1/2) is a user-specified parameter. They left as an open question whether it is possible to improve this to polylogarithmic space. Despite much progress on clustering and sliding windows, this question has remained open for more than a decade.
In this paper, we partially answer the main open question posed by Babcock, Datar, Motwani and O'Callaghan. We present an algorithm yielding an exponential improvement in space compared to the previous result given in Babcock, et al. In particular, we give the first polylogarithmic space (alpha,beta)-approximation for metric k-median clustering in the sliding window model, where alpha and beta are constants, under the assumption, also made by Babcock et al., that the optimal k-median cost on any given window is bounded by a polynomial in the window size. We justify this assumption by showing that when the cost is exponential in the window size, no sublinear space approximation is possible. Our main technical contribution is a simple but elegant extension of smooth functions as introduced by Braverman and Ostrovsky, which allows us to apply well-known techniques for solving problems in the sliding window model
to functions that are not smooth, such as the k-median cost.
Cite as
Vladimir Braverman, Harry Lang, Keith Levin, and Morteza Monemizadeh. Clustering on Sliding Windows in Polylogarithmic Space. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 350-364, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{braverman_et_al:LIPIcs.FSTTCS.2015.350,
author = {Braverman, Vladimir and Lang, Harry and Levin, Keith and Monemizadeh, Morteza},
title = {{Clustering on Sliding Windows in Polylogarithmic Space}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {350--364},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.350},
URN = {urn:nbn:de:0030-drops-56549},
doi = {10.4230/LIPIcs.FSTTCS.2015.350},
annote = {Keywords: Streaming, Clustering, Sliding windows}
}
Document
Congestion Games with Multisets of Resources and Applications in Synthesis
Abstract
In classical congestion games, players' strategies are subsets of resources. We introduce and study multiset congestion games, where players' strategies are multisets of resources. Thus, in each strategy a player may need to use each resource a different number of times, and his cost for using the resource depends on the load that he and the other players generate on the resource.
Beyond the theoretical interest in examining the effect of a repeated use of resources, our study enables better understanding of non-cooperative systems and environments whose behavior is not covered by previously studied models. Indeed, congestion games with multiset-strategies arise, for example, in production planing
and network formation with tasks that are more involved than reachability. We study in detail the application of synthesis from component libraries: different users synthesize systems by gluing together components from a component library. A component may be used in several systems and may be used several times in a system. The performance of a component and hence the system's quality depends on the load on it.
Our results reveal how the richer setting of multisets congestion games affects the stability and equilibrium efficiency compared to standard congestion games. In particular, while we present very simple instances with no pure Nash equilibrium and prove tighter and simpler lower bounds for equilibrium inefficiency, we are also able to show that some of the positive results known for affine and weighted congestion games apply to the richer setting of multisets.
Cite as
Guy Avni, Orna Kupferman, and Tami Tamir. Congestion Games with Multisets of Resources and Applications in Synthesis. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 365-379, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{avni_et_al:LIPIcs.FSTTCS.2015.365,
author = {Avni, Guy and Kupferman, Orna and Tamir, Tami},
title = {{Congestion Games with Multisets of Resources and Applications in Synthesis}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {365--379},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.365},
URN = {urn:nbn:de:0030-drops-56358},
doi = {10.4230/LIPIcs.FSTTCS.2015.365},
annote = {Keywords: Congestion games, Multiset strategies, Equilibrium existence and computation, Equilibrium inefficiency}
}
Document
The Sensing Cost of Monitoring and Synthesis
Abstract
In FSTTCS 2014, we introduced sensing as a new complexity measure for the complexity of regular languages. Intuitively, the sensing cost quantifies the detail in which a random input word has to be read by a deterministic automaton in order to decide its membership in the language. In this paper, we consider sensing in two principal applications of deterministic automata. The first is monitoring: we are given a computation in an on-line manner, and we have to decide whether it satisfies the specification. The second is synthesis: we are given a sequence of inputs in an on-line manner and we have to generate a sequence of outputs so that the resulting computation satisfies the specification. In the first, our goal is to design a monitor that handles all computations and minimizes the expected average number of sensors used in the monitoring process. In the second, our goal is to design a transducer that realizes the specification for all input sequences and minimizes the expected average number of sensors used for reading the inputs.
We argue that the two applications require new and different frameworks for reasoning about sensing, and develop such frameworks. We focus on safety languages. We show that for monitoring, minimal sensing is attained by a monitor
based on the minimal deterministic automaton for the language. For synthesis, however, the setting is
more challenging: minimizing the sensing may require exponentially bigger transducers, and the problem of synthesizing a minimally-sensing transducer is EXPTIME-complete even for safety specifications given by deterministic automata.
Cite as
Shaull Almagor, Denis Kuperberg, and Orna Kupferman. The Sensing Cost of Monitoring and Synthesis. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 380-393, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.FSTTCS.2015.380,
author = {Almagor, Shaull and Kuperberg, Denis and Kupferman, Orna},
title = {{The Sensing Cost of Monitoring and Synthesis}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {380--393},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.380},
URN = {urn:nbn:de:0030-drops-56563},
doi = {10.4230/LIPIcs.FSTTCS.2015.380},
annote = {Keywords: Automata, regular languages, omega-regular languages, complexity, sensing, minimization}
}
Document
An omega-Algebra for Real-Time Energy Problems
Abstract
We develop a *-continuous Kleene omega-algebra of real-time energy functions. Together with corresponding automata, these can be used to model systems which can consume and regain energy (or other types of resources) depending on available time. Using recent results on *-continuous Kleene omega-algebras and computability of certain manipulations on real-time energy functions, it follows that reachability and Büchi acceptance in real-time energy automata can be decided in a static way which only involves manipulations of real-time energy functions.
Cite as
David Cachera, Uli Fahrenberg, and Axel Legay. An omega-Algebra for Real-Time Energy Problems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 394-407, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{cachera_et_al:LIPIcs.FSTTCS.2015.394,
author = {Cachera, David and Fahrenberg, Uli and Legay, Axel},
title = {{An omega-Algebra for Real-Time Energy Problems}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {394--407},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.394},
URN = {urn:nbn:de:0030-drops-56511},
doi = {10.4230/LIPIcs.FSTTCS.2015.394},
annote = {Keywords: Energy problem, Real time, Star-continuous Kleene algebra}
}
Document
Parameterized Complexity of Secluded Connectivity Problems
Abstract
The Secluded Path problem introduced by Chechik et al. in [ESA 2013] models a situation where a sensitive information has to be transmitted between a pair of nodes along a path in a network.
The measure of the quality of a selected path is its exposure, which is the total weight of vertices in its closed neighborhood. In order to minimize the risk of intercepting the information, we are interested in selecting a secluded path, i.e. a path with a small exposure. Similarly, the Secluded Steiner Tree problem is to find a tree in a graph connecting a given set of terminals such that the exposure of the tree is minimized. In this work, we obtain the following results about parameterized complexity of secluded connectivity problems.
We start from an observation that being parameterized by the size of the exposure, the problem is fixed-parameter tractable (FPT). More precisely, we give an algorithm deciding if a graph G with a given cost function w:V(G)->N contains a secluded path of exposure at most k with the cost at most C in time O(3^{k/3}(n+m) log W), where W is the maximum value of w on an input graph G. Similarly,
Secluded Steiner Tree is solvable in time O(2^{k}k^2 (n+m) log W).
The main result of this paper is about "above guarantee" parameterizations for secluded problems. We show that Secluded Steiner Tree is FPT being parameterized by r+p, where p is the number of the terminals, l the size of an optimum Steiner tree, and r=k-l. We complement this result by showing that the problem is co-W[1]-hard when parameterized by r only.
We also investigate Secluded Steiner Tree from kernelization perspective and provide several lower and upper bounds when parameters are the treewidth, the size of a vertex cover, maximum vertex degree and the solution size. Finally, we refine the algorithmic result of Chechik et al. by improving the exponential dependence from the treewidth of the input graph.
Cite as
Fedor V. Fomin, Petr A. Golovach, Nikolay Karpov, and Alexander S. Kulikov. Parameterized Complexity of Secluded Connectivity Problems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 408-419, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fomin_et_al:LIPIcs.FSTTCS.2015.408,
author = {Fomin, Fedor V. and Golovach, Petr A. and Karpov, Nikolay and Kulikov, Alexander S.},
title = {{Parameterized Complexity of Secluded Connectivity Problems}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {408--419},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.408},
URN = {urn:nbn:de:0030-drops-56318},
doi = {10.4230/LIPIcs.FSTTCS.2015.408},
annote = {Keywords: Secluded path, Secluded Steiner tree, parameterized complexity}
}
Document
Parameterized Algorithms for Deletion to (r,ell)-Graphs
Abstract
For fixed integers r,ell geq 0, a graph G is called an (r,ell)-graph if the vertex set V(G) can be partitioned into r independent sets and ell cliques. This brings us to the following natural parameterized questions: Vertex (r,ell)-Partization and Edge (r,ell)-Partization. An input to these problems consist of a graph G and a positive integer k and the objective is to decide whether there exists a set S subseteq V(G) (S subseteq E(G)) such that the deletion of S from G results in an (r,ell)-graph. These problems generalize well studied problems such as Odd Cycle Transversal, Edge Odd Cycle Transversal, Split Vertex Deletion and Split Edge Deletion. We do not hope to get parameterized algorithms for either Vertex (r, ell)-Partization or Edge (r,ell)-Partization when either of r or ell is at least 3 as the recognition problem itself is NP-complete. This leaves the case of r,ell in {1,2}. We almost complete the parameterized complexity dichotomy for these problems by obtaining the following results:
- We show that Vertex (r,ell)-Partization is fixed parameter tractable (FPT) for r,ell in {1,2}. Then we design an Oh(sqrt log n)-factor approximation algorithms for these problems. These approximation algorithms are then utilized to design polynomial sized randomized Turing kernels for these problems.
- Edge (r,ell)-Partization is FPT when (r,ell)in{(1,2),(2,1)}. However, the parameterized complexity of Edge (2,2)-Partization remains open.
For our approximation algorithms and thus for Turing kernels we use
an interesting finite forbidden induced graph characterization, for a class of graphs known as (r,ell)-split graphs, properly containing the class of (r,ell)-graphs. This approach to obtain approximation algorithms could be of an independent interest.
Cite as
Sudeshna Kolay and Fahad Panolan. Parameterized Algorithms for Deletion to (r,ell)-Graphs. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 420-433, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kolay_et_al:LIPIcs.FSTTCS.2015.420,
author = {Kolay, Sudeshna and Panolan, Fahad},
title = {{Parameterized Algorithms for Deletion to (r,ell)-Graphs}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {420--433},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.420},
URN = {urn:nbn:de:0030-drops-56456},
doi = {10.4230/LIPIcs.FSTTCS.2015.420},
annote = {Keywords: FPT, Turing kernels, Approximation algorithms}
}
Document
Finding Even Subgraphs Even Faster
Abstract
Problems of the following kind have been the focus of much recent research in the realm of parameterized complexity: Given an input graph (digraph) on n vertices and a positive integer parameter k, find if there exist k edges(arcs) whose deletion results in a graph that satisfies some specified parity constraints. In particular, when the objective is to obtain a connected graph in which all the
vertices have even degrees--where the resulting graph is Eulerian,the problem is called Undirected Eulerian Edge Deletion. The corresponding
problem in digraphs where the resulting graph should be strongly connected and every vertex should have the same in-degree as its
out-degree is called Directed Eulerian Edge Deletion. Cygan et al.[Algorithmica, 2014] showed that these problems are fixed parameter tractable (FPT), and gave algorithms with the running time
2^O(k log k)n^O(1). They also asked, as an open problem, whether there exist FPT algorithms which solve these problems in time
2^O(k)n^O(1). It was also posed as an open problem at the School on Parameterized Algorithms and Complexity 2014, Bedlewo, Poland.
In this paper we answer their question in the affirmative: using the technique of computing representative families of co-graphic matroids we design algorithms which solve these problems in time 2^O(k)n^O(1). The crucial insight we bring to these problems is to view the solution as an independent set of a co-graphic matroid. We believe that this view-point/approach will be useful in other problems where one of the constraints that need to be satisfied is that of connectivity.
Cite as
Prachi Goyal, Pranabendu Misra, Fahad Panolan, Geevarghese Philip, and Saket Saurabh. Finding Even Subgraphs Even Faster. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 434-447, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{goyal_et_al:LIPIcs.FSTTCS.2015.434,
author = {Goyal, Prachi and Misra, Pranabendu and Panolan, Fahad and Philip, Geevarghese and Saurabh, Saket},
title = {{Finding Even Subgraphs Even Faster}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {434--447},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.434},
URN = {urn:nbn:de:0030-drops-56336},
doi = {10.4230/LIPIcs.FSTTCS.2015.434},
annote = {Keywords: Eulerian Edge Deletion, FPT, Representative Family.}
}
Document
The Parameterized Complexity of the Minimum Shared Edges Problem
Abstract
We study the NP-complete Minimum Shared Edges (MSE) problem. Given an undirected graph, a source and a sink vertex, and two integers p and k, the question is whether there are p paths in the graph connecting the source with the sink and sharing at most k edges. Herein, an edge is shared if it appears in at least two paths. We show that MSE is W[1]-hard when parameterized by the treewidth of the input graph and the number k of shared edges combined. We show that MSE is fixed-parameter tractable with respect to p, but does not admit a polynomial-size kernel (unless NP is a subset of coNP/poly). In the proof of the fixed-parameter tractability of MSE parameterized by p, we employ the treewidth reduction technique due to Marx, O'Sullivan, and Razgon [ACM TALG 2013].
Cite as
Till Fluschnik, Stefan Kratsch, Rolf Niedermeier, and Manuel Sorge. The Parameterized Complexity of the Minimum Shared Edges Problem. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 448-462, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fluschnik_et_al:LIPIcs.FSTTCS.2015.448,
author = {Fluschnik, Till and Kratsch, Stefan and Niedermeier, Rolf and Sorge, Manuel},
title = {{The Parameterized Complexity of the Minimum Shared Edges Problem}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {448--462},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.448},
URN = {urn:nbn:de:0030-drops-56323},
doi = {10.4230/LIPIcs.FSTTCS.2015.448},
annote = {Keywords: Parameterized complexity, kernelization, treewidth, treewidth reduction}
}
Document
Control Improvisation
Abstract
We formalize and analyze a new automata-theoretic problem termed control improvisation. Given an automaton, the problem is to produce an improviser, a probabilistic algorithm that randomly generates words in its language, subject to two additional constraints: the satisfaction of an admissibility predicate, and the exhibition of a specified amount of randomness. Control improvisation has multiple applications, including, for example, generating musical improvisations that satisfy rhythmic and melodic constraints, where admissibility is determined by some bounded divergence from a reference melody. We analyze the complexity of the control improvisation problem, giving cases where it is efficiently solvable and cases where it is #P-hard or undecidable. We also show how symbolic techniques based on Boolean satisfiability (SAT) solvers can be used to approximately solve some of the intractable cases.
Cite as
Daniel J. Fremont, Alexandre Donzé, Sanjit A. Seshia, and David Wessel. Control Improvisation. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 463-474, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fremont_et_al:LIPIcs.FSTTCS.2015.463,
author = {Fremont, Daniel J. and Donz\'{e}, Alexandre and Seshia, Sanjit A. and Wessel, David},
title = {{Control Improvisation}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {463--474},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.463},
URN = {urn:nbn:de:0030-drops-56596},
doi = {10.4230/LIPIcs.FSTTCS.2015.463},
annote = {Keywords: finite automata, random sampling, Boolean satisfiability, testing, computational music, control theory}
}
Document
A Provably Correct Sampler for Probabilistic Programs
Abstract
We consider the problem of inferring the implicit distribution specified by a probabilistic program. A popular inference technique for probabilistic programs called Markov Chain Monte Carlo or
MCMC sampling involves running the program repeatedly and generating sample values by perturbing values produced in "previous runs". This simulates a Markov chain whose stationary distribution is the distribution specified by the probabilistic program. However, it is non-trivial to implement MCMC sampling for probabilistic programs since each variable could be updated at multiple program points. In such cases, it is unclear which values from the "previous run" should be used to generate samples for the "current run". We present an algorithm to solve this problem for the general case and formally prove that the algorithm is correct. Our algorithm handles variables that are updated multiple times along the same path, updated along different paths in a conditional statement, or repeatedly updated inside loops, We have implemented our algorithm in a tool called InferX. We empirically demonstrate that InferX produces the correct result for various benchmarks, whereas existing tools such as R2 and Stan produce incorrect results on several of these benchmarks.
Cite as
Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, and Selva Samuel. A Provably Correct Sampler for Probabilistic Programs. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 475-488, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{hur_et_al:LIPIcs.FSTTCS.2015.475,
author = {Hur, Chung-Kil and Nori, Aditya V. and Rajamani, Sriram K. and Samuel, Selva},
title = {{A Provably Correct Sampler for Probabilistic Programs}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {475--488},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.475},
URN = {urn:nbn:de:0030-drops-56553},
doi = {10.4230/LIPIcs.FSTTCS.2015.475},
annote = {Keywords: Probabilistic Programming, Program Correctness, Probabilistic Inference, Markov Chain Monte Carlo Sampling}
}
Document
On the Problem of Computing the Probability of Regular Sets of Trees
Abstract
We consider the problem of computing the probability of regular languages of infinite trees with respect to the natural coin-flipping measure. We propose an algorithm which computes the probability of languages recognizable by game automata. In particular this algorithm is applicable to all deterministic automata. We then use the algorithm to prove through examples three properties of measure: (1) there exist regular sets having irrational probability, (2) there exist comeager regular sets having probability 0 and (3) the probability of game languages W_{i,k}, from automata theory, is 0 if k is odd and is 1 otherwise.
Cite as
Henryk Michalewski and Matteo Mio. On the Problem of Computing the Probability of Regular Sets of Trees. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 489-502, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{michalewski_et_al:LIPIcs.FSTTCS.2015.489,
author = {Michalewski, Henryk and Mio, Matteo},
title = {{On the Problem of Computing the Probability of Regular Sets of Trees}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {489--502},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.489},
URN = {urn:nbn:de:0030-drops-56390},
doi = {10.4230/LIPIcs.FSTTCS.2015.489},
annote = {Keywords: regular languages of trees, probability, meta-parity games}
}
Document
Probabilistic Regular Expressions and MSO Logic on Finite Trees
Abstract
We introduce probabilistic regular tree expressions and give a Kleene-like theorem for probabilistic tree automata (PTA). Furthermore, we define probabilistic MSO logic. This logic is more expressive than PTA. We define bottom-up PTA, which are strictly more expressive than PTA. Using bottom-up PTA, we prove a Büchi-like theorem for probabilistic MSO logic. We obtain a Nivat-style theorem as an additional result.
Cite as
Thomas Weidner. Probabilistic Regular Expressions and MSO Logic on Finite Trees. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 503-516, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{weidner:LIPIcs.FSTTCS.2015.503,
author = {Weidner, Thomas},
title = {{Probabilistic Regular Expressions and MSO Logic on Finite Trees}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {503--516},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.503},
URN = {urn:nbn:de:0030-drops-56303},
doi = {10.4230/LIPIcs.FSTTCS.2015.503},
annote = {Keywords: Probabilistic Regular Expressions, MSO Logic, Tree Automata}
}
Document
Rumors Across Radio, Wireless, Telephone
Abstract
We study the problem of computing a minimum time schedule to spread rumors in a given graph under several models: In the radio model, all neighbors of a transmitting node listen to the messages and are able to record it only when no other neighbor is transmitting; In the wireless model (also called the edge-star model), each transmitter is at a different frequency to which any neighbor can tune to, but only one neighboring transmission can be accessed in this way; In the telephone model, the set of transmitter-receiver pairs form a matching in the graph. The rumor spreading problems assume a message at one or several nodes of the graph that must reach a target node or set of nodes. The transmission proceeds in synchronous rounds under the rules of the corresponding model. The goal is to compute a schedule that completes in the minimum number of rounds.
We present a comprehensive study of approximation algorithms for these problems, and show several reductions from the harder to the easier models for special demands. We show a new hardness of approximation of Omega(n^1/2 - epsilon) for the minimum radio gossip time by a connection to maximum induced matchings. We give the first sublinear approximation algorithms for the most general case of the problem under the wireless model; we also consider various special cases such as instances with symmetric demands and give better approximation algorithms. Our work exposes the relationships across the models and opens up several new avenues for further study.
Cite as
Jennifer Iglesias, Rajmohan Rajaraman, R. Ravi, and Ravi Sundaram. Rumors Across Radio, Wireless, Telephone. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 517-528, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{iglesias_et_al:LIPIcs.FSTTCS.2015.517,
author = {Iglesias, Jennifer and Rajaraman, Rajmohan and Ravi, R. and Sundaram, Ravi},
title = {{Rumors Across Radio, Wireless, Telephone}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {517--528},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.517},
URN = {urn:nbn:de:0030-drops-56383},
doi = {10.4230/LIPIcs.FSTTCS.2015.517},
annote = {Keywords: Broadcast, Gossip, Approximation algorithms, Graph algorithms, Hardness of Approximation}
}
Document
The Price of Local Power Control in Wireless Scheduling
Abstract
We consider the problem of scheduling wireless links in the physical model, where we seek an assignment of power levels and a partition of the given set of links into the minimum number of subsets satisfying the signal-to-interference-and-noise-ratio (SINR) constraints. Specifically, we are interested in the efficiency of local power assignment schemes, or oblivious power schemes, in approximating wireless scheduling. Oblivious power schemes are motivated by networking scenarios when power levels must be decided in advance, and not as part of the scheduling computation.
We present the first O(log log Delta)-approximation algorithm, which is known to be best possible (in terms of Delta) for oblivious power schemes, where Delta is the longest to shortest link length ratio. We achieve this by representing interference by a conflict graph, which allows the application of graph-theoretic results for a variety of related problems, including the weighted capacity problem. We explore further the contours of approximability and find the choice of power assignment matters; that not all metric spaces are equal; and that the presence of weak links makes the problem harder. Combined, our results resolve the price of local power for wireless scheduling, or the value of allowing unfettered power control.
Cite as
Magnús M. Halldórsson and Tigran Tonoyan. The Price of Local Power Control in Wireless Scheduling. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 529-542, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{halldorsson_et_al:LIPIcs.FSTTCS.2015.529,
author = {Halld\'{o}rsson, Magn\'{u}s M. and Tonoyan, Tigran},
title = {{The Price of Local Power Control in Wireless Scheduling}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {529--542},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.529},
URN = {urn:nbn:de:0030-drops-56243},
doi = {10.4230/LIPIcs.FSTTCS.2015.529},
annote = {Keywords: Wireless Scheduling, Physical Model, Oblivious Power}
}
Document
Allocation of Divisible Goods Under Lexicographic Preferences
Abstract
We present a simple and natural non-pricing mechanism for allocating divisible goods among strategic agents having lexicographic preferences. Our mechanism has favorable properties of strategy-proofness (incentive compatibility). In addition (and even when extended to the case of Leontief bundles) it enjoys Pareto efficiency, envy-freeness, and time efficiency.
Cite as
Leonard J. Schulman and Vijay V. Vazirani. Allocation of Divisible Goods Under Lexicographic Preferences. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 543-559, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{schulman_et_al:LIPIcs.FSTTCS.2015.543,
author = {Schulman, Leonard J. and Vazirani, Vijay V.},
title = {{Allocation of Divisible Goods Under Lexicographic Preferences}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {543--559},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.543},
URN = {urn:nbn:de:0030-drops-56279},
doi = {10.4230/LIPIcs.FSTTCS.2015.543},
annote = {Keywords: Mechanism design, lexicographic preferences, strategyproof, Pareto optimal, incentive compatible}
}
Document
On the Expressiveness of Multiparty Sessions
Abstract
This paper explores expressiveness of asynchronous multiparty
sessions. We model the behaviours of endpoint implementations in several ways: (i) by the existence of different buffers and queues used to store messages exchanged asynchronously, (ii) by the ability for an endpoint to lightly reconfigure his behaviour at runtime (flexibility), (iii) by the presence of explicit parallelism or interruptions (exceptional actions) in endpoint behaviour. For a given protocol we define several denotations, based on traces of
events, corresponding to the different implementations and compare
them.
Cite as
Romain Demangeon and Nobuko Yoshida. On the Expressiveness of Multiparty Sessions. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 560-574, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{demangeon_et_al:LIPIcs.FSTTCS.2015.560,
author = {Demangeon, Romain and Yoshida, Nobuko},
title = {{On the Expressiveness of Multiparty Sessions}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {560--574},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.560},
URN = {urn:nbn:de:0030-drops-56217},
doi = {10.4230/LIPIcs.FSTTCS.2015.560},
annote = {Keywords: concurrency, message-passing, session, asynchrony, expressiveness}
}
Document
Secure Refinements of Communication Channels
Abstract
It is a common practice to design a protocol (say Q) assuming some secure channels. Then the secure channels are implemented using any standard protocol, e.g. TLS. In this paper, we study when such a practice is indeed secure.
We provide a characterization of both confidential and authenticated channels. As an application, we study several protocols of the literature including TLS and BAC protocols. Thanks to our result, we can consider a larger number of sessions when analyzing complex protocols resulting from explicit implementation of the secure channels of some more abstract protocol Q.
Cite as
Vincent Cheval, Véronique Cortier, and Eric le Morvan. Secure Refinements of Communication Channels. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 575-589, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{cheval_et_al:LIPIcs.FSTTCS.2015.575,
author = {Cheval, Vincent and Cortier, V\'{e}ronique and le Morvan, Eric},
title = {{Secure Refinements of Communication Channels}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {575--589},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.575},
URN = {urn:nbn:de:0030-drops-56583},
doi = {10.4230/LIPIcs.FSTTCS.2015.575},
annote = {Keywords: Protocol, Composition, Formal methods, Channels, Implementation}
}
Document
Failure-aware Runtime Verification of Distributed Systems
Abstract
Prior runtime-verification approaches for distributed systems are limited as they do not account for network failures and they assume that system messages are received in the order they are sent. To overcome these limitations, we present an online algorithm for verifying observed system behavior at runtime with respect to specifications written in the real-time logic MTL that efficiently handles out-of-order message deliveries and operates in the presence of failures. Our algorithm uses a three-valued semantics for MTL, where the third truth value models knowledge gaps, and it resolves knowledge gaps as it propagates Boolean values through the formula structure. We establish the algorithm's soundness and provide completeness guarantees. We also show that it supports distributed system monitoring, where multiple monitors cooperate and exchange their observations and conclusions.
Cite as
David Basin, Felix Klaedtke, and Eugen Zalinescu. Failure-aware Runtime Verification of Distributed Systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 590-603, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{basin_et_al:LIPIcs.FSTTCS.2015.590,
author = {Basin, David and Klaedtke, Felix and Zalinescu, Eugen},
title = {{Failure-aware Runtime Verification of Distributed Systems}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {590--603},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Harsha, Prahladh and Ramalingam, G.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.590},
URN = {urn:nbn:de:0030-drops-56194},
doi = {10.4230/LIPIcs.FSTTCS.2015.590},
annote = {Keywords: Runtime verification, monitoring algorithm, real-time logics, multi-valued semantics, distributed systems, asynchronous communication}
}