Automated Verification: Assignment 8

Due Date: February 28, 1999

Note: This assignments is based on Lecture 10.

Consider the sequence G₀, G₁... of DAGs derived from an accepting DAG run G of a UCW. Show that G_2i has ultimate width at most n-i.
Show that the automaton A_f that we constructed from a PLTL formula phi accepts a strategy f iff f realizes phi.

Note: The assignment need to be typeset. Submit the assignment to vardi@cs.rice.edu.