The Automaton/logic Connection
Introduction: : Throughout the entire 150 years (or so) history of computer science, one can see an attempt on part of researchers to understand reasoning as well as computation in a unified setting. This direction of thinking is best captured by Hilbert in one of his famous speeches made in the early 1900s in which he challenged the mathematical community with 23 open problems. Many of these problems are still open, and some were solved only decades after Hilbert’s speech. One of the conjectures of Hilbert was that the entire body of mathematics could perhaps be “formalized.” What this meant is basically that mathematicians had no more creative work to carry out; if they wanted to discover a new result in mathematics, all they had to do was to program a computer to systematically crank out all possible proofs, and check to see whether the theorem whose proof they are interested in appears in one of these proofs!
In 1931, Kurt G¨odel dropped his ‘bomb-shell.3 He formally stated and proved the result, “Such a device as Hilbert proposed is impossible!” By this time, Turing, Church, and others demonstrated the true limits of computing through concrete computational devices such as Turing machines and the Lambda calculus. The rest “is history!”
The Automaton/Logic Connection: Scientists now have a firm understanding of how computation and logic are inexorably linked together. The work in the mid 1960s, notably that of J.R. B¨uchi, furthered these connections by relating branches of mathematics known as Presburger arithmetic and branches of logic known as WS1S4 with deterministic finite automata. Work in the late 1970s, notably by Pnueli, resulted in the adoption of temporal logic as a formal logic to reason about concurrency. Temporal logic was popularized by Manna and Pnueli through several textbooks and papers. Work in the 1980s, notably by Emerson, Clarke, Kurshan, Sistla, Sifakis, Vardi, and Wolper established deep connections between temporal logic and automata on infinite words (in particular B¨uchi automata). Work in the late 1980s, notably by Bryant, brought back yet another thread of connection between logic and automata by the proposal of using binary decision diagrams, essentially minimized deterministic finite automata for the finite language of satisfying instances of a Boolean formula, as a data structure for Boolean functions. The symbolic model checking algorithm proposed by McMillan in the late 1980s hastened the adoption of BDDs in verification, thus providing means to tackle the correctness problem in computer science. Also, spanning several decades, several scientists, including McCarthy, Wos, Constable, Boyer, Moore, Gordon, and Rushby, led efforts on the development of mechanical theorem-proving tools that provide another means to tackle the correctness problem in computer science.
DFA can ‘scan’ and also ‘do logic’
In terms of practical applications, the most touted application domain for the theory of finite automata is in string processing – pattern matching, recognizing tokens in input streams, scanner construction, etc. However, the theory of finite automata is much more fundamental to computing. Most in-depth studies about computing in areas such as concurrency theory, trace theory, process algebras, Petri nets, and temporal logics rest on the student having a solid foundation on classical automata, such as we have studied so far. This chapter introduces some of the less touted, but nevertheless equally important, ramifications of the theory of finite automata in computing. It shows how the theory of DFA helps arrive at an important method for representing Boolean functions known as binary decision diagrams. The efficient representation as well as manipulation of Boolean functions is central to automated reasoning in several areas of computing, including computeraided design and formal verification. We now turn to binary decision diagrams, the subject of this section.
Note: We use ∨ and interchangeably, depending on what looks more readable in a given context; they both mean the same (the or function).