The University of New South Wales

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

    date             = {2018-7-9},
    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},
    pages            = {306-323},
    author           = {Jantsch, Simon and Norrish, Michael},
    address          = {Oxford}