## Certifying Emptiness of Timed Büchi Automata

Simon Wimmer

Frédéric Herbreteau

Jaco van de Pol

## Motivation

We know that:

- Real-time systems (RTSs) are often safety critical
- RTSs can be modeled well with timed automata (TA)
- Model checkers (MCs) for TA can efficiently analyze practical TA models
- We thus have an effective way to verify RTSs

What if the model checker has a bug?

## Trust Reduction

#### Certification

- - Only Soundness
- + Less meta-theory, less verification effort
- + Any approximation
- + Parallel checking

VS

#### Verification

- + Soundness & Completeness
- + Independent tool

## Zone Graph

## Subsumption Graphs

Zone graph
Liveness
Compatible
Incompatible
## Subsumption Graphs

#### Spurious cycle

Zone graph
Liveness
Compatible
Incompatible
## An Algorithm

## Implicit Abstraction

- Typical algorithms apply an abstraction $\alpha$ to every zone,
e.g. $\alpha = Extra_{LU}^+$
**[BehrmannBFL2006]**
- Behrmann et al. also defined $\alpha_{LU}$ with $Extra_{LU}^+(Z) \subseteq
\alpha_{LU}(Z)$
**But**: $\alpha_{LU}(Z)$ is not always a zone
- Subsumption with abstraction $Z \subseteq \alpha_{LU}(Z')$ can be checked
efficiently
**[HerbreteauSW2016]**
- Compatible with our certification techniques

## Results

Previous paper: typical speedup to verified MC by one order of magnitude