Document Open Access Logo

Undecidable Problems for Probabilistic Network Programming

Author David M. Kahn

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2017.68.pdf
  • Filesize: 0.49 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • Software-defined networking
  • NetKAT
  • ProbNetKAT
  • Undecidability
  • Probabilistic finite automata

Metrics

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

Abstract

The software-defined networking language NetKAT is able to verify many useful properties of networks automatically via a PSPACE decision procedure for program equality. However, for its probabilistic extension ProbNetKAT, no such decision procedure is known. We show that several potentially useful properties of ProbNetKAT are in fact undecidable, including emptiness of support intersection and certain kinds of distribution bounds and program comparisons. We do so by embedding the Post Correspondence Problem in ProbNetKAT via direct product expressions, and by directly embedding probabilistic finite automata.

Cite As Get BibTex

David M. Kahn. Undecidable Problems for Probabilistic Network Programming. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 68:1-68:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.MFCS.2017.68

Author Details

David M. Kahn

References

  1. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: Semantic foundations for networks. In Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL'14), pages 113-126, San Diego, California, USA, January 2014. ACM. Google Scholar
  2. Vincent D Blondel, Vincent Canterini, et al. Undecidable problems for probabilistic automata of fixed dimension. Theory of Computing systems, 36(3):231-245, 2003. Google Scholar
  3. Corinna Cortes, Mehryar Mohri, and Ashish Rastogi. On the Computation of Some Standard Distances Between Probabilistic Automata, pages 137-149. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006. URL: http://dx.doi.org/10.1007/11812128_14.
  4. Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic NetKAT. In Peter Thiemann, editor, 25th European Symposium on Programming (ESOP 2016), volume 9632 of Lecture Notes in Computer Science, pages 282-309, Eindhoven, The Netherlands, April 2016. Springer. Google Scholar
  5. Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for NetKAT. In Proc. 42nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL'15), pages 343-355, Mumbai, India, January 2015. ACM. Google Scholar
  6. Hugo Gimbert and Youssouf Oualhadj. Probabilistic Automata on Finite Words: Decidable and Undecidable Problems, pages 527-538. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14162-1_44,
  7. Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. On the Complexity of the Equivalence Problem for Probabilistic Automata, pages 467-481. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28729-9_31.
  8. Dexter Kozen. Kleene algebra with tests and commutativity conditions. In T. Margaria and B. Steffen, editors, Proc. Second Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), volume 1055 of Lecture Notes in Computer Science, pages 14-33, Passau, Germany, March 1996. Springer-Verlag. Google Scholar
  9. Dexter Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3):427-443, May 1997. Google Scholar
  10. Dexter Kozen. NetKAT: A formal system for the verification of networks. In Jacques Garrigue, editor, Proc. 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), volume 8858 of Lecture Notes in Computer Science, Singapore, November 17-19 2014. Asian Association for Foundation of Software (AAFS), Springer. Google Scholar
  11. Steffen Smolka, David Kahn, Praveen Kumar, and Nate Foster. Deciding probabilistic program equivalence in NetKAT. http://www.cs.cornell.edu/~smolka/papers/mcnetkat.pdf, 2017.
  12. Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. Cantor meets Scott: Domain-theoretic foundations for probabilistic network programming. In Proc. 44th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL'17), pages 557-571, Paris, France, January 2017. ACM. Google Scholar
  13. Wen-Guey Tzeng. A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing, 21(2):216-227, 1992. URL: http://dx.doi.org/10.1137/0221017.
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact