Trustworthy Systems

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

Download