Certifying Emptiness of Timed Büchi Automata

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Simon Wimmer, Technische Universität München
  • ,
  • Frédéric Herbreteau, Universite de Bordeaux
  • ,
  • 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 further increasing the trust in their verification results, in particular for checking liveness properties. To this end, we develop an approach for extracting certificates for the emptiness of timed Büchi automata from model checking runs. These certificates can be double checked by a certifier that we formally verify in Isabelle/HOL. We study liveness certificates in an abstract setting and show that our approach is sound and complete. To also demonstrate its feasibility, we extract certificates for several models checked by TChecker and Imitator, and validate them with our verified certifier.

Original languageEnglish
Title of host publicationFormal Modeling and Analysis of Timed Systems : 18th International Conference, FORMATS 2020
EditorsNathalie Bertrand, Nils Jansen
Number of pages18
Place of publicationCham
Publication year2020
ISBN (print)9783030576271
Publication statusPublished - 2020
Event18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020 - Vienna, Austria
Duration: 1 Sep 20203 Sep 2020


Conference18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020
SeriesLecture Notes in Computer Science
Volume12288 LNCS

    Research areas

  • Certification, Model checking, Timed automata

See relations at Aarhus University Citationformats

ID: 196438350