eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
0
0
10.4230/LIPIcs.FSTTCS.2019
article
LIPIcs, Volume 150, FSTTCS'19, Complete Volume
Chattopadhyay, Arkadev
1
Gastin, Paul
2
https://orcid.org/0000-0002-1313-7722
Tata Institute of Fundamental Research, Mumbai, India
LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
LIPIcs, Volume 150, FSTTCS'19, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019/LIPIcs.FSTTCS.2019.pdf
Theory of computation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
0:i
0:xii
10.4230/LIPIcs.FSTTCS.2019.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Chattopadhyay, Arkadev
1
Gastin, Paul
2
https://orcid.org/0000-0002-1313-7722
Tata Institute of Fundamental Research, Mumbai, India
LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.0/LIPIcs.FSTTCS.2019.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
1:1
1:12
10.4230/LIPIcs.FSTTCS.2019.1
article
Practical Formal Methods for Real World Cryptography (Invited Talk)
Bhargavan, Karthikeyan
1
Naldurg, Prasad
1
Inria, Paris, France
Cryptographic algorithms, protocols, and applications are difficult to implement correctly, and errors and vulnerabilities in their code can remain undiscovered for long periods before they are exploited. Even highly-regarded cryptographic libraries suffer from bugs like buffer overruns, incorrect numerical computations, and timing side-channels, which can lead to the exposure of sensitive data and long-term secrets. We describe a tool chain and framework based on the F* programming language to formally specify, verify and compile high-performance cryptographic software that is secure by design. This tool chain has been used to build a verified cryptographic library called HACL*, and provably secure implementations of sophisticated secure communication protocols like Signal and TLS. We describe these case studies and conclude with ongoing work on using our framework to build verified implementations of privacy preserving machine learning software.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.1/LIPIcs.FSTTCS.2019.1.pdf
Formal verification
Applied cryptography
Security protocols
Machine learning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
2:1
2:1
10.4230/LIPIcs.FSTTCS.2019.2
article
Sketching Graphs and Combinatorial Optimization (Invited Talk)
Krauthgamer, Robert
1
Weizmann Institute of Science, Rehovot, Israel
Graph-sketching algorithms summarize an input graph G in a manner that suffices to later answer (perhaps approximately) one or more optimization problems on G, like distances, cuts, and matchings. Two famous examples are the Gomory-Hu tree, which represents all the minimum st-cuts in a graph G using a tree on the same vertex set V(G); and the cut-sparsifier of Benczúr and Karger, which is a sparse graph (often a reweighted subgraph) that approximates every cut in G within factor 1 +/- epsilon. Another genre of these problems limits the queries to designated terminal vertices, denoted T subseteq V(G), and the sketch size depends on |T| instead of |V(G)|.
The talk will survey this topic, particularly cut and flow problems such as the three examples above. Currently, most known sketches are based on a graphical representation, often called edge and vertex sparsification, which leaves room for potential improvements like smaller storage by using another representation, and faster running time to answer a query. These algorithms employ a host of techniques, ranging from combinatorial methods, like graph partitioning and edge or vertex sampling, to standard tools in data-stream algorithms and in sparse recovery. There are also several lower bounds known, either combinatorial (for the graphical representation) or based on communication complexity and information theory.
Many of the recent efforts focus on characterizing the tradeoff between accuracy and sketch size, yet many intriguing and very accessible problems are still open, and I will describe them in the talk.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.2/LIPIcs.FSTTCS.2019.2.pdf
Sketching
edge sparsification
vertex sparsification
Gomory-Hu tree
mimicking networks
graph sampling
succinct data structures
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
3:1
3:2
10.4230/LIPIcs.FSTTCS.2019.3
article
Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk)
Lazić, Ranko
1
DIMAP, Department of Computer Science, University of Warwick, UK
Studying one-dimensional grammar vector addition systems has long been advocated by Alain Finkel. In this presentation, we shall see how research on those systems has led to the recent breakthrough tower lower bound for the reachability problem on vector addition systems, obtained by Czerwiński et al. In fact, we shall look at how appropriate modifications of an underlying technical construction can lead to counter-examples to several conjectures on one-dimensional grammar vector addition systems, fixed-dimensional vector addition systems, and fixed-dimensional flat vector addition systems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.3/LIPIcs.FSTTCS.2019.3.pdf
Petri nets
vector addition systems
reachability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
4:1
4:1
10.4230/LIPIcs.FSTTCS.2019.4
article
Progress in Lifting and Applications in Lower Bounds (Invited Talk)
Pitassi, Toniann
1
2
University of Toronto, Canada
Institute for Advanced Study, Princeton, NJ, USA
Ever since Yao introduced the communication complexity model in 1979, it has played a pivotal role in our understanding of limitations for a wide variety of problems in Computer Science. In this talk, I will present the lifting method, whereby communication lower bounds are obtained by lifting much simpler lower bounds. I will show how lifting theorems have been used to solve many open problems in a variety of areas of computer science, including: circuit complexity, proof complexity, combinatorial optimization (size of linear programming formulations), cryptography (linear secret sharing schemes), game theory and privacy.
At the end of the talk, I will sketch the proof of a unified lifting theorem for deterministic and randomized communication (joint with Arkadev Chattopadyhay, Yuval Filmus, Sajin Koroth, and Or Meir.)
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.4/LIPIcs.FSTTCS.2019.4.pdf
complexity theory
lower bounds
communication complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
5:1
5:1
10.4230/LIPIcs.FSTTCS.2019.5
article
How Computer Science Informs Modern Auction Design (Invited Talk)
Roughgarden, Tim
1
Columbia University, Department of Computer Science, New York, USA
Over the last twenty years, computer science has relied on concepts borrowed from game theory and economics to reason about applications ranging from internet routing to real-time auctions for online advertising. More recently, ideas have increasingly flowed in the opposite direction, with concepts and techniques from computer science beginning to influence economic theory and practice.
In this lecture, I will illustrate this point with a detailed case study of the 2016-2017 Federal Communications Commission incentive auction for repurposing wireless spectrum. Computer science techniques, ranging from algorithms for NP-hard problems to nondeterministic communication complexity, have played a critical role both in the design of the reverse auction (with the government procuring existing licenses from television broadcasters) and in the analysis of the forward auction (when the procured licenses sell to the highest bidder).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.5/LIPIcs.FSTTCS.2019.5.pdf
Game Theory
Auction Design
Algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
6:1
6:1
10.4230/LIPIcs.FSTTCS.2019.6
article
An Algebraic Framework to Reason About Concurrency (Invited Talk)
Silva, Alexandra
1
University College London, United Kingdom
Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Hoare, Struth, and collaborators proposed a concurrent extension of Kleene Algebra (CKA) as a first step towards developing algebraic reasoning for concurrent programs. Completing their research program and extending KAT to encompass concurrent behaviour has however proven to be more challenging than initially expected. The core problem appears because when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with expected axioms for reasoning about concurrency lead to an unexpected equation about programs. In this talk, we will revise the literature on CKA(T) and explain the challenges and solutions in the development of an algebraic framework for concurrency.
The talk is based on a series of papers joint with Tobias Kappé, Paul Brunet, Bas Luttik, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi [Tobias Kappé et al., 2017; Tobias Kappé et al., 2019; Kappé et al., 2018]. Additional references can be found on the CoNeCo project website: https://coneco-project.org/.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.6/LIPIcs.FSTTCS.2019.6.pdf
Kleene Algebra
Concurrency
Automata
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
7:1
7:14
10.4230/LIPIcs.FSTTCS.2019.7
article
Connected Search for a Lazy Robber
Adler, Isolde
1
Paul, Christophe
2
Thilikos, Dimitrios M.
2
School of Computing, University of Leeds, Leeds, United Kingdom
CNRS, LIRMM, Université de Montpellier, Montpellier, France
The node search game against a lazy (or, respectively, agile) invisible robber has been introduced as a search-game analogue of the treewidth parameter (and, respectively, pathwidth). In the connected variants of the above two games, we additionally demand that, at each moment of the search, the clean territories are connected. The connected search game against an agile and invisible robber has been extensively examined. The monotone variant (where we also demand that the clean territories are progressively increasing) of this game, corresponds to the graph parameter of connected pathwidth. It is known that the price of connectivty to search for an agile robber is bounded by 2, that is the connected pathwidth of a graph is at most twice (plus some constant) its pathwidth. In this paper, we investigate the connected search game against a lazy robber. A lazy robber moves only when the searchers' strategy threatens the location that he currently occupies. We introduce two alternative graph-theoretic formulations of this game, one in terms of connected tree decompositions, and one in terms of (connected) layouts, leading to the graph parameter of connected treewidth. We observe that connected treewidth parameter is closed under contractions and prove that for every k >= 2, the set of contraction obstructions of the class of graphs with connected treewidth at most k is infinite. Our main result is a complete characterization of the obstruction set for k=2. One may observe that, so far, only a few complete obstruction sets are explicitly known for contraction closed graph classes. We finally show that, in contrast to the agile robber game, the price of connectivity is unbounded.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.7/LIPIcs.FSTTCS.2019.7.pdf
Graph searching
Tree-decomposition
Obstructions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
8:1
8:20
10.4230/LIPIcs.FSTTCS.2019.8
article
Parameterized Streaming Algorithms for Min-Ones d-SAT
Agrawal, Akanksha
1
Biswas, Arindam
2
Bonnet, Édouard
3
Brettell, Nick
4
Curticapean, Radu
5
6
Marx, Dániel
7
Miltzow, Tillmann
8
Raman, Venkatesh
2
Saurabh, Saket
2
9
Department of Computer Science, Ben-Gurion University of the Negev, Beer-Sheva, Israel
The Institute of Mathematical Sciences, HBNI, Chennai, India
CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP UMR5668, France
Department of Computer Science, Durham University, Durham, UK
BARC, University of Copenhagen, Copenhagen, Denmark
ITU Copenhagen, Copenhagen, Denmark
Institute for Computer Science and Control, MTA SZTAKI, Budapest, Hungary
Department of Computer Science, Utrecht University, Utrecht, Netherlands
Department of Computer Science, University of Bergen, Bergen, Norway
In this work, we initiate the study of the Min-Ones d-SAT problem in the parameterized streaming model. An instance of the problem consists of a d-CNF formula F and an integer k, and the objective is to determine if F has a satisfying assignment which sets at most k variables to 1. In the parameterized streaming model, input is provided as a stream, just as in the usual streaming model. A key difference is that the bound on the read-write memory available to the algorithm is O(f(k) log n) (f: N -> N, a computable function) as opposed to the O(log n) bound of the usual streaming model. The other important difference is that the number of passes the algorithm makes over its input must be a (preferably small) function of k.
We design a (k + 1)-pass parameterized streaming algorithm that solves Min-Ones d-SAT (d >= 2) using space O((kd^(ck) + k^d)log n) (c > 0, a constant) and a (d + 1)^k-pass algorithm that uses space O(k log n). We also design a streaming kernelization for Min-Ones 2-SAT that makes (k + 2) passes and uses space O(k^6 log n) to produce a kernel with O(k^6) clauses.
To complement these positive results, we show that any k-pass algorithm for or Min-Ones d-SAT (d >= 2) requires space Omega(max{n^(1/k) / 2^k, log(n / k)}) on instances (F, k). This is achieved via a reduction from the streaming problem POT Pointer Chasing (Guha and McGregor [ICALP 2008]), which might be of independent interest. Given this, our (k + 1)-pass parameterized streaming algorithm is the best possible, inasmuch as the number of passes is concerned.
In contrast to the results of Fafianie and Kratsch [MFCS 2014] and Chitnis et al. [SODA 2015], who independently showed that there are 1-pass parameterized streaming algorithms for Vertex Cover (a restriction of Min-Ones 2-SAT), we show using lower bounds from Communication Complexity that for any d >= 1, a 1-pass streaming algorithm for Min-Ones d-SAT requires space Omega(n). This excludes the possibility of a 1-pass parameterized streaming algorithm for the problem. Additionally, we show that any p-pass algorithm for the problem requires space Omega(n/p).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.8/LIPIcs.FSTTCS.2019.8.pdf
min
ones
sat
d-sat
parameterized
kernelization
streaming
space
efficient
algorithm
parameter
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
9:1
9:14
10.4230/LIPIcs.FSTTCS.2019.9
article
Fast Exact Algorithms Using Hadamard Product of Polynomials
Arvind, V.
1
Chatterjee, Abhranil
1
Datta, Rajit
2
Mukhopadhyay, Partha
2
Institute of Mathematical Sciences (HBNI), Chennai, India
Chennai Mathematical Institute, Chennai, India
Let C be an arithmetic circuit of poly(n) size given as input that computes a polynomial f in F[X], where X={x_1,x_2,...,x_n} and F is any field where the field arithmetic can be performed efficiently. We obtain new algorithms for the following two problems first studied by Koutis and Williams [Ioannis Koutis, 2008; Ryan Williams, 2009; Ioannis Koutis and Ryan Williams, 2016].
- (k,n)-MLC: Compute the sum of the coefficients of all degree-k multilinear monomials in the polynomial f.
- k-MMD: Test if there is a nonzero degree-k multilinear monomial in the polynomial f.
Our algorithms are based on the fact that the Hadamard product f o S_{n,k}, is the degree-k multilinear part of f, where S_{n,k} is the k^{th} elementary symmetric polynomial.
- For (k,n)-MLC problem, we give a deterministic algorithm of run time O^*(n^(k/2+c log k)) (where c is a constant), answering an open question of Koutis and Williams [Ioannis Koutis and Ryan Williams, 2016]. As corollaries, we show O^*(binom{n}{downarrow k/2})-time exact counting algorithms for several combinatorial problems: k-Tree, t-Dominating Set, m-Dimensional k-Matching.
- For k-MMD problem, we give a randomized algorithm of run time 4.32^k * poly(n,k). Our algorithm uses only poly(n,k) space. This matches the run time of a recent algorithm [Cornelius Brand et al., 2018] for k-MMD which requires exponential (in k) space.
Other results include fast deterministic algorithms for (k,n)-MLC and k-MMD problems for depth three circuits.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.9/LIPIcs.FSTTCS.2019.9.pdf
Hadamard Product
Multilinear Monomial Detection and Counting
Rectangular Permanent
Symmetric Polynomial
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
10:1
10:15
10.4230/LIPIcs.FSTTCS.2019.10
article
Approximate Online Pattern Matching in Sublinear Time
Chakraborty, Diptarka
1
Das, Debarati
2
Koucký, Michal
3
National University of Singapore, Singapore
University of Copenhagen, Denmark
Computer Science Institute of Charles University, Czech Republic
We consider the approximate pattern matching problem under edit distance. In this problem we are given a pattern P of length m and a text T of length n over some alphabet Sigma, and a positive integer k. The goal is to find all the positions j in T such that there is a substring of T ending at j which has edit distance at most k from the pattern P. Recall, the edit distance between two strings is the minimum number of character insertions, deletions, and substitutions required to transform one string into the other. For a position t in {1,...,n}, let k_t be the smallest edit distance between P and any substring of T ending at t. In this paper we give a constant factor approximation to the sequence k_1,k_2,...,k_n. We consider both offline and online settings.
In the offline setting, where both P and T are available, we present an algorithm that for all t in {1,...,n}, computes the value of k_t approximately within a constant factor. The worst case running time of our algorithm is O~(n m^(3/4)).
In the online setting, we are given P and then T arrives one symbol at a time. We design an algorithm that upon arrival of the t-th symbol of T computes k_t approximately within O(1)-multiplicative factor and m^(8/9)-additive error. Our algorithm takes O~(m^(1-(7/54))) amortized time per symbol arrival and takes O~(m^(1-(1/54))) additional space apart from storing the pattern P. Both of our algorithms are randomized and produce correct answer with high probability. To the best of our knowledge this is the first algorithm that takes worst-case sublinear (in the length of the pattern) time and sublinear extra space for the online approximate pattern matching problem. To get our result we build on the technique of Chakraborty, Das, Goldenberg, Koucký and Saks [FOCS'18] for computing a constant factor approximation of edit distance in sub-quadratic time.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.10/LIPIcs.FSTTCS.2019.10.pdf
Approximate Pattern Matching
Online Pattern Matching
Edit Distance
Sublinear Algorithm
Streaming Algorithm
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
11:1
11:14
10.4230/LIPIcs.FSTTCS.2019.11
article
Constructing Faithful Homomorphisms over Fields of Finite Characteristic
Chatterjee, Prerona
1
https://orcid.org/0000-0003-2643-8142
Saptharishi, Ramprasad
1
https://orcid.org/0000-0002-7485-3220
Tata Institute of Fundamental Research, Mumbai, India
We study the question of algebraic rank or transcendence degree preserving homomorphisms over finite fields. This concept was first introduced by Beecken et al. [Malte Beecken et al., 2013] and exploited by them and Agrawal et al. [Manindra Agrawal et al., 2016] to design algebraic independence based identity tests using the Jacobian criterion over characteristic zero fields. An analogue of such constructions over finite characteristic fields were unknown due to the failure of the Jacobian criterion over finite characteristic fields.
Building on a recent criterion of Pandey, Saxena and Sinhababu [Anurag Pandey et al., 2018], we construct explicit faithful maps for some natural classes of polynomials in fields of positive characteristic, when a certain parameter called the inseparable degree of the underlying polynomials is bounded (this parameter is always 1 in fields of characteristic zero). This presents the first generalisation of some of the results of Beecken, Mittmann and Saxena [Malte Beecken et al., 2013] and Agrawal, Saha, Saptharishi, Saxena [Manindra Agrawal et al., 2016] in the positive characteristic setting.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.11/LIPIcs.FSTTCS.2019.11.pdf
Faithful Homomorphisms
Identity Testing
Algebraic Independence
Finite characteristic fields
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
12:1
12:14
10.4230/LIPIcs.FSTTCS.2019.12
article
Maximum-Area Rectangles in a Simple Polygon
Choi, Yujin
1
Lee, Seungjun
2
Ahn, Hee-Kap
2
https://orcid.org/0000-0001-7177-1679
Technische Universität Berlin, Germany
Pohang University of Science and Technology, Pohang, Korea
We study the problem of finding maximum-area rectangles contained in a polygon in the plane. There has been a fair amount of work for this problem when the rectangles have to be axis-aligned or when the polygon is convex. We consider this problem in a simple polygon with n vertices, possibly with holes, and with no restriction on the orientation of the rectangles. We present an algorithm that computes a maximum-area rectangle in O(n^3 log n) time using O(kn^2) space, where k is the number of reflex vertices of P. Our algorithm can report all maximum-area rectangles in the same time using O(n^3) space. We also present a simple algorithm that finds a maximum-area rectangle contained in a convex polygon with n vertices in O(n^3) time using O(n) space.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.12/LIPIcs.FSTTCS.2019.12.pdf
Maximum-area rectangle
largest rectangle
simple polygon
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
13:1
13:14
10.4230/LIPIcs.FSTTCS.2019.13
article
Motif Counting in Preferential Attachment Graphs
Dreier, Jan
1
https://orcid.org/0000-0002-2662-5303
Rossmanith, Peter
1
https://orcid.org/0000-0003-0177-8028
Department of Computer Science, RWTH Aachen University, Germany
Network motifs are small patterns that occur in a network significantly more often than expected. They have gathered a lot of interest, as they may describe functional dependencies of complex networks and yield insights into their basic structure [Milo et al., 2002]. Therefore, a large amount of work went into the development of methods for network motif detection in complex networks [Kashtan et al., 2004; Schreiber and Schwöbbermeyer, 2005; Chen et al., 2006; Wernicke, 2006; Grochow and Kellis, 2007; Alon et al., 2008; Omidi et al., 2009]. The underlying problem of motif detection is to count how often a copy of a pattern graph H occurs in a target graph G. This problem is #W[1]-hard when parameterized by the size of H [Flum and Grohe, 2004] and cannot be solved in time f(|H|)n^o(|H|) under #ETH [Chen et al., 2005].
Preferential attachment graphs [Barabási and Albert, 1999] are a very popular random graph model designed to mimic complex networks. They are constructed by a random process that iteratively adds vertices and attaches them preferentially to vertices that already have high degree. Preferential attachment has been empirically observed in real growing networks [Newman, 2001; Jeong et al., 2003].
We show that one can count subgraph copies of a graph H in the preferential attachment graph G^n_m (with n vertices and nm edges, where m is usually a small constant) in expected time f(|H|) m^O(|H|^6) log(n)^O(|H|^12) n. This means the motif counting problem can be solved in expected quasilinear FPT time on preferential attachment graphs with respect to the parameters |H| and m. In particular, for fixed H and m the expected run time is O(n^(1+epsilon)) for every epsilon>0.
Our results are obtained using new concentration bounds for degrees in preferential attachment graphs. Assume the (total) degree of a set of vertices at a time t of the random process is d. We show that if d is sufficiently large then the degree of the same set at a later time n is likely to be in the interval (1 +/- epsilon)d sqrt(n/t) (for epsilon > 0) for all n >= t. More specifically, the probability that this interval is left is exponentially small in d.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.13/LIPIcs.FSTTCS.2019.13.pdf
random graphs
motif counting
average case analysis
preferential attachment graphs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
14:1
14:15
10.4230/LIPIcs.FSTTCS.2019.14
article
Parameterized k-Clustering: Tractability Island
Fomin, Fedor V.
1
Golovach, Petr A.
1
Simonov, Kirill
1
Department of Informatics, University of Bergen, Norway
In k-Clustering we are given a multiset of n vectors X subset Z^d and a nonnegative number D, and we need to decide whether X can be partitioned into k clusters C_1, ..., C_k such that the cost sum_{i=1}^k min_{c_i in R^d} sum_{x in C_i} |x-c_i|_p^p <= D, where |*|_p is the Minkowski (L_p) norm of order p. For p=1, k-Clustering is the well-known k-Median. For p=2, the case of the Euclidean distance, k-Clustering is k-Means. We study k-Clustering from the perspective of parameterized complexity. The problem is known to be NP-hard for k=2 and it is also NP-hard for d=2. It is a long-standing open question, whether the problem is fixed-parameter tractable (FPT) for the combined parameter d+k. In this paper, we focus on the parameterization by D. We complement the known negative results by showing that for p=0 and p=infty, k-Clustering is W1-hard when parameterized by D. Interestingly, the complexity landscape of the problem appears to be more intricate than expected. We discover a tractability island of k-Clustering: for every p in (0,1], k-Clustering is solvable in time 2^O(D log D) (nd)^O(1).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.14/LIPIcs.FSTTCS.2019.14.pdf
clustering
parameterized complexity
k-means
k-median
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
15:1
15:14
10.4230/LIPIcs.FSTTCS.2019.15
article
Nonnegative Rank Measures and Monotone Algebraic Branching Programs
Fournier, Hervé
1
Malod, Guillaume
1
Szusterman, Maud
1
Tavenas, Sébastien
2
Université de Paris, IMJ-PRG, CNRS, F-75013 Paris, France
Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, France
Inspired by Nisan’s characterization of noncommutative complexity (Nisan 1991), we study different notions of nonnegative rank, associated complexity measures and their link with monotone computations. In particular we answer negatively an open question of Nisan asking whether nonnegative rank characterizes monotone noncommutative complexity for algebraic branching programs. We also prove a rather tight lower bound for the computation of elementary symmetric polynomials by algebraic branching programs in the monotone setting or, equivalently, in the homogeneous syntactically multilinear setting.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.15/LIPIcs.FSTTCS.2019.15.pdf
Elementary symmetric polynomials
lower bounds
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
16:1
16:13
10.4230/LIPIcs.FSTTCS.2019.16
article
Unambiguous Catalytic Computation
Gupta, Chetan
1
Jain, Rahul
1
https://orcid.org/0000-0002-8567-9475
Sharma, Vimal Raj
1
Tewari, Raghunath
1
Indian Institute of Technology Kanpur, India
The catalytic Turing machine is a model of computation defined by Buhrman, Cleve, Koucký, Loff, and Speelman (STOC 2014). Compared to the classical space-bounded Turing machine, this model has an extra space which is filled with arbitrary content in addition to the clean space. In such a model we study if this additional filled space can be used to increase the power of computation or not, with the condition that the initial content of this extra filled space must be restored at the end of the computation.
In this paper, we define the notion of unambiguous catalytic Turing machine and prove that under a standard derandomization assumption, the class of problems solved by an unambiguous catalytic Turing machine is same as the class of problems solved by a general nondeterministic catalytic Turing machine in the logspace setting.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.16/LIPIcs.FSTTCS.2019.16.pdf
Catalytic computation
Logspace
Reinhardt-Allender
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
17:1
17:14
10.4230/LIPIcs.FSTTCS.2019.17
article
A Fast Exponential Time Algorithm for Max Hamming Distance X3SAT
Hoi, Gordon
1
Jain, Sanjay
1
Stephan, Frank
2
1
School of Computing, National University of Singapore, Singapore 117417, Republic of Singapore
Dept. of Mathematics, National University of Singapore, Singapore 119076, Republic of Singapore
X3SAT is the problem of whether one can satisfy a given set of clauses with up to three literals such that in every clause, exactly one literal is true and the others are false. A related question is to determine the maximal Hamming distance between two solutions of the instance. Dahllöf provided an algorithm for Maximum Hamming Distance XSAT, which is more complicated than the same problem for X3SAT, with a runtime of O(1.8348^n); Fu, Zhou and Yin considered Maximum Hamming Distance for X3SAT and found for this problem an algorithm with runtime O(1.6760^n). In this paper, we propose an algorithm in O(1.3298^n) time to solve the Max Hamming Distance X3SAT problem; the algorithm actually counts for each k the number of pairs of solutions which have Hamming Distance k.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.17/LIPIcs.FSTTCS.2019.17.pdf
X3SAT Problem
Maximum Hamming Distance of Solutions
Exponential Time Algorithms
DPLL Algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
18:1
18:15
10.4230/LIPIcs.FSTTCS.2019.18
article
Exact and Approximate Digraph Bandwidth
Jain, Pallavi
1
Kanesh, Lawqueen
2
Lochet, William
3
Saurabh, Saket
2
Sharma, Roohani
2
Ben-Gurion University of the Negev, Beer-Sheva, Israel
The Institute of Mathematical Sciences, HBNI, India
University of Bergen, Norway
In this paper, we introduce a directed variant of the classical Bandwidth problem and study it from the view-point of moderately exponential time algorithms, both exactly and approximately. Motivated by the definitions of the directed variants of the classical Cutwidth and Pathwidth problems, we define Digraph Bandwidth as follows. Given a digraph D and an ordering sigma of its vertices, the digraph bandwidth of sigma with respect to D is equal to the maximum value of sigma(v)-sigma(u) over all arcs (u,v) of D going forward along sigma (that is, when sigma(u) < sigma (v)). The Digraph Bandwidth problem takes as input a digraph D and asks to output an ordering with the minimum digraph bandwidth. The undirected Bandwidth easily reduces to Digraph Bandwidth and thus, it immediately implies that Directed Bandwidth is {NP-hard}. While an O^*(n!) time algorithm for the problem is trivial, the goal of this paper is to design algorithms for Digraph Bandwidth which have running times of the form 2^O(n). In particular, we obtain the following results. Here, n and m denote the number of vertices and arcs of the input digraph D, respectively.
- Digraph Bandwidth can be solved in O^*(3^n * 2^m) time. This result implies a 2^O(n) time algorithm on sparse graphs, such as graphs of bounded average degree.
- Let G be the underlying undirected graph of the input digraph. If the treewidth of G is at most t, then Digraph Bandwidth can be solved in time O^*(2^(n + (t+2) log n)). This result implies a 2^(n+O(sqrt(n) log n)) algorithm for directed planar graphs and, in general, for the class of digraphs whose underlying undirected graph excludes some fixed graph H as a minor.
- Digraph Bandwidth can be solved in min{O^*(4^n * b^n), O^*(4^n * 2^(b log b log n))} time, where b denotes the optimal digraph bandwidth of D. This allow us to deduce a 2^O(n) algorithm in many cases, for example when b <= n/(log^2n).
- Finally, we give a (Single) Exponential Time Approximation Scheme for Digraph Bandwidth. In particular, we show that for any fixed real epsilon > 0, we can find an ordering whose digraph bandwidth is at most (1+epsilon) times the optimal digraph bandwidth, in time O^*(4^n * (ceil[4/epsilon])^n).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.18/LIPIcs.FSTTCS.2019.18.pdf
directed bandwidth
digraph bandwidth
approximation scheme
exact exponential algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
19:1
19:14
10.4230/LIPIcs.FSTTCS.2019.19
article
An O(n^(1/4 +epsilon)) Space and Polynomial Algorithm for Grid Graph Reachability
Jain, Rahul
1
https://orcid.org/0000-0002-8567-9475
Tewari, Raghunath
1
Indian Institute of Technology Kanpur, India
The reachability problem is to determine if there exists a path from one vertex to another in a graph. Grid graphs are the class of graphs where vertices are present on the lattice points of a two-dimensional grid, and an edge can occur between a vertex and its immediate horizontal or vertical neighbor only.
Asano et al. presented the first simultaneous time space bound for reachability in grid graphs by presenting an algorithm that solves the problem in polynomial time and O(n^(1/2 + epsilon)) space. In 2018, the space bound was improved to O~(n^(1/3)) by Ashida and Nakagawa.
In this paper, we show that reachability in an n vertex grid graph can be decided by an algorithm using O(n^(1/4 + epsilon)) space and polynomial time simultaneously.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.19/LIPIcs.FSTTCS.2019.19.pdf
graph reachability
grid graph
graph algorithm
sublinear space algorithm
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
20:1
20:15
10.4230/LIPIcs.FSTTCS.2019.20
article
Popular Roommates in Simply Exponential Time
Kavitha, Telikepalli
1
Tata Institute of Fundamental Research, Mumbai, India
We consider the popular matching problem in a graph G = (V,E) on n vertices with strict preferences. A matching M is popular if there is no matching N in G such that vertices that prefer N to M outnumber those that prefer M to N. It is known that it is NP-hard to decide if G has a popular matching or not. There is no faster algorithm known for this problem than the brute force algorithm that could take n! time. Here we show a simply exponential time algorithm for this problem, i.e., one that runs in O^*(k^n) time, where k is a constant.
We use the recent breakthrough result on the maximum number of stable matchings possible in such instances to analyze our algorithm for the popular matching problem. We identify a natural (also, hard) subclass of popular matchings called truly popular matchings and show an O^*(2^n) time algorithm for the truly popular matching problem.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.20/LIPIcs.FSTTCS.2019.20.pdf
Roommates instance
Popular matching
Stable matching
Dual certificate
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
21:1
21:12
10.4230/LIPIcs.FSTTCS.2019.21
article
The Complexity of Finding S-Factors in Regular Graphs
Kolisetty, Sanjana
1
Le, Linh
1
Volkovich, Ilya
2
Yannakakis, Mihalis
3
Departments of Mathematics and EECS, CSE Division, University of Michigan, Ann Arbor, MI, USA
Department of EECS, CSE Division, University of Michigan, Ann Arbor, MI, USA
Department of Computer Science, Columbia University, New York, NY, USA
A graph G has an S-factor if there exists a spanning subgraph F of G such that for all v in V: deg_F(v) in S. The simplest example of such factor is a 1-factor, which corresponds to a perfect matching in a graph. In this paper we study the computational complexity of finding S-factors in regular graphs. Our techniques combine some classical as well as recent tools from graph theory.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.21/LIPIcs.FSTTCS.2019.21.pdf
constraint satisfaction problem
Dichotomy theorem
Graph Factors
Regular Graphs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
22:1
22:14
10.4230/LIPIcs.FSTTCS.2019.22
article
More on AC^0[oplus] and Variants of the Majority Function
Limaye, Nutan
1
Srinivasan, Srikanth
2
Tripathi, Utkarsh
2
Department of Computer Science and Engineering, IIT Bombay, India
Department of Mathematics, IIT Bombay, India
In this paper we prove two results about AC^0[oplus] circuits.
(1) We show that for d(N) = o(sqrt(log N/log log N)) and N <= s(N) <= 2^(dN^(1/4d^2)) there is an explicit family of functions {f_N:{0,1}^N - > {0,1}} such that
- f_N has uniform AC^0 formulas of depth d and size at most s;
- f_N does not have AC^0[oplus] formulas of depth d and size s^epsilon, where epsilon is a fixed absolute constant.
This gives a quantitative improvement on the recent result of Limaye, Srinivasan, Sreenivasaiah, Tripathi, and Venkitesh, (STOC, 2019), which proved a similar Fixed-Depth Size-Hierarchy theorem but for d << log log N and s << exp(N^(1/2^Omega(d))).
As in the previous result, we use the Coin Problem to prove our hierarchy theorem. Our main technical result is the construction of uniform size-optimal formulas for solving the coin problem with improved sample complexity (1/delta)^O(d) (down from (1/delta)^(2^O(d)) in the previous result).
(2) In our second result, we show that randomness buys depth in the AC^0[oplus] setting. Formally, we show that for any fixed constant d >= 2, there is a family of Boolean functions that has polynomial-sized randomized uniform AC^0 circuits of depth d but no polynomial-sized (deterministic) AC^0[oplus] circuits of depth d.
Previously Viola (Computational Complexity, 2014) showed that an increase in depth (by at least 2) is essential to avoid superpolynomial blow-up while derandomizing randomized AC^0 circuits. We show that an increase in depth (by at least 1) is essential even for AC^0[oplus].
As in Viola’s result, the separating examples are promise variants of the Majority function on N inputs that accept inputs of weight at least N/2 + N/(log N)^(d-1) and reject inputs of weight at most N/2 - N/(log N)^(d-1).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.22/LIPIcs.FSTTCS.2019.22.pdf
AC^0[oplus]
Coin Problem
Promise Majority
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
23:1
23:15
10.4230/LIPIcs.FSTTCS.2019.23
article
Planted Models for k-Way Edge and Vertex Expansion
Louis, Anand
1
Venkat, Rakesh
2
Indian Institute of Science, Bangalore, India
Indian Institute of Technology, Hyderabad, India
Graph partitioning problems are a central topic of study in algorithms and complexity theory. Edge expansion and vertex expansion, two popular graph partitioning objectives, seek a 2-partition of the vertex set of the graph that minimizes the considered objective. However, for many natural applications, one might require a graph to be partitioned into k parts, for some k >=slant 2. For a k-partition S_1, ..., S_k of the vertex set of a graph G = (V,E), the k-way edge expansion (resp. vertex expansion) of {S_1, ..., S_k} is defined as max_{i in [k]} Phi(S_i), and the balanced k-way edge expansion (resp. vertex expansion) of G is defined as min_{{S_1, ..., S_k} in P_k} max_{i in [k]} Phi(S_i) , where P_k is the set of all balanced k-partitions of V (i.e each part of a k-partition in P_k should have cardinality |V|/k), and Phi(S) denotes the edge expansion (resp. vertex expansion) of S subset V. We study a natural planted model for graphs where the vertex set of a graph has a k-partition S_1, ..., S_k such that the graph induced on each S_i has large expansion, but each S_i has small edge expansion (resp. vertex expansion) in the graph. We give bi-criteria approximation algorithms for computing the balanced k-way edge expansion (resp. vertex expansion) of instances in this planted model.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.23/LIPIcs.FSTTCS.2019.23.pdf
Vertex Expansion
k-way partitioning
Semi-Random models
Planted Models
Approximation Algorithms
Beyond Worst Case Analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
24:1
24:12
10.4230/LIPIcs.FSTTCS.2019.24
article
Online Non-Preemptive Scheduling to Minimize Maximum Weighted Flow-Time on Related Machines
Lucarelli, Giorgio
1
Moseley, Benjamin
2
Thang, Nguyen Kim
3
Srivastav, Abhinav
3
Trystram, Denis
4
LCOMS, University of Lorraine, Metz, France
Tepper School of Business, Carnegie Mellon University, USA
IBISC, Univ. Paris-Saclay, France
Univ. Grenoble Alpes, CNRS, Inria, Grenoble INP, LIG, France
We consider the problem of scheduling jobs to minimize the maximum weighted flow-time on a set of related machines. When jobs can be preempted this problem is well-understood; for example, there exists a constant competitive algorithm using speed augmentation. When jobs must be scheduled non-preemptively, only hardness results are known. In this paper, we present the first online guarantees for the non-preemptive variant. We present the first constant competitive algorithm for minimizing the maximum weighted flow-time on related machines by relaxing the problem and assuming that the online algorithm can reject a small fraction of the total weight of jobs. This is essentially the best result possible given the strong lower bounds on the non-preemptive problem without rejection.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.24/LIPIcs.FSTTCS.2019.24.pdf
Online Algorithms
Scheduling
Resource Augmentation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
25:1
25:14
10.4230/LIPIcs.FSTTCS.2019.25
article
On the AC^0[oplus] Complexity of Andreev’s Problem
Potukuchi, Aditya
1
https://orcid.org/0000-0001-7233-7532
Department of Computer Science, Rutgers University, USA
Andreev’s Problem is the following: Given an integer d and a subset of S subset F_q x F_q, is there a polynomial y = p(x) of degree at most d such that for every a in F_q, (a,p(a)) in S? We show an AC^0[oplus] lower bound for this problem.
This problem appears to be similar to the list recovery problem for degree-d Reed-Solomon codes over F_q which states the following: Given subsets A_1,...,A_q of F_q, output all (if any) the Reed-Solomon codewords contained in A_1 x *s x A_q. In particular, we study this problem when the lists A_1, ..., A_q are randomly chosen, and are of a certain size. This may be of independent interest.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.25/LIPIcs.FSTTCS.2019.25.pdf
List Recovery
Sharp Threshold
Fourier Analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
26:1
26:15
10.4230/LIPIcs.FSTTCS.2019.26
article
The Preemptive Resource Allocation Problem
Sarpatwar, Kanthi
1
https://orcid.org/0000-0002-7737-1200
Schieber, Baruch
2
Shachnai, Hadas
3
IBM T. J. Watson Research Center, Yorktown Heights, NY, United States of America
Computer Science Department, New Jersey Institute of Technology, Newark, NJ, United States of America
Computer Science Department, Technion, Haifa, Israel
We revisit a classical scheduling model to incorporate modern trends in data center networks and cloud services. Addressing some key challenges in the allocation of shared resources to user requests (jobs) in such settings, we consider the following variants of the classic resource allocation problem (RAP). The input to our problems is a set J of jobs and a set M of homogeneous hosts, each has an available amount of some resource. A job is associated with a release time, a due date, a weight and a given length, as well as its resource requirement. A feasible schedule is an allocation of the resource to a subset of the jobs, satisfying the job release times/due dates as well as the resource constraints. A crucial distinction between classic RAP and our problems is that we allow preemption and migration of jobs, motivated by virtualization techniques.
We consider two natural objectives: throughput maximization (MaxT), which seeks a maximum weight subset of the jobs that can be feasibly scheduled on the hosts in M, and resource minimization (MinR), that is finding the minimum number of (homogeneous) hosts needed to feasibly schedule all jobs. Both problems are known to be NP-hard. We first present an Omega(1)-approximation algorithm for MaxT instances where time-windows form a laminar family of intervals. We then extend the algorithm to handle instances with arbitrary time-windows, assuming there is sufficient slack for each job to be completed. For MinR we study a more general setting with d resources and derive an O(log d)-approximation for any fixed d >= 1, under the assumption that time-windows are not too small. This assumption can be removed leading to a slightly worse ratio of O(log d log^* T), where T is the maximum due date of any job.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.26/LIPIcs.FSTTCS.2019.26.pdf
Machine Scheduling
Resource Allocation
Vector Packing
Approximation Algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
27:1
27:14
10.4230/LIPIcs.FSTTCS.2019.27
article
Online and Offline Algorithms for Circuit Switch Scheduling
Schwartz, Roy
1
Singh, Mohit
2
Yazdanbod, Sina
2
Technion - Israel Institute of Technology, Haifa, Israel
Georgia Institute of Technology, Atlanta, GA, USA
Motivated by the use of high speed circuit switches in large scale data centers, we consider the problem of circuit switch scheduling. In this problem we are given demands between pairs of servers and the goal is to schedule at every time step a matching between the servers while maximizing the total satisfied demand over time. The crux of this scheduling problem is that once one shifts from one matching to a different one a fixed delay delta is incurred during which no data can be transmitted.
For the offline version of the problem we present a (1-(1/e)-epsilon) approximation ratio (for any constant epsilon >0). Since the natural linear programming relaxation for the problem has an unbounded integrality gap, we adopt a hybrid approach that combines the combinatorial greedy with randomized rounding of a different suitable linear program. For the online version of the problem we present a (bi-criteria) ((e-1)/(2e-1)-epsilon)-competitive ratio (for any constant epsilon >0 ) that exceeds time by an additive factor of O(delta/epsilon). We note that no uni-criteria online algorithm is possible. Surprisingly, we obtain the result by reducing the online version to the offline one.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.27/LIPIcs.FSTTCS.2019.27.pdf
approximation algorithm
online
matching
scheduling
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
28:1
28:14
10.4230/LIPIcs.FSTTCS.2019.28
article
On the Probabilistic Degrees of Symmetric Boolean Functions
Srinivasan, Srikanth
1
Tripathi, Utkarsh
1
Venkitesh, S.
1
Department of Mathematics, Indian Institute of Technology Bombay, Mumbai, India
The probabilistic degree of a Boolean function f:{0,1}^n -> {0,1} is defined to be the smallest d such that there is a random polynomial P of degree at most d that agrees with f at each point with high probability. Introduced by Razborov (1987), upper and lower bounds on probabilistic degrees of Boolean functions - specifically symmetric Boolean functions - have been used to prove explicit lower bounds, design pseudorandom generators, and devise algorithms for combinatorial problems.
In this paper, we characterize the probabilistic degrees of all symmetric Boolean functions up to polylogarithmic factors over all fields of fixed characteristic (positive or zero).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.28/LIPIcs.FSTTCS.2019.28.pdf
Symmetric Boolean function
probabilistic degree
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
29:1
29:14
10.4230/LIPIcs.FSTTCS.2019.29
article
Classification Among Hidden Markov Models
Akshay, S.
1
Bazille, Hugo
2
Fabre, Eric
2
Genest, Blaise
3
IIT Bombay, India
Univ Rennes, Inria, IRISA, France
Univ Rennes, CNRS, IRISA, France
An important task in AI is one of classifying an observation as belonging to one class among several (e.g. image classification). We revisit this problem in a verification context: given k partially observable systems modeled as Hidden Markov Models (also called labeled Markov chains), and an execution of one of them, can we eventually classify which system performed this execution, just by looking at its observations? Interestingly, this problem generalizes several problems in verification and control, such as fault diagnosis and opacity. Also, classification has strong connections with different notions of distances between stochastic models.
In this paper, we study a general and practical notion of classifiers, namely limit-sure classifiers, which allow misclassification, i.e. errors in classification, as long as the probability of misclassification tends to 0 as the length of the observation grows. To study the complexity of several notions of classification, we develop techniques based on a simple but powerful notion of stationary distributions for HMMs. We prove that one cannot classify among HMMs iff there is a finite separating word from their stationary distributions. This provides a direct proof that classifiability can be checked in PTIME, as an alternative to existing proofs using separating events (i.e. sets of infinite separating words) for the total variation distance. Our approach also allows us to introduce and tackle new notions of classifiability which are applicable in a security context.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.29/LIPIcs.FSTTCS.2019.29.pdf
verification: probabilistic systems
partially observable systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
30:1
30:15
10.4230/LIPIcs.FSTTCS.2019.30
article
Minimisation of Event Structures
Baldan, Paolo
1
https://orcid.org/0000-0001-9357-5599
Raffaetà, Alessandra
2
https://orcid.org/0000-0002-0295-8787
University of Padova, Italy
Ca' Foscari University of Venice, Italy
Event structures are fundamental models in concurrency theory, providing a representation of events in computation and of their relations, notably concurrency, conflict and causality. In this paper we present a theory of minimisation for event structures. Working in a class of event structures that generalises many stable event structure models in the literature, (e.g., prime, asymmetric, flow and bundle event structures) we study a notion of behaviour-preserving quotient, taking hereditary history preserving bisimilarity as a reference behavioural equivalence. We show that for any event structure a uniquely determined minimal quotient always exists. We observe that each event structure can be seen as the quotient of a prime event structure, and that quotients of general event structures arise from quotients of (suitably defined) corresponding prime event structures. This gives a special relevance to quotients in the class of prime event structures, which are then studied in detail, providing a characterisation and showing that also prime event structures always admit a unique minimal quotient.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.30/LIPIcs.FSTTCS.2019.30.pdf
Event structures
minimisation
history-preserving bisimilarity
behaviour-preserving quotient
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
31:1
31:15
10.4230/LIPIcs.FSTTCS.2019.31
article
Concurrent Parameterized Games
Bertrand, Nathalie
1
https://orcid.org/0000-0002-9957-5394
Bouyer, Patricia
2
https://orcid.org/0000-0002-2823-0911
Majumdar, Anirban
1
2
Univ. Rennes, Inria, CNRS, IRISA, Rennes, France
LSV, CNRS & ENS Paris-Saclay, Univ. Paris-Saclay, Cachan, France
Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. In this paper, we introduce a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear regular languages to describe the possible move combinations that lead from one vertex to another.
We consider the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve’s strategy should be independent of the number of opponents she actually has. Technically, this paper focuses on an a priori simpler setting where the languages labeling transitions only constrain the number of opponents (but not their precise action choices). These constraints are described as semilinear sets, finite unions of intervals, or intervals.
We establish the precise complexities of the parameterized reachability game problem, ranging from PTIME-complete to PSPACE-complete, in a variety of situations depending on the contraints (semilinear predicates, unions of intervals, or intervals) and on the presence or not of non-determinism.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.31/LIPIcs.FSTTCS.2019.31.pdf
concurrent games
parameterized verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
32:1
32:15
10.4230/LIPIcs.FSTTCS.2019.32
article
Expected Window Mean-Payoff
Bordais, Benjamin
1
Guha, Shibashis
2
Raskin, Jean-François
2
ENS Rennes, France
Université libre de Bruxelles, Belgium
We study the expected value of the window mean-payoff measure in Markov decision processes (MDPs) and Markov chains (MCs). The window mean-payoff measure strengthens the classical mean-payoff measure by measuring the mean-payoff over a window of bounded length that slides along an infinite path. This measure ensures better stability properties than the classical mean-payoff. Window mean-payoff has been introduced previously for two-player zero-sum games. As in the case of games, we study several variants of this definition: the measure can be defined to be prefix-independent or not, and for a fixed window length or for a window length that is left parametric. For fixed window length, we provide polynomial time algorithms for the prefix-independent version for both MDPs and MCs. When the length is left parametric, the problem of computing the expected value on MDPs is as hard as computing the mean-payoff value in two-player zero-sum games, a problem for which it is not known if it can be solved in polynomial time. For the prefix-dependent version, surprisingly, the expected window mean-payoff value cannot be computed in polynomial time unless P=PSPACE. For the parametric case and the prefix-dependent case, we manage to obtain algorithms with better complexities for MCs.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.32/LIPIcs.FSTTCS.2019.32.pdf
mean-payoff
Markov decision processes
synthesis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
33:1
33:14
10.4230/LIPIcs.FSTTCS.2019.33
article
Interval Temporal Logic for Visibly Pushdown Systems
Bozzelli, Laura
1
Montanari, Angelo
2
Peron, Adriano
1
University of Napoli "Federico II", Napoli, Italy
University of Udine, Udine, Italy
In this paper, we introduce and investigate an extension of Halpern and Shoham’s interval temporal logic HS for the specification and verification of branching-time context-free requirements of pushdown systems under a state-based semantics over Kripke structures. Both homogeneity and visibility are assumed. The proposed logic, called nested BHS, supports branching-time both in the past and in the future, and is able to express non-regular properties of linear and branching behaviours of procedural contexts in a natural way. It strictly subsumes well-known linear time context-free extensions of LTL such as CaRet [R. Alur et al., 2004] and NWTL [R. Alur et al., 2007]. The main result is the decidability of the visibly pushdown model-checking problem against nested BHS. The proof exploits a non-trivial automata-theoretic construction.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.33/LIPIcs.FSTTCS.2019.33.pdf
Pushdown systems
Interval temporal logic
Model checking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
34:1
34:14
10.4230/LIPIcs.FSTTCS.2019.34
article
Taming the Complexity of Timeline-Based Planning over Dense Temporal Domains
Bozzelli, Laura
1
Montanari, Angelo
2
Peron, Adriano
1
University of Napoli "Federico II", Napoli, Italy
University of Udine, Udine, Italy
The problem of timeline-based planning (TP) over dense temporal domains is known to be undecidable. In this paper, we introduce two semantic variants of TP, called strong minimal and weak minimal semantics, which allow to express meaningful properties. Both semantics are based on the minimality in the time distances of the existentially-quantified time events from the universally-quantified reference event, but the weak minimal variant distinguishes minimality in the past from minimality in the future. Surprisingly, we show that, despite the (apparently) small difference in the two semantics, for the strong minimal one, the TP problem is still undecidable, while for the weak minimal one, the TP problem is just PSPACE-complete. Membership in PSPACE is determined by exploiting a strictly more expressive extension (ECA^+) of the well-known robust class of Event-Clock Automata (ECA) that allows to encode the weak minimal TP problem and to reduce it to non-emptiness of Timed Automata (TA). Finally, an extension of ECA^+ (ECA^{++}) is considered, proving that its non-emptiness problem is undecidable. We believe that the two extensions of ECA (ECA^+ and ECA^{++}), introduced for technical reasons, are actually valuable per sé in the field of TA.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.34/LIPIcs.FSTTCS.2019.34.pdf
Timeline-based planning
timed automata
event-clock automata
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
35:1
35:14
10.4230/LIPIcs.FSTTCS.2019.35
article
Dynamics on Games: Simulation-Based Techniques and Applications to Routing
Brihaye, Thomas
1
Geeraerts, Gilles
2
Hallet, Marion
3
Monmege, Benjamin
4
https://orcid.org/0000-0002-4717-9955
Quoitin, Bruno
1
Université de Mons, Mons, Belgium
Université libre Bruxelles, Brussels, Belgium
Université de Mons, Mons, Belgium, Université libre Bruxelles, Brussels, Belgium
Aix Marseille Univ, CNRS, LIS, Université de Toulon, France
We consider multi-player games played on graphs, in which the players aim at fulfilling their own (not necessarily antagonistic) objectives. In the spirit of evolutionary game theory, we suppose that the players have the right to repeatedly update their respective strategies (for instance, to improve the outcome w.r.t. the current strategy profile). This generates a dynamics in the game which may eventually stabilise to an equilibrium. The objective of the present paper is twofold. First, we aim at drawing a general framework to reason about the termination of such dynamics. In particular, we identify preorders on games (inspired from the classical notion of simulation between transitions systems, and from the notion of graph minor) which preserve termination of dynamics. Second, we show the applicability of the previously developed framework to interdomain routing problems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.35/LIPIcs.FSTTCS.2019.35.pdf
games on graphs
dynamics
simulation
network
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
36:1
36:14
10.4230/LIPIcs.FSTTCS.2019.36
article
Query Preserving Watermarking Schemes for Locally Treelike Databases
Chattopadhyay, Agnishom
1
2
Praveen, M.
1
2
Chennai Mathematical Institute, Chennai, India
UMI ReLaX, Indo-French joint research unit
Watermarking is a way of embedding information in digital documents. Much research has been done on techniques for watermarking relational databases and XML documents, where the process of embedding information shouldn't distort query outputs too much. Recently, techniques have been proposed to watermark some classes of relational structures preserving first-order and monadic second order queries. For relational structures whose Gaifman graphs have bounded degree, watermarking can be done preserving first-order queries.
We extend this line of work and study watermarking schemes for other classes of structures. We prove that for relational structures whose Gaifman graphs belong to a class of graphs that have locally bounded tree-width and is closed under minors, watermarking schemes exist that preserve first-order queries. We use previously known properties of logical formulas and graphs, and build on them with some technical work to make them work in our context. This constitutes a part of the first steps to understand the extent to which techniques from algorithm design and computational learning theory can be adapted for watermarking.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.36/LIPIcs.FSTTCS.2019.36.pdf
Locally bounded tree-width
closure under minors
first-order queries
watermarking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
37:1
37:15
10.4230/LIPIcs.FSTTCS.2019.37
article
Complexity of Liveness in Parameterized Systems
Chini, Peter
1
Meyer, Roland
1
Saivasan, Prakash
1
TU Braunschweig, Germany
We investigate the fine-grained complexity of liveness verification for leader contributor systems. These consist of a designated leader thread and an arbitrary number of identical contributor threads communicating via a shared memory. The liveness verification problem asks whether there is an infinite computation of the system in which the leader reaches a final state infinitely often. Like its reachability counterpart, the problem is known to be NP-complete. Our results show that, even from a fine-grained point of view, the complexities differ only by a polynomial factor.
Liveness verification decomposes into reachability and cycle detection. We present a fixed point iteration solving the latter in polynomial time. For reachability, we reconsider the two standard parameterizations. When parameterized by the number of states of the leader L and the size of the data domain D, we show an (L + D)^O(L + D)-time algorithm. It improves on a previous algorithm, thereby settling an open problem. When parameterized by the number of states of the contributor C, we reuse an O^*(2^C)-time algorithm. We show how to connect both algorithms with the cycle detection to obtain algorithms for liveness verification. The running times of the composed algorithms match those of reachability, proving that the fine-grained lower bounds for liveness verification are met.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.37/LIPIcs.FSTTCS.2019.37.pdf
Liveness Verification
Fine-Grained Complexity
Parameterized Systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
38:1
38:14
10.4230/LIPIcs.FSTTCS.2019.38
article
Greibach Normal Form for omega-Algebraic Systems and Weighted Simple omega-Pushdown Automata
Droste, Manfred
1
Dziadek, Sven
1
Kuich, Werner
2
Institut für Informatik, Universität Leipzig, Germany
Institut für Diskrete Mathematik und Geometrie, Technische Unversität Wien, Austria
In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of omega-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted languages, or omega-algebraic series, can be represented as solutions of mixed omega-algebraic systems of equations and by weighted omega-pushdown automata.
In our first main result, we show that mixed omega-algebraic systems can be transformed into Greibach normal form. Our second main result proves that simple omega-reset pushdown automata recognize all omega-algebraic series that are a solution of an omega-algebraic system in Greibach normal form. Simple reset automata do not use epsilon-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted languages.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.38/LIPIcs.FSTTCS.2019.38.pdf
Weighted omega-Context-Free Grammars
Algebraic Systems
Greibach Normal Form
Weighted Automata
omega-Pushdown Automata
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
39:1
39:14
10.4230/LIPIcs.FSTTCS.2019.39
article
Transformations of Boolean Functions
Dudek, Jeffrey M.
1
https://orcid.org/0000-0001-9980-0320
Fried, Dror
2
Department of Computer Science, Rice University, Houston, TX, USA
Department of Mathematics and Computer Science, The Open University of Israel, Ra’anana, Israel
Boolean functions are characterized by the unique structure of their solution space. Some properties of the solution space, such as the possible existence of a solution, are well sought after but difficult to obtain. To better reason about such properties, we define transformations as functions that change one Boolean function to another while maintaining some properties of the solution space. We explore transformations of Boolean functions, compactly described as Boolean formulas, where the property is to maintain is the number of solutions in the solution spaces. We first discuss general characteristics of such transformations. Next, we reason about the computational complexity of transforming one Boolean formula to another. Finally, we demonstrate the versatility of transformations by extensively discussing transformations of Boolean formulas to "blocks," which are solution spaces in which the set of solutions makes a prefix of the solution space under a lexicographic order of the variables.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.39/LIPIcs.FSTTCS.2019.39.pdf
Boolean Formulas
Boolean Functions
Transformations
Model Counting
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
40:1
40:14
10.4230/LIPIcs.FSTTCS.2019.40
article
Two-Way Parikh Automata
Filiot, Emmanuel
1
Guha, Shibashis
1
Mazzocchi, Nicolas
1
Université libre de Bruxelles, Belgium
Parikh automata extend automata with counters whose values can only be tested at the end of the computation, with respect to membership into a semi-linear set. Parikh automata have found several applications, for instance in transducer theory, as they enjoy a decidable emptiness problem.
In this paper, we study two-way Parikh automata. We show that emptiness becomes undecidable in the non-deterministic case. However, it is PSpace-C when the number of visits to any input position is bounded and the semi-linear set is given as an existential Presburger formula. We also give tight complexity bounds for the inclusion, equivalence and universality problems. Finally, we characterise precisely the complexity of those problems when the semi-linear constraint is given by an arbitrary Presburger formula.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.40/LIPIcs.FSTTCS.2019.40.pdf
Parikh automata
two-way automata
Presburger arithmetic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
41:1
41:15
10.4230/LIPIcs.FSTTCS.2019.41
article
The Well Structured Problem for Presburger Counter Machines
Finkel, Alain
1
Gupta, Ekanshdeep
2
LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, IUF, France
Chennai Mathematical Institute, Chennai, India
We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.41/LIPIcs.FSTTCS.2019.41.pdf
Well structured transition systems
infinite state systems
Presburger counter machines
reachability
coverability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
42:1
42:15
10.4230/LIPIcs.FSTTCS.2019.42
article
A Categorical Account of Replicated Data Types
Gadducci, Fabio
1
http://orcid.org/0000-0003-0690-3051
Melgratti, Hernán
2
3
https://orcid.org/0000-0003-0760-0618
Roldán, Christian
2
https://orcid.org/0000-0001-9997-4857
Sammartino, Matteo
4
https://orcid.org/0000-0003-1456-2242
Dipartimento di Informatica, Università di Pisa, Italia
Departamento de Computación, Universidad de Buenos Aires, Argentina
ICC-CONICET-UBA, Buenos Aires, Argentina
Department of Computer Science, University College London, UK
Replicated Data Types (RDTs) have been introduced as a suitable abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature, RDTs are commonly specified in terms of two relations: visibility, which accounts for the different views that a store may have, and arbitration, which states the logical order imposed on the operations executed over the store. Different flavours, e.g., operational, axiomatic and functional, have recently been proposed for the specification of RDTs. In this work, we propose an algebraic characterisation of RDT specifications. We define categories of visibility relations and arbitrations, show the existence of relevant limits and colimits, and characterize RDT specifications as functors between such categories that preserve these additional structures.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.42/LIPIcs.FSTTCS.2019.42.pdf
Replicated data type
Specification
Functorial characterisation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
43:1
43:14
10.4230/LIPIcs.FSTTCS.2019.43
article
New Results on Cutting Plane Proofs for Horn Constraint Systems
Kleine Büning, Hans
1
Wojciechowski, Piotr
2
Subramani, K.
2
Universität Paderborn, Paderborn, Germany
LDCSEE, West Virginia University, Morgantown, WV, USA
In this paper, we investigate properties of cutting plane based refutations for a class of integer programs called Horn constraint systems (HCS). Briefly, a system of linear inequalities A * x >= b is called a Horn constraint system, if each entry in A belongs to the set {0,1,-1} and furthermore there is at most one positive entry per row. Our focus is on deriving refutations i.e., proofs of unsatisfiability of such programs using cutting planes as a proof system. We also look at several properties of these refutations. Horn constraint systems can be considered as a more general form of propositional Horn formulas, i.e., CNF formulas with at most one positive literal per clause. Cutting plane calculus (CP) is a well-known calculus for deciding the unsatisfiability of propositional CNF formulas and integer programs. Usually, CP consists of a pair of inference rules. These are called the addition rule (ADD) and the division rule (DIV). In this paper, we show that cutting plane calculus is still complete for Horn constraints when every intermediate constraint is required to be Horn. We also investigate the lengths of cutting plane proofs for Horn constraint systems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.43/LIPIcs.FSTTCS.2019.43.pdf
Horn constraints
cutting planes
proof length
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
44:1
44:14
10.4230/LIPIcs.FSTTCS.2019.44
article
The Tree-Generative Capacity of Combinatory Categorial Grammars
Kuhlmann, Marco
1
https://orcid.org/0000-0002-2492-9872
Maletti, Andreas
2
https://orcid.org/0000-0003-3202-0498
Schiffer, Lena Katharina
2
https://orcid.org/0000-0002-0164-2932
Dept. of Computer and Information Science, Linköping University, SE-581 83 Linköping, Sweden
Institute for Computer Science, Universität Leipzig, P.O. box 100 920, D-04009 Leipzig, Germany
The generative capacity of combinatory categorial grammars as acceptors of tree languages is investigated. It is demonstrated that the such obtained tree languages can also be generated by simple monadic context-free tree grammars. However, the subclass of pure combinatory categorial grammars cannot even accept all regular tree languages. Additionally, the tree languages accepted by combinatory categorial grammars with limited rule degrees are characterized: If only application rules are allowed, then they can accept only a proper subset of the regular tree languages, whereas they can accept exactly the regular tree languages once first degree composition rules are permitted.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.44/LIPIcs.FSTTCS.2019.44.pdf
Combinatory Categorial Grammar
Regular Tree Language
Linear Context-free Tree Language
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
45:1
45:14
10.4230/LIPIcs.FSTTCS.2019.45
article
Cyclic Proofs and Jumping Automata
Kuperberg, Denis
1
https://orcid.org/0000-0001-5406-717X
Pinault, Laureline
1
Pous, Damien
1
https://orcid.org/0000-0002-1220-4399
Univ Lyon, CNRS, ENS de Lyon, UCBL, LIP UMR 5668, F-69342, LYON Cedex 07, France
We consider a fragment of a cyclic sequent proof system for Kleene algebra, and we see it as a computational device for recognising languages of words. The starting proof system is linear and we show that it captures precisely the regular languages. When adding the standard contraction rule, the expressivity raises significantly; we characterise the corresponding class of languages using a new notion of multi-head finite automata, where heads can jump.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.45/LIPIcs.FSTTCS.2019.45.pdf
Cyclic proofs
regular languages
multi-head automata
transducers
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
46:1
46:16
10.4230/LIPIcs.FSTTCS.2019.46
article
Reachability in Concurrent Uninterpreted Programs
La Torre, Salvatore
1
Parthasarathy, Madhusudan
2
Università degli Studi di Salerno, Italia
University of Illinois, Urbana-Champaign, USA
We study the safety verification (reachability problem) for concurrent programs with uninterpreted functions/relations. By extending the notion of coherence, recently identified for sequential programs, to concurrent programs, we show that reachability in coherent concurrent programs under various scheduling restrictions is decidable by a reduction to multistack pushdown automata, and establish precise complexity bounds for them. We also prove that the coherence restriction for these various scheduling restrictions is itself a decidable property.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.46/LIPIcs.FSTTCS.2019.46.pdf
Verification
uninterpreted programs
concurrent programs
shared memory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
47:1
47:14
10.4230/LIPIcs.FSTTCS.2019.47
article
Distance Between Mutually Reachable Petri Net Configurations
Leroux, Jérôme
1
LaBRI, CNRS, Univ. Bordeaux, France
Petri nets are a classical model of concurrency widely used and studied in formal verification with many applications in modeling and analyzing hardware and software, data bases, and reactive systems. The reachability problem is central since many other problems reduce to reachability questions. In 2011, we proved that a variant of the reachability problem, called the reversible reachability problem is exponential-space complete. Recently, this problem found several unexpected applications in particular in the theory of population protocols. In this paper we revisit the reversible reachability problem in order to prove that the minimal distance in the reachability graph of two mutually reachable configurations is linear with respect to the Euclidean distance between those two configurations.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.47/LIPIcs.FSTTCS.2019.47.pdf
Petri nets
Vector addition systems
Formal verification
Reachability problem
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
48:1
48:15
10.4230/LIPIcs.FSTTCS.2019.48
article
Boolean Algebras from Trace Automata
Mansard, Alexandre
1
LIM, University of La Réunion, France
We consider trace automata. Their vertices are Mazurkiewicz traces and they accept finite words. Considering the length of a trace as the length of its Foata normal form, we define the operations of level-length synchronization and of superposition of trace automata. We show that if a family F of trace automata is closed under these operations, then for any deterministic automaton H in F, the word languages accepted by the deterministic automata of F that are length-reducible to H form a Boolean algebra. We show that the family of trace suffix automata with level-regular contexts and the subfamily of vector addition systems satisfy these closure properties. In particular, this yields various Boolean algebras of word languages accepted by deterministic vector addition systems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.48/LIPIcs.FSTTCS.2019.48.pdf
Boolean algebras
traces
automata
synchronization
pushdown automata
vector addition systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
49:1
49:14
10.4230/LIPIcs.FSTTCS.2019.49
article
Widths of Regular and Context-Free Languages
Mestel, David
1
University of Luxembourg
Given a partially-ordered finite alphabet Sigma and a language L subseteq Sigma^*, how large can an antichain in L be (where L is given the lexicographic ordering)? More precisely, since L will in general be infinite, we should ask about the rate of growth of maximum antichains consisting of words of length n. This fundamental property of partial orders is known as the width, and in a companion work [Mestel, 2019] we show that the problem of computing the information leakage permitted by a deterministic interactive system modeled as a finite-state transducer can be reduced to the problem of computing the width of a certain regular language. In this paper, we show that if L is regular then there is a dichotomy between polynomial and exponential antichain growth. We give a polynomial-time algorithm to distinguish the two cases, and to compute the order of polynomial growth, with the language specified as an NFA. For context-free languages we show that there is a similar dichotomy, but now the problem of distinguishing the two cases is undecidable. Finally, we generalise the lexicographic order to tree languages, and show that for regular tree languages there is a trichotomy between polynomial, exponential and doubly exponential antichain growth.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.49/LIPIcs.FSTTCS.2019.49.pdf
Formal languages
combinatorics on words
information flow
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
50:1
50:14
10.4230/LIPIcs.FSTTCS.2019.50
article
Degrees of Ambiguity of Büchi Tree Automata
Rabinovich, Alexander
1
https://orcid.org/0000-0002-1460-2358
Tiferet, Doron
1
Tel Aviv University, Israel
An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. An automaton is boundedly ambiguous if there is k in N, such that for every input it has at most k accepting computations. We consider nondeterministic Büchi automata (NBA) over infinite trees and prove that it is decidable in polynomial time, whether an automaton is unambiguous, boundedly ambiguous, finitely ambiguous, or countably ambiguous.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.50/LIPIcs.FSTTCS.2019.50.pdf
automata on infinite trees
ambiguous automata
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-12-04
150
51:1
51:15
10.4230/LIPIcs.FSTTCS.2019.51
article
Regular Separability and Intersection Emptiness Are Independent Problems
Thinniyam, Ramanathan S.
1
https://orcid.org/0000-0002-9926-0931
Zetzsche, Georg
1
https://orcid.org/0000-0002-6421-4388
Max Planck Institute for Software Systems (MPI-SWS), Germany
The problem of regular separability asks, given two languages K and L, whether there exists a regular language S that includes K and is disjoint from L. This problem becomes interesting when the input languages K and L are drawn from language classes beyond the regular languages. For such classes, a mild and useful assumption is that they are full trios, i.e. closed under rational transductions.
All the results on regular separability for full trios obtained so far exhibited a noteworthy correspondence with the intersection emptiness problem: In each case, regular separability is decidable if and only if intersection emptiness is decidable. This raises the question whether for full trios, regular separability can be reduced to intersection emptiness or vice-versa.
We present counterexamples showing that neither of the two problems can be reduced to the other. More specifically, we describe full trios C_1, D_1, C_2, D_2 such that (i) intersection emptiness is decidable for C_1 and D_1, but regular separability is undecidable for C_1 and D_1 and (ii) regular separability is decidable for C_2 and D_2, but intersection emptiness is undecidable for C_2 and D_2.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol150-fsttcs2019/LIPIcs.FSTTCS.2019.51/LIPIcs.FSTTCS.2019.51.pdf
Regular separability
intersection emptiness
decidability