Schimpf, Alexander and Smaus, Jan-Georg
Büchi Automata Optimisations Formalised in Isabelle/HOL.
(2015)
In: 6th Indian Conference on Logics and its Applications (ICLA 2015), 8 January 2015 - 10 January 2015 (Mumbai, India).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 311kB |
Official URL: https://doi.org/10.1007/978-3-662-45824-2_11
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.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information: | Thanks to Springer editor. This papers appears in Volume 8923 of Lecture Notes in Computer Science ISSN : 0302-9743 ISBN: 978-3-662-45823-5 The original PDF is available at: https://link.springer.com/chapter/10.1007/978-3-662-45824-2_11 |
| HAL Id: | hal-01782564 |
| Audience (conference): | International conference proceedings |
| Uncontrolled Keywords: | |
| Institution: | French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE) Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) Other partners > Universität Freiburg (GERMANY) |
| Laboratory name: | |
| Funders: | DFG grant CAVA, Computer Aided Verification of Automata |
| Statistics: | download |
| Deposited On: | 30 Mar 2018 13:56 |
Repository Staff Only: item control page
