Interval-based Synthesis

In this paper, we introduce the synthesis problem for Halpern and Shoham's interval temporal logic [5] extended with an equivalence relation similar to over time points (HS similar to for short). In analogy to the case of monadic second- order logic of one successor [2], given an HS similar to formula j and a finite set Sigma(T)(square) of proposition letters and temporal requests, the problem consists of establishing whether or not, for all possible evaluations of elements in Sigma(T)(square) 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 j. We focus our attention on the decidability of the synthesis problem for some meaningful fragments of HS similar to, whose modalities are drawn from {A (meets), (A) over bar (met by), B (begun by), (B) over bar (begins) }, interpreted over finite linear orders and natural numbers. We prove that the synthesis problem for AB (B) over bar similar to over finite linear orders is decidable (non- primitive recursive hard), while A (A) over barB (B) over bar 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 AB (B) over bar