Tool support for learning Büchi automata and linear temporal logic

Abstract

Abstract. Automata and logics are intimately related, and understanding their relation is instrumental in discovering algorithmic solutions to formal reasoning problems or simply in using those solutions. This applies to Büchi automata and linear temporal logic, which have become fundamental components of the model-checking approach to formal verification of concurrent systems. Translation of a propositional temporal formula into an equivalent Büchi automaton is routinely performed in many model-checking algorithms and tools. Albeit the possibility of mechanical translation, a temporal formula and its equivalent automaton appear to be two very different artifacts and their correspondence is not easy to grasp. In this paper, we introduce a graphical interactive tool, named GOAL, that can assist the user in understanding the relation between Büchi automata and linear temporal logic, and suggest possible usages and benefits of the tool in courses where model-checking techniques are covered. GOAL builds on the successful JFLAP tool for classic theory of automata and formal languages. One main function of GOAL is translation of a propositional temporal formula into an equivalent Büchi automaton that can be visually manipulated, for example, running the automaton on some input. GOAL also supports various standard operations and tests, including equivalence test, on Büchi automata. We believe that, with an easy access to temporal formulae and their graphically presented equivalent Büchi automata, the student’s understanding of the two formalisms and their relation will be greatly enhanced. 1