Abstract
This last lecture of 2014-2015 introduces implicit methods for manipulating transition systems, through Boolean calculus methods used both for formal verification and for optimizing electronic circuits and programs that can be reduced to Boolean calculus.
These methods have revolutionized the field by enabling formal verification of systems whose explicit computation of states and transitions is impossible, since the size of the formulas manipulated by implicit methods is largely independent of that of the systems they describe. We first explain the Boolean encodings of sets, relations and functions, and show how to compute the direct image and inverse image of subsets by functions. We then study Boolean encodings of deterministic and non-deterministic automata, and their implementation in electronic circuits. We recall that the circuit canonically associated with a non-deterministic automaton is itself deterministic like all combinatorically acyclic circuits, which clearly shows that the qualifier "non-determinism" is particularly ill-chosen: in Boolean verification as in circuit optimization, it is pointless to determinize automata, and often harmful because of the exponential explosion that determinization can produce. We show how the formal verification of safety properties defined by observers reduces to the computation of reachable states, and how to perform this computation implicitly. We introduce the first fundamental structure of Boolean calculus, the Binary Decision Diagrams, developed by R. Bryant in the mid-1980s (and independently by J-P. Billion at Bull in France), and explain why they enable the computations needed to scale up; we mention their limitations, which are unavoidable because Boolean calculus is NP-complete. BDDs will be studied in much greater depth in the 2015-2015 lecture.
