This lecture is about representing Boolean Functions. We saw that for the algorithm for CTL model checking, we needed to represent sets of states in such a way that a number of operations can be done efficiently. In particular, union, intersection, complements, or the normal set operations, but also, we should deal with steps. In particular, if we are given sets T and U, it should be possible to find the sets consisting of the elements from T in such a way that you can do a step towards an element from U, and that's represented by the set. In explicit state model checking, such sets are represented just by enumerating all of their elements. But this is not feasible for state spaces if they are a little bit large. For instance, if they are more than 10 to the power of 10 elements, and that is what you easily reach. If you have five variables running from 1-100, you are already on this number. So easily in practice, you exceed this number for which explicit state based model checking is feasible. Therefore, we want something else, and that's called symbolic model checking. In this lecture, we will just investigate desired requirements for alternative representations for Boolean functions. In NuSMV, the variable types are finite sets. In particular, Booleans or integers with a restricted range, like a number variable a running from 1-100. But we can represent all of this only in Booleans. For numbers, we can choose a binary notation, and if we have a binary notation, we just represent a number by a number of Boolean variables. For instance, if we have the range one to 100, that's less than 2 to the power of 7, so we need seven bits for it. We have seen in our lecture, in our MOOC on satisfiability, that the basic operations on integers dealing with addition and also multiplication can all be expressed in Boolean formulas. Atomic propositions like a is less than b plus 5 can be also expressed directly in binary notation. We write 0,1 for the Booleans, and 0 stands for false, 1 stands for true, and then we can say state space is just B to the power n. This lecture, we want to represent and manipulate subsets of the state space. An important observation is that such a subset can be identified by a Boolean function. Just give the value true if it is in the set, and give the value false if it is not in the set. So s is an element of u if and only if the Boolean function on s yields 1. We want to represent and manipulate Boolean functions efficiently. More precisely, we want that every Boolean function has a unique representation that's convenient for various purposes, and we can obtain that. It's important to realize that for the normal formula representations, this doesn't hold. We have several ways to represent the same Boolean functions. For instance, if we have a function that yields true if p and q both are true, and false otherwise, here we have two representations for this function. All operations needed for CTL model checking including the normal Boolean operations like negation, disjunction, and conjunction should be efficiently computable, but also, the steps from the set d to the set u. This does not hold for explicit state representation, even just the operation, negation already is infeasible to do in explicit state representation. False corresponds to the empty set, and that's easily represented, but its negation is true, and that corresponds to the full set. The full set has 2 to the power n elements, and if n is, say, greater than 30, it's impossible to represent all of these 2 to the power n elements separately. Last, we want that many Boolean functions have an efficient representation. A first idea would be, of course, all Boolean functions should have an efficient representation, but that's not possible. So that's what we figure out now, why is this not possible for all Boolean functions? Well, there are some counting argument. We count how many Boolean functions that exists. Assume that we have n variables, then a Boolean function is represented by a truth table, and the truth table consists of 2 to the power n lines. In every line, we fill in 0 and 1, so that means that in total, we have 2 to the power n distinct Boolean function. This is an extremely big number. For instance, think about six variables, and a 6. How many Boolean functions do you think there exists on an element? Well, a first guess would be maybe a few hundreds, a few thousands, maybe a million, but it turns out to be much more. It turns out to be this 2 to the power 64 since 2 to the power 6 is 64, so this number should be 2 to the power 64. 2 the power 64 is an extremely big number, it's roughly a 2 with 19 zeros in decimal notation. It's obvious that this is very infeasible to deal with. So if all of these 2 to the power 2 to the n, distinct Boolean functions should have a distinct representation, then on average, we need at least 2 to the power n bits for that. This is intractable for n, let's say, exceeding 30. This information theoretic argument shows that it is unavoidable that most of the Boolean functions have an intractable representation. So the best we may hope for is that what we meet in practice is among the very minor part of all Boolean functions that have an efficient representation. That the most Boolean functions that have an intractable representation, that we do not meet them in practice, and we do not need to worry about it. Binary Decision Diagrams, abbreviated to BDDs. That's a data structure for which all of these properties we just investigated hold. So this serves well for our goals, and this is exactly what is used in practice. For instance, in the tool NuSMV, as we use it. In the next few lectures, we will define them, and give some main properties. Thank you.
