|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 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.