Authors
A Prasad Sistla, Moshe Y Vardi, Pierre Wolper
Publication date
1987/1/1
Journal
Theoretical Computer Science
Volume
49
Issue
2-3
Pages
217-237
Publisher
Elsevier
Description
The problem of complementing Büchi automata arises when developing decision 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.
Total citations
Scholar articles
AP Sistla, MY Vardi, P Wolper - Theoretical Computer Science, 1987