Converting Linear-Time Temporal Logic to Generalized Büchi Automata by Alexander Schimpf and Peter Lammich May 28
A Fully Verified Executable LTL Model Checker by Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf and Jan-Georg Smaus May 28