PhD Application Talk: Reactive Synthesis - From Realizability to Optimization

The common statement of the problem asks for any solution to the problem. In practice, this can yield an unsuitable solution, in part due to missing expressivity of the specification logic. The liveness-operator 'eventually' can delay responses arbitrarily long - as long as there exists a path suffix delivering a response - without violating the specification.
Therefore I propose using a parametric version of temporal logic, adding expressivity to the specification logic. The parameters express upper bounds on the path operators, s.t. responses have to be delivered before the time bound. They form a realizability design space for the system, which is able to visualize the impact of additional requirements or components on the response guarantees for the system designer.
In this talk, I will give results on a fragment of this logic, showing decidability and algorithmic approaches to solve this problem in the context of reactive systems synthes.