20 Search Results for "Chistikov, Dmitry"

Document
Invited Paper
DOI: 10.4230/LIPIcs.FSTTCS.2024.1
An Introduction to the Theory of Linear Integer Arithmetic (Invited Paper)

Authors: Dmitry Chistikov

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)

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
DOI: 10.4230/LIPIcs.CONCUR.2024.17
Invariants for One-Counter Automata with Disequality Tests

Authors: Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks, and Nicolas Waldburger

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value. This reachability problem has been known to be NP-hard and in PSPACE, and characterising its computational complexity has been left as a challenging open question by Almagor, Cohen, Pérez, Shirmohammadi, and Worrell (2020). We reduce the complexity gap, placing the problem into the second level of the polynomial hierarchy, namely into the class coNP^NP. In the presence of both equality and disequality tests, our upper bound is at the third level, P^NP^NP. To prove this result, we show that non-reachability can be witnessed by a pair of invariants (forward and backward). These invariants are almost inductive. They aim to over-approximate only a "core" of the reachability set instead of the entire set. The invariants are also leaky: it is possible to escape the set. We complement this with separate checks as the leaks can only occur in a controlled way.
Cite as

Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks, and Nicolas Waldburger. Invariants for One-Counter Automata with Disequality Tests. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2024.17,
  author =	{Chistikov, Dmitry and Leroux, J\'{e}r\^{o}me and Sinclair-Banks, Henry and Waldburger, Nicolas},
  title =	{{Invariants for One-Counter Automata with Disequality Tests}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{17:1--17:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.17},
  URN =		{urn:nbn:de:0030-drops-207898},
  doi =		{10.4230/LIPIcs.CONCUR.2024.17},
  annote =	{Keywords: Inductive invariant, Vector addition system, One-counter automaton}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2024.5
Fine-Grained Complexity of Program Analysis (Invited Talk)

Authors: Rupak Majumdar

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
There is a well-known "cubic bottleneck" in program analysis and language theory: many program analysis problems can be solved in time cubic in the size of the input but, despite years of effort, there are no known sub-cubic algorithms. For example, context-free reachability (whether there is a path in a labeled graph that is labeled with a word from a context-free language), the emptiness problem for pushdown automata, and the recognition problem for two-way nondeterministic pushdown automata all belong to the cubic class. We survey the status of these problems through the lens of fine-grained complexity. We study the related certification task: given an instance of any of these problems, are there small and efficiently checkable certificates for the existence and for the non-existence of a path? We show that, in both scenarios, there exist succinct certificates (O(n²) in the size of the problem) and these certificates can be checked in subcubic (matrix multiplication) time. Thus, all these problems lie in nondeterministic and co-nondeterministic subcubic time. We also study a hierarchy of program analysis problems above the cubic bottleneck. A representative problem here is the recognition problem for two-way nondeterministic pushdown automata with k heads. We show fine-grained hardness results for this hierarchy. We also discuss purely language-theoretic consequences of these results: for example, we obtain hardest languages accepted by two-way nondeterministic multihead pushdown automata, as well as separations between language classes. (Joint work with A. R. Balasubramanian, Dmitry Chistikov, and Philipp Schepper.)
Cite as

Rupak Majumdar. Fine-Grained Complexity of Program Analysis (Invited Talk). In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{majumdar:LIPIcs.MFCS.2024.5,
  author =	{Majumdar, Rupak},
  title =	{{Fine-Grained Complexity of Program Analysis}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{5:1--5:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.5},
  URN =		{urn:nbn:de:0030-drops-205619},
  doi =		{10.4230/LIPIcs.MFCS.2024.5},
  annote =	{Keywords: Fine-grained complexity, CFL reachability, 2NPDA recognition, PDA emptiness}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.132
Integer Linear-Exponential Programming in NP by Quantifier Elimination

Authors: Dmitry Chistikov, Alessio Mansutti, and Mikhail R. Starchak

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
This paper provides an NP procedure that decides whether a linear-exponential system of constraints has an integer solution. Linear-exponential systems extend standard integer linear programs with exponential terms 2^x and remainder terms (x mod 2^y). Our result implies that the existential theory of the structure (ℕ,0,1,+,2^(⋅),V_2(⋅,⋅), ≤) has an NP-complete satisfiability problem, thus improving upon a recent EXPSPACE upper bound. This theory extends the existential fragment of Presburger arithmetic with the exponentiation function x ↦ 2^x and the binary predicate V_2(x,y) that is true whenever y ≥ 1 is the largest power of 2 dividing x. Our procedure for solving linear-exponential systems uses the method of quantifier elimination. As a by-product, we modify the classical Gaussian variable elimination into a non-deterministic polynomial-time procedure for integer linear programming (or: existential Presburger arithmetic).
Cite as

Dmitry Chistikov, Alessio Mansutti, and Mikhail R. Starchak. Integer Linear-Exponential Programming in NP by Quantifier Elimination. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 132:1-132:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2024.132,
  author =	{Chistikov, Dmitry and Mansutti, Alessio and Starchak, Mikhail R.},
  title =	{{Integer Linear-Exponential Programming in NP by Quantifier Elimination}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{132:1--132:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.132},
  URN =		{urn:nbn:de:0030-drops-202758},
  doi =		{10.4230/LIPIcs.ICALP.2024.132},
  annote =	{Keywords: decision procedures, integer programming, quantifier elimination}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.16
Acyclic Petri and Workflow Nets with Resets

Authors: Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Filip Mazowiecki, and Henry Sinclair-Banks

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. Namely, we add an acyclicity condition that only applies to the consumptions and productions, not the resets. The first class is acyclic Petri nets with resets, and we show that coverability is PSPACE-complete for them. This contrasts the known Ackermann-hardness for coverability in (not necessarily acyclic) Petri nets with resets. We prove that the reachability problem remains undecidable for acyclic Petri nets with resets. The second class concerns workflow nets, a practically motivated and natural subclass of Petri nets. Here, we show that both coverability and reachability in acyclic workflow nets with resets are PSPACE-complete. Without the acyclicity condition, reachability and coverability in workflow nets with resets are known to be equally hard as for Petri nets with resets, that being Ackermann-hard and undecidable, respectively.
Cite as

Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Filip Mazowiecki, and Henry Sinclair-Banks. Acyclic Petri and Workflow Nets with Resets. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.FSTTCS.2023.16,
  author =	{Chistikov, Dmitry and Czerwi\'{n}ski, Wojciech and Hofman, Piotr and Mazowiecki, Filip and Sinclair-Banks, Henry},
  title =	{{Acyclic Petri and Workflow Nets with Resets}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.16},
  URN =		{urn:nbn:de:0030-drops-193892},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.16},
  annote =	{Keywords: Petri nets, Workflow Nets, Resets, Acyclic, Reachability, Coverability}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.112
The Complexity of Presburger Arithmetic with Power or Powers

Authors: Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We investigate expansions of Presburger arithmetic (Pa), i.e., the theory of the integers with addition and order, with additional structure related to exponentiation: either a function that takes a number to the power of 2, or a predicate 2^ℕ for the powers of 2. The latter theory, denoted Pa(2^ℕ(·)), was introduced by Büchi as a first attempt at characterizing the sets of tuples of numbers that can be expressed using finite automata; Büchi’s method does not give an elementary upper bound, and the complexity of this theory has been open. The former theory, denoted as Pa(λx.2^|x|), was shown decidable by Semenov; while the decision procedure for this theory differs radically from the automata-based method proposed by Büchi, Semenov’s method is also non-elementary. And in fact, the theory with the power function has a non-elementary lower bound. In this paper, we show that while Semenov’s and Büchi’s approaches yield non-elementary blow-ups for Pa(2^ℕ(·)), the theory is in fact decidable in triply exponential time, similarly to the best known quantifier-elimination algorithm for Pa. We also provide a NExpTime upper bound for the existential fragment of Pa(λx.2^|x|), a step towards a finer-grained analysis of its complexity. Both these results are established by analyzing a single parameterized satisfiability algorithm for Pa(λx.2^|x|), which can be specialized to either the setting of Pa(2^ℕ(·)) or the existential theory of Pa(λx.2^|x|). Besides the new upper bounds for the existential theory of Pa(λx.2^|x|) and Pa(2^ℕ(·)), we believe our algorithm provides new intuition for the decidability of these theories, and for the features that lead to non-elementary blow-ups.
Cite as

Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti. The Complexity of Presburger Arithmetic with Power or Powers. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 112:1-112:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{benedikt_et_al:LIPIcs.ICALP.2023.112,
  author =	{Benedikt, Michael and Chistikov, Dmitry and Mansutti, Alessio},
  title =	{{The Complexity of Presburger Arithmetic with Power or Powers}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{112:1--112:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.112},
  URN =		{urn:nbn:de:0030-drops-181641},
  doi =		{10.4230/LIPIcs.ICALP.2023.112},
  annote =	{Keywords: arithmetic theories, exponentiation, decision procedures}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.33
Higher-Order Quantified Boolean Satisfiability

Authors: Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, and Alessio Mansutti

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
The Boolean satisfiability problem plays a central role in computational complexity and is often used as a starting point for showing NP lower bounds. Generalisations such as Succinct SAT, where a Boolean formula is succinctly represented as a Boolean circuit, have been studied in the literature in order to lift the Boolean satisfiability problem to higher complexity classes such as NEXP. While, in theory, iterating this approach yields complete problems for k-NEXP for all k > 0, using such iterations of Succinct SAT is at best tedious when it comes to proving lower bounds. The main contribution of this paper is to show that the Boolean satisfiability problem has another canonical generalisation in terms of higher-order Boolean functions that is arguably more suitable for showing lower bounds beyond NP. We introduce a family of problems HOSAT(k,d), k ≥ 0, d ≥ 1, in which variables are interpreted as Boolean functions of order at most k and there are d quantifier alternations between functions of order exactly k. We show that the unbounded HOSAT problem is TOWER-complete, and that HOSAT(k,d) is complete for the weak k-EXP hierarchy with d alternations for fixed k,d ≥ 1 and d odd. We illustrate the usefulness of HOSAT by characterising the complexity of weak Presburger arithmetic, the first-order theory of the integers with addition and equality but without order. It has been a long-standing open problem whether weak Presburger arithmetic has the same complexity as standard Presburger arithmetic. We answer this question affirmatively, even for the negation-free fragment and the Horn fragment of weak Presburger arithmetic.
Cite as

Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, and Alessio Mansutti. Higher-Order Quantified Boolean Satisfiability. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.MFCS.2022.33,
  author =	{Chistikov, Dmitry and Haase, Christoph and Hadizadeh, Zahra and Mansutti, Alessio},
  title =	{{Higher-Order Quantified Boolean Satisfiability}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{33:1--33:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.33},
  URN =		{urn:nbn:de:0030-drops-168313},
  doi =		{10.4230/LIPIcs.MFCS.2022.33},
  annote =	{Keywords: Boolean satisfiability problem, higher-order Boolean functions, weak k-EXP hierarchies, non-elementary complexity, Presburger arithmetic}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.17
Adaptive Synchronisation of Pushdown Automata

Authors: A. R. Balasubramanian and K. S. Thejaswini

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
We introduce the notion of adaptive synchronisation for pushdown automata, in which there is an external observer who has no knowledge about the current state of the pushdown automaton, but can observe the contents of the stack. The observer would then like to decide if it is possible to bring the automaton from any state into some predetermined state by giving inputs to it in an adaptive manner, i.e., the next input letter to be given can depend on how the contents of the stack changed after the current input letter. We show that for non-deterministic pushdown automata, this problem is 2-EXPTIME-complete and for deterministic pushdown automata, we show EXPTIME-completeness. To prove the lower bounds, we first introduce (different variants of) subset-synchronisation and show that these problems are polynomial-time equivalent with the adaptive synchronisation problem. We then prove hardness results for the subset-synchronisation problems. For proving the upper bounds, we consider the problem of deciding if a given alternating pushdown system has an accepting run with at most k leaves and we provide an n^O(k²) time algorithm for this problem.
Cite as

A. R. Balasubramanian and K. S. Thejaswini. Adaptive Synchronisation of Pushdown Automata. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{balasubramanian_et_al:LIPIcs.CONCUR.2021.17,
  author =	{Balasubramanian, A. R. and Thejaswini, K. S.},
  title =	{{Adaptive Synchronisation of Pushdown Automata}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{17:1--17:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.17},
  URN =		{urn:nbn:de:0030-drops-143948},
  doi =		{10.4230/LIPIcs.CONCUR.2021.17},
  annote =	{Keywords: Adaptive synchronisation, Pushdown automata, Alternating pushdown systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.41
The Big-O Problem for Labelled Markov Chains and Weighted Automata

Authors: Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Given two weighted automata, we consider the problem of whether one is big-O of the other, i.e., if the weight of every finite word in the first is not greater than some constant multiple of the weight in the second. We show that the problem is undecidable, even for the instantiation of weighted automata as labelled Markov chains. Moreover, even when it is known that one weighted automaton is big-O of another, the problem of finding or approximating the associated constant is also undecidable. Our positive results show that the big-O problem is polynomial-time solvable for unambiguous automata, coNP-complete for unlabelled weighted automata (i.e., when the alphabet is a single character) and decidable, subject to Schanuel’s conjecture, when the language is bounded (i.e., a subset of w_1^* … w_m^* for some finite words w_1,… ,w_m). On labelled Markov chains, the problem can be restated as a ratio total variation distance, which, instead of finding the maximum difference between the probabilities of any two events, finds the maximum ratio between the probabilities of any two events. The problem is related to ε-differential privacy, for which the optimal constant of the big-O notation is exactly exp(ε).
Cite as

Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser. The Big-O Problem for Labelled Markov Chains and Weighted Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2020.41,
  author =	{Chistikov, Dmitry and Kiefer, Stefan and Murawski, Andrzej S. and Purser, David},
  title =	{{The Big-O Problem for Labelled Markov Chains and Weighted Automata}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{41:1--41:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.41},
  URN =		{urn:nbn:de:0030-drops-128534},
  doi =		{10.4230/LIPIcs.CONCUR.2020.41},
  annote =	{Keywords: weighted automata, labelled Markov chains, probabilistic systems}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.116
Rational Subsets of Baumslag-Solitar Groups

Authors: Michaël Cadilhac, Dmitry Chistikov, and Georg Zetzsche

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
We consider the rational subset membership problem for Baumslag-Solitar groups. These groups form a prominent class in the area of algorithmic group theory, and they were recently identified as an obstacle for understanding the rational subsets of GL(2,ℚ). We show that rational subset membership for Baumslag-Solitar groups BS(1,q) with q ≥ 2 is decidable and PSPACE-complete. To this end, we introduce a word representation of the elements of BS(1,q): their pointed expansion (PE), an annotated q-ary expansion. Seeing subsets of BS(1,q) as word languages, this leads to a natural notion of PE-regular subsets of BS(1,q): these are the subsets of BS(1,q) whose sets of PE are regular languages. Our proof shows that every rational subset of BS(1,q) is PE-regular. Since the class of PE-regular subsets of BS(1,q) is well-equipped with closure properties, we obtain further applications of these results. Our results imply that (i) emptiness of Boolean combinations of rational subsets is decidable, (ii) membership to each fixed rational subset of BS(1,q) is decidable in logarithmic space, and (iii) it is decidable whether a given rational subset is recognizable. In particular, it is decidable whether a given finitely generated subgroup of BS(1,q) has finite index.
Cite as

Michaël Cadilhac, Dmitry Chistikov, and Georg Zetzsche. Rational Subsets of Baumslag-Solitar Groups. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 116:1-116:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cadilhac_et_al:LIPIcs.ICALP.2020.116,
  author =	{Cadilhac, Micha\"{e}l and Chistikov, Dmitry and Zetzsche, Georg},
  title =	{{Rational Subsets of Baumslag-Solitar Groups}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{116:1--116:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.116},
  URN =		{urn:nbn:de:0030-drops-125238},
  doi =		{10.4230/LIPIcs.ICALP.2020.116},
  annote =	{Keywords: Rational subsets, Baumslag-Solitar groups, decidability, regular languages, pointed expansion}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.119
On the Power of Ordering in Linear Arithmetic Theories

Authors: Dmitry Chistikov and Christoph Haase

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
We study the problems of deciding whether a relation definable by a first-order formula in linear rational or linear integer arithmetic with an order relation is definable in absence of the order relation. Over the integers, this problem was shown decidable by Choffrut and Frigeri [Discret. Math. Theor. C., 12(1), pp. 21 - 38, 2010], albeit with non-elementary time complexity. Our contribution is to establish a full geometric characterisation of those sets definable without order which in turn enables us to prove coNP-completeness of this problem over the rationals and to establish an elementary upper bound over the integers. We also provide a complementary Π₂^P lower bound for the integer case that holds even in a fixed dimension. This lower bound is obtained by showing that universality for ultimately periodic sets, i.e., semilinear sets in dimension one, is Π₂^P-hard, which resolves an open problem of Huynh [Elektron. Inf.verarb. Kybern., 18(6), pp. 291 - 338, 1982].
Cite as

Dmitry Chistikov and Christoph Haase. On the Power of Ordering in Linear Arithmetic Theories. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 119:1-119:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2020.119,
  author =	{Chistikov, Dmitry and Haase, Christoph},
  title =	{{On the Power of Ordering in Linear Arithmetic Theories}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{119:1--119:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.119},
  URN =		{urn:nbn:de:0030-drops-125265},
  doi =		{10.4230/LIPIcs.ICALP.2020.119},
  annote =	{Keywords: logical definability, linear arithmetic theories, semi linear sets, ultimately periodic sets, numerical semigroups}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.123
The Strahler Number of a Parity Game

Authors: Laure Daviaud, Marcin Jurdziński, and K. S. Thejaswini

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
The Strahler number of a rooted tree is the largest height of a perfect binary tree that is its minor. The Strahler number of a parity game is proposed to be defined as the smallest Strahler number of the tree of any of its attractor decompositions. It is proved that parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices n and linear in (d/(2k))^k, where d is the number of priorities and k is the Strahler number. This complexity is quasi-polynomial because the Strahler number is at most logarithmic in the number of vertices. The proof is based on a new construction of small Strahler-universal trees. It is shown that the Strahler number of a parity game is a robust, and hence arguably natural, parameter: it coincides with its alternative version based on trees of progress measures and - remarkably - with the register number defined by Lehtinen (2018). It follows that parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices and linear in (d/(2k))^k, where k is the register number. This significantly improves the running times and space achieved for parity games of bounded register number by Lehtinen (2018) and by Parys (2020). The running time of the algorithm based on small Strahler-universal trees yields a novel trade-off k ⋅ lg(d/k) = O(log n) between the two natural parameters that measure the structural complexity of a parity game, which allows solving parity games in polynomial time. This includes as special cases the asymptotic settings of those parameters covered by the results of Calude, Jain Khoussainov, Li, and Stephan (2017), of Jurdziński and Lazić (2017), and of Lehtinen (2018), and it significantly extends the range of such settings, for example to d = 2^O(√{lg n}) and k = O(√{lg n}).
Cite as

Laure Daviaud, Marcin Jurdziński, and K. S. Thejaswini. The Strahler Number of a Parity Game. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 123:1-123:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{daviaud_et_al:LIPIcs.ICALP.2020.123,
  author =	{Daviaud, Laure and Jurdzi\'{n}ski, Marcin and Thejaswini, K. S.},
  title =	{{The Strahler Number of a Parity Game}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{123:1--123:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.123},
  URN =		{urn:nbn:de:0030-drops-125304},
  doi =		{10.4230/LIPIcs.ICALP.2020.123},
  annote =	{Keywords: parity game, attractor decomposition, progress measure, universal tree, Strahler number}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.10
Asymmetric Distances for Approximate Differential Privacy

Authors: Dmitry Chistikov, Andrzej S. Murawski, and David Purser

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Differential privacy is a widely studied notion of privacy for various models of computation, based on measuring differences between probability distributions. We consider (epsilon,delta)-differential privacy in the setting of labelled Markov chains. For a given epsilon, the parameter delta can be captured by a variant of the total variation distance, which we call lv_{alpha} (where alpha = e^{epsilon}). First we study lv_{alpha} directly, showing that it cannot be computed exactly. However, the associated approximation problem turns out to be in PSPACE and #P-hard. Next we introduce a new bisimilarity distance for bounding lv_{alpha} from above, which provides a tighter bound than previously known distances while remaining computable with the same complexity (polynomial time with an NP oracle). We also propose an alternative bound that can be computed in polynomial time. Finally, we illustrate the distances on case studies.
Cite as

Dmitry Chistikov, Andrzej S. Murawski, and David Purser. Asymmetric Distances for Approximate Differential Privacy. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2019.10,
  author =	{Chistikov, Dmitry and Murawski, Andrzej S. and Purser, David},
  title =	{{Asymmetric Distances for Approximate Differential Privacy}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.10},
  URN =		{urn:nbn:de:0030-drops-109121},
  doi =		{10.4230/LIPIcs.CONCUR.2019.10},
  annote =	{Keywords: Bisimilarity distances, Differential privacy, Labelled Markov chains}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.FSTTCS.2018.1
Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper)

Authors: Rupak Majumdar

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
Random testing has proven to be an effective way to catch bugs in concurrent and distributed systems. This is surprising, as the space of executions is enormous and conventional formal methods intuition would suggest that bad behaviors would only be found by extremely unlikely coincidences. Empirically, many bugs in distributed systems can be explained by interactions among only a small number of features. Thus, one can attempt to explain the effectiveness of random testing under various "small depth" hypotheses. In particular, it may be possible to test all interactions of k features for a small constant k by executing a family of tests that is exponentially or even doubly-exponentially smaller than the family of all tests. Moreover, under certain conditions, a randomly chosen small set of tests is sufficient to cover all k-wise interactions with high probability. I will describe two concrete scenarios. First, I will describe bugs in distributed systems caused by network partition faults. In many practical instances, these bugs occur due to two or three key nodes, such as leaders or replicas, not being able to communicate, or because the leading node finds itself in a block of the partition without quorum. In this case, I will show using the probabilistic method that a small set of randomly chosen tests will cover all "small partition" scenarios with high probability. Second, I will consider bugs that arise due to unexpected schedules (interleavings) of concurrent events. Again, many bugs depend only on the relative ordering of a small number of events (the "bug depth" of the bug). In this case, I will show a testing algorithm that prioritizes low depth interleavings and a randomized testing algorithm that bounds the probability of sampling any behavior of bug depth k for a fixed k. The testing algorithm is based on combinatorial insights from the theory of partial orders, such as the notion of dimension and its generalization to d-hitting families as well as results on online chain partitioning. Beyond the potential for designing or explaining random testing procedures, the technical arguments show the potential of combining "Theory A" and "Theory B" results to the important domain of software testing. This is joint work primarily with Filip Niksic [Filip Niksic, 2018], and with Dmitry Chistikov, Simin Oraee, Burcu Kulahcioglu Özkan, Mitra Tabaei Befrouei, and Georg Weissenbacher. This work was partially funded by an ERC Synergy Award (ImPACT).
Cite as

Rupak Majumdar. Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper). In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{majumdar:LIPIcs.FSTTCS.2018.1,
  author =	{Majumdar, Rupak},
  title =	{{Random Testing for Distributed Systems with Theoretical Guarantees}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.1},
  URN =		{urn:nbn:de:0030-drops-99000},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.1},
  annote =	{Keywords: Random testing, Hitting families}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2018.114
O-Minimal Invariants for Linear Loops

Authors: Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

Abstract
The termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Such deceptively simple questions also relate to a number of deep open problems, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this paper, we introduce the class of o-minimal invariants, which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel's conjecture in transcendental number theory.
Cite as

Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell. O-Minimal Invariants for Linear Loops. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 114:1-114:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.ICALP.2018.114,
  author =	{Almagor, Shaull and Chistikov, Dmitry and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{O-Minimal Invariants for Linear Loops}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{114:1--114:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.114},
  URN =		{urn:nbn:de:0030-drops-91188},
  doi =		{10.4230/LIPIcs.ICALP.2018.114},
  annote =	{Keywords: Invariants, linear loops, linear dynamical systems, non-termination, o-minimality}
}
  • Refine by Author
  • 16 Chistikov, Dmitry
  • 4 Haase, Christoph
  • 3 Mansutti, Alessio
  • 2 Kiefer, Stefan
  • 2 Majumdar, Rupak
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 3 decision procedures
  • 2 Presburger arithmetic
  • 2 integer programming
  • 2 labelled Markov chains
  • 2 quantifier elimination
  • Show More...

  • Refine by Type
  • 20 document

  • Refine by Publication Year
  • 4 2020
  • 4 2024
  • 2 2016
  • 2 2017
  • 2 2018
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact