Reactive synthesis from interval temporal logic specifications

In this paper, we deal with the synthesis problem for Halpern and Shoham's interval temporal logic HS extended with an equivalence relation $sim$ over time points (HSsim for short). The definition of the problem is analogous to that for $MSO(omega, <)$. Given an HSsim formula $arphi$ and a finite set $moves^{spoiler}$ of proposition letters and temporal requests, it consists of determining, whether or not, for all possible valuations of elements in $moves^{spoiler}$ 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 $arphi$. We focus on the decidability and complexity of the problem for some meaningful fragments of HSsim, whose modalities are drawn from the set ${A (meets), ar{A} (met by), B (begun by), ar{B} (begins) }$ interpreted over finite linear orders and $bN$. We prove that, over finite linear orders, the problem is decidable ( extsc{Ackermann}-hard) for $ABBsim$ and undecidable for $AABB$. Moroever, we show that if we replace finite linear orders by $bN$, then it becomes undecidable even for $ABB$. Finally, we study the generalization of $ABBsim$ to $ABBwidesim{k}$, where $k$ is the number of distinct equivalence relations. Despite the fact that the satisfiability problem for $ABBwidesim{k}$, 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.