Orna Kupferman ; Gal Vardi - Flow Logic

lmcs:4595 - Logical Methods in Computer Science, November 14, 2019, Volume 15, Issue 4 - https://doi.org/10.23638/LMCS-15(4:9)2019
Flow LogicArticle

Authors: Orna Kupferman ; Gal Vardi

    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.


    Volume: Volume 15, Issue 4
    Published on: November 14, 2019
    Accepted on: August 29, 2019
    Submitted on: June 18, 2018
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • From correct to high-quality reactive systems; Funder: European Commission; Code: 278410

    Consultation statistics

    This page has been seen 1667 times.
    This article's PDF has been downloaded 409 times.