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.

Interval-based Synthesis

MONTANARI, Angelo;
2014-01-01

Abstract

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.
File in questo prodotto:
File Dimensione Formato  
GandALF2014cr.pdf

accesso aperto

Tipologia: Versione Editoriale (PDF)
Licenza: Creative commons
Dimensione 288.18 kB
Formato Adobe PDF
288.18 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/1037153
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact