Verification Series

Good-for-games omega-pushdown automata

12th May 2020, 11:00 add to calender
Karoliina Lehtinen

Abstract

Good-for-gameness is the new determinism, and not just for solving games.
Good-for-games automata, originally due to Henzinger and Piterman, are nondeterministic automata that have many of the desirable properties of deterministic automata and can therefore often be used in their stead to circumvent determinisation. In the context of regular languages of infinite words they can be exponentially more concise than any equivalent deterministic automaton.

In this talk I will first give an overview of good-for-games automata and then discuss what happens when good-for-gameness is lifted into the context-free setting. In brief, it turns our that good-for-games pushdown automata are more expressive and not just more concise than their deterministic counterparts. This gives us a novel class of languages for which solving games and universality -- which are both undecidable for pushdown automata -- are decidable in EXPTIME.

This talk is based on joint work with Martin Zimmermann, accepted for publication at LICS'2020.
add to calender (including abstract)