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.

The lack of truly subcubic algorithms for pushdown reachability is difficult to justify by fine-grained reductions from SAT.

A decision procedure for Presburger arithmetic based on semilinear sets runs in triply exponential time.

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 relative to alternation depth.

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.

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?

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.

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?

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?

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?

We propose a definition of synchronizing words for nested word automata.

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.

What happens with reachability and coverability sets of VASS where counters can go negative and support reset? Also, a Π₂P lower bound on the inclusion problem for linear sets.

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.

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.

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.

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.

To measure how semilinear sets “grow” under Boolean operations, we keep track of the maximum norm of generators.

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 Π₂P-complete.