Academic
Publications
Observations on Determinization of Büchi Automata

Observations on Determinization of Büchi Automata,10.1007/11605157_22,Christoph Schulte Althoff,Wolfgang Thomas,Nico Wallmeier

Observations on Determinization of Büchi Automata   (Citations: 16)
BibTex | RIS | RefWorks Download
The two determinization procedures of Safra and Muller-Schupp for Buchi automata are compared, based on an implementation in a program called OmegaDet.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Indeed, the automata-theoretic techniques used in reasoning about infinite trees are notoriously difficult [25, 28] and have resisted efficient implementation...
    • ...This upper bound, however, is established using sophisticated infinite-tree automata-theoretic techniques (cf., e.g., [24]), which so far have resisted attempts at practically efficient implementation [25, 28], due to the use of Safra’s determinization construction [23] and parity games [18]...

    Diego Calvaneseet al. An Automata-Theoretic Approach to Regular XPath

    • ...Unfortunately, Safra’s algorithm is difficult to implement [10,26,13], and the underlying data structures (trees of subsets of states) do not allow the use of symbolic set representations...

    Andreas Morgensternet al. From LTL to Symbolically Represented Deterministic Automata

    • ...Safra’s determinization construction has been notoriously resistant to efficient implementations [2,29] (An alternative construction is equally hard [2]...
    • ...Safra’s determinization construction has been notoriously resistant to efficient implementations [2,29] (An alternative construction is equally hard [2]...

    Orna Kupfermanet al. Safraless Compositional Synthesis

    • ...Only recently, 16 years after the publications of Safra’s construction, it was nally implemented [THB95,KB05,ATW05]...
    • ...The common way to solve a game G = hV; ; Ni where N is an NBW, is by constructing an equivalent DPW D [Pit06] and solving the product game G D. Unfortunately, determinization has deed implementation until recently, and it cannot be implemented symbolically [THB95,ATW05,KB05]...
    • ...Existing implementations of Safra’s construction [ATW05,KB05] enumerate the states...

    Thomas A. Henzingeret al. Solving Games Without Determinization

    • ...Like Safra’s construction, however, this translation is very complicated [ATW05]...

    Orna Kupfermanet al. Safraless Decision Procedures

Sort by: