Marc Segelken: Abstraction and Counterexample-Guided Construction of <i>omega</i> -Automata for Model Checking of Step-Discrete Linear Hybrid Models. CAV 2007: 433-448