Equivalence and reachability problems on stack-based infinite-state systems

Stefan Göller (University of Bremen)

When: November 18, 2pm

Where: room G2.91b/G215

Abstract

In the first part of my talk I will introduce a class of register machines whose registers can be updated by polynomial functions when a transition is taken, and the domain of the registers is restricted by linear constraints. This model strictly generalises a variety of known formalisms such as various classes of Vector Addition Systems with states. The main result is that reachability in our class is PSPACE-complete when restricted to one register. This part is based on joint work with Alain Finkel and Christoph Haase.

In the second part of my talk I will give the proof idea for a nonelementary lower bound on bisimulation equivalence on (normed) pushdown automata. The previously best-known lower bound for this problem has been EXPTIME-hardness shown by Kucera and Mayr, whereas decidability has been shown by Senizergues. This is part is based on joint work with Michael Benedikt, Stefan Kiefer and Andrzej Murawski.