Title :
On simultaneously determinizing and complementing ω-automata
Author :
Emerson, E. Allen ; Jutla, Charanjit S.
Author_Institution :
Dept. of Comput. Sci., Texas Univ., Austin, TX, USA
Abstract :
The authors give a construction to determine and complement simultaneously a Buchi automaton in infinite strings, with an exponential blowup in states and a linear blowup in the number of pairs. An exponential lower bound is already known. The previous best construction was double exponential. The present result permits exponentially improved essentially optimal decision procedures for various modal logics of programs. It also gives exponentially improved conversions between various kinds of ω automata
Keywords :
automata theory; formal logic; ω-automata; Buchi automaton; exponential blowup; exponential lower bound; infinite strings; modal logics of programs; optimal decision procedures; Asynchronous circuits; Automata; Automatic testing; Character generation; Computational modeling; Computer science; Contracts; Feedback amplifiers; Logic; Mathematics;
Conference_Titel :
Logic in Computer Science, 1989. LICS '89, Proceedings., Fourth Annual Symposium on
Conference_Location :
Pacific Grove, CA
Print_ISBN :
0-8186-1954-6
DOI :
10.1109/LICS.1989.39188
