I've been busy these last few years trying to get a clear
picture of the complexity of problems that arise from the use of
well-quasi-orders and well-structured transition systems. Here
is some of the material I co-authored on the subject:
A write-up on non-elementary complexity classes and
problems: Complexity Hierarchies Beyond
Elementary. Ultimately, I think the main point I try to make in the technical developments is that people should forget all the low-level details found in this paper—which are shown to have little to no impact at such high complexities—, and just use the classes without worrying.
The slides of a talk on the
subject. (Warning: those are heavy HTML5 slides.)
Joint work with David Baelde from LSV and Simon Lunel and based on Simon's Master Thesis. As a first dive into proof systems for data-aware logics, in the context of the ANR Prodaq project, we propose a sequent calculus for a modal fragment of DataXPath. We further show that proof search in this calculus can be performed in PSPACE, which is optimal for the logic.
Joint work with R. Lazić from U. Warwick. We re-prove Bozzelli & Ganty's 2EXP upper bound on the backward coverability algorithm for VAS using ideal representations of downwards-closed sets. This yields a generic means of proving complexity upper bounds for coverability in WSTS. Presented at RP 2015.
Joint work with M. Jurdziński and R. Lazić from U. Warwick. We show that multi-dimensional energy games can be solved in pseudo-polynomial time when the dimension is fixed, answering an open question of Chaloupka (2013). This entails a 2EXP upper bound for multidimensional energy games when both the dimension and the initial credit are part of the input, answering an open question of Brázdil et al. (2010), and closes the gap with 2EXP hardness proven last year with J.-B. Courtois. Presented at ICALP 2015.
Joint work with J. Leroux from LaBRI. The decidability of reachability in vector addition systems (VAS), or equivalently in Petri nets, is arguably one of the landmark results in theoretical computer science. The first proof by Mayr (1981) and its further simplifications by Kosaraju (1982) and Lambert (1992) are extremely complex on two accounts.
First, on a conceptual side, they rely on a somewhat magical decomposition technique. We expose the tricks involved in this construction, by showing that this decomposition technique can be recast as the computation of an ideal decomposition of the set of runs, for an appropriately chosen well-quasi-ordering on runs.
Second, on a complexity side, no upper bounds were known until now for the decomposition algorithms. Using recent results on the complexity of algorithms that terminate thanks to well-quasi-orderings, we provide the first known upper bound on the VAS reachability problem: it belongs to ${\mathbf{F}}_{{\omega}^{3}}$, a non primitive-recursive complexity class, among the lowest multiply-recursive complexites.
Well-quasi-orders provide termination or finiteness arguments for many
algorithms, and miniaturised versions can furthermore be employed to
prove complexity upper bounds for those algorithms. We have however
an issue with these bounds: they go way beyond the familiar complexity
classes used in complexity theory. I shall discuss a definition of
complexity classes suitable for the task. In particular, unlike the
subrecursive classes they are based on, those classes support the
usual notions of reduction and completeness. The talk will be based on the article Complexity hierarchies beyond Elementary to appear in ToCT.
Chalk talk on ideals in VAS reachability. The decidability of the reachability problem for vector addition systems is a notoriously difficult result. First shown by Mayr in 1981 after a decade of unsuccessful attempts and partial results, its proof has been simplified and refined several times, by Kosaraju and Lambert, and re-proven by very different techniques by Leroux in 2011. The principles behind the original proof remained however obscure.
In this seminar, I presented the ideas behind the algorithms of Mayr, Kosaraju, and Lambert (the KLM algorithm) in the light of ideals of well-quasi-orders. The interest here is that ideals provide a semantics to the structures manipulated in the KLM algorithm, bringing some new understanding to its proof of correctness. This approach is based on a joint work with Jérôme Leroux (LaBRI) presented at LICS'15.
Chalk talk on ideals of well-quasi-orders. These irreducible downwards-closed sets of elements were first invented in the 1970's but rediscovered in recent years in the theory of well-structured transition systems, notably by Finkel and Goubault-Larrecq. Ideals provide indeed finite effective representations of downwards-closed sets, in the same way as bases of minimal elements provide representations of upwards-closed sets. After defining ideals and establishing some of their properties, I illustrated their use in a concrete setting. I presented some recent results by Czerwiński, Martens, van Rooijen, and Zeitoun (FCT'15) on the decidability of piecewise-testable separability in the light of ideals. This seminar was also a warm-up for the next seminar on reachability in vector addition systems.