Büchi Automata Optimisations Formalised in Isabelle/HOL

Alexander Schimpf (1) , Jan-Georg Smaus (2)

1 University of Freiburg [Freiburg]
2 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées

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.

Mots clés: Model checking; Büchi automata; Isabelle; Interactive theorem proving

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

Alexander Schimpf, Jan-Georg Smaus. Büchi Automata Optimisations Formalised in Isabelle/HOL. 6th Indian Conference on Logics and its Applications (ICLA 2015), Jan 2015, Mumbai, India. pp.158-169, ⟨10.1007/978-3-662-45824-2_11⟩. ⟨hal-01782564⟩