Webinar Link: https://usc.zoom.us/webinar/register/WN_zyIBh_1gQLmKpMJG0GyLxw 

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. 

Time permitting, I will present results that support the usage of synthesis in model-driven development and robot control.

Biography: Nir Piterman is a professor of computer science at the University of Gothenburg in Sweden.  Before that he was an associate professor at the University of Leicester, held postdoctoral research positions at Imperial College London and the Ecole Polytechnique Federal de Lausanne, and completed his PhD at the Weizmann Institute of Science. His research interests include formal verification and automata theory. Particularly, he has worked on model checking, temporal logic, reactive synthesis, and game solving.  His current research is funded by the European Research Council (ERC), the Swedish Research Council (VR), and the Wallenberg Autonomous Systems Program (WASP(. He is currently the editor in chief of the journal Formal Methods in System Design.

--- 

Host: Pierluigi Nuzzo

Center for Cyber-Physical Systems and the Internet of Things (CCI) http://cci.usc.edu

Center for Autonomy and AI (AAI) https://aai.usc.edu