Verification Series
Good-for-games omega-pushdown automata
12th May 2020, 11:00
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.
Ashton Street, Liverpool, L69 3BX
United Kingdom
Call the department
+44 (0)151 795 4275