Stefan Goeller

"Equivalence checking of stack-based infinite-state systems"

(Vortrag im Rahmen der "MPI Distinguished Lecture Series" in Kooperation mit dem Fachbereich Informatik)

In the context of program refinement, it is of particular interest to be able to automatically check whether the implementation of a specification before the refinement step behaves equivalently to the implementation after the refinement step.

Since equivalence checking of programs is generally undecidable, one is typically confronted with a trade-off problem. On the one hand, one wishes to carry out the equivalence check fully automatically and therefore needs to model/abstract the program in such a way that equivalence checking remains at least decidable. On the other hand, the modeling/abstraction of the program should be expressive enough to model the program as faithfully as possible.

Infinite-state systems are a suitable means for faithfully modeling computer programs. For instance, the call and return behavior of recursive programs can faithfully be modeled using pushdown systems (the transition graphs induced by pushdown automata).

The focus of my talk will be on some recent work on bisimulation equivalence checking of stack-based infinite-state systems, i.e. infinite-state systems whose states and transitions involve the manipulation of a stack.

I will present in a bit more detail a PSPACE upper bound on deciding bisimulation equivalence of one-counter systems, which are pushdown systems over a unary stack alphabet, and an NLOGSPACE upper bound on bisimulation equivalence of deterministic one-counter systems, closing a long-standing complexity gap. Furthermore I will give some intuition why bisimulation equivalence checking of pushdown systems and higher-order pushdown systems is much more difficult to decide from a computational perspective, being nonelementary and undecidable, respectively. I will conclude with some challenging open problems in this area of research.

Bio: Stefan Goeller is a research associate at the University of Bremen. He received his PhD from the University of Leipzig in 2008. His research interests are in the verification of infinite-state systems, logic, and automata theory. In particular, his recent research has focused on the problem of checking bisimulation equivalences between infinite state systems.