Rome, November 3, 2009
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:
Prior knowledge of LTL and model checking is desired but not essential.
Photos (courtesy of Alberto Pettorossi)
Giuseppe De Giacomo
Dottorato di Ricerca in Ingegneria Informatica
Dipartamento di Informatica e Sistemistica,
Universita di Roma "La Sapienza"