Interval-based Synthesis

TL;DR

This paper investigates the synthesis problem for a modal logic of intervals with an equivalence relation, analyzing decidability for various fragments over finite linear orders and natural numbers.

Contribution

It introduces the synthesis problem for an extended interval logic, establishing decidability results for specific fragments and demonstrating undecidability in others.

Findings

ABBbareq fragment is decidable but non-primitive recursive

AAbarBBbar fragment is undecidable

Synthesis over natural numbers is undecidable for ABBbar

Abstract

We introduce the synthesis problem for Halpern and Shoham's modal logic of intervals extended with an equivalence relation over time points, abbreviated HSeq. In analogy to the case of monadic second-order logic of one successor, the considered synthesis problem receives as input an HSeq formula phi and a finite set Sigma of propositional variables and temporal requests, and it establishes whether or not, for all possible evaluations of elements in Sigma in every interval structure, there exists an evaluation of the remaining propositional variables and temporal requests such that the resulting structure is a model for phi. We focus our attention on decidability of the synthesis problem for some meaningful fragments of HSeq, whose modalities are drawn from the set A (meets), Abar (met by), B (begins), Bbar (begun by), interpreted over finite linear orders and natural numbers. We prove that the fragment ABBbareq is decidable (non-primitive recursive hard), while the fragment AAbarBBbar turns out to be undecidable. In addition, we show that even the synthesis problem for ABBbar becomes undecidable if we replace finite linear orders by natural numbers.