PhD Course:
Temporal Verification and Synthesis of Reactive Systems
By Amir Pnueli (New York University and Weizmann Institute of Science)
Summer 2006


Rome, November 3, 2009

Dear Noga,
I just learned the sad news. Amir gave a course here in Rome on June 2006. The course was fantastic, it generated a lot of interest. A student of mine, Fabio Patrizi, actually changed the subject of his PhD thesis and started to apply Amir late work on synthesis by model checking for doing service and agent composition. I also joined this research and started advertising Amir's work on synthesis by model checking within the Artificial Intelligence, Knowledge Representation, and Planning communities. Even earlier today I was reading an Amir's 2005 paper on fair simulation to prepare my next submission.

I am honored to have met him. I feel a great loss.
The scientific community will greatly miss him.


This mini course deals with verification and synthesis of reactive systems relative to Temporal Logic Specifications. The main topic of the course is presentation of algorithms for the synthesis of reactive systems (including digital circuits) from TL specifications. The algorithms are based on solutions of fixed-point equations, using symbolic (BDD-based) methods. The complexity of the algorithms is polynomial where the degree is determined by the location of the specification formula in the hierarchy of temporal properties. For example, we present a linear time algorithm for specifications which are invariance formulas, and a quadratic time algorithm for response properties.

As a background, we present also the the theory of LTL model checking in order to introduce our computational model, the hierarchy of LTL properties, and point out the strong analogy between model checking and synthesis algorithms where we can get the second from the first by simply replacing the "predecessor" operator in the fixed-point expression.

The general plan of the course is as follows:

  1. The Computational model of Fair Discrete Systems. Linear Temporal Logic (LTL) and the hierarchy of temporal properties.
  2. Temporal Testers, and symbolic model checking of LTL properties.
  3. The synthesis problem: realizability, the game frameworks, and game structures for controller synthesis.
  4. Solving games for Safety, Response, Generalized Response properties and Reactivity(1). Extracting a strategy (program) from a game analysis.
  5. Solving the general Reactivity(k) game. Design synthesis.

Prior knowledge of LTL and model checking is desired but not essential.


  1. Part 1 (4up)
  2. Part 2 (4up)
  3. Part 3 (4up)

Amir in Rome, June 2006 - 1 Amir in Rome, June 2006 - 2
Photos (courtesy of Alberto Pettorossi)

Giuseppe De Giacomo
Dottorato di Ricerca in Ingegneria Informatica

Dipartamento di Informatica e Sistemistica,
Universita di Roma "La Sapienza"