SKEDSOFT
Stabilization at a Fixed-Point: In every finite-state system modeled using a finite-state Boolean transition system, the least fixed-point is always reached in a finite number of steps. Let us try to argue this fact first using only a simple observation. The observation is that all the Boolean expressions generated during the course of fixed-point computation are over the same set of variables. Since there are exactly 22N Boolean functions over N Boolean variables (see Illustration 4.5.2), eventually two of the approximants in the fixed-point computation process will have to be the same Boolean function. However, this argument does not address whether it is possible to have “evasive” or “oscillatory” approximants Pi, Pi 1, . . . , Pj such that i = j and Pj = Pi. If this were possible, it would be possible to cycle through Pi, . . . , Pj without ever stabilizing on a fixed-point.
Fortunately, this is not possible! Each approximant Pi 1 is more defined than the previous approximant Pi, in the sense defined by the implication lattice defined in Illustration 4.5.3. With this requirement, the number of these ascending approximants is finite, and one of these would be the least fixed-point. See Andersson’s paper [7] for additional examples of forward reachability. The book by Clarke et.al. [20] gives further theoretical insights.
An example with multiple fixed-points: Consider the state transition system in Figure 11.6 with initial state s0 (called MultiFP). The set of its reachable states is simply {s0} (and is characterized by the formula a ∧ b), as there is no reachable node from s0. Now, a fixed-point iteration beginning with the initial approximant
for the reachable states set to P0 = false will converge to the fixedpoint a ∧ b. What are the other fixed-points one can attain in this system? Here they are:
- With the initial approximant set to {s0,s1}, which is characterized by b, the iteration would reach the fixed-point of a ∨ b, which characterizes {s0,s1,s2}.
- Finally, we may iterate starting from the initial approximant being 1, corresponding to {s0,s1,s2,s3}. The fixed-point attained in this case is 1, which happens to be the greatest fixed-point of the recursive equation characterizing reachable states.
Hence, in this example, there are three distinct fixed-points for the recursive formula defining reachable states. Of these, the least fixedpoint is a∧b, and truly characterizes the set of reachable states; a∨b is the intermediate fixed-point, and 1 is the greatest fixed-point. It is clear that (a ∧ b) ⇒ (a ∨ b) and (a ∨ b) ⇒ 1, which justifies these fixed-point orderings. Figure 11.6 also describes the BED commands to produce this intermediate fixed-point.
Fig. 11.6. Example where multiple fixed-points exist. This figure shows attainment
of a fixed-point a ∨ b which is between the least fixed-point of a ∧ b and the greatest fixed-point of 1. The figure shows the initial approximant P0 and the next approximant P1
Playing tic-tac-toe using BDDs: What good are state-space traversal techniques using BDDs? How does one obtain various interesting answers from real-world problems?While we cannot answer these questions in detail, we hope to leave this chapter with a discussion of how one may model a game such as tic-tac-toe and,
say, compute the set of all draws in one fell swoop. Following through this example, the reader would obtain a good idea of how to employ mathematical logic to specify a transition system through constraints, and reason about it. We assume the reader knows the game of tic-tactoe (briefly explained in the passing).
Modeling the players and the board: We model two players, A and B. The state of the game board is modeled using a pair of variables ai,j, bi,j (we omit the pairing symbols for brevity) for each square i, j where i ∈ 3 and j ∈ 3. We assume that player A marks square i, j with an o, by setting ai,j and resetting bi,j , while player B marks square i, j with an x, by resetting ai,j and setting bi,j. We use variable turn to model whose turn it is to play (with turn = 0 meaning it is A’s turn). The state transition relation for each square will be specified using the four variables ai,j, ai,jp, bi,j , and bi,jp. We model the conditions for a row or column remaining the same, using predicates samerowi and samecoli.We define nine possible moves for both A and for B. For example, M00 model’s A’s move into cell 0, 0; Similarly, we employ N00 to model B’s move into cell 0, 0, and so on for the remaining cells. The transition relation is now defined as a disjunction of the Mi,j and Ni,j moves. We now capture the constraint atmostone that says that, at most one player can play into any square.
We then enumerate the gameboard for all possible wins and draws. In the world of BDDs, these computations are achieved through “symbolic breadth first” traversals. We compute the reachable set of states, first querying it to make sure that only the correct states are generated. Then we compute the set of states defining draw configurations. The complete BED definitions are given in Appendix B.
