流动逻辑
摘要：流网络在计算机科学中引起了很多研究。实际上，在许多应用领域中，许多问题可以归结为流网络的问题。这些应用中的许多都可以从一个可以形式化地推理流网络属性的框架中受益。我们介绍了流逻辑：一种将流函数作为显式的一阶对象处理，并能够规范地描述流网络丰富属性的模态逻辑。我们逻辑BFL*（分支流逻辑）的语法类似于时间逻辑CTL*的语法，除了原子断言可能是流命题（如$>gamma$或$geqgamma$，其中$gammaIn mathbb{N}$，它们表示顶点中的流的值），并且第一阶量化可以应用于路径和流函数。我们对BFL*和其扩展和片段进行了全面的研究。我们的扩展包括流量量词，其范围是非整数流函数或最大流函数的流量量词，路径量词范围是非零流量传输路径，过去算子，以及流量值的一阶量化。我们集中讨论模型检测问题，并表明它与CTL*一样是PSPACE完全的。然而，处理流量量词会增加复杂性，使得网络的复杂性增加到${\mbox{m P}}^{\mbox{m NP}}$，即使对于LTL和CTL的流量片段LFL和BFL也是如此。然而，我们仍然能够指出BFL*的一个有用子集，模型检测问题可以在多项式时间内解决。最后，我们引入并研究了BFL*的查询检测问题，其中欠指定的BFL*公式用于网络探索。
作者：Orna Kupferman, Gal Vardi
论文ID：1806.05956
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22