Interval-based Synthesis

In this paper, we introduce the synthesis problem for Halpern and Shoham's interval temporal logic extended with an equivalence relation sim over time points (HSsim for short). In analogy to the case of monadic second-order logic of one successor, given an HSsim formula phi and a finite set Sigma^T_spoiler of proposition letters and temporal requests, the problem consists of establishing whether or not, for all possible evaluations of elements in Sigma^T_spoiler in every interval structure, there is an evaluation of the remaining proposition letters and temporal requests such that the resulting structure is a model for phi. We focus our attention on the decidability of the synthesis problem for some meaningful fragments of HSsim, whose modalities are drawn from {meets, met by, begun by, begins}, interpreted over finite linear orders and natural numbers. We prove that the synthesis problem for ABBbar+sim over finite linear orders is decidable (non-primitive recursive hard), while AAbarBBbatr$ turns out to be undecidable. In addition, we show that if we replace finite linear orders by natural numbers, then the problem becomes undecidable even for ABBbar.