Automata Over Infinite Words# Acceptance Conditions, Expressiveness, Algorithms and Constructions. Translation Between Types of Automata. Temporal Logic# Linear Temporal Logic (ltl), Monadic Second-order Logic (mso) and The Fragment S1s. Translation Between Logics And Automata. Ltl Model Checking. Games# Infinite Games On Graphs. Solving Reachability, Buchi and Parity Games. Ltl Synthesis Using Parity Games. Learning Outcomes# By The End of The Course, The Student Will Be Able To# - Construct Automata For Omega-regular Language in Various Acceptance Conditions, Characterize Their Languages and Translate Between Models._ --describe Properties in Temporal Logic, and Translate Them To Automata. - Solve Parity Games. - Prove Hardness Results On Translations Between Logic and Automata, And Between Types of Automata.

Faculty: Computer Science
|Undergraduate Studies |Graduate Studies

Pre-required courses

(234129 - Int. to Set Theory and Automata For Cs and 236343 - Theory of Computation)

Semestrial Information