Skip to main content

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

Authors

Simon Jantsch and Michael Norrish

DATA61

Technical University Dresden

Australian National University

Abstract

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

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

Download