# Publications on decision problems

**M. Benedikt, D. Chistikov, A. Mansutti. The complexity of Presburger arithmetic with power or powers.**ICALP 2023. [DROPS]Existence of solutions over N to systems of linear equations and constraints of the form

*y*=2^{x}can be decided in nondeterministic exponential time. Also, linear integer arithmetic extended with a predicate for powers of 2 can be decided in triply exponential time.

**D. Chistikov, R. Majumdar, P. Schepper. Subcubic certificates for CFL reachability.**POPL 2022. [doi]The lack of truly subcubic algorithms for pushdown reachability is difficult to justify by fine-grained reductions from SAT.

**D. Chistikov, C. Haase, A. Mansutti. Geometric decision procedures and the VC dimension of linear arithmetic theories.**LICS 2022. [WRAP]A decision procedure for Presburger arithmetic based on semilinear sets runs in triply exponential time.

**D. Chistikov, C. Haase, A. Mansutti. Quantifier elimination for counting extensions of Presburger arithmetic.**FoSSaCS 2022. [doi]We extend linear integer arithmetic with quantifiers of the form “there exists at least

*c*values of*x*” and similar. It turns out such theories still support efficient quantifier elimination, even in bounded alternation depth.

**D. Chistikov, C. Haase, Z. Hadizadeh, A. Mansutti. Higher-order Boolean satisfiability.**MFCS 2022. [DROPS]The decision problem for linear arithmetic over Z with just equality (no inequalities) is as hard as for standard linear integer arithmetic. To prove this, we define and study the complexity of a quantified version of SAT that supports higher-order Boolean functions.

**D. Chistikov, S. Kiefer, A. Murawski, D. Purser. The big-O problem.**Logical Methods in Computer Science (2022). [doi]Given two weighted automata (or labelled Markov chains), is there a constant

*c*such that the weight of every word in the first automaton is at most*c*times its weight in the second?

**S. Almagor, D. Chistikov, J. Ouaknine, J. Worrell. O-minimal invariants for discrete-time dynamical systems.**ACM Transactions on Computational Logic (2022). Extended version of the ICALP’18 paper. [doi]For

*while*loops of the form “while*x*in*S*do*x:=A*x*” (where*x*is initialized to a rational vector,*A*is a rational matrix, and*S*is a nice set), minimal invariants look like truncated cones.

**D. Chistikov, G. Lisowski, M. Paterson, P. Turrini. Convergence of opinion diffusion is PSPACE-complete.**AAAI 2020. [arXiv]Suppose in a directed graph each node is coloured 0 or 1. Update colours of all nodes simultaneously, each to the

*majority*among the incoming edges. Does this dynamics converge to a fixed colouring?

**D. Chistikov, C. Haase. On the power of ordering in linear arithmetic theories.**ICALP 2020. [DROPS] [WRAP]Given a formula of linear arithmetic, can we decide if the same set can be defined by another formula that uses just equality, without inequalities?

**D. Chistikov, M. Cadilhac, G. Zetzsche. Rational subsets of Baumslag-Solitar groups.**ICALP 2020. [DROPS] [arXiv]Imagine a “blind” Turing machine that cannot read bits written on the tape, but can increment a decrement them. The content of the tape is interpreted as the binary expansion of a rational number, and increments and decrements simply add and subtract (possibly negative) powers of two. What sets of numbers do these machines accept?

**D. Chistikov, S. Kiefer, A. Murawski, D. Purser. The big-O problem for labelled Markov chains and weighted automata.**CONCUR 2020. [DROPS] Extended version in Logical Methods in Computer Science (2022).

**D. Chistikov, P. Martyugin, M. Shirmohammadi. Synchronizing automata over nested words.**Journal of Automata, Languages and Combinatorics (2019). Extended version of the FoSSaCS’16 paper. [WRAP]We propose a definition of synchronizing words for nested word automata.

**D. Chistikov, A. Murawski, D. Purser. Asymmetric distances for approximate differential privacy.**CONCUR 2019. [DROPS]We measure distances between states in labelled Markov chains in the spirit of bisimilarity relation. It turns out that asymmetric distance functions are, in some sense, better.

**D. Chistikov, C. Haase, S. Halfon. Context-free commutative grammars with integer counters and resets.**Theoretical Computer Science (2018). Special issue for RP’14. [WRAP] [arXiv]What happens with reachability and coverability sets of VASS where counters can go negative and support reset? Also, a Π

_{2}P lower bound on the inclusion problem for linear sets.

**S. Almagor, D. Chistikov, J. Ouaknine, J. Worrell. O-minimal invariants for linear loops.**ICALP 2018. [DROPS] Extended version in ACM Transactions on Computational Logic (2022).

**D. Chistikov, A. Murawski, D. Purser. Bisimilarity distances for approximate differential privacy.**ATVA 2018. [arXiv]A pair of states in a labelled Markov chain can be bisimilar or not bisimilar. We extend this equivalence relation to a

*distance*function which upper-bounds the δ parameter in approximate differential privacy.

**D. Chistikov, R. Dimitrova, R. Majumdar. Approximate counting in SMT and value estimation for probabilistic programs.**ACTA Informatica (2017). Special issue for TACAS’15. [WRAP] [arXiv]Relying on ideas of Sipser and Stockmeyer, existing SMT solvers can do approximate model counting (discrete counting or volume estimation) for logical theories of arithmetic.

**D. Chistikov, C. Haase. On the complexity of quantified integer programming.**ICALP 2017. [DROPS] [pdf]If some variables in integer programs are quantified universally instead of existentially, then the decision problem becomes complete for the

*k*-th level of the polynomial hierarchy, assuming*k*quantifier blocks.

**D. Chistikov, S. Kiefer, I. Marušić, M. Shirmohammadi, J. Worrell. On restricted nonnegative matrix factorization.**ICALP 2016. [DROPS] [arXiv]There exists a pair of 3D polytopes with rational vertices, one inside the other, such that every

*intermediate*polytope with 5 vertices must have a vertex with an irrational coordinate.

**D. Chistikov, C. Haase. The taming of the semi-linear set.**ICALP 2016. [DROPS]To measure how semilinear sets “grow” under Boolean operations, we keep track of the maximum

*norm*of generators.

**D. Chistikov, P. Martyugin, M. Shirmohammadi. Synchronizing automata over nested words.**FoSSaCS 2016. Extended version in Journal of Automata, Languages and Combinatorics (2019).

**D. Chistikov, R. Dimitrova, R. Majumdar. Approximate counting in SMT and value estimation for probabilistic programs.**TACAS 2015. Extended version in Acta Informatica (2017).

**D. Chistikov, R. Majumdar. Unary pushdown automata and straight-line programs.**ICALP 2014. [arXiv]DPDA equivalence is in P for unary (singleton) input alphabet. This relies on algorithmics for grammar-compressed strings. Also, deciding if a CFG generates words of all lengths is Π

_{2}P-complete.