Certifying Emptiness of Timed Büchi Automata

Simon Wimmer, Frédéric Herbreteau, Jaco van de Pol

Model checkers for timed automata are widely used to verify safety-critical, real-time systems. State-of-the-art tools achieve scalability by intricate abstractions. We aim at furt…