MW 1:15-2:30, Hollister 306.
By appointment. Please contact Rosemary Adessa, 5147 Upson, 255-9555.
Workload will be minimal. Occasional readings as assigned. Optional homework exercises. Final paper, project, or exam at the student's option.
Automata on infinite objects
Rabin tree theorem
The modal mu-calculus
Games and alternating automata
Applications to type inference
Kleene algebra and Kleene algebra with tests
Dynamic Logic by Harel, Kozen, and Tiuryn. MIT Press, 2000.
K. R. Apt and E.-R. Olderog, Verification of Sequential and Concurrent Programs, Springer-Verlag, 1991.
C. A. R. Hoare. An axiomatic basis for computer programming. Comm. Assoc. Comput. Mach. 12 (1969), 576-580, 583.
M. C. B. Hennessy and G. D. Plotkin. Full abstraction for a simple programming language. In: Proc. Math. Found. Comput. Sci., Springer-Verlag Lect. Notes in Comput. Sci. 74, New York, 1979, 108-120.
W. Thomas. Languages, Automata, and Logic. Manuscript, May 1996.
M. Vardi, Alternating automata and program verification.
R. Kaivola, Using Automata to Characterise Fixed Point Temporal Logics, PhD thesis, University of Edinburgh, Dept. of Computer Science, Report CST-135-97, April 1997.
A. Mader, Verification of Modal Properties Using Boolean Equation Systems, PhD thesis, Fakultät für Informatik, Technische Universität München, September 1997.
A. Arnold, An initial semantics for the mu-calculus on trees and Rabin's complementation lemma, Research Report, University of Bordeaux, 1997.
A. Arnold, The mu-calculus on trees and Rabin's complementation theorem, Research Report, University of Bordeaux, 1997.
D. E. Muller and P. E. Schupp, Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra, Theoretical Computer Science 141 (1995), 69-107.
Final exam solutions are posted. That's all, folks! Thanks to everyone for their participation in the course. Have a great summer.
Homework 2 Solutions
A few homework problems on topology from F98 Solutions
Homework 3 Solutions
Homework 4 Solutions
Notes on Safra's construction
Final exam Solutions