BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Synthesis from Temporal Specifications - Nir Piterman (Imperial Co
 llege London)
DTSTART:20071106T130000Z
DTEND:20071106T140000Z
UID:TALK8508@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Speaker: Nir Piterman\n\nOne of the most ambitious goals in th
 e field of verification is to automatically produce designs from their spe
 cifications\, a process called _synthesis_. We are interested in _reactive
  systems_\, systems that continuously interact with other programs\, users
 \, or their environment (like CPUs). The complexity of reactive system doe
 s not necessarily arise from computing complicated functions but rather fr
 om the fact that they have to be able to react to all possible inputs and 
 \nmaintain their behavior forever. Classical solutions to synthesis use ei
 ther two player games or tree automata and require the construction of det
 erministic automata.\nHowever\, determinization for automata on infinite w
 ords is extremely complicated and does not work well in practice. Here we 
 suggest a syntactic approach that restricts the kind of properties users a
 re allowed to write. We claim that this approach is general enough and can
  be extended to cover most properties written in practice. The main advant
 age of our approach is that it is tailored to the use of BDDs and uses the
  structure of given properties to handle them more efficiently.\nWe discus
 s how to extend our approach to handle more general properties and a few o
 pen issues.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR