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 Image 1 for short). The definition of the problem is analogous to that for M S O ( ω, < ). Given an HS Image 1 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 Image 1, whose modalities are drawn from the set { A ( m e e t s ), A ¯ ( m e t b y ), B ( b e g u n b y ), B ¯ ( b e g i n s ) } interpreted over finite linear orders and N. We prove that, over finite linear orders, the problem is decidable (Ackermann-hard) for Image 2 and undecidable for A A ¯ B B ¯. Moreover, we show that if we replace finite linear orders by N, then it becomes undecidable even for AB B ¯. Finally, we study the generalization of Image 2 to Image 3, where k is the number of distinct equivalence relations. Despite the fact that the satisfiability problem for Image 3, 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.

Authors

• Angelo Montanari
• Pietro Sala

Keywords

• Synthesis
• Interval temporal logic
• Decidability
• Complexity