Selected publications by Stefan Schwoon

The automata-theoretic approach to LTL verification relies on an algorithm for finding accepting cycles in a Büchi automaton. Explicit-state model checkers typically construct the automaton ``on the fly'' and explore its states using depth-first search. We survey algorithms proposed for this purpose and identify two good algorithms, a new algorithm based on nested DFS, and another based on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.

   address = {Edinburgh, Scotland, UK},
   author = {Schwoon, Stefan and Esparza, Javier},
   booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'05)},
   editor = {Halbwachs, Nicolas and Zuck, Lenore D.},
   month = apr,
   pages = {174-190},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {A Note on On-The-Fly Verification Algorithms},
   url = {},
   volume = {3440},
   year = {2005},

About LSV