CTL* synthesis via LTL synthesis

Roderick Bloem, Sven Schewe, Ayrat Khalimov

We reduce synthesis for CTL* properties to synthesis for LTL. In the context of model checking this is impossible - CTL* is more expressive than LTL. Yet, in synthesis we have know…