Temporal logics of computations 


                                 Valentin Goranko

The course will include the following topics, grouped in 5 2-hour lectures: 

i) Transition systems and models of computations. Linear and branching
time models of sequential, concurrent, and reactive systems. Expressing
properties of computations using temporal languages. 

ii) Temporal logics of programs and processes: overview of basic
systems. Some decidability, complexity and completeness results. Using
temporal logics for program specification and verification. 

iii) Automata-theoretic techniques for satisfiability and model checking
in temporal logics. 

iv) Modal mu-calculus and model-checking. 

v) Open and multi-agent systems. Concurrent game structures and
alternating-time temporal logics. 

Prerequisites: basic knowledge of logic. In addition, introductory
knowledge on modal logics, as well as basic knowledge of models of
computation, program specification and verification would be an
advantage.