References & Citations
Computer Science > Logic in Computer Science
Title: Flow Logic
(Submitted on 15 Jun 2018 (v1), last revised 13 Nov 2019 (this version, v3))
Abstract: 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.
Submission history
From: Gal Vardi [view email] [via LOGICAL proxy][v1] Fri, 15 Jun 2018 13:40:51 GMT (189kb,D)
[v2] Sun, 2 Jun 2019 21:13:36 GMT (191kb,D)
[v3] Wed, 13 Nov 2019 08:59:43 GMT (334kb,D)
Link back to: arXiv, form interface, contact.