Search Results

Documents authored by Chistikov, Dmitry

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
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.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
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
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}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.94
On the Complexity of Quantified Integer Programming

Authors: Dmitry Chistikov and Christoph Haase

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
Quantified integer programming is the problem of deciding assertions of the form Q_k x_k ... forall x_2 exists x_1 : A * x >= c where vectors of variables x_k,..,x_1 form the vector x, all variables are interpreted over N (alternatively, over Z), and A and c are a matrix and vector over Z of appropriate sizes. We show in this paper that quantified integer programming with alternation depth k is complete for the kth level of the polynomial hierarchy.
Cite as

Dmitry Chistikov and Christoph Haase. On the Complexity of Quantified Integer Programming. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 94:1-94:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2017.94,
  author =	{Chistikov, Dmitry and Haase, Christoph},
  title =	{{On the Complexity of Quantified Integer Programming}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{94:1--94:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.94},
  URN =		{urn:nbn:de:0030-drops-75024},
  doi =		{10.4230/LIPIcs.ICALP.2017.94},
  annote =	{Keywords: integer programming, semi-linear sets, Presburger arithmetic, quantifier elimination}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.23
Fractional Coverings, Greedy Coverings, and Rectifier Networks

Authors: Dmitry Chistikov, Szabolcs Iván, Anna Lubiw, and Jeffrey Shallit

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
A rectifier network is a directed acyclic graph with distinguished sources and sinks; it is said to compute a Boolean matrix M that has a 1 in the entry (i,j) iff there is a path from the j-th source to the i-th sink. The smallest number of edges in a rectifier network that computes M is a classic complexity measure on matrices, which has been studied for more than half a century. We explore two techniques that have hitherto found little to no applications in this theory. They build upon a basic fact that depth-2 rectifier networks are essentially weighted coverings of Boolean matrices with rectangles. Using fractional and greedy coverings (defined in the standard way), we obtain new results in this area. First, we show that all fractional coverings of the so-called full triangular matrix have cost at least n log n. This provides (a fortiori) a new proof of the tight lower bound on its depth-2 complexity (the exact value has been known since 1965, but previous proofs are based on different arguments). Second, we show that the greedy heuristic is instrumental in tightening the upper bound on the depth-2 complexity of the Kneser-Sierpinski (disjointness) matrix. The previous upper bound is O(n^{1.28}), and we improve it to O(n^{1.17}), while the best known lower bound is Omega(n^{1.16}). Third, using fractional coverings, we obtain a form of direct product theorem that gives a lower bound on unbounded-depth complexity of Kronecker (tensor) products of matrices. In this case, the greedy heuristic shows (by an argument due to Lovász) that our result is only a logarithmic factor away from the "full" direct product theorem. Our second and third results constitute progress on open problem 7.3 and resolve, up to a logarithmic factor, open problem 7.5 from a recent book by Jukna and Sergeev (in Foundations and Trends in Theoretical Computer Science (2013)).
Cite as

Dmitry Chistikov, Szabolcs Iván, Anna Lubiw, and Jeffrey Shallit. Fractional Coverings, Greedy Coverings, and Rectifier Networks. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 23:1-23:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.STACS.2017.23,
  author =	{Chistikov, Dmitry and Iv\'{a}n, Szabolcs and Lubiw, Anna and Shallit, Jeffrey},
  title =	{{Fractional Coverings, Greedy Coverings, and Rectifier Networks}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{23:1--23:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.23},
  URN =		{urn:nbn:de:0030-drops-70107},
  doi =		{10.4230/LIPIcs.STACS.2017.23},
  annote =	{Keywords: rectifier network, OR-circuit, biclique covering, fractional covering, greedy covering}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.103
On Restricted Nonnegative Matrix Factorization

Authors: Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative n*m matrix M into a product of a nonnegative n*d matrix W and a nonnegative d*m matrix H. Restricted NMF requires in addition that the column spaces of M and W coincide. Finding the minimal inner dimension d is known to be NP-hard, both for NMF and restricted NMF. We show that restricted NMF is closely related to a question about the nature of minimal probabilistic automata, posed by Paz in his seminal 1971 textbook. We use this connection to answer Paz's question negatively, thus falsifying a positive answer claimed in 1974. Furthermore, we investigate whether a rational matrix M always has a restricted NMF of minimal inner dimension whose factors W and H are also rational. We show that this holds for matrices M of rank at most 3 and we exhibit a rank-4 matrix for which W and H require irrational entries.
Cite as

Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. On Restricted Nonnegative Matrix Factorization. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 103:1-103:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2016.103,
  author =	{Chistikov, Dmitry and Kiefer, Stefan and Marusic, Ines and Shirmohammadi, Mahsa and Worrell, James},
  title =	{{On Restricted Nonnegative Matrix Factorization}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{103:1--103:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.103},
  URN =		{urn:nbn:de:0030-drops-62389},
  doi =		{10.4230/LIPIcs.ICALP.2016.103},
  annote =	{Keywords: nonnegative matrix factorization, nonnegative rank, probabilistic automata, labelled Markov chains, minimization}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.128
The Taming of the Semi-Linear Set

Authors: Dmitry Chistikov and Christoph Haase

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
Semi-linear sets, which are rational subsets of the monoid (Z^d,+), have numerous applications in theoretical computer science. Although semi-linear sets are usually given implicitly, by formulas in Presburger arithmetic or by other means, the effect of Boolean operations on semi-linear sets in terms of the size of description has primarily been studied for explicit representations. In this paper, we develop a framework suitable for implicitly presented semi-linear sets, in which the size of a semi-linear set is characterized by its norm—the maximal magnitude of a generator. We put together a toolbox of operations and decompositions for semi-linear sets which gives bounds in terms of the norm (as opposed to just the bit-size of the description), a unified presentation, and simplified proofs. This toolbox, in particular, provides exponentially better bounds for the complement and set-theoretic difference. We also obtain bounds on unambiguous decompositions and, as an application of the toolbox, settle the complexity of the equivalence problem for exponent-sensitive commutative grammars.
Cite as

Dmitry Chistikov and Christoph Haase. The Taming of the Semi-Linear Set. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 128:1-128:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chistikov_et_al:LIPIcs.ICALP.2016.128,
  author =	{Chistikov, Dmitry and Haase, Christoph},
  title =	{{The Taming of the Semi-Linear Set}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{128:1--128:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.128},
  URN =		{urn:nbn:de:0030-drops-62636},
  doi =		{10.4230/LIPIcs.ICALP.2016.128},
  annote =	{Keywords: semi-linear sets, convex polyhedra, triangulations, integer linear programming, commutative grammars}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.339
Notes on Counting with Finite Machines

Authors: Dmitry Chistikov

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We determine the descriptional complexity (smallest number of states, up to constant factors) of recognizing languages {1^n} and {1^{t n} : t = 0, 1, 2, ...} with state-based finite machines of various kinds. This task is understood as counting to n and modulo n, respectively, and was previously studied for classes of finite-state automata by Kupferman, Ta-Shma, and Vardi (2001). We show that for Turing machines it requires log(n)/log(log(n)) states in the worst case, and individual values are related to Kolmogorov complexity of the binary encoding of n. For deterministic pushdown and counter automata, the complexity is log(n) and sqrt(n), respectively; for alternating counter automata, we show an upper bound of log(n). For visibly pushdown automata, i.e., if the stack movements are determined by input symbols, we consider languages {a^n b^n} and {a^{t n} b^{t n} : n t = 0, 1, 2, ...} and determine their complexity, of sqrt(n) and min(n_1 + n_2), respectively, with minimum over all factorizations n = n_1 n_2.
Cite as

Dmitry Chistikov. Notes on Counting with Finite Machines. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 339-350, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{chistikov:LIPIcs.FSTTCS.2014.339,
  author =	{Chistikov, Dmitry},
  title =	{{Notes on Counting with Finite Machines}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{339--350},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.339},
  URN =		{urn:nbn:de:0030-drops-48547},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.339},
  annote =	{Keywords: State complexity, Unary languages, Counting}
}
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 Imprint Privacy Contact