DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2017.68

Undecidable Problems for Probabilistic Network Programming

Authors: David M. Kahn

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

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

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)

Copy BibTex To Clipboard

@InProceedings{kahn:LIPIcs.MFCS.2017.68,
  author =	{Kahn, David M.},
  title =	{{Undecidable Problems for Probabilistic Network Programming}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{68:1--68:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.68},
  URN =		{urn:nbn:de:0030-drops-80969},
  doi =		{10.4230/LIPIcs.MFCS.2017.68},
  annote =	{Keywords: Software-defined networking, NetKAT, ProbNetKAT, Undecidability, Probabilistic finite automata}
}

Search Results

Documents authored by Kahn, David M.

Undecidable Problems for Probabilistic Network Programming

Abstract

Cite as

Thanks for your feedback!

Could not send message