{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:51:58Z","timestamp":1764402718057},"publisher-location":"Berlin, Heidelberg","reference-count":53,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662494974"},{"type":"electronic","value":"9783662494981"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49498-1_12","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T13:36:06Z","timestamp":1458567366000},"page":"282-309","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":46,"title":["Probabilistic NetKAT"],"prefix":"10.1007","author":[{"given":"Nate","family":"Foster","sequence":"first","affiliation":[]},{"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[]},{"given":"Konstantinos","family":"Mamouras","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Reitblatt","sequence":"additional","affiliation":[]},{"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Anderson, C., Foster, N., Guha, A., Jeannin, J., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: POPL 2014, ACM (2014)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-19718-5_5","volume-title":"Programming Languages and Systems","author":"J Borgstr\u00f6m","year":"2011","unstructured":"Borgstr\u00f6m, J., Gordon, A.D., Greenberg, M., Margetson, J., Van Gael, J.: Measure transformer semantics for Bayesian machine learning. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 77\u201396. Springer, Heidelberg (2011)"},{"issue":"3","key":"12_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/2656877.2656890","volume":"44","author":"P Bosshart","year":"2014","unstructured":"Bosshart, P., Daly, D., et al.: P4: programming protocol-independent packet processors. ACM SIGCOMM Comput. Commun. Rev. 44(3), 87\u201395 (2014)","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-45694-5_25","volume-title":"CONCUR 2002 - Concurrency Theory","author":"S Cattani","year":"2002","unstructured":"Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371\u2013385. Springer, Heidelberg (2002)"},{"key":"12_CR5","volume-title":"A Course in Probability Theory","author":"KL Chung","year":"1974","unstructured":"Chung, K.L.: A Course in Probability Theory, 2nd edn. Academic Press, New York (1974)","edition":"2"},{"issue":"1","key":"12_CR6","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1109\/18.61109","volume":"37","author":"R Cruz","year":"1991","unstructured":"Cruz, R.: A calculus for network delay, parts I and II. IEEE Trans. Inf. Theor. 37(1), 114\u2013141 (1991)","journal-title":"IEEE Trans. Inf. Theor."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Demers, A., Gealy, M., Greene, D., Hauser, C., Irish, W., Larson, J., Manning, S., Shenker, S., Sturgis, H., Swinehart, D., Terry, D., Woods, D.: Epidemic algorithms for replicated database maintenance. In: PODC 1987, ACM (1987)","DOI":"10.1145\/41840.41841"},{"issue":"2","key":"12_CR8","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1006\/inco.2001.2962","volume":"179","author":"J Desharnais","year":"2002","unstructured":"Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163\u2013193 (2002)","journal-title":"Inf. Comput."},{"issue":"3","key":"12_CR9","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/j.tcs.2003.09.013","volume":"318","author":"J Desharnais","year":"2004","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: A metric for labelled Markov processes. Theor. Comput. Sci. 318(3), 323\u2013354 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR10","series-title":"Studies in Informatics","doi-asserted-by":"publisher","DOI":"10.1201\/9781584889427","volume-title":"Stochastic Relations: Foundations for Markov Transition Systems","author":"E Doberkat","year":"2007","unstructured":"Doberkat, E.: Stochastic Relations: Foundations for Markov Transition Systems. Studies in Informatics. Chapman Hall, New York (2007)"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Foster, N., Harrison, R., Freedman, M., Monsanto, C., Rexford, J., Story, A., Walker, D.: Frenetic: a network programming language. In: ICFP 2011, ACM (2011)","DOI":"10.1145\/2034773.2034812"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for NetKAT. In: POPL 2015, ACM (2015)","DOI":"10.1145\/2676726.2677011"},{"key":"12_CR13","unstructured":"Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT (full version). \n                    http:\/\/hdl.handle.net\/1813\/40335"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Gill, P., Jain, N., Nagappan, N.: Understanding network failures in data centers: measurement, analysis, and implications. In: SIGCOMM 2011, ACM (2011)","DOI":"10.1145\/2018436.2018477"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Gordon, A., Henzinger, T., Nori, A., Rajamani, S.: Probabilistic programming. In: ICSE 2014, IEEE (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"12_CR16","first-page":"199","volume":"319","author":"F Gretz","year":"2015","unstructured":"Gretz, F., Jansen, N., Kaminski, B., Katoen, J., McIver, A., Olmedo, F.: Conditioning in probabilistic programming. MFPS 2015 Electron. Notes Theor. Comput. Sci. 319, 199\u2013216 (2015)","journal-title":"MFPS 2015 Electron. Notes Theor. Comput. Sci."},{"key":"12_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9440-2","volume-title":"Measure Theory","author":"PR Halmos","year":"1950","unstructured":"Halmos, P.R.: Measure Theory. Van Nostrand, New York (1950)"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Jiang, Y.: A basic stochastic network calculus. In: SIGCOMM 2006, ACM (2006)","DOI":"10.1145\/1159913.1159929"},{"key":"12_CR19","unstructured":"Jones, C.: Probabilistic nondeterminism. Ph.D. thesis, Edinburgh University (1990)"},{"key":"12_CR20","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS 1991, IEEE (1991)"},{"key":"12_CR21","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: NSDI 2012, USENIX (2012)"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.: VeriFlow: verifying network-wide invariants in real time. In: NSDI 2013, USENIX (2013)","DOI":"10.1145\/2342441.2342452"},{"key":"12_CR23","first-page":"328","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. JCSS 22, 328\u2013350 (1981)","journal-title":"JCSS"},{"issue":"2","key":"12_CR24","first-page":"162","volume":"30","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. JCSS 30(2), 162\u2013178 (1985)","journal-title":"JCSS"},{"issue":"3","key":"12_CR25","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. TOPLAS 19(3), 427\u2013443 (1997)","journal-title":"TOPLAS"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"655","DOI":"10.1007\/978-3-642-40313-2_58","volume-title":"Mathematical Foundations of Computer Science 2013","author":"D Kozen","year":"2013","unstructured":"Kozen, D., Mardare, R., Panangaden, P.: Strong completeness for Markovian logics. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 655\u2013666. Springer, Heidelberg (2013)"},{"issue":"7","key":"12_CR27","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., et al.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027\u20131077 (2007)","journal-title":"Inf. Comput."},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"681","DOI":"10.1007\/978-3-642-32589-2_59","volume-title":"Mathematical Foundations of Computer Science 2012","author":"KG Larsen","year":"2012","unstructured":"Larsen, K.G., Mardare, R., Panangaden, P.: Taking It to the limit: approximate reasoning for Markov processes. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 681\u2013692. Springer, Heidelberg (2012)"},{"key":"12_CR29","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K Larsen","year":"1991","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 456\u2013471 (1991)","journal-title":"Inf. Comput."},{"key":"12_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45318-0","volume-title":"Network Calculus: A Theory of Deterministic Queuing Systems for the Internet","author":"J Boudec Le","year":"2001","unstructured":"Le Boudec, J., Thiran, P.: Network Calculus: A Theory of Deterministic Queuing Systems for the Internet. Springer-Verlag, Heidelberg (2001)"},{"issue":"1","key":"12_CR31","first-page":"90","volume":"76","author":"A McIver","year":"2008","unstructured":"McIver, A., Cohen, E., Morgan, C., Gonzalia, C.: Using probabilistic Kleene algebra pKA for protocol verification. JLAP 76(1), 90\u2013111 (2008)","journal-title":"JLAP"},{"key":"12_CR32","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, New York (2005)"},{"issue":"2","key":"12_CR33","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1355734.1355746","volume":"38","author":"N McKeown","year":"2008","unstructured":"McKeown, N., Anderson, T., et al.: Openflow: enabling innovation in campus networks. SIGCOMM CCR 38(2), 69\u201374 (2008)","journal-title":"SIGCOMM CCR"},{"issue":"4","key":"12_CR34","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1145\/964725.633041","volume":"32","author":"A. Medina","year":"2002","unstructured":"Medina, A., Taft, N., Salamatian, K., Bhattacharyya, S., Diot, C.: Traffic matrix estimation: existing techniques and new directions. In: SIGCOMM 2002, ACM (2002)","journal-title":"ACM SIGCOMM Computer Communication Review"},{"key":"12_CR35","unstructured":"Monsanto, C., Reich, J., Foster, N., Rexford, J., Walker, D.: Composing software defined networks. In NSDI 2013, USENIX (2013)"},{"issue":"3","key":"12_CR36","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. TOPLAS 18(3), 325\u2013353 (1996)","journal-title":"TOPLAS"},{"key":"12_CR37","unstructured":"Nelson, T., Ferguson, A., Scheer, M., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. In: NSDI 2014, USENIX (2014)"},{"key":"12_CR38","unstructured":"Panangaden, P.: Probabilistic relations. In: School of Computer Science, McGill University, Montreal, pp. 59\u201374 (1998)"},{"key":"12_CR39","doi-asserted-by":"publisher","DOI":"10.1142\/p595","volume-title":"Labelled Markov Processes","author":"P Panangaden","year":"2009","unstructured":"Panangaden, P.: Labelled Markov Processes. Imperial College Press, London (2009)"},{"key":"12_CR40","volume-title":"Introduction to Probabilistic Automata","author":"A Paz","year":"1971","unstructured":"Paz, A.: Introduction to Probabilistic Automata. Academic Press, Orlando (1971)"},{"key":"12_CR41","unstructured":"Ramshaw, L.H.: Formalizing the analysis of algorithms. Ph.D. thesis, Stanford University (1979)"},{"key":"12_CR42","volume-title":"Measure Theory and Integration","author":"MM Rao","year":"1987","unstructured":"Rao, M.M.: Measure Theory and Integration. Wiley-Interscience, New York (1987)"},{"key":"12_CR43","unstructured":"Roy, D.: Computability, inference and modeling in probabilistic programming. Ph.D. thesis, Massachusetts Institute of Technology (2011)"},{"key":"12_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-08921-7_92","volume-title":"Mathematical Foundations of Computer Science 1978","author":"N Saheb-Djahromi","year":"1978","unstructured":"Saheb-Djahromi, N.: Probabilistic LCF. In: Winkowski, J. (ed.) Mathematical Foundations of Computer Science 1978. Lecture Notes in Computer Science, vol. 64, pp. 442\u2013451. Springer, Heidelberg (1978)"},{"key":"12_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/11817949_5","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"R Segala","year":"2006","unstructured":"Segala, R.: Probability and nondeterminism in operational models of concurrency. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 64\u201378. Springer, Heidelberg (2006)"},{"key":"12_CR46","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. NJC 2, 250\u2013273 (1995)","journal-title":"NJC"},{"key":"12_CR47","doi-asserted-by":"crossref","unstructured":"Smolka, S., Eliopoulos, S., Foster, N., Guha, A.: A fast compiler for NetKAT. In: ICFP 2015, ACM (2015)","DOI":"10.1145\/2784731.2784761"},{"key":"12_CR48","first-page":"3","volume":"222","author":"R Tix","year":"2009","unstructured":"Tix, R., Keimel, K., Plotkin, G.: Semantic domains for combining probability and nondeterminism. ENTCS 222, 3\u201399 (2009)","journal-title":"ENTCS"},{"issue":"2","key":"12_CR49","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1137\/0211027","volume":"11","author":"L Valiant","year":"1982","unstructured":"Valiant, L.: A scheme for fast parallel communication. SIAM J. Comput. 11(2), 350\u2013361 (1982)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"12_CR50","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1017\/S0960129505005074","volume":"16","author":"D Varacca","year":"2006","unstructured":"Varacca, D., Winskel, G.: Distributing probability over non-determinism. Math. Struct. Comput. Sci. 16(1), 87\u2013113 (2006)","journal-title":"Math. Struct. Comput. Sci."},{"key":"12_CR51","doi-asserted-by":"crossref","unstructured":"Voellmy, A., Wang, J., Yang, Y., Ford, B., Hudak, P.: Maple: simplifying SDN programming using algorithmic policies. In: SIGCOMM (2013)","DOI":"10.1145\/2486001.2486030"},{"key":"12_CR52","unstructured":"Zeng, H., Zhang, S., et al.: Libra: divide and conquer to verify forwarding tables in huge networks. In: NSDI (2014)"},{"key":"12_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/11499169_15","volume-title":"Quality of Service \u2013 IWQoS 2005","author":"Z-S Rui","year":"2005","unstructured":"Rui, Z.-S., McKeown, N.: Designing a predictable internet backbone with valiant load-balancing. In: de Meer, H., Bhatti, N. (eds.) IWQoS 2005. LNCS, vol. 3552, pp. 178\u2013192. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49498-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T01:04:27Z","timestamp":1584925467000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}