Instructor: |
Paritosh K. Pandya |

Time and Venue: |
Monday 4:00 to 6:00 p.m in D405
Wednesday 11:00 to 13:00 a.m. in AG69 |

Automata on Infinite Objects:

- Omega words, Buchi, Muller, Rabin,Streett automata. Closure properties. Safra's determinisation construction.
- * omega tree automata, Rabin's tree theorem.
Logics for Infinite Behaviours:

- Monadic second-order logic over omega words, Linear temporal logic, CTL, CTL*, Mu calculus, Interval temporal logic
- * Recent developments: Alternating automata, Transitive closure logics, partial order methods, abstraction and reduction techniques, compositional model checking.
- * Monadic second order logic over trees and graphs.
Model checkers based on Automata on Infinite objects and Symbolic Model checkers:

- OBDDs and symbolic model-checking
- SPIN, SMV, MONA, DCVALID.
Timed Automata:

- Timed Buchi automata, Alur-Dill region construction, Closure properties.
- Closure under complementation: Event-clock and state-clock automata.
Logics for Timed and Continuous Behaviors:

- MTL, TPTL, TCTL, Duration calculus.
* Theory of Hybrid automata:Model-checkers for Timed and Hybrid Systems:

- Uppal, Hytech.