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

Certification

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

Experiments

Results

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

Conclusion