Minimisation questions on semi-linear sets and infinite-state systems

Semi-linear sets are a generalisation of ultimately periodic sets of integers to higher dimensions. They appear in a variety of Theoretical Computer Science topics; for instance, the Frobenius coin problem can be interpreted as the problem of finding the largest integer not contained in a given (1-dimensional) semi-linear set of a restricted form. In formal verification, the family of semi-linear sets forms a theoretical basis for a range of verification algorithms, by the virtue of coinciding with the family of sets definable in Presburger arithmetic, the first-order theory of the integers with addition and order. Periodic behaviour in software systems, especially those featuring concurrency, can often be captured by this logic, and then automated decision procedures (such as those implemented in satisfiability modulo theory solvers) pave the way for verification of these systems.

Because of the high computational complexity of the underlying decision problems, this approach relies on small representations of inputs. Depending on the exact setup, the semi-linear set may be represented using its generators (explicitly), by a formula in Presburger arithmetic, or even as an automaton or grammar arising as a formal model of a computer program. Succinct representations may, however, bring the complexity further up, which means that a tradeoff needs to be sought. However, for any given representation formalism, this raises the question of minimising representation size.

This project looks at minimisation and economy of description questions for semi-linear sets in several key representations, with the goals of finding (1) new characterizations, (2) efficient minimisation procedures, and (3) lower bound arguments. Lower bounds on representation size are of particular interest: for modeling formalisms that involve nondeterministic choice (such as automata, and non-deterministic infinite-state systems more widely) obtaining tight lower bounds on the representation size is a well-known challenge. In the present context, we expect to take advantage of the link to logic and geometry and of the new developments in the understanding of Presburger arithmetic, not explored previously in the context of minimisation and economy of description. We will consider several complexity measures, such as the number of bits and the number of sets in generator representation, the number of states of automata (such as counter automata, register machines, etc.). We will also be able to capitalise on recent advances in the theory of verification of infinite-state systems, such as the nonelementary lower bound for the reachability problem in vector addition systems.