Avoiding Determinization

Automata on infinite objects are extensively used in system specification, verification, and synthesis. While some applications of the automata-theoretic approach have been well accepted by the industry, some have not yet been reduced to practice. Applications that involve determinization of automata on infinite words have been doomed to belong to the second category. This has to do with the intricacy of Safra’s optimal determinization construction, the fact that the state space that results from determinization is awfully complex and is not amenable to optimizations and a symbolic implementation, and the fact that determinization

• Type: Conference
• Year: 2006
• Where: LICS
• Authors: Orna Kupferman
• Keywords: Automata-theoretic Approach, Computer Science, Infinite Objects, LICS 2006, Safra’s Optimal Determinization