In this paper, we deal with the synthesis problem for Halpern and Shoham's interval temporal logic HS extended with an equivalence relation ∼ over time points (HS[Formula presented] for short). The definition of the problem is analogous to that for MSO(ω,<). Given an HS[Formula presented] formula φ and a finite set Σφ⋄ of proposition letters and temporal requests, it consists of determining, whether or not, for all possible valuations of elements in Σφ⋄ in every interval structure, there is a valuation of the remaining proposition letters and temporal requests such that the resulting structure is a model for φ. We focus on the decidability and complexity of the problem for some meaningful fragments of HS[Formula presented], whose modalities are drawn from the set {A(meets),A ̄(metby),B(begunby),B ̄(begins)} interpreted over finite linear orders and N. We prove that, over finite linear orders, the problem is decidable (ACKERMANN-hard) for [Formula presented] and undecidable for AA ̄BB ̄. Moreover, we show that if we replace finite linear orders by N, then it becomes undecidable even for ABB ̄. Finally, we study the generalization of [Formula presented] to [Formula presented], where k is the number of distinct equivalence relations. Despite the fact that the satisfiability problem for [Formula presented], with k>1, over finite linear orders, is already undecidable, we prove that, under a natural semantic restriction (refinement condition), the synthesis problem turns out to be decidable.
