Increasing the Scalability of LTL Synthesis: Generalized Rabin(1) Decision Procedures and Symbolic Bounded Synthesis

Speaker

Rüdiger Ehlers, Uni Saarbrücken

Title Increasing the Scalability of LTL Synthesis: Generalized Rabin(1) Decision Procedures and Symbolic Bounded Synthesis
When 16.09..2010, 15:00
Where Seminarraum Informatik 11
Abstract Synthesis of reactive systems from temporal logic specification is an ambitious challenge that attracted a lot of interest in the last few decades. From a practical point of view, current approaches to tackle this problem can broadly be classified into two groups: (1) approaches that aim at handling the full expressivity of commonly used specification logics such as linear time temporal logic (LTL), and (2) techniques that trade the full expressivity of LTL against the possibility to use simpler and faster algorithms for the synthesis process.

In this talk, some recent advancements in both of these areas are presented.

 

Slides