Flow Logic
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 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 \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. 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 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 P^{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.
Flow Network
Temporal Logic
9:1-9:18
Regular Paper
Orna
Kupferman
Orna Kupferman
Gal
Vardi
Gal Vardi
10.4230/LIPIcs.CONCUR.2017.9
R.K. Ahuja, T.L. Magnanti, and J.B. Orlin. Network flows: Theory, algorithms, and applications. Prentice Hall Englewood Cliffs, 1993.
R. Alur and T.A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181-204, 1994.
R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002.
R. Beigel. Bounded queries to sat and the boolean hierarchy. Theoretical Computer Science, 84(2):199-223, 1991.
M. Canini, D. Venzano, P. Perešíni, D. Kostić, and J. Rexford. A nice way to test openflow applications. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12), pages 127-140, 2012.
K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. In Proc. 18th Int. Conf. on Concurrency Theory, pages 59-73, 2007.
E. Clarke, T.A. Henzinger, and H. Veith. Handbook of Model Checking. Elsvier, 2016. Forthcoming.
E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer, 1981.
E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
T.H. Cormen, C.E. Leiserson, and R.L. Rivest. Introduction to Algorithms. MIT Press and McGraw-Hill, 1990.
E.A. Dinic. Algorithm for solution of a problem of maximum flow in a network with power estimation. Soviet Math. Dokl, 11(5):1277-1280, 1970. English translation by RF. Rinehart.
J. Edmonds and R.M. Karp. Theoretical improvements in algorithmic efficiency for network flow problems. Journal of the ACM, 19(2):248-264, 1972.
E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8:275-306, 1987.
S. Even, A. Itai, and A. Shamir. On the complexity of timetable and multicommodity flow problems. SIAM Journal on Computing, 5(4):691-703, 1976.
D. Fisman, O. Kupferman, and Y. Lustig. Rational synthesis. In Proc. 16th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science, pages 190-204. Springer, 2010.
L.R. Ford and D.R. Fulkerson. Maximal flow through a network. Canadian journal of Mathematics, 8(3):399-404, 1956.
L.R. Ford and D.R. Fulkerson. Flows in networks. Princeton Univ. Press, Princeton, 1962.
A.V. Goldberg, É. Tardos, and R.E. Tarjan. Network flow algorithms. Technical report, DTIC Document, 1989.
A.V. Goldberg and R.E. Tarjan. A new approach to the maximum-flow problem. Journal of the ACM, 35(4):921-940, 1988.
D. Granata, R. Cerulli, M.G. Scutellá, and A. Raiconi. Maximum flow problems and an NP-complete variant on edge-labeled graphs. In Handbook of Combinatorial Optimization, pages 1913-1948. Springer, 2013.
J.Y. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3):549-587, 1990.
P. Kazemian, M. Chang, H. Zeng, G. Varghese, N. McKeown, and S. Whyte. Real time network policy checking using header space analysis. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13), pages 99-111, 2013.
P. Kazemian, G. Varghese, and N. McKeown. Header space analysis: Static checking for networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12), pages 113-126, 2012.
A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P.B. Godfrey. Veriflow: verifying network-wide invariants in real time. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13), pages 15-27, 2013.
O. Kupferman, A. Pnueli, and M.Y. Vardi. Once and forall. Journal of Computer and Systems Science, 78(3):981-996, 2012.
O. Kupferman and T. Tamir. Properties and utilization of capacitated automata. In Proc. 34th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 29 of LIPIcs, pages 33-44. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2014.
O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312-360, 2000.
M. Kuzniar, P. Peresini, M. Canini, D. Venzano, and D. Kostic. A soft way for openflow switch interoperability testing. In Proceedings of the 8th international conference on Emerging networking experiments and technologies, pages 265-276. ACM, 2012.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th ACM Symp. on Principles of Programming Languages, pages 97-107, 1985.
B.T. Loo, T. Condie, M. Garofalakis, D.E. Gay, J.M. Hellerstein, P. Maniatis, R. Ramakrishnan, T. Roscoe, and I. Stoica. Declarative networking: language, execution and optimization. In Proceedings of the 2006 ACM SIGMOD international conference on Management of data, pages 97-108. ACM, 2006.
N.P. Lopes, N. Bjørner, P. Godefroid, K. Jayaraman, and G. Varghese. Checking beliefs in dynamic networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pages 499-512, 2015.
A. Madry. Computing maximum flow with augmenting electrical flows. In Foundations of Computer Science (FOCS), 2016 IEEE 57th Annual Symposium on, pages 593-602. IEEE, 2016.
R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd Int. Joint Conf. on Artificial Intelligence, pages 481-489. British Computer Society, 1971.
J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 9th ACM Symp. on Principles of Programming Languages, volume 137 of Lecture Notes in Computer Science, pages 337-351. Springer, 1982.
A. Schrijver. Combinatorial Optimization. Springer, 2003.
B.L. Schwartz. Possible winners in partially completed tournaments. SIAM Review, 8(3):302-308, 1966.
A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32:733-749, 1985.
É. Tardos. A strongly polynomial minimum cost circulation algorithm. Combinatorica, 5(3):247-255, 1985.
Y. Velner, K. Alpernas, A. Panda, A. Rabinovich, M. Sagiv, S. Shenker, and S. Shoham. Some complexity results for stateful network verification. In Proc. 22nd Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pages 811-830. Springer, 2016.
A. Wang, P. Basu, B.T. Loo, and O. Sokolsky. Declarative network verification. In International Symposium on Practical Aspects of Declarative Languages, pages 61-75. Springer, 2009.
G. Wechsung. On the boolean closure of np. In Proceedings of the International Conference on Fundamentals of Computation Theory, volume 199 of Lecture Notes in Computer Science, pages 485-493. Springer, 1985.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode