基于区间的综合
Interval-based Synthesis
摘要：
我们介绍了Halpern和Shoham的模态逻辑的时间点上的等价关系扩展的间隔，简称HSeq的综合问题。类似于一个后继者的一元二阶逻辑的情况，所考虑的合成问题接收HSeq公式phi和命题变量和时间请求的有限集合Sigma作为输入，并且它确定对于每个区间结构中的Sigma中的元素的所有可能的评估，存在对剩余的命题变量和时间请求的评估，使得所得到的结构是Φ的模型。我们将注意力集中在HSeq的一些有意义的片段的合成问题的可判定性上，其模态来自集合A（满足），Abar（满足），B（开始），Bbar（开始），在有限的线性顺序和自然数上解释。我们证明了片段ABBbareq是可判定的（非原始递归硬），而片段AAbarBBbar原来是不可判定的。此外，我们表明，即使ABBbar的合成问题变得不可判定，如果我们用自然数取代有限的线性订单。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
