In the beginning of the 60’s J. R. Büchi and C. C. Elgot proved that finite automata have the same expressive power as the formulae of certain logics. The extensive theory which has grown around this discovery is now increasingly oriented towards computer science applications, especially in the area of finite-state system specification and verification. This paper presents work aiming at practical tools for such applications done at the University of Aarhus. The theoretical foundations are clarified in an expository section in which the author reviews binary decision diagrams, Boolean logic, finite automata, tree automata, and weak second-order logics of one or two successors (WS1S, WS2S). Also implementation and complexity issues are discussed. Then the MONA tool which implements automaton based decision procedures for WS1S and WS2S is described. The system includes also a higher-level language FIDO into which many usual programming language constructs have been incorporated. All concepts and the use of FIDO are amply illustrated by examples.
For the entire collection see [Zbl 0891.00021].