Kupferman, Orna ;
Vardi, Gal
Flow Logic
Abstract
A flow network is a directed graph in which each edge has a capacity, bounding the amount of flow that can travel through it. 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. This includes direct applications, namely a search for a maximal flow in networks, as well as less direct applications, like maximal matching or optimal scheduling. 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 firstorder 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 \N, which refer to the value of the flow in a vertex, and that firstorder quantification can be applied both to paths and to flow functions. For example, the BFL* formula \Ef ((\geq 100) \wedge AG({\it low} \rightarrow (\leq 20)) states that there is a legal flow function in which the flow is above 100 and in all paths, the amount of flow that travels through vertices with low security is at most 20.
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 nonintegral flow functions or over maximal flow functions, path quantification that ranges over paths along which nonzero flow travels, past operators, and firstorder quantification of flow values. We focus on the modelchecking problem and show that it is PSPACEcomplete, as it is for CTL*. Handling of flow quantifiers, however, increases the complexity in terms of the network to P^{NP}, even for the LFL and BFL fragments, which are the flowcounterparts of LTL and CTL. We are still able to point to a useful fragment of BFL* for which the modelchecking problem can be solved in polynomial time.
BibTeX  Entry
@InProceedings{kupferman_et_al:LIPIcs:2017:7779,
author = {Orna Kupferman and Gal Vardi},
title = {{Flow Logic}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {9:19:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770484},
ISSN = {18688969},
year = {2017},
volume = {85},
editor = {Roland Meyer and Uwe Nestmann},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7779},
URN = {urn:nbn:de:0030drops77796},
doi = {10.4230/LIPIcs.CONCUR.2017.9},
annote = {Keywords: Flow Network, Temporal Logic}
}
01.09.2017
Keywords: 

Flow Network, Temporal Logic 
Seminar: 

28th International Conference on Concurrency Theory (CONCUR 2017)

Issue date: 

2017 
Date of publication: 

01.09.2017 