Logic and Computation introductory course:
Temporal logics for specification and verification.
Teacher
Course material: Goranko-ESSLLI2009CourseNotes.pdf
Abstract:
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.