Volume
LIPIcs, Volume 323
44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)
Publication Details
- published at: 2024-12-05
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-355-3
- DBLP: db/conf/fsttcs/fsttcs2024
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 323, FSTTCS 2024, Complete Volume
Abstract
LIPIcs, Volume 323, FSTTCS 2024, Complete Volume
Cite as
44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 1-670, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Proceedings{barman_et_al:LIPIcs.FSTTCS.2024,
title = {{LIPIcs, Volume 323, FSTTCS 2024, Complete Volume}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {1--670},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024},
URN = {urn:nbn:de:0030-drops-225763},
doi = {10.4230/LIPIcs.FSTTCS.2024},
annote = {Keywords: LIPIcs, Volume 323, FSTTCS 2024, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{barman_et_al:LIPIcs.FSTTCS.2024.0,
author = {Barman, Siddharth and Lasota, S{\l}awomir},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.0},
URN = {urn:nbn:de:0030-drops-225754},
doi = {10.4230/LIPIcs.FSTTCS.2024.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
An Introduction to the Theory of Linear Integer Arithmetic (Invited Paper)
Abstract
Presburger arithmetic, or linear integer arithmetic (LIA), is a logic that allows one to express linear constraints on integers: equalities, inequalities, and divisibility by nonzero n ∈ ℤ. More formally, it is the first-order theory of integers with addition and ordering. This paper offers a short introduction: what can be expressed in this logical theory, decision problems, and automated reasoning methods.
We begin with an elementary introduction, explaining the language of linear arithmetic constraints by examples. We adopt a theoretical perspective, focusing on the decision problem: determining the truth value of a logical sentence. The following three views on Presburger arithmetic give us three effective methods for decision procedures: a view from geometry (using semi-linear sets), from automata theory (using finite automata and recognizable sets), and from symbolic computation (using quantifier elimination).
The decision problem for existential formulas of Presburger arithmetic is essentially the feasibility problem of integer linear programming. By a fundamental result due to Borosh and Treybig [Proc. Am. Math. Soc. 55(2), 1976] and Papadimitriou [J. ACM 28(4), 1981], it belongs to the complexity class NP. Echoing the three views discussed above, we sketch three proofs of this result and discuss how these ideas have been used and developed in the recent research literature.
This is a companion paper for a conference talk focused on the three views on Presburger arithmetic and their applications. The reader will require background knowledge at the level of undergraduate computer science curricula. The discussion of complexity aspects is more advanced.
Cite as
Dmitry Chistikov. An Introduction to the Theory of Linear Integer Arithmetic (Invited Paper). In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 1:1-1:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{chistikov:LIPIcs.FSTTCS.2024.1,
author = {Chistikov, Dmitry},
title = {{An Introduction to the Theory of Linear Integer Arithmetic}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {1:1--1:36},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.1},
URN = {urn:nbn:de:0030-drops-221909},
doi = {10.4230/LIPIcs.FSTTCS.2024.1},
annote = {Keywords: Logical theories of arithmetic, decision procedures}
}
Document
Invited Paper
Advances in Algorithmic Meta Theorems (Invited Paper)
Abstract
Tractability results for the model checking problem of logics yield powerful algorithmic meta theorems of the form:
Every computational problem expressible in a logic ℒ can be solved efficiently on every class C of structures satisfying certain conditions.
The most prominent logics studied in the field are (counting) monadic second-order logic (C)MSO and first-order logic FO and its extensions. The complexity of CMSO model checking in general and of FO model checking on monotone graph classes is very well understood. In recent years there has been a rapid and exciting development of new algorithmic meta theorems. On the one hand there has been major progress for FO model checking on hereditary graph classes. This progress was driven by the development of a combinatorial structure theory for the logically defined monadically stable and monadically dependent graph classes, as well as by the advent of the new width measure twinwidth. On the other hand new algorithmic meta theorems for new logics with expressive power between FO and CMSO offer a new unifying view on methods like the irrelevant vertex technique and recursive understanding. In this paper we overview the recent advances in algorithmic meta theorems and provide rough sketches for the methods to prove them.
Cite as
Sebastian Siebertz and Alexandre Vigny. Advances in Algorithmic Meta Theorems (Invited Paper). In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 2:1-2:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{siebertz_et_al:LIPIcs.FSTTCS.2024.2,
author = {Siebertz, Sebastian and Vigny, Alexandre},
title = {{Advances in Algorithmic Meta Theorems}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {2:1--2:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.2},
URN = {urn:nbn:de:0030-drops-221912},
doi = {10.4230/LIPIcs.FSTTCS.2024.2},
annote = {Keywords: Algorithmic meta theorems, monadic second-order logic, first-order logic, disjoint paths logic, algorithmic graph structure theory}
}
Document
Execution-Time Opacity Problems in One-Clock Parametric Timed Automata
Abstract
Parametric timed automata (PTAs) extend the concept of timed automata, by allowing timing delays not only specified by concrete values but also by parameters, allowing the analysis of systems with uncertainty regarding timing behaviors. The full execution-time opacity is defined as the problem in which an attacker must never be able to deduce whether some private location was visited, by only observing the execution time. The problem of full ET-opacity emptiness (i.e., the emptiness over the parameter valuations for which full execution-time opacity is satisfied) is known to be undecidable for general PTAs. We therefore focus here on one-clock PTAs with integer-valued parameters over dense time. We show that the full ET-opacity emptiness is undecidable for a sufficiently large number of parameters, but is decidable for a single parameter, and exact synthesis can be effectively achieved. Our proofs rely on a novel construction as well as on variants of Presburger arithmetics. We finally prove an additional decidability result on an existential variant of execution-time opacity.
Cite as
Étienne André, Johan Arcile, and Engel Lefaucheux. Execution-Time Opacity Problems in One-Clock Parametric Timed Automata. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{andre_et_al:LIPIcs.FSTTCS.2024.3,
author = {Andr\'{e}, \'{E}tienne and Arcile, Johan and Lefaucheux, Engel},
title = {{Execution-Time Opacity Problems in One-Clock Parametric Timed Automata}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {3:1--3:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.3},
URN = {urn:nbn:de:0030-drops-221923},
doi = {10.4230/LIPIcs.FSTTCS.2024.3},
annote = {Keywords: Timed opacity, Parametric timed automata, Presburger arithmetic}
}
Document
The Parallel Dynamic Complexity of the Abelian Cayley Group Membership Problem
Abstract
Let G be a finite group given as input by its multiplication table. For a subset S ⊆ G and an element g ∈ G the Cayley Group Membership Problem (CGM) is to check if g belongs to the subgroup generated by S. While this problem is easily seen to be in polynomial time, pinpointing its parallel complexity has been of research interest over the years. Barrington et al [Barrington et al., 2001] have shown that for abelian groups the CGM problem can be solved in O(log log |G|) parallel time. In this paper we further explore the parallel complexity of the abelian CGM problem, with focus on the dynamic setting: the generating set S changes with insertions and deletions and the goal is to maintain a data structure that supports efficient membership queries to the subgroup ⟨S⟩. Though the static version of the CGM problem can be easily reduced to digraph reachability, the reduction does not carry over to the dynamic setting. We obtain the following results:
1) First, we consider the more general problem of Monoid Membership, where G is a monoid input by its multiplication table. When G is a commutative monoid we show there is a deterministic dynamic AC⁰ algorithm for membership testing that supports O(1) insertions and deletions in each step.
2) Building on the previous result we show that there is a dynamic randomized AC⁰ algorithm for abelian CGM that supports polylog(|G|) insertions/deletions to S in each step.
3) If the number of insertions/deletions is at most O(log n/log log n) then we obtain a deterministic dynamic AC⁰ algorithm for abelian CGM.
4) Applying these algorithms we obtain analogous results for the dynamic abelian Group Isomorphism. We can also handle sub-linearly many changes to the multiplication table for G, utilizing the hamming distance between multiplication tables of any two distinct groups.
Cite as
V. Arvind, Samir Datta, Asif Khan, Shivdutt Sharma, Yadu Vasudev, and Shankar Ram Vasudevan. The Parallel Dynamic Complexity of the Abelian Cayley Group Membership Problem. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{arvind_et_al:LIPIcs.FSTTCS.2024.4,
author = {Arvind, V. and Datta, Samir and Khan, Asif and Sharma, Shivdutt and Vasudev, Yadu and Vasudevan, Shankar Ram},
title = {{The Parallel Dynamic Complexity of the Abelian Cayley Group Membership Problem}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {4:1--4:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.4},
URN = {urn:nbn:de:0030-drops-221939},
doi = {10.4230/LIPIcs.FSTTCS.2024.4},
annote = {Keywords: Dynamic Complexity, Group Theory, Cayley Group Membership, Abelian Group Isomorphism}
}
Document
Concurrent Stochastic Games with Stateful-Discounted and Parity Objectives: Complexity and Algorithms
Abstract
We study two-player zero-sum concurrent stochastic games with finite state and action space played for an infinite number of steps. In every step, the two players simultaneously and independently choose an action. Given the current state and the chosen actions, the next state is obtained according to a stochastic transition function. An objective is a measurable function on plays (or infinite trajectories) of the game, and the value for an objective is the maximal expectation that the player can guarantee against the adversarial player. We consider: (a) stateful-discounted objectives, which are similar to the classic discounted-sum objectives, but states are associated with different discount factors rather than a single discount factor; and (b) parity objectives, which are a canonical representation for ω-regular objectives. For stateful-discounted objectives, given an ordering of the discount factors, the limit value is the limit of the value of the stateful-discounted objectives, as the discount factors approach zero according to the given order.
The computational problem we consider is the approximation of the value within an arbitrary additive error. The above problem is known to be in EXPSPACE for the limit value of stateful-discounted objectives and in PSPACE for parity objectives. The best-known algorithms for both the above problems are at least exponential time, with an exponential dependence on the number of states and actions. Our main results for the value approximation problem for the limit value of stateful-discounted objectives and parity objectives are as follows: (a) we establish TFNP[NP] complexity; and (b) we present algorithms that improve the dependency on the number of actions in the exponent from linear to logarithmic. In particular, if the number of states is constant, our algorithms run in polynomial time.
Cite as
Ali Asadi, Krishnendu Chatterjee, Raimundo Saona, and Jakub Svoboda. Concurrent Stochastic Games with Stateful-Discounted and Parity Objectives: Complexity and Algorithms. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{asadi_et_al:LIPIcs.FSTTCS.2024.5,
author = {Asadi, Ali and Chatterjee, Krishnendu and Saona, Raimundo and Svoboda, Jakub},
title = {{Concurrent Stochastic Games with Stateful-Discounted and Parity Objectives: Complexity and Algorithms}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {5:1--5:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.5},
URN = {urn:nbn:de:0030-drops-221942},
doi = {10.4230/LIPIcs.FSTTCS.2024.5},
annote = {Keywords: Concurrent Stochastic Games, Parity Objectives, Discounted-sum Objectives}
}
Document
A Decomposition Approach to the Weighted k-Server Problem
Abstract
A natural variant of the classical online k-server problem is the weighted k-server problem, where the cost of moving a server is its weight times the distance through which it moves. Despite its apparent simplicity, the weighted k-server problem is extremely poorly understood. Specifically, even on uniform metric spaces, finding the optimum competitive ratio of randomized algorithms remains an open problem - the best upper bound known is 2^{2^{k+O(1)}} due to a deterministic algorithm (Bansal et al., 2018), and the best lower bound known is Ω(2^k) (Ayyadevara and Chiplunkar, 2021).
With the aim of closing this exponential gap between the upper and lower bounds, we propose a decomposition approach for designing a randomized algorithm for weighted k-server on uniform metrics. Our first contribution includes two relaxed versions of the problem and a technique to obtain an algorithm for weighted k-server from algorithms for the two relaxed versions. Specifically, we prove that if there exists an α₁-competitive algorithm for one version (which we call Weighted k-Server - Service Pattern Construction) and there exists an α₂-competitive algorithm for the other version (which we call Weighted k-server - Revealed Service Pattern), then there exists an (α₁α₂)-competitive algorithm for weighted k-server on uniform metric spaces. Our second contribution is a 2^O(k²)-competitive randomized algorithm for Weighted k-server - Revealed Service Pattern. As a consequence, the task of designing a 2^poly(k)-competitive randomized algorithm for weighted k-server on uniform metrics reduces to designing a 2^poly(k)-competitive randomized algorithm for Weighted k-Server - Service Pattern Construction. Finally, we also prove that the Ω(2^k) lower bound for weighted k-server, in fact, holds for Weighted k-server - Revealed Service Pattern.
Cite as
Nikhil Ayyadevara, Ashish Chiplunkar, and Amatya Sharma. A Decomposition Approach to the Weighted k-Server Problem. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{ayyadevara_et_al:LIPIcs.FSTTCS.2024.6,
author = {Ayyadevara, Nikhil and Chiplunkar, Ashish and Sharma, Amatya},
title = {{A Decomposition Approach to the Weighted k-Server Problem}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {6:1--6:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.6},
URN = {urn:nbn:de:0030-drops-221954},
doi = {10.4230/LIPIcs.FSTTCS.2024.6},
annote = {Keywords: Online Algorithms, k-server, paging}
}
Document
Minimum Consistent Subset in Trees and Interval Graphs
Abstract
In the Minimum Consistent Subset (MCS) problem, we are presented with a connected simple undirected graph G, consisting of a vertex set V(G) of size n and an edge set E(G). Each vertex in V(G) is assigned a color from the set {1,2,…, c}. The objective is to determine a subset V' ⊆ V(G) with minimum possible cardinality, such that for every vertex v ∈ V(G), at least one of its nearest neighbors in V' (measured in terms of the hop distance) shares the same color as v. The decision problem, indicating whether there exists a subset V' of cardinality at most l for some positive integer l, is known to be NP-complete even for planar graphs.
In this paper, we establish that the MCS problem is NP-complete on trees. We also provide a fixed-parameter tractable (FPT) algorithm for MCS on trees parameterized by the number of colors (c) running in O(2^{6c} n^6) time, significantly improving the currently best-known algorithm whose running time is O(2^{4c} n^{2c+3}). In an effort to comprehensively understand the computational complexity of the MCS problem across different graph classes, we extend our investigation to interval graphs. We show that it remains NP-complete for interval graphs, thus enriching graph classes where MCS remains intractable.
Cite as
Aritra Banik, Sayani Das, Anil Maheshwari, Bubai Manna, Subhas C. Nandy, Krishna Priya K. M., Bodhayan Roy, Sasanka Roy, and Abhishek Sahu. Minimum Consistent Subset in Trees and Interval Graphs. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{banik_et_al:LIPIcs.FSTTCS.2024.7,
author = {Banik, Aritra and Das, Sayani and Maheshwari, Anil and Manna, Bubai and Nandy, Subhas C. and Priya K. M., Krishna and Roy, Bodhayan and Roy, Sasanka and Sahu, Abhishek},
title = {{Minimum Consistent Subset in Trees and Interval Graphs}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {7:1--7:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.7},
URN = {urn:nbn:de:0030-drops-221960},
doi = {10.4230/LIPIcs.FSTTCS.2024.7},
annote = {Keywords: Nearest-Neighbor Classification, Minimum Consistent Subset, Trees, Interval Graphs, Parameterized complexity, NP-complete}
}
Document
Beyond Decisiveness of Infinite Markov Chains
Abstract
Verification of infinite-state Markov chains is still a challenge despite several fruitful numerical or statistical approaches. For decisive Markov chains, there is a simple numerical algorithm that frames the reachability probability as accurately as required (however with an unknown complexity). On the other hand when applicable, statistical model checking is in most of the cases very efficient. Here we study the relation between these two approaches showing first that decisiveness is a necessary and sufficient condition for almost sure termination of statistical model checking. Afterwards we develop an approach with application to both methods that substitutes to a non decisive Markov chain a decisive Markov chain with the same reachability probability. This approach combines two key ingredients: abstraction and importance sampling (a technique that was formerly used for efficiency). We develop this approach on a generic formalism called layered Markov chain (LMC). Afterwards we perform an empirical study on probabilistic pushdown automata (an instance of LMC) to understand the complexity factors of the statistical and numerical algorithms. To the best of our knowledge, this prototype is the first implementation of the deterministic algorithm for decisive Markov chains and required us to solve several qualitative and numerical issues.
Cite as
Benoît Barbot, Patricia Bouyer, and Serge Haddad. Beyond Decisiveness of Infinite Markov Chains. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{barbot_et_al:LIPIcs.FSTTCS.2024.8,
author = {Barbot, Beno\^{i}t and Bouyer, Patricia and Haddad, Serge},
title = {{Beyond Decisiveness of Infinite Markov Chains}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {8:1--8:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.8},
URN = {urn:nbn:de:0030-drops-221977},
doi = {10.4230/LIPIcs.FSTTCS.2024.8},
annote = {Keywords: Markov Chains, Infinite State Systems, Numerical and Statistical Verification}
}
Document
Plan Logic
Abstract
When reasoning about games, one is often interested in verifying more intricate strategic properties than the mere existence of a winning strategy for a given coalition. Several languages, among which the very expressive Strategy Logic (SL), have been proposed that explicitly quantify over strategies in order to express and verify such properties. However, quantifying over strategies poses serious issues: not only does this lead to a non-elementary model-checking problem, but the classic Tarskian semantics is not fully adequate, both from a conceptual and practical viewpoint, since it does not guarantee the realisability of the strategies involved.
In this paper, we follow a different approach and introduce Plan Logic (PL), a logic that takes plans, i.e., sequences of actions, as first-class citizens instead of strategies. Since plans are much simpler objects than strategies, it becomes easier to enforce realisability. In this setting, we can recover strategic reasoning by means of a compositional hyperteams semantics, inspired by the well-known team semantics. We show that the Conjunctive-Goal and Disjunctive-Goal fragments of SL are captured by PL, with an effective polynomial translation. This result relies on the definition of a suitable game-theoretic semantics for the two fragments. We also investigate the model-checking problem for PL. For the full prenex fragment, the problem is shown to be fixed-parameter-tractable: it is polynomial in the size of the model, when the formula is fixed, and 2-ExpTimeC in the size of the formula. For the Conjunctive-Goal and Disjunctive-Goal fragments of PL this result can be improved to match the optimal polynomial complexity in the size of the model, regardless of the size of the formula.
Cite as
Dylan Bellier, Massimo Benerecetti, Fabio Mogavero, and Sophie Pinchinat. Plan Logic. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bellier_et_al:LIPIcs.FSTTCS.2024.9,
author = {Bellier, Dylan and Benerecetti, Massimo and Mogavero, Fabio and Pinchinat, Sophie},
title = {{Plan Logic}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.9},
URN = {urn:nbn:de:0030-drops-221988},
doi = {10.4230/LIPIcs.FSTTCS.2024.9},
annote = {Keywords: Logic for strategic reasoning, Strategy Logic, Realisable strategies, Strategies vs. plans, Hyperteam semantics}
}
Document
Explicit Commutative ROABPs from Partial Derivatives
Abstract
The dimension of partial derivatives (Nisan and Wigderson, 1997) is a popular measure for proving lower bounds in algebraic complexity. It is used to give strong lower bounds on the Waring decomposition of polynomials (called Waring rank). This naturally leads to an interesting open question: does this measure essentially characterize the Waring rank of any polynomial?
The well-studied model of Read-once Oblivious ABPs (ROABPs for short) lends itself to an interesting hierarchy of "sub-models": Any-Order-ROABPs (ARO), Commutative ROABPs, and Diagonal ROABPs. It follows from previous works that for any polynomial, a bound on its Waring rank implies an analogous bound on its Diagonal ROABP complexity (called the duality trick), and a bound on its dimension of partial derivatives implies an analogous bound on its "ARO complexity": ROABP complexity in any order (Nisan, 1991). Our work strengthens the latter connection by showing that a bound on the dimension of partial derivatives in fact implies a bound on the commutative ROABP complexity. Thus, we improve our understanding of partial derivatives and move a step closer towards answering the above question.
Our proof builds on the work of Ramya and Tengse (2022) to show that the commutative-ROABP-width of any homogeneous polynomial is at most the dimension of its partial derivatives. The technique itself is a generalization of the proof of the duality trick due to Saxena (2008).
Cite as
Vishwas Bhargava and Anamay Tengse. Explicit Commutative ROABPs from Partial Derivatives. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 10:1-10:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bhargava_et_al:LIPIcs.FSTTCS.2024.10,
author = {Bhargava, Vishwas and Tengse, Anamay},
title = {{Explicit Commutative ROABPs from Partial Derivatives}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {10:1--10:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.10},
URN = {urn:nbn:de:0030-drops-221994},
doi = {10.4230/LIPIcs.FSTTCS.2024.10},
annote = {Keywords: Partial derivatives, Apolar ideals, Commuting matrices, Branching programs}
}
Document
Many Flavors of Edit Distance
Abstract
Several measures exist for string similarity, including notable ones like the edit distance and the indel distance. The former measures the count of insertions, deletions, and substitutions required to transform one string into another, while the latter specifically quantifies the number of insertions and deletions. Many algorithmic solutions explicitly address one of these measures, and frequently techniques applicable to one can also be adapted to work with the other. In this paper, we investigate whether there exists a standardized approach for applying results from one setting to another. Specifically, we demonstrate the capability to reduce questions regarding string similarity over arbitrary alphabets to equivalent questions over a binary alphabet. Furthermore, we illustrate how to transform questions concerning indel distance into equivalent questions based on edit distance. This complements an earlier result of Tiskin (2007) which addresses the inverse direction.
Cite as
Sudatta Bhattacharya, Sanjana Dey, Elazar Goldenberg, and Michal Koucký. Many Flavors of Edit Distance. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bhattacharya_et_al:LIPIcs.FSTTCS.2024.11,
author = {Bhattacharya, Sudatta and Dey, Sanjana and Goldenberg, Elazar and Kouck\'{y}, Michal},
title = {{Many Flavors of Edit Distance}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {11:1--11:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.11},
URN = {urn:nbn:de:0030-drops-222004},
doi = {10.4230/LIPIcs.FSTTCS.2024.11},
annote = {Keywords: Edit distance, Indel distance, Embedding, LCS, Alphabet Reduction}
}
Document
Parallel Complexity of Geometric Bipartite Matching
Abstract
In this work, we study the parallel complexity of the geometric minimum-weight bipartite perfect matching (GWBPM) problem in ℝ². Here our graph is the complete bipartite graph G on two sets of points A and B in ℝ² (|A| = |B| = n) and the weight of each edge (a,b) ∈ A × B is the 𝓁_p distance (for some integer p ≥ 2) between the corresponding points, i.e., ||a-b||_p. The objective is to find a minimum weight perfect matching of A∪ B. In their seminal work, Mulmuley, Vazirani, and Vazirani (STOC 1987) showed that the weighted perfect matching problem on general bipartite graphs is in RNC. Almost three decades later, Fenner, Gurjar, and Thierauf (STOC 2016) showed that the problem is in Quasi-NC. Both of these results work only when the weights are of O(log n) bits. It is a long-standing open question to show the problem to be in NC.
First, we show that in a geometric bipartite graph under the 𝓁_p metric for any p ≥ 2, unless we take Ω(n) bits of approximation for weights, we cannot distinguish the minimum-weight perfect matching from other perfect matchings. This means that we cannot hope for an MVV-like NC/RNC algorithm for solving GWBPM exactly (even when vertex coordinates are small integers).
Next, we give an NC algorithm (assuming vertex coordinates are small integers) that solves GWBPM up to 1/poly(n) additive error, under the l_p metric for any p ≥ 2.
Cite as
Sujoy Bhore, Sarfaraz Equbal, and Rohit Gurjar. Parallel Complexity of Geometric Bipartite Matching. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bhore_et_al:LIPIcs.FSTTCS.2024.12,
author = {Bhore, Sujoy and Equbal, Sarfaraz and Gurjar, Rohit},
title = {{Parallel Complexity of Geometric Bipartite Matching}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {12:1--12:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.12},
URN = {urn:nbn:de:0030-drops-222014},
doi = {10.4230/LIPIcs.FSTTCS.2024.12},
annote = {Keywords: Parallel algorithms, Geometric matching, Derandomization, Isolation Lemma}
}
Document
PosSLP and Sum of Squares
Abstract
The problem PosSLP is the problem of determining whether a given straight-line program (SLP) computes a positive integer. PosSLP was introduced by Allender et al. to study the complexity of numerical analysis (Allender et al., 2009). PosSLP can also be reformulated as the problem of deciding whether the integer computed by a given SLP can be expressed as the sum of squares of four integers, based on the well-known result by Lagrange in 1770, which demonstrated that every natural number can be represented as the sum of four non-negative integer squares.
In this paper, we explore several natural extensions of this problem by investigating whether the positive integer computed by a given SLP can be written as the sum of squares of two or three integers. We delve into the complexity of these variations and demonstrate relations between the complexity of the original PosSLP problem and the complexity of these related problems. Additionally, we introduce a new intriguing problem called Div2SLP and illustrate how Div2SLP is connected to DegSLP and the problem of whether an SLP computes an integer expressible as the sum of three squares.
By comprehending the connections between these problems, our results offer a deeper understanding of decision problems associated with SLPs and open avenues for further exciting research.
Cite as
Markus Bläser, Julian Dörfler, and Gorav Jindal. PosSLP and Sum of Squares. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{blaser_et_al:LIPIcs.FSTTCS.2024.13,
author = {Bl\"{a}ser, Markus and D\"{o}rfler, Julian and Jindal, Gorav},
title = {{PosSLP and Sum of Squares}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.13},
URN = {urn:nbn:de:0030-drops-222028},
doi = {10.4230/LIPIcs.FSTTCS.2024.13},
annote = {Keywords: PosSLP, Straight-line program, Polynomial identity testing, Sum of squares}
}
Document
Unifying Asynchronous Logics for Hyperproperties
Abstract
We introduce and investigate a powerful hyper logical framework in the linear-time setting that we call generalized HyperLTL with stuttering and contexts (GHyperLTL_{S+C}} for short). GHyperLTL_{S+C} unifies the asynchronous extensions of HyperLTL called HyperLTL_S and HyperLTL_C, and the well-known extension KLTL of LTL with knowledge modalities under both the synchronous and asynchronous perfect recall semantics. As a main contribution, we identify a meaningful fragment of GHyperLTL_{S+C}, that we call simple GHyperLTL_{S+C}, with a decidable model-checking problem, which is more expressive than HyperLTL and known fragments of asynchronous extensions of HyperLTL with a decidable model-checking problem. Simple GHyperLTL_{S+C} subsumes KLTL under the synchronous semantics and the one-agent fragment of KLTL under the asynchronous semantics and to the best of our knowledge, it represents the unique hyper logic with a decidable model-checking problem which can express powerful non-regular trace properties when interpreted on singleton sets of traces. We justify the relevance of simple GHyperLTL_{S+C} by showing that it can express diagnosability properties, interesting classes of information-flow security policies, both in the synchronous and asynchronous settings, and bounded termination (more in general, global promptness in the style of Prompt LTL).
Cite as
Alberto Bombardelli, Laura Bozzelli, César Sánchez, and Stefano Tonetta. Unifying Asynchronous Logics for Hyperproperties. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bombardelli_et_al:LIPIcs.FSTTCS.2024.14,
author = {Bombardelli, Alberto and Bozzelli, Laura and S\'{a}nchez, C\'{e}sar and Tonetta, Stefano},
title = {{Unifying Asynchronous Logics for Hyperproperties}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.14},
URN = {urn:nbn:de:0030-drops-222034},
doi = {10.4230/LIPIcs.FSTTCS.2024.14},
annote = {Keywords: Asynchronous hyperproperties, Temporal logics for hyperproperties, Expressiveness, Decidability, Model checking}
}
Document
Promptness and Fairness in Muller LTL Formulas
Abstract
In this paper we consider two different views of the model checking problem for the Linear Temporal Logic (LTL). On the one hand, we consider the universal model checking problem for LTL, where one asks that for a given system and a given formula all the runs of the system satisfy the formula. On the other hand, the fair model checking problem for LTL asks that for a given system and a given formula almost all the runs of the system satisfy the formula.
It was shown that these two problems have the same theoretical complexity, i.e. PSPACE-complete. A less expensive fragment was identified in a previous work, namely the Muller fragment, which consists of combinations of repeated reachability properties.
We consider prompt LTL formulas (pLTL), that extend LTL with an additional operator, i.e. the prompt-eventually. This operator ensures the existence of a bound such that reachability properties are satisfied within this bound. This extension comes at no cost since the model checking problem remains PSPACE-complete.
We show that the corresponding Muller fragment of pLTL, with prompt repeated reachability properties, enjoys similar computational improvements. Another feature of Muller formulas is that the model checking problem becomes easier under the fairness assumption. This distinction is lost in the prompt setting, as we show that the two problems are equivalent instance-wise. Subsequently, we identify a new prefix independent fragment of pLTL for which the fair model checking problem is less expensive than the universal one.
Cite as
Damien Busatto-Gaston, Youssouf Oualhadj, Léo Tible, and Daniele Varacca. Promptness and Fairness in Muller LTL Formulas. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{busattogaston_et_al:LIPIcs.FSTTCS.2024.15,
author = {Busatto-Gaston, Damien and Oualhadj, Youssouf and Tible, L\'{e}o and Varacca, Daniele},
title = {{Promptness and Fairness in Muller LTL Formulas}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {15:1--15:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.15},
URN = {urn:nbn:de:0030-drops-222044},
doi = {10.4230/LIPIcs.FSTTCS.2024.15},
annote = {Keywords: Model checking, Fairness, Temporal logics}
}
Document
Learning Partitions Using Rank Queries
Abstract
We consider the problem of learning an unknown partition of an n element universe using rank queries. Such queries take as input a subset of the universe and return the number of parts of the partition it intersects. We give a simple O(n)-query, efficient, deterministic algorithm for this problem. We also generalize to give an O(n + klog r)-rank query algorithm for a general partition matroid where k is the number of parts and r is the rank of the matroid.
Cite as
Deeparnab Chakrabarty and Hang Liao. Learning Partitions Using Rank Queries. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 16:1-16:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{chakrabarty_et_al:LIPIcs.FSTTCS.2024.16,
author = {Chakrabarty, Deeparnab and Liao, Hang},
title = {{Learning Partitions Using Rank Queries}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {16:1--16:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.16},
URN = {urn:nbn:de:0030-drops-222051},
doi = {10.4230/LIPIcs.FSTTCS.2024.16},
annote = {Keywords: Query Complexity, Hypergraph Learning, Matroids}
}
Document
Two Results on LPT: A Near-Linear Time Algorithm and Parcel Delivery Using Drones
Abstract
The focus of this paper is to increase our understanding of the Longest Processing Time First (LPT) heuristic. LPT is a classical heuristic for the fundamental problem of uniform machine scheduling. For different machine speeds, LPT was first considered by Gonzalez et al. (SIAM J. Comput. 6(1):155–166, 1977). Since then, extensive work has been done to improve the approximation factor of the LPT heuristic. However, all known implementations of the LPT heuristic take O(mn) time, where m is the number of machines and n is the number of jobs. In this work, we come up with the first near-linear time implementation for LPT. Specifically, the running time is O((n+m)(log²m + log n)). Somewhat surprisingly, the result is obtained by mapping the problem to dynamic maintenance of lower envelope of lines, which has been well studied in the computational geometry community.
Our second contribution is to analyze the performance of LPT for the Drones Warehouse Problem (DWP), which is a natural generalization of the uniform machine scheduling problem motivated by drone-based parcel delivery from a warehouse. In this problem, a warehouse has multiple drones and wants to deliver parcels to several customers. Each drone picks a parcel from the warehouse, delivers it, and returns to the warehouse (where it can also get charged). The speeds and battery lives of the drones could be different, and due to the limited battery life, each drone has a bounded range in which it can deliver parcels. The goal is to assign parcels to the drones so that the time taken to deliver all the parcels is minimized. We prove that the natural approach of solving this problem via the LPT heuristic has an approximation factor of ϕ, where ϕ ≈ 1.62 is the golden ratio.
Cite as
L. Sunil Chandran, Rishikesh Gajjala, Shravan Mehra, and Saladi Rahul. Two Results on LPT: A Near-Linear Time Algorithm and Parcel Delivery Using Drones. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{chandran_et_al:LIPIcs.FSTTCS.2024.17,
author = {Chandran, L. Sunil and Gajjala, Rishikesh and Mehra, Shravan and Rahul, Saladi},
title = {{Two Results on LPT: A Near-Linear Time Algorithm and Parcel Delivery Using Drones}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {17:1--17:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.17},
URN = {urn:nbn:de:0030-drops-222060},
doi = {10.4230/LIPIcs.FSTTCS.2024.17},
annote = {Keywords: Scheduling, Approximation algorithms, Fine-grained complexity}
}
Document
Circuits, Proofs and Propositional Model Counting
Abstract
In this paper we present a new proof system framework CLIP (Circuit Linear Induction Proposition) for propositional model counting (#SAT). A CLIP proof firstly involves a Boolean circuit, calculating the cumulative function (or running count) of models counted up to a point, and secondly a propositional proof arguing for the correctness of the circuit.
This concept is remarkably simple and CLIP is modular so it allows us to use existing checking formats from propositional logic, especially strong proof systems. CLIP has polynomial-size proofs for XOR-pairs which are known to require exponential-size proofs in MICE [Fichte et al., 2022]. The existence of a strong proof system that can tackle these hard problems was posed as an open problem in Beyersdorff et al. [Olaf Beyersdorff et al., 2023]. In addition, CLIP systems can p-simulate all other existing #SAT proofs systems (KCPS(#SAT) [Florent Capelli, 2019], CPOG [Bryant et al., 2023], MICE). Furthermore, CLIP has a theoretical advantage over the other #SAT proof systems in the sense that CLIP only has lower bounds from its propositional proof system or if 𝖯^#𝖯 is not contained in P/poly, which is a major open problem in circuit complexity.
CLIP uses unrestricted circuits in its proof as compared to restricted structures used by the existing #SAT proof systems. In this way, CLIP avoids hardness or limitations due to circuit restrictions.
Cite as
Sravanthi Chede, Leroy Chew, and Anil Shukla. Circuits, Proofs and Propositional Model Counting. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{chede_et_al:LIPIcs.FSTTCS.2024.18,
author = {Chede, Sravanthi and Chew, Leroy and Shukla, Anil},
title = {{Circuits, Proofs and Propositional Model Counting}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {18:1--18:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.18},
URN = {urn:nbn:de:0030-drops-222079},
doi = {10.4230/LIPIcs.FSTTCS.2024.18},
annote = {Keywords: Propositional model counting, Boolean circuits, #SAT, Proof Systems, Certified Partition Operation Graph (CPOG)}
}
Document
Quantum Sabotage Complexity
Abstract
Given a Boolean function f : {0,1}ⁿ → {0,1}, the goal in the usual query model is to compute f on an unknown input x ∈ {0,1}ⁿ while minimizing the number of queries to x. One can also consider a "distinguishing" problem denoted by f_sab: given an input x ∈ f^{-1}(0) and an input y ∈ f^{-1}(1), either all differing bits are replaced by a *, or all differing bits are replaced by †, and an algorithm’s goal is to identify which of these is the case while minimizing the number of queries.
Ben-David and Kothari [ToC'18] introduced the notion of randomized sabotage complexity of a Boolean function to be the zero-error randomized query complexity of f_sab. A natural follow-up question is to understand the 𝖰(f_sab), the quantum query complexity of f_sab. In this paper, we initiate a systematic study of this. The following are our main results for all Boolean functions f : {0,1}ⁿ → {0,1}.
- If we have additional query access to x and y, then 𝖰(f_sab) = O(min{𝖰(f),√n}).
- If an algorithm is also required to output a differing index of a 0-input and a 1-input, then 𝖰(f_sab) = O(min{𝖰(f)^{1.5}, √n}).
- 𝖰(f_sab) = Ω(√{fbs(f)}), where fbs(f) denotes the fractional block sensitivity of f. By known results, along with the results in the previous bullets, this implies that 𝖰(f_sab) is polynomially related to 𝖰(f).
- The bound above is easily seen to be tight for standard functions such as And, Or, Majority and Parity. We show that when f is the Indexing function, 𝖰(f_sab) = Θ(fbs(f)), ruling out the possibility that 𝖰(f_sab) = Θ(√{fbs(f)}) for all f.
Cite as
Arjan Cornelissen, Nikhil S. Mande, and Subhasree Patro. Quantum Sabotage Complexity. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{cornelissen_et_al:LIPIcs.FSTTCS.2024.19,
author = {Cornelissen, Arjan and Mande, Nikhil S. and Patro, Subhasree},
title = {{Quantum Sabotage Complexity}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {19:1--19:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.19},
URN = {urn:nbn:de:0030-drops-222082},
doi = {10.4230/LIPIcs.FSTTCS.2024.19},
annote = {Keywords: Sabotage complexity, quantum query complexity, Boolean functions, fractional block sensitivity}
}
Document
The Isomorphism Problem of Power Graphs and a Question of Cameron
Abstract
We study the isomorphism problem of graphs that are defined in terms of groups, namely power graphs, directed power graphs, and enhanced power graphs. We design polynomial-time algorithms for the isomorphism problems for the power graphs, the directed power graphs and the enhanced power graphs arising from finite nilpotent groups. In contrast, no polynomial-time algorithm is known for the group isomorphism problem, even for nilpotent groups of class 2.
Our algorithms do not require the underlying groups of the input graphs to be given. A crucial step in our algorithms is to reconstruct the directed power graph from the given power graph or the enhanced power graph. The problem of efficiently computing the directed power graph from a power graph or an enhanced power graph is due to Cameron [IJGT'22]. Bubboloni and Pinzauti [Arxiv'22] gave a polynomial-time algorithm to reconstruct the directed power graph from a power graph. We give an efficient algorithm to compute the directed power graph from an enhanced power graph. The tools and techniques that we design are general enough to give a different algorithm to compute the directed power graph from a power graph as well.
Cite as
Bireswar Das, Jinia Ghosh, and Anant Kumar. The Isomorphism Problem of Power Graphs and a Question of Cameron. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 20:1-20:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.FSTTCS.2024.20,
author = {Das, Bireswar and Ghosh, Jinia and Kumar, Anant},
title = {{The Isomorphism Problem of Power Graphs and a Question of Cameron}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {20:1--20:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.20},
URN = {urn:nbn:de:0030-drops-222095},
doi = {10.4230/LIPIcs.FSTTCS.2024.20},
annote = {Keywords: Graph Isomorphism, Graphs defined on Groups, Power Graphs, Enhanced Power Graphs, Directed Power Graphs, Nilpotent Groups}
}
Document
A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets
Abstract
The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to the Myhill-Nerode theorem and a canonical automaton, which in turn, is the basis of several automata learning algorithms. A Nerode-like equivalence has been studied for various classes of timed languages.
In this work, we focus on timed automata with integer resets. This class is known to have good automata-theoretic properties and is also useful for practical modeling. Our main contribution is a Nerode-style equivalence for this class that depends on a constant K. We show that the equivalence leads to a Myhill-Nerode theorem and a canonical one-clock integer-reset timed automaton with maximum constant K. Based on the canonical form, we develop an Angluin-style active learning algorithm whose query complexity is polynomial in the size of the canonical form.
Cite as
Kyveli Doveri, Pierre Ganty, and B. Srivathsan. A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{doveri_et_al:LIPIcs.FSTTCS.2024.21,
author = {Doveri, Kyveli and Ganty, Pierre and Srivathsan, B.},
title = {{A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {21:1--21:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.21},
URN = {urn:nbn:de:0030-drops-222108},
doi = {10.4230/LIPIcs.FSTTCS.2024.21},
annote = {Keywords: Timed languages, Timed automata, Canonical representation, Myhill-Nerode equivalence, Integer reset}
}
Document
Counterfactual Explanations for MITL Violations
Abstract
MITL is a temporal logic that facilitates the verification of real-time systems by expressing the critical timing constraints placed on these systems. MITL specifications can be checked against system models expressed as networks of timed automata. A violation of an MITL specification is then witnessed by a timed trace of the network, i.e., an execution consisting of both discrete actions and real-valued delays between these actions. Finding and fixing the root cause of such a violation requires significant manual effort since both discrete actions and real-time delays have to be considered. In this paper, we present an automatic explanation method that eases this process by computing the root causes for the violation of an MITL specification on the execution of a network of timed automata. This method is based on newly developed definitions of counterfactual causality tailored to networks of timed automata in the style of Halpern and Pearl’s actual causality. We present and evaluate a prototype implementation that demonstrates the efficacy of our method on several benchmarks from the literature.
Cite as
Bernd Finkbeiner, Felix Jahn, and Julian Siber. Counterfactual Explanations for MITL Violations. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 22:1-22:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{finkbeiner_et_al:LIPIcs.FSTTCS.2024.22,
author = {Finkbeiner, Bernd and Jahn, Felix and Siber, Julian},
title = {{Counterfactual Explanations for MITL Violations}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {22:1--22:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.22},
URN = {urn:nbn:de:0030-drops-222116},
doi = {10.4230/LIPIcs.FSTTCS.2024.22},
annote = {Keywords: Timed automata, actual causality, metric interval temporal logic}
}
Document
Oblivious Complexity Classes Revisited: Lower Bounds and Hierarchies
Abstract
In this work we study oblivious complexity classes. These classes capture the power of interactive proofs where the prover(s) are only given the input size rather than the actual input. In particular, we study the connections between the symmetric polynomial time - S₂P and its oblivious counterpart - O₂P. Among our results:
- For each k ∈ ℕ, we construct an explicit language L_k ∈ O₂P that cannot be computed by circuits of size n^k.
- We prove a hierarchy theorem for O₂TIME. In particular, for any time constructible function t:ℕ → ℕ and any ε > 0 we show that: O₂TIME[t(n)] ⊊ O₂TIME[t(n)^{1 + ε}].
- We prove new structural results connecting O₂P and S₂P.
- We make partial progress towards the resolution of an open question posed by Goldreich and Meir (TOCT 2015) that relates the complexity of NP to its oblivious counterpart - ONP.
- We identify a natural class of problems in O₂P from computational Ramsey theory, that are not expected to be in 𝖯 or even BPP.
To the best of our knowledge, these results constitute the first explicit fixed-polynomial lower bound and hierarchy theorem for O₂P. The smallest uniform complexity class for which such lower bounds were previously known was S₂P due to Cai (JCSS 2007). In addition, this is the first uniform hierarchy theorem for a semantic class. All previous results required some non-uniformity. In order to obtain some of the results in the paper, we introduce the notion of uniformly-sparse extensions which could be of independent interest.
Our techniques build upon the de-randomization framework of the powerful Range Avoidance problem that has yielded many new interesting explicit circuit lower bounds.
Cite as
Karthik Gajulapalli, Zeyong Li, and Ilya Volkovich. Oblivious Complexity Classes Revisited: Lower Bounds and Hierarchies. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{gajulapalli_et_al:LIPIcs.FSTTCS.2024.23,
author = {Gajulapalli, Karthik and Li, Zeyong and Volkovich, Ilya},
title = {{Oblivious Complexity Classes Revisited: Lower Bounds and Hierarchies}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.23},
URN = {urn:nbn:de:0030-drops-222122},
doi = {10.4230/LIPIcs.FSTTCS.2024.23},
annote = {Keywords: fixed circuit lower bounds, semantic time hierarchy, oblivious complexity, range avoidance}
}
Document
When Far Is Better: The Chamberlin-Courant Approach to Obnoxious Committee Selection
Abstract
Classical work on metric space based committee selection problem interprets distance as "near is better". In this work, motivated by real-life situations, we interpret distance as "far is better". Formally stated, we initiate the study of "obnoxious" committee scoring rules when the voters' preferences are expressed via a metric space. To accomplish this, we propose a model where large distances imply high satisfaction (in contrast to the classical setting where shorter distances imply high satisfaction) and study the egalitarian avatar of the well-known Chamberlin-Courant voting rule and some of its generalizations. For a given integer value λ between 1 and k, the committee size, a voter derives satisfaction from only the λth favorite committee member; the goal is to maximize the satisfaction of the least satisfied voter. For the special case of λ = 1, this yields the egalitarian Chamberlin-Courant rule. In this paper, we consider general metric space and the special case of a d-dimensional Euclidean space.
We show that when λ is 1 and k, the problem is polynomial-time solvable in ℝ² and general metric space, respectively. However, for λ = k-1, it is NP-hard even in ℝ². Thus, we have "double-dichotomy" in ℝ² with respect to the value of λ, where the extreme cases are solvable in polynomial time but an intermediate case is NP-hard. Furthermore, this phenomenon appears to be "tight" for ℝ² because the problem is NP-hard for general metric space, even for λ = 1. Consequently, we are motivated to explore the problem in the realm of (parameterized) approximation algorithms and obtain positive results. Interestingly, we note that this generalization of Chamberlin-Courant rules encodes practical constraints that are relevant to solutions for certain facility locations.
Cite as
Sushmita Gupta, Tanmay Inamdar, Pallavi Jain, Daniel Lokshtanov, Fahad Panolan, and Saket Saurabh. When Far Is Better: The Chamberlin-Courant Approach to Obnoxious Committee Selection. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 24:1-24:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{gupta_et_al:LIPIcs.FSTTCS.2024.24,
author = {Gupta, Sushmita and Inamdar, Tanmay and Jain, Pallavi and Lokshtanov, Daniel and Panolan, Fahad and Saurabh, Saket},
title = {{When Far Is Better: The Chamberlin-Courant Approach to Obnoxious Committee Selection}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {24:1--24:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.24},
URN = {urn:nbn:de:0030-drops-222135},
doi = {10.4230/LIPIcs.FSTTCS.2024.24},
annote = {Keywords: Metric Space, Parameterized Complexity, Approximation, Obnoxious Facility Location}
}
Document
Better Boosting of Communication Oracles, or Not
Abstract
Suppose we have a two-party communication protocol for f which allows the parties to make queries to an oracle computing g; for example, they may query an Equality oracle. To translate this protocol into a randomized protocol, we must replace the oracle with a randomized subroutine for solving g. If q queries are made, the standard technique requires that we boost the error of each subroutine down to O(1/q), leading to communication complexity which grows as q log q. For which oracles g can this naïve boosting technique be improved?
We focus on the oracles which can be computed by constant-cost randomized protocols, and show that the naïve boosting strategy can be improved for the Equality oracle but not the 1-Hamming Distance oracle. Two surprising consequences are (1) a new example of a problem where the cost of computing k independent copies grows superlinear in k, drastically simplifying the only previous example due to Blais & Brody (CCC 2019); and (2) a new proof that Equality is not complete for the class of constant-cost randomized communication (Harms, Wild, & Zamaraev, STOC 2022; Hambardzumyan, Hatami, & Hatami, Israel Journal of Mathematics 2022).
Cite as
Nathaniel Harms and Artur Riazanov. Better Boosting of Communication Oracles, or Not. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 25:1-25:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{harms_et_al:LIPIcs.FSTTCS.2024.25,
author = {Harms, Nathaniel and Riazanov, Artur},
title = {{Better Boosting of Communication Oracles, or Not}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {25:1--25:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.25},
URN = {urn:nbn:de:0030-drops-222143},
doi = {10.4230/LIPIcs.FSTTCS.2024.25},
annote = {Keywords: oracles, error reduction, communication complexity}
}
Document
Two Views on Unification: Terms as Strategies
Abstract
In [Furio Honsell et al., 2024], the authors have shown that linear application in Geometry of Interaction (GoI) models of λ-calculus amounts to resolution between principal types of linear λ-terms. This analogy also works in the reverse direction. Indeed, an alternative definition of unification between algebraic terms can be given by viewing the terms to be unified as strategies, i.e. sets of pairs of occurrences of the same variable, and verifying the termination of the GoI interaction obtained by playing the two strategies. In this paper we prove that such a criterion of unification is equivalent to the standard one. It can be viewed as a local, bottom-up, definition of unification. Dually, it can be understood as the GoI interpretation of unification. The proof requires generalizing earlier work to arbitrary algebraic constructors and allowing for multiple occurrences of the same variable in terms. In particular, we show that two terms σ and τ unify if and only if R(σ) ⊆̂(τ) ;̂ ({R}(σ) ;̂ {R}(τ))^* and (τ) ⊆̂(σ) ;̂ ({R}(τ) ;̂ {R}(σ))^*, where {R}(σ) denotes the set of pairs of paths leading to the same variable in the term σ, ⊆̂ denotes "inclusion up to substitution" and ;̂ denotes "composition up to substitution".
Cite as
Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Two Views on Unification: Terms as Strategies. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 26:1-26:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{honsell_et_al:LIPIcs.FSTTCS.2024.26,
author = {Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan},
title = {{Two Views on Unification: Terms as Strategies}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {26:1--26:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.26},
URN = {urn:nbn:de:0030-drops-222158},
doi = {10.4230/LIPIcs.FSTTCS.2024.26},
annote = {Keywords: unification, geometry of interaction, games}
}
Document
On Approximation Schemes for Stabbing Rectilinear Polygons
Abstract
We study the problem of stabbing rectilinear polygons, where we are given n rectilinear polygons in the plane that we want to stab, i.e., we want to select horizontal line segments such that for each given rectilinear polygon there is a line segment that intersects two opposite (parallel) edges of it. Our goal is to find a set of line segments of minimum total length such that all polygons are stabbed. For the special case of rectangles, there is an O(1)-approximation algorithm and the problem is NP-hard [Chan, van Dijk, Fleszar, Spoerhase, and Wolff, 2018]. Also, the problem admits a QPTAS [Eisenbrand, Gallato, Svensson, and Venzin, 2021] and even a PTAS [Khan, Subramanian, and Wiese, 2022]. However, the approximability for the setting of more general polygons, e.g., L-shapes or T-shapes, is completely open.
In this paper, we give conditions under which the problem admits a (1+ε)-approximation algorithm. We assume that each input polygon is composed of rectangles that are placed on top of each other. We show that if all input polygons satisfy the hourglass condition, then the problem admits a quasi-polynomial time approximation scheme. In particular, it is thus unlikely that this case is APX-hard. Furthermore, we show that there exists a PTAS if each input polygon is composed out of rectangles with a bounded range of widths. On the other hand, we prove that the general case of the problem (in which the input polygons may not satisfy these conditions) is APX-hard, already if all input polygons have only eight edges. We remark that all polygons with fewer edges automatically satisfy the hourglass condition. For arbitrary rectilinear polygons we even show a lower bound of Ω(log n) for the possible approximation ratio, which implies that the best possible ratio is in Θ(log n) since the problem is a special case of Set Cover.
Cite as
Arindam Khan, Aditya Subramanian, Tobias Widmann, and Andreas Wiese. On Approximation Schemes for Stabbing Rectilinear Polygons. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{khan_et_al:LIPIcs.FSTTCS.2024.27,
author = {Khan, Arindam and Subramanian, Aditya and Widmann, Tobias and Wiese, Andreas},
title = {{On Approximation Schemes for Stabbing Rectilinear Polygons}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.27},
URN = {urn:nbn:de:0030-drops-222166},
doi = {10.4230/LIPIcs.FSTTCS.2024.27},
annote = {Keywords: Approximation Algorithms, Stabbing, Rectangles, Rectilinear Polygons, QPTAS, APX-hardness}
}
Document
Maximizing Phylogenetic Diversity Under Ecological Constraints: A Parameterized Complexity Study
Abstract
In the NP-hard Optimizing Phylogenetic Diversity with Dependencies(PDD) problem, the input consists of a phylogenetic tree 𝒯 over a set of taxa X, a food-web that describes the prey-predator relationships in X, and integers k and D. The task is to find a set S of k species that is viable in the food-web such that the subtree of 𝒯 obtained by retaining only the vertices of S has total edge weight at least D. Herein, viable means that for every predator taxon of S, the set S contains at least one prey taxon.
We provide the first systematic analysis of PDD and its special case with star trees, s-PDD, from a parameterized complexity perspective. For solution-size related parameters, we show that PDD is fixed-parameter tractable (FPT) with respect to D and with respect to k plus the height of the phylogenetic tree. Moreover, we consider structural parameterizations of the food-web. For example, we show an FPT-algorithm for the parameter that measures the vertex deletion distance to graphs where every connected component is a complete graph. Finally, we show that s-PDD admits an FPT-algorithm for the treewidth of the food-web. This disproves, unless P = NP, a conjecture of Faller et al. [Annals of Combinatorics, 2011] who conjectured that s-PDD is NP-hard even when the food-web is a tree.
Cite as
Christian Komusiewicz and Jannik Schestag. Maximizing Phylogenetic Diversity Under Ecological Constraints: A Parameterized Complexity Study. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{komusiewicz_et_al:LIPIcs.FSTTCS.2024.28,
author = {Komusiewicz, Christian and Schestag, Jannik},
title = {{Maximizing Phylogenetic Diversity Under Ecological Constraints: A Parameterized Complexity Study}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.28},
URN = {urn:nbn:de:0030-drops-222175},
doi = {10.4230/LIPIcs.FSTTCS.2024.28},
annote = {Keywords: phylogenetic diversity, food-webs, structural parameterization, color-coding, dynamic programming}
}
Document
Matchings in Low-Arboricity Graphs in the Dynamic Graph Stream Model
Abstract
We consider the problem of estimating the size of a maximum matching in low-arboricity graphs in the dynamic graph stream model. In this setting, an algorithm with limited memory makes multiple passes over a stream of edge insertions and deletions, resulting in a low-arboricity graph. Let n be the number of vertices of the input graph, and α be its arboricity. We give the following results.
1) As our main result, we give a three-pass streaming algorithm that produces an (α + 2)(1 + ε)-approximation and uses space O(ε^{-2}⋅α²⋅n^{1/2}⋅log n). This result should be contrasted with the Ω(α^{-5/2}⋅n^{1/2}) space lower bound established by [Assadi et al., SODA'17] for one-pass algorithms, showing that, for graphs of constant arboricity, the one-pass space lower bound can be achieved in three passes (up to poly-logarithmic factors). Furthermore, we obtain a two-pass algorithm that uses space O(ε^{-2}⋅α²⋅n^{3/5}⋅log n).
2) We also give a (1+ε)-approximation multi-pass algorithm, where the space used is parameterized by an upper bound on the size of a largest matching. For example, using O(log log n) passes, the space required is O(ε^{-1}⋅α²⋅k⋅log n), where k denotes an upper bound on the size of a largest matching. Finally, we define a notion of arboricity in the context of matrices. This is a natural measure of the sparsity of a matrix that is more nuanced than simply bounding the total number of nonzero entries, but less restrictive than bounding the number of nonzero entries in each row and column. For such matrices, we exploit our results on estimating matching size to present upper bounds for the problem of rank estimation in the dynamic data stream model.
Cite as
Christian Konrad, Andrew McGregor, Rik Sengupta, and Cuong Than. Matchings in Low-Arboricity Graphs in the Dynamic Graph Stream Model. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 29:1-29:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{konrad_et_al:LIPIcs.FSTTCS.2024.29,
author = {Konrad, Christian and McGregor, Andrew and Sengupta, Rik and Than, Cuong},
title = {{Matchings in Low-Arboricity Graphs in the Dynamic Graph Stream Model}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {29:1--29:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.29},
URN = {urn:nbn:de:0030-drops-222187},
doi = {10.4230/LIPIcs.FSTTCS.2024.29},
annote = {Keywords: Data Streams, Graph Matching, Graph Arboricity}
}
Document
Improved Linearly Ordered Colorings of Hypergraphs via SDP Rounding
Abstract
We consider the problem of linearly ordered (LO) coloring of hypergraphs. A hypergraph has an LO coloring if there is a vertex coloring, using a set of ordered colors, so that (i) no edge is monochromatic, and (ii) each edge has a unique maximum color. It is an open question as to whether or not a 2-LO colorable 3-uniform hypergraph can be LO colored with 3 colors in polynomial time. Nakajima and Živný recently gave a polynomial-time algorithm to color such hypergraphs with Õ(n^{1/3}) colors and asked if SDP methods can be used directly to obtain improved bounds. Our main result is to show how to use SDP-based rounding methods to produce an LO coloring with Õ(n^{1/5}) colors for such hypergraphs. We show how to reduce the problem to cases with highly structured SDP solutions, which we call balanced hypergraphs. Then we discuss how to apply classic SDP-rounding tools in this case to obtain improved bounds.
Cite as
Anand Louis, Alantha Newman, and Arka Ray. Improved Linearly Ordered Colorings of Hypergraphs via SDP Rounding. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{louis_et_al:LIPIcs.FSTTCS.2024.30,
author = {Louis, Anand and Newman, Alantha and Ray, Arka},
title = {{Improved Linearly Ordered Colorings of Hypergraphs via SDP Rounding}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {30:1--30:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.30},
URN = {urn:nbn:de:0030-drops-222199},
doi = {10.4230/LIPIcs.FSTTCS.2024.30},
annote = {Keywords: hypergraph coloring, SDP rounding, promise constraint satisfaction problems}
}
Document
Parameterized Algorithms and Hardness for the Maximum Edge q-Coloring Problem
Abstract
An edge q-coloring of a graph G is a coloring of its edges such that every vertex sees at most q colors on the edges incident on it. The size of an edge q-coloring is the total number of colors used in the coloring. Given a graph G and a positive integer t, the Maximum Edge q-Coloring problem is about whether G has an edge q-coloring of size t. Studies on this coloring problem were motivated by its application in the channel assignment problem in wireless networks.
Goyal, Kamat, and Misra (MFCS 2013) studied Maximum Edge 2-Coloring from the perspective of parameterized complexity. Given a graph on n vertices, they considered the standard parameter t, the number of colors in an optimal edge 2-coloring, and the dual parameter 𝓁, where n-𝓁 is the number of colors in an optimal edge 2-coloring. They designed FPT algorithms for Maximum Edge 2-Coloring parameterized by t and 𝓁. In this paper, we revisit and study Maximum Edge 2-Coloring from the perspective of parameterized complexity and show the following results.
1) Let γ(G) denote the maximum matching size in a given graph G. It is easy to see that a maximum edge 2-coloring of G is of size at least γ(G). Goyal, Kamat, and Misra (MFCS 2013) had asked if there exists an FPT algorithm for Maximum Edge 2-Coloring parameterized by k, where k: = (size of a maximum edge 2-coloring of G) - γ(G). We show that Maximum Edge 2-Coloring parameterized by k is W[1] hard.
2) On the positive side, we show that there is an algorithm that, given a graph G on n vertices and a tree decomposition of width tw, runs in time 2^{O(qtw log {q tw})}n and outputs a maximum edge q-coloring of G.
Cite as
Rogers Mathew, Fahad Panolan, and Seshikanth. Parameterized Algorithms and Hardness for the Maximum Edge q-Coloring Problem. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 31:1-31:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{mathew_et_al:LIPIcs.FSTTCS.2024.31,
author = {Mathew, Rogers and Panolan, Fahad and Seshikanth},
title = {{Parameterized Algorithms and Hardness for the Maximum Edge q-Coloring Problem}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {31:1--31:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.31},
URN = {urn:nbn:de:0030-drops-222202},
doi = {10.4230/LIPIcs.FSTTCS.2024.31},
annote = {Keywords: FPT algorithm, Edge coloring, Treewidth, W\lbrack1\rbrack-hardness}
}
Document
Additive Word Complexity and Walnut
Abstract
In combinatorics on words, a classical topic of study is the number of specific patterns appearing in infinite sequences. For instance, many works have been dedicated to studying the so-called factor complexity of infinite sequences, which gives the number of different factors (contiguous subblocks of their symbols), as well as abelian complexity, which counts factors up to a permutation of letters. In this paper, we consider the relatively unexplored concept of additive complexity, which counts the number of factors up to additive equivalence. We say that two words are additively equivalent if they have the same length and the total weight of their letters is equal. Our contribution is to expand the general knowledge of additive complexity from a theoretical point of view and consider various famous examples. We show a particular case of an analog of the long-standing conjecture on the regularity of the abelian complexity of an automatic sequence. In particular, we use the formalism of logic, and the software Walnut, to decide related properties of automatic sequences. We compare the behaviors of additive and abelian complexities, and we also consider the notion of abelian and additive powers. Along the way, we present some open questions and conjectures for future work.
Cite as
Pierre Popoli, Jeffrey Shallit, and Manon Stipulanti. Additive Word Complexity and Walnut. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{popoli_et_al:LIPIcs.FSTTCS.2024.32,
author = {Popoli, Pierre and Shallit, Jeffrey and Stipulanti, Manon},
title = {{Additive Word Complexity and Walnut}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {32:1--32:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.32},
URN = {urn:nbn:de:0030-drops-222218},
doi = {10.4230/LIPIcs.FSTTCS.2024.32},
annote = {Keywords: Combinatorics on words, Abelian complexity, Additive complexity, Automatic sequences, Walnut software}
}
Document
Pseudo-Deterministic Construction of Irreducible Polynomials over Finite Fields
Abstract
We present a polynomial-time pseudo-deterministic algorithm for constructing irreducible polynomial of degree d over finite field 𝔽_q. A pseudo-deterministic algorithm is allowed to use randomness, but with high probability it must output a canonical irreducible polynomial. Our construction runs in time Õ(d⁴log⁴q).
Our construction extends Shoup’s deterministic algorithm (FOCS 1988) for the same problem, which runs in time Õ(d⁴p^{1/2}log⁴q) (where p is the characteristic of the field 𝔽_q). Shoup had shown a reduction from constructing irreducible polynomials to factoring polynomials over finite fields. We show that by using a fast randomized factoring algorithm, the above reduction yields an efficient pseudo-deterministic algorithm for constructing irreducible polynomials over finite fields.
Cite as
Shanthanu S. Rai. Pseudo-Deterministic Construction of Irreducible Polynomials over Finite Fields. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 33:1-33:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{rai:LIPIcs.FSTTCS.2024.33,
author = {Rai, Shanthanu S.},
title = {{Pseudo-Deterministic Construction of Irreducible Polynomials over Finite Fields}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {33:1--33:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.33},
URN = {urn:nbn:de:0030-drops-222227},
doi = {10.4230/LIPIcs.FSTTCS.2024.33},
annote = {Keywords: Algebra and Computation, Finite fields, Factorization, Pseudo-deterministic, Polynomials}
}
Document
A Quadratic Upper Bound on the Reset Thresholds of Synchronizing Automata Containing a Transitive Permutation Group
Abstract
For any synchronizing n-state deterministic automaton, Černý conjectures the existence of a synchronizing word of length at most (n-1)². We prove that there exists a synchronizing word of length at most 2n² - 7n + 7 for every synchronizing n-state deterministic automaton that satisfies the following two properties: 1. The image of the action of each letter contains at least n-1 states; 2. The actions of bijective letters generate a transitive permutation group on the state set.
Cite as
Yinfeng Zhu. A Quadratic Upper Bound on the Reset Thresholds of Synchronizing Automata Containing a Transitive Permutation Group. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 34:1-34:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{zhu:LIPIcs.FSTTCS.2024.34,
author = {Zhu, Yinfeng},
title = {{A Quadratic Upper Bound on the Reset Thresholds of Synchronizing Automata Containing a Transitive Permutation Group}},
booktitle = {44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
pages = {34:1--34:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-355-3},
ISSN = {1868-8969},
year = {2024},
volume = {323},
editor = {Barman, Siddharth and Lasota, S{\l}awomir},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.34},
URN = {urn:nbn:de:0030-drops-222236},
doi = {10.4230/LIPIcs.FSTTCS.2024.34},
annote = {Keywords: \v{C}ern\'{y} conjecture, deterministic finite automaton, permutation group, reset threshold, synchronizing automaton}
}