Bibtex de la publication

@InProceedings{ Sc2015.2,
author = {Schimpf, Alexander and Smaus, Jan-Georg},
title = "{Büchi Automata Optimisations Formalised in Isabelle/HOL (regular paper)}",
booktitle = "{Indian Conference on Logics and its Applications (ICLA), Mumbai, India, 08/01/2015-10/01/2015}",
editor = {Banerjee, Mohua and Krishna, Shankara Narayanan},
year = {2015},
publisher = {Springer Berlin / Heidelberg},
address = {http://www.springer.com},
volume = {8923},
series = {Lecture Notes in Computer Science},
pages = {158--169},
language = {anglais},
URL = {http://dx.doi.org/10.1007/978-3-662-45824-2_11},
keywords = {Model Checking, Büchi automata, Isabelle, interactive theorem proving},
abstract = {In applications of automata theory, one is interested in reductions in the size of automata that preserve the recognised language. For Büchi automata, two optimisations have been proposed: bisimulation reduction, which computes equivalence classes of states and collapses them, and $a$-balls reduction, which collapses strongly connected components (SCCs) of an automaton that only contain one single letter as edge label. In this paper, we present a formalisation of these algorithms in Isabelle/HOL, providing a formally verified implementation.}
}