License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2017.68
URN: urn:nbn:de:0030-drops-80969
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/8096/
Go to the corresponding LIPIcs Volume Portal

Kahn, David M.

Undecidable Problems for Probabilistic Network Programming

pdf-format:
LIPIcs-MFCS-2017-68.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{kahn:LIPIcs:2017:8096,
  author =	{David M. Kahn},
  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 =	{Kim G. Larsen and Hans L. Bodlaender and Jean-Francois Raskin},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/8096},
  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}
}

Keywords: Software-defined networking, NetKAT, ProbNetKAT, Undecidability, Probabilistic finite automata
Collection: 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)
Issue Date: 2017
Date of publication: 01.12.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI