On the reachability problem in low-dimensional polynomial maps

Abstract

In this talk, I will introduce nondeterministic polynomial maps and related reachability problems. Polynomial maps can be seen as generalization of Vector Addition Systems, where the register updates are not restricted to incrementing and decrementing the current value but can be defined by arbitrary polynomials. In the reachability problem for polynomial maps we are asked whether there exists a finite composition of polynomials such that the given initial register value is evaluated to zero.

We consider different parameters in polynomial maps and study their effect on the decidability status of the reachability problem. In particular, we will show that the reachability problem is undecidable for three-dimensional affine maps and is PSPACE-complete for one-dimensional polynomial maps. We also investigate the role of VAS-like updates of the form x=x+a for some integer a. Surprisingly, we see that if we exclude the updates of this form, the problem becomes decidable in any dimension.

Bio

Reino Niskanen is a postdoc working on formal verification of string-manipulating programs at University of Oxford. Prior to arriving to Oxford, he did his PhD at University of Liverpool, where he studied decidability and complexity of the reachability problems in different models.