M2 (9 a 12hs) Synthesis from Temporal Specifications with Applications in Robotics and Model-driven Development

Profesor: Nir Piterman (Imperial College London, UK). Horario: Turno mañana de 9 a 12 horas. En inglés.

Profesor: Nir Piterman

Horario: Lunes a viernes de 9 a 12 horas. Aula 4 y Labo 4 (pabellón 1).

Idioma: inglés. El profesor maneja bien el castellano, así que podrá responder preguntas en ese idioma, de ser necesario.

Evaluación: trabajo práctico - Bajar el enunciado.

Resumen:

Reactive systems such as robot controllers and web interfaces are systems whose main role is to persistently interact with their environment. Such systems are notoriously hard to design and implement. Synthesis is a technique for automatically generating correct-by-construction reactive systems from high-level descriptions. This is one of the greatest challenges in the area of formal methods. Recent years have seen significant theoretical and practical progress in this field leading to applications in hardware design, robotics, user programming, and model-driven development.

In this course I will teach the theoretical background that supports these applications. We will cover linear temporal logic and how to extend its expressive power. I will introduce the underlying framework of two-player games of infinite duration, the main framework that underlies applications of synthesis. We will then show how to extract controllers from winning strategies in games and reconnect games solutions to specifications in temporal logic. Finally, we will discuss the successful application of generalized reactivity[1] games to application in the above mentioned fields.