The complementation problem for Büchi automata with applications to temporal logic

This work uses a construction that involves only an exponential blow-up in the size of the automaton to prove a polynomial space upper bound for the propositional temporal logic of regular events and to prove the complexity hierarchy result for quantified propositionalporal logic.

Abstract

The problem of complementing Büchi automata arises when developing procedures for temporal logics of programs. Unfortunately, previously known constructions for complementing Büchi automata involve a doubly exponential blow-up in the size of the automaton. We present a construction that involves only an exponential blow-up. We use this construction to prove a polynomial space upper bound for the propositional temporal logic of regular events and to prove a complexity hierarchy result for quantified propositional temporal logic.