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

Australian National University


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              = {\_18},
    month            = jul,
    booktitle        = {International Conference on Interactive Theorem Proving},
    paperurl         = {},
    year             = {2018},
    editor           = {{Jeremy Avigad and Assia Mahboubi}},
    title            = {Verifying the {LTL} to {B}\"{u}chi Automata Translation via Very Weak Alternating Automata},
    author           = {Jantsch, Simon and Norrish, Michael},
    address          = {Oxford},
    date             = {2018-7-9},
    pages            = {306-323}