Selected publications by Stefan Schwoon

Abstract:
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.

@inproceedings{SE-tacas05,
   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 = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/se-tacas05.ps},
   volume = {3440},
   year = {2005},
}

About LSV