{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:37:42Z","timestamp":1753889862293,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2019,11,14]],"date-time":"2019-11-14T00:00:00Z","timestamp":1573689600000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,11,14]],"date-time":"2019-11-14T00:00:00Z","timestamp":1573689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,11,14]],"date-time":"2019-11-14T00:00:00Z","timestamp":1573689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["278410"],"award-info":[{"award-number":["278410"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>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 $&amp;gt; \\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.<\/jats:p>","DOI":"10.23638\/lmcs-15(4:9)2019","type":"journal-article","created":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:37:38Z","timestamp":1743701858000},"source":"Crossref","is-referenced-by-count":0,"title":["Flow Logic"],"prefix":"10.23638","volume":"Volume 15, Issue 4","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Gal","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2019,11,14]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/arxiv.org\/pdf\/1806.05956v3","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/arxiv.org\/pdf\/1806.05956v3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:37:39Z","timestamp":1743701859000},"score":1,"resource":{"primary":{"URL":"http:\/\/lmcs.episciences.org\/4595"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,14]]},"references-count":0,"URL":"https:\/\/doi.org\/10.23638\/lmcs-15(4:9)2019","relation":{"has-preprint":[{"id-type":"arxiv","id":"1806.05956v2","asserted-by":"subject"},{"id-type":"arxiv","id":"1806.05956v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1806.05956","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1806.05956","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2019,11,14]]},"article-number":"4595"}}