From ω-regular expressions to Büchi automata via partial derivatives

Abstract

We extend Brzozowski derivatives and partial derivatives from regular expressions to ω-regular expressions and establish their basic properties. We observe that the existing derivative-based automaton constructions do not scale to ω-regular expressions. We define a new variant of the partial derivative that operates on linear factors and prove that this variant gives rise to a translation from ω-regular expressions to nondeterministic B¨uchi automata.