Let's go back to CTL model checking. How can we do CTL model checking so checking the property of a program by CTL model checking by representing large sets of states by ROBDDs? We already saw an abstract algorithm for CTL model checking but we observe that if the set of states is very large, we need another way to represent sets of states and now we will use ROBDDs for that. First, recall the abstract algorithm for CTL model checking. How does it look like? All CTL operators can be expressed in boolean operators and the operators, EX, EG, and EU. You can watch the lecture on this again if you don't remember but now we will focus on the building blocks we need there. For computing EX, EG, and EU, we saw that we only needed the following building blocks; set union, set intersection, and we should be able to compute if we have given sets T and U and we have given a transition relation, we should be able to compute the set of sets in T such a way that they can do a step towards an element in U and that's denoted by this set. This set we should compute and once we can do this we can compute EX, EG, and EU. EX can be done directly and for EG and EU, we need some loops, but in the loops we only call the computation of this set and unions, and intersection, and no more than that. So we should focus on computing this set. Sets are described by boolean functions. An element is in the set if and only if the boolean function yields true. Then union and intersection corresponds to disjunction and conjunction for which we already gave an algorithm for ROBDD representations. So for doing full CTL model checking in ROBDD representation, the only missing link is to compute the representation of this particular set as we are given. For given T and U, the set of states that are in T and can do a step towards an element of U, for this set we need ROBDD representation. As all variables are from finite sets, they can be encoded binary and that will be done. So for instance, if we have an integer running from 1 to 100, we simply encode as binary and we need seven boolean variables for it. So we assume that after this encoding binary, we have only boolean variables, let's call them a_1 until a_n. Now, the sets T and U of states are described by boolean functions on these variables a_1 until a_2 given in ROBDD representation. So the ROBDD of T yields true for a particular state if and only if that state is in T and the same for U. We will deal with formulas and in these formulas where we deal with the implication, we do not only have the variable a_i but we also have next a_i. To consider this next a_i just as variable and write it simply shorter, we simply write a_i prime for it rather than the full next a_i. Now, the transition relation arrow is given by a boolean function on these 2n variables, the normal a_1 to a_n, these are the values of the variables before the step and a_1 prime until a_n prime, the values after the step again in ROBDD representation. In this setting, we have to compute the set V consisting of the set of elements of T that can do a step towards an element of U in a situation where we have ROBDDs given of the set T, the set U, and the transition relation arrow. That means V is the intersection of T and the element a_1 until a_n representing a state such a way that from this state we can do a step towards a prime state and the prime state should be in U. These requirements are written in P, and what is P? P is defined as indeed we can do a step from the a's to the a primes, and the primes should be in U. Now, the first question is can we compute the ROBDD of P? Well, P consists of two parts. The first part is just the transition relation step from the a's to the a primes and for that a ROBDD was assumed to be given. The second part is the requirement that the primes are in U. We have ROBDD of U was given, but that's an ROBDD in the non primed variables. But if we assume that the order in such a way that the order of the a's is the same as the order of the a primes, for instance, using this order, then the ROBDD of the requirement that the primes are in U is obtained by just replacing every a_i by a_i prime in the ROBDD of U and that's simply done. So if we take the conjunction of these two parts, we have the ROBDD of this P. Now, the only thing to be done is we should compute V being the intersection of T and some quantification over B. So that is what you should compute. We should think about, what does it mean there exists a_1 prime, a_2 prime until a_n prime? Remember that a_1 primes are just booleans and big quantification over a number of boolean variables is the same as a quantification successively. So the big quantification can be replaced by there exists a_1 prime, exists a_2 prime, and so on. Next, we should eliminate each of these existential quantifications. Now, we should think about what is the meaning if we have a boolean variable x and we have a formula Phi in which x occurs, what is the meaning of there exists an x in such a way that Phi holds? Well, that means either Phi holds when replacing x by false or Phi holds after replacing x by true. So that means that this should be computable. Once we have a ROBDD of Phi and we have a boolean variable x occurring in it, we can simply make an ROBDD of Phi in which x is replaced by false simply by always choosing the right branch of x and eliminate the x in that way and for true the same, but then we choose the left branch. So this is computable and the disjunction of these two is also computable. So in this way, we can eliminate a single existential quantification over a boolean variable. Now, the idea is we simply should do this n times. First for a_n prime, then for a_n minus 1 prime, and so on, until all existential quantification have been eliminated. Then we have the ROBDD over a_1 until a_n and just taking the conjunction of this resulting ROBDD in only the variables a_1 until a_n and the ROBDD of T yields the required ROBDD of V. Combining this gives an algorithm to compute the ROBDD of the set of states satisfying any CTL formula. Here, the transition relation arrow is given as an ROBDD. This is essentially the algorithm as it is used in tools like NuSMV to do symbolic model checking. In contrast to explicit state based model checking, it can deal with very large state spaces. In contrast to bounded model checking, it can deal with a great number of steps. In next lectures, we will focus on a number of examples where we can apply these techniques. Thank you.
