1. (16 points) Compute the full intersection for the two Buchi Automaton in Figure 1. Be sure to clearly indicate accept states.

2. (20 points) Compute the full intersection for the two Buchi Automaton in Figure 2. Be sure to clearly indicate accept states.

3. (20 points) Apply double-depth-first search to the automaton from the intersection in Problem 1 to detect a cycle in the intersection. Always visit the 0-input edge first. Assign each state a pre-order visit number. States that are visited twice (once if the first search and again in the second search) should have two pre-order visit numbers. If a cycle is detected, then clearly indicate that cycle. Grading is on the pre-order visit numbers.

4. (20 points) Repeat Problem 2, only this time use a double-depth-first search to detect a cycle at the same time that the intersection is being computed. This is often referred to as on-the-fly model checking. As in the previous problem, always visit the 0-input edge first. Assign each state a pre-order visit number. States that are visited twice (once if the first search and again in the second search) should have two pre-order visit numbers. If a cycle is detected, then clearly indicate that cycle. Grading is on the pre-order visit numbers. Did the entire intersection get enumerated before a cycle is detected?

5. (20 points) Consider the states space and never-claim in Figure 5. Perform on-the-fly model checking to see if an accepting cycle exists. Visit edge-labels in alphabetical order (e.g., A, then B, and then C). If there is a non-deterministic choice of edges, the visit the edge leading the least state-label first (e.g., $s_3$ is visited before $s_5$).