Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata

Simon Jantsch; Michael Norrish

doi:10.1007/978-3-319-94821-8_18

Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata

Simon Jantsch^*, Michael Norrish

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

2 Citations (Scopus)

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.

Original language	English
Title of host publication	Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
Editors	Jeremy Avigad, Assia Mahboubi
Publisher	Springer Verlag
Pages	306-323
Number of pages	18
ISBN (Print)	9783319948201
DOIs	https://doi.org/10.1007/978-3-319-94821-8_18
Publication status	Published - 2018
Event	9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10895 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/Territory	United Kingdom
City	Oxford
Period	9/07/18 → 12/07/18

Access to Document

10.1007/978-3-319-94821-8_18

Cite this

Jantsch, S., & Norrish, M. (2018). Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. In J. Avigad, & A. Mahboubi (Eds.), Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 306-323). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10895 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-94821-8_18

Jantsch, Simon ; Norrish, Michael. / Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. editor / Jeremy Avigad ; Assia Mahboubi. Springer Verlag, 2018. pp. 306-323 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e8ee6660cab44225b031a61283f96194,

title = "Verifying the LTL to B{\"u}chi Automata Translation via Very Weak Alternating Automata",

abstract = "We present a formalization of a translation from LTL formulae to generalized B{\"u}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{\"u}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.",

author = "Simon Jantsch and Michael Norrish",

note = "Publisher Copyright: {\textcopyright} 2018, Springer International Publishing AG, part of Springer Nature.; 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 09-07-2018 Through 12-07-2018",

year = "2018",

doi = "10.1007/978-3-319-94821-8_18",

language = "English",

isbn = "9783319948201",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "306--323",

editor = "Jeremy Avigad and Assia Mahboubi",

booktitle = "Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

address = "Germany",

}

Jantsch, S & Norrish, M 2018, Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. in J Avigad & A Mahboubi (eds), Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10895 LNCS, Springer Verlag, pp. 306-323, 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 9/07/18. https://doi.org/10.1007/978-3-319-94821-8_18

Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. / Jantsch, Simon; Norrish, Michael.
Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. ed. / Jeremy Avigad; Assia Mahboubi. Springer Verlag, 2018. p. 306-323 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10895 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata

AU - Jantsch, Simon

AU - Norrish, Michael

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85049911487&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-94821-8_18

DO - 10.1007/978-3-319-94821-8_18

M3 - Conference contribution

SN - 9783319948201

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 306

EP - 323

BT - Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

A2 - Avigad, Jeremy

A2 - Mahboubi, Assia

PB - Springer Verlag

T2 - 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018

Y2 - 9 July 2018 through 12 July 2018

ER -

Jantsch S, Norrish M. Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. In Avigad J, Mahboubi A, editors, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer Verlag. 2018. p. 306-323. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-94821-8_18

Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this