一句话：提出流逻辑 BFL*，将流函数作为一阶对象刻画流网络性质，并系统分析其模型检测复杂度。
流网络应用广泛，但既有研究多关注最大流，缺乏形式化推理其更丰富性质的框架。本文提出流逻辑（Flow Logics），将流函数视为显式一阶对象。其分支流逻辑 BFL* 语法类似 CTL*，原子断言可为流命题（如 >γ、≥γ），并可对路径与流函数进行一阶量化。作者系统研究 BFL* 及其扩展与片段，包括非整数流、最大流、非零流路径、过去算子和流量值量化。结果表明，BFL* 的模型检测问题是 PSPACE 完全的，与 CTL* 相同；引入流量化后复杂度升至 P^NP，即使对 LFL/BFL 片段亦然；但仍存在多项式时间可解的有用片段。最后提出并研究 BFL* 的查询检测，用于网络探索。
Flow networks have attracted a lot of research in computer science. Indeed, many questions in numerous application areas can be reduced to questions about flow networks. Many of these applications would benefit from a framework in which one can formally reason about properties of flow networks that go beyond their maximal flow. We introduce Flow Logics: modal logics that treat flow functions as explicit first-order objects and enable the specification of rich properties of flow networks. The syntax of our logic BFL* (Branching Flow Logic) is similar to the syntax of the temporal logic CTL*, except that atomic assertions may be flow propositions, like $> \gamma$ or $\geq \gamma$, for $\gamma \in \mathbb{N}$, which refer to the value of the flow in a vertex, and that first-order quantification can be applied both to paths and to flow functions. We present an exhaustive study of the theoretical and practical aspects of BFL*, as well as extensions and fragments of it. Our extensions include flow quantifications that range over non-integral flow functions or over maximal flow functions, path quantification that ranges over paths along which non-zero flow travels, past operators, and first-order quantification of flow values. We focus on the model-checking problem and show that it is PSPACE-complete, as it is for CTL*. Handling of flow quantifiers, however, increases the complexity in terms of the network to ${\rm P}^{\rm NP}$, even for the LFL and BFL fragments, which are the flow-counterparts of LTL and CTL. We are still able to point to a useful fragment of BFL* for which the model-checking problem can be solved in polynomial time. Finally, we introduce and study the query-checking problem for BFL*, where under-specified BFL* formulas are used for network exploration.