Logic and Computation introductory course:
Temporal logics for specification and verification.
Course material: Goranko-ESSLLI2009CourseNotes.pdfAbstract:
The course will cover the following topics:
I. Transition systems and computations. Important properties of transition systems: safety, eventualities, fairness, reachability. Formal specification and verification of properties of transition systems. Temporal logics as languages for specification.
II. Linear and branching time models of computations.
Linear time temporal logics. Expressing properties of computations in transition systems using LTL.
Satisfiability of LTL specifications. Verification of LTL specifications by model checking. Branching-time temporal logics. Expressing properties of computations in transition systems using CTL and CTL*.
Satisfiability of CTL specifications. Verification of CTL specifications by model checking.
III. Buchi automata on infinite words and trees. Automata recognizing models of temporal formulae.
Automata-based methods for satisfiability and model checking of linear and branching time temporal formulae.
IV. Tableau-based methods for testing satisfiability and model-checking of linear and branching time temporal formulae.
V. Optional, subject to time availability: Introduction to modal mu-calculus. Model checking of mu-calculus formulae.