Document Open Access Logo

Flow Logic

Authors Orna Kupferman, Gal Vardi



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.9.pdf
  • Filesize: 0.55 MB
  • 18 pages

Document Identifiers

Author Details

Orna Kupferman
Gal Vardi

Cite AsGet BibTex

Orna Kupferman and Gal Vardi. Flow Logic. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 9:1-9:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.9

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 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.
Keywords
  • Flow Network
  • Temporal Logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. R.K. Ahuja, T.L. Magnanti, and J.B. Orlin. Network flows: Theory, algorithms, and applications. Prentice Hall Englewood Cliffs, 1993. Google Scholar
  2. R. Alur and T.A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181-204, 1994. Google Scholar
  3. R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. Google Scholar
  4. R. Beigel. Bounded queries to sat and the boolean hierarchy. Theoretical Computer Science, 84(2):199-223, 1991. Google Scholar
  5. 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. Google Scholar
  6. K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. In Proc. 18th Int. Conf. on Concurrency Theory, pages 59-73, 2007. Google Scholar
  7. E. Clarke, T.A. Henzinger, and H. Veith. Handbook of Model Checking. Elsvier, 2016. Forthcoming. Google Scholar
  8. 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. Google Scholar
  9. E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999. Google Scholar
  10. T.H. Cormen, C.E. Leiserson, and R.L. Rivest. Introduction to Algorithms. MIT Press and McGraw-Hill, 1990. Google Scholar
  11. 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. Google Scholar
  12. J. Edmonds and R.M. Karp. Theoretical improvements in algorithmic efficiency for network flow problems. Journal of the ACM, 19(2):248-264, 1972. Google Scholar
  13. E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8:275-306, 1987. Google Scholar
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. L.R. Ford and D.R. Fulkerson. Maximal flow through a network. Canadian journal of Mathematics, 8(3):399-404, 1956. Google Scholar
  17. L.R. Ford and D.R. Fulkerson. Flows in networks. Princeton Univ. Press, Princeton, 1962. Google Scholar
  18. A.V. Goldberg, É. Tardos, and R.E. Tarjan. Network flow algorithms. Technical report, DTIC Document, 1989. Google Scholar
  19. A.V. Goldberg and R.E. Tarjan. A new approach to the maximum-flow problem. Journal of the ACM, 35(4):921-940, 1988. Google Scholar
  20. 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. Google Scholar
  21. J.Y. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3):549-587, 1990. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. 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. Google Scholar
  25. O. Kupferman, A. Pnueli, and M.Y. Vardi. Once and forall. Journal of Computer and Systems Science, 78(3):981-996, 2012. Google Scholar
  26. 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. Google Scholar
  27. 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. Google Scholar
  28. 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. Google Scholar
  29. 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. Google Scholar
  30. 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. Google Scholar
  31. 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. Google Scholar
  32. 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. Google Scholar
  33. 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. Google Scholar
  34. 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. Google Scholar
  35. A. Schrijver. Combinatorial Optimization. Springer, 2003. Google Scholar
  36. B.L. Schwartz. Possible winners in partially completed tournaments. SIAM Review, 8(3):302-308, 1966. Google Scholar
  37. A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32:733-749, 1985. Google Scholar
  38. É. Tardos. A strongly polynomial minimum cost circulation algorithm. Combinatorica, 5(3):247-255, 1985. Google Scholar
  39. 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. Google Scholar
  40. 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. Google Scholar
  41. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail