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 ∼ 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.