Objective:

- Practice intersecting Buchi automaton showing how accepts states are tracked
- Intersect a Buchi automaton with a verification model and show how the intersection algorithm changes when all the states in the verification model are accepting states
- Learn the double-depth-first search for detecting cycles
- Verify liveness properties in SPIN

**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$).