Automated Verification: Assignment 1

Due Date: November 11, 1998

Let A=(Sigma,S,S₀,rho,G) be a nondeterministic Müller automaton, where G={F₁,...F_k). Construct a Büchi automaton A^b such that A and A^b define the same omega-language. Prove the correctness of your construction.

Note: The assignment need to be typeset.