Show simple item record

dc.contributor.authorKahn, David
dc.date.accessioned2017-07-07T21:06:16Z
dc.date.available2017-07-07T21:06:16Z
dc.date.issued2017-07-07
dc.identifier.urihttps://hdl.handle.net/1813/51765
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.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 in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Statistics