eCommons

 

Undecidable Problems for Probabilistic Network Programming

dc.contributor.authorKahn, David
dc.date.accessioned2017-07-07T21:06:16Z
dc.date.available2017-07-07T21:06:16Z
dc.date.issued2017-07-07
dc.description.abstractThe 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.en_US
dc.identifier.urihttps://hdl.handle.net/1813/51765
dc.language.isoenen_US
dc.subjectSoftware-defined networkingen_US
dc.subjectNetKATen_US
dc.subjectProbNetKATen_US
dc.subjectUndecidabilityen_US
dc.subjectProbabilistic finite automataen_US
dc.titleUndecidable Problems for Probabilistic Network Programmingen_US
dc.typetechnical reporten_US

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
undecidable probabilistic.pdf
Size:
558.6 KB
Format:
Adobe Portable Document Format
Description: