When: Thursday, June 24, 2021, 3pm (CEST).

Where: Zoom online, check the address in the Google Calendar Event.

Topic: Synthesis From Temporal Specifications.

Speaker: Nir Piterman, Associate Professor at the University of Gothenburg.

Abstract

In this talk I will present the GR(1) approach to synthesis, the automatic production of designs from their temporal logic specifications. We are interested in reactive systems, systems that continuously interact with other programs, users, or their environment and specifications in linear temporal logic. Classical solutions to synthesis use either two player games or tree automata. I will give a short introduction to the technique of using two player games for synthesis.

The classical solution to synthesis requires the usage of deterministic automata. This solution is 2EXPTIME-complete, is quite complicated, and does not work well in practice. I will present a syntactic approach that restricts the kind of properties users are allowed to write. It turns out that this approach is general enough and can be extended to cover many properties written in practice.

I will survey some results in model-driven development and robot control.

Short Bio

Nir Piterman completed his PhD in 2005 at the Weizmann Institute of Science under the supervision of Amir Pnueli. Between 2005-2007 he was a postdoc in Tom Henzinger’s group in the Ecoloe Polytechnique Federal de Lausanne. Between 2007-2010 he was a research Fellow in Imperial College London working with Michael Huth. Then, he joined the University of Leicester in 2010 as a Lecturer, was promoted to Reader/Associate Professor in 2012. In March 2019 he joined the Department of Computer Science and Engineering at the University of Gothenburg as a Universitets Lektor / Associate Professor.

Material

  • Video (Passcode: X?+96uYw)