Skip to main content

Verifying the LTL to Büchi automata translation via very weak alternating automata


Simon Jantsch and Michael Norrish


Technical University Dresden


We present a formalization of a translation from LTL formulae to generalized Büchi automata in the HOL4 theorem prover. Translations from temporal logics to automata are at the core of model checking algorithms based on automata-theoretic techniques. The translation we verify proceeds in two steps: it produces very weak alternating automata at an intermediate stage, and then ultimately produces a generalized Büchi automaton. After verifying both transformations, we also encode both of these automata models using a generic, functional graph type, and use the CakeML compiler to generate fully verified machine code implementing the translation.

BibTeX Entry

    publisher        = {Springer},
    doi              = {10.1007/978-3-319-94821-8\_18},
    booktitle        = {International Conference on Interactive Theorem Proving},
    author           = {Jantsch, Simon and Norrish, Michael},
    month            = jul,
    editor           = {{Jeremy Avigad and Assia Mahboubi}},
    year             = {2018},
    date             = {2018-7-9},
    title            = {Verifying the {LTL} to {B}\"{u}chi Automata Translation via Very Weak Alternating Automata},
    pages            = {306-323},
    address          = {Oxford}


Served by Apache on Linux on seL4.