论文标题
LTL具有本地和远程数据约束
LTL with Local and Remote Data Constraints
论文作者
论文摘要
我们考虑线性时间逻辑（LTL）的扩展，并在混凝土域上解释了本地和远程数据约束。该扩展是约束LTL的自然扩展和重复值的时间逻辑，这是之前已经研究过的。我们将使用以前的结果来证明此逻辑的可满足性问题是可决定的。此外，我们将看到试图通过使其表现力更具表现力来扩展这种逻辑可能导致不可证明性。
We consider an extension of linear-time temporal logic (LTL) with both local and remote data constraints interpreted over a concrete domain. This extension is a natural extension of constraint LTL and the Temporal Logic of Repeating Values, which have been studied before. We shall use previous results to prove that the satisfiability problem for this logic is decidable. Further, we shall see that trying to extend this logic by making it more expressive can lead to undecidability.
