Certifying Emptiness of Timed B\"uchi Automata

TL;DR

This paper presents a method to generate and verify certificates for the emptiness of timed B"uchi automata, enhancing trust in model checking results for real-time systems, especially for liveness properties.

Contribution

We introduce a novel approach for extracting and formally verifying certificates of automata emptiness, improving the reliability of model checking in safety-critical applications.

Findings

Certificates can be extracted from model checking runs.

The approach is sound and complete.

Certificates are validated with a verified certifier.

Abstract

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\"uchi 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.