@inproceedings{herbreteau:hal-00477149,
    Abstract = {{The B{\"u}chi non-emptiness problem for timed automata concerns deciding if a given automaton has an infinite non-Zeno run satisfying the B{\"u}chi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, we show that this simple transformation may sometimes result in an exponential blowup. We propose a method avoiding this blowup.}},
    Address = {Edinburgh, United Kingdom},
    Author = {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and Walukiewicz, Igor},
    BookTitle = {{Special issue on Computer Aided Verification (CAV'10)}},
    Editor = {Touili, Tayssir and Cook, Byron and Jackson, Paul},
    File = {Efficient Emptiness Check for Timed Büchi Automata - Herbreteau, Srivathsan, Walukiewicz (0) (0) - a - a - j.pdf},
    Journal = {Formal Methods in System Design},
    Language = {English},
    Month = {July},
    Number = {2},
    PDF = {http://hal.archives-ouvertes.fr/hal-00477149/PDF/m.pdf},
    Pages = {148-161},
    Publisher = {Springer},
    Series = {Lecture Notes in Computer Science},
    Title = {{Efficient Emptiness Check for Timed B{\"u}chi Automata}},
    URL = {http://hal.archives-ouvertes.fr/hal-00477149},
    Volume = {6174},
    Year = {2010},
    affiliation = {Laboratoire Bordelais de Recherche en Informatique - LaBRI},
    audience = {international},
    bdsk-url-1 = {http://hal.archives-ouvertes.fr/hal-00477149},
    bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-14295-6\%5C\_15},
    date-added = {2013-12-28 17:34:33 +0000},
    date-modified = {2013-12-28 17:34:33 +0000},
    hal_id = {hal-00477149},
    doi = {10.1007/978-3-642-14295-6_15}
}

@inproceedings{herbreteau:hal-00477149, Abstract = {{The B{\"u}chi non-emptiness problem for timed automata concerns deciding if a given automaton has an infinite non-Zeno run satisfying the B{\"u}chi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, we show that this simple transformation may sometimes result in an exponential blowup. We propose a method avoiding this blowup.}}, Address = {Edinburgh, United Kingdom}, Author = {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and Walukiewicz, Igor}, BookTitle = {{Special issue on Computer Aided Verification (CAV'10)}}, Editor = {Touili, Tayssir and Cook, Byron and Jackson, Paul}, File = {Efficient Emptiness Check for Timed Büchi Automata - Herbreteau, Srivathsan, Walukiewicz (0) (0) - a - a - j.pdf}, Journal = {Formal Methods in System Design}, Language = {English}, Month = {July}, Number = {2}, PDF = {http://hal.archives-ouvertes.fr/hal-00477149/PDF/m.pdf}, Pages = {148-161}, Publisher = {Springer}, Series = {Lecture Notes in Computer Science}, Title = {{Efficient Emptiness Check for Timed B{\"u}chi Automata}}, URL = {http://hal.archives-ouvertes.fr/hal-00477149}, Volume = {6174}, Year = {2010}, affiliation = {Laboratoire Bordelais de Recherche en Informatique - LaBRI}, audience = {international}, bdsk-url-1 = {http://hal.archives-ouvertes.fr/hal-00477149}, bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-14295-6\%5C_15}, date-added = {2013-12-28 17:34:33 +0000}, date-modified = {2013-12-28 17:34:33 +0000}, hal_id = {hal-00477149}, doi = {10.1007/978-3-642-14295-6_15} }