We study the reactive synthesis problem (RS) for specifications given in Metric Interval Temporal Logic (MITL). RS is known to be undecidable in a very general setting, but on infinite words only; and only the very restrictive BResRS subcase is known to be decidable (see D'Souza et al. and Bouyer et al.). In this paper, we precise the decidabil-ity border of MITL synthesis. We show RS is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit BResRS and introduce an efficient on-the-fly algorithm to solve it.
['Thomas Brihaye', 'Morgane Estievenart', 'Gilles Geeraerts', 'Hsi Ming H.M. Ho', 'Benjamin Monmege', 'Nathalie Sznajder']
Real-Time Synthesis is Hard!