On Refinement of Büchi Automata for Explicit Model Checking. - Frantisek Blahoudek; Alexandre Duret-Lutz; Vojtech Rujbr; Jan Strejcek (SPIN, 2015)