{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:54Z","timestamp":1776333414958,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642120015","type":"print"},{"value":"9783642120022","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12002-2_3","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T01:20:25Z","timestamp":1268011225000},"page":"23-37","source":"Crossref","is-referenced-by-count":75,"title":["Assume-Guarantee Verification for Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongyang","family":"Qu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-44685-0_24","volume-title":"CONCUR 2001 - Concurrency Theory","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T., Jhala, R.: Compositional methods for probabilistic systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 351\u2013365. Springer, Heidelberg (2001)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of Algorithms\u00a015(1) (1990)","DOI":"10.1016\/0196-6774(90)90021-6"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026. Springer, Heidelberg (1995)"},{"key":"3_CR4","unstructured":"Chatterjee, K., de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga, M.: Compositional quantitative reasoning. In: Proc. QEST 2006 (2006)"},{"key":"3_CR5","unstructured":"Cheshire, S., Adoba, B., Gutterman, E.: Dynamic configuration of IPv4 link local addresses, http:\/\/www.ietf.org\/rfc\/rfc3927.txt"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"494","DOI":"10.1007\/978-3-540-31862-0_35","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"L. Cheung","year":"2005","unstructured":"Cheung, L., Lynch, N., Segala, R., Vaandrager, F.: Switched probabilistic I\/O automata. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol.\u00a03407, pp. 494\u2013510. Springer, Heidelberg (2005)"},{"key":"3_CR7","unstructured":"Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. QEST 2006 (2006)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032043","volume-title":"Automata, Languages and Programming","author":"C. Courcoubetis","year":"1990","unstructured":"Courcoubetis, C., Yannakakis, M.: Markov decision processes and regular events. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443. Springer, Heidelberg (1990)"},{"key":"3_CR9","unstructured":"Delahaye, B., Caillaud, B.: A model for probabilistic reasoning on assume\/guarantee contracts. Tech. Rep. 6719, INRIA (2008)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71209-1_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Etessami","year":"2007","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M.Y., Yannakakis, M.: Multi-objective Model Checking of Markov Decision Processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 50\u201365. Springer, Heidelberg (2007)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"3_CR12","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. Tech. Rep. RR-09-17, Oxford University Computing Laboratory (December 2009)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design\u00a029 (2006)","DOI":"10.1007\/s10703-006-0005-2"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 194\u2013206. Springer, Heidelberg (2001)"},{"issue":"4","key":"3_CR15","doi-asserted-by":"publisher","first-page":"977","DOI":"10.1137\/S0097539704446487","volume":"37","author":"N. Lynch","year":"2007","unstructured":"Lynch, N., Segala, R., Vaandrager, F.: Observing branching structure through probabilistic contexts. SIAM Journal on Computing\u00a037(4), 977\u20131013 (2007)","journal-title":"SIAM Journal on Computing"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Pasareanu, C., Giannakopoulou, D., Bobaru, M., Cobleigh, J., Barringer, H.: Learning to divide and conquer: Applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design\u00a032(3) (2008)","DOI":"10.1007\/s10703-008-0049-6"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Pavese, E., Braberman, V., Uchitel, S.: Probabilistic environments in the quantitative analysis of (non-probabilistic) behaviour models. In: Proc. ESEC\/FSE 2009 (2009)","DOI":"10.1145\/1595696.1595760"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Pogosyants, A., Segala, R., Lynch, N.: Verification of the randomized consensus algorithm of Aspnes and Herlihy: A case study. Dist. Comp.\u00a013(4) (2000)","DOI":"10.1007\/PL00008917"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/3-540-60218-6_17","volume-title":"CONCUR \u201995 Concurrency Theory","author":"R. Segala","year":"1995","unstructured":"Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 234\u2013248. Springer, Heidelberg (1995)"},{"key":"3_CR20","unstructured":"Segala, R.: Modelling and Verification of Randomized Distributed Real Time Systems. Ph.D. thesis, Massachusetts Institute of Technology (1995)"},{"key":"3_CR21","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing\u00a02(2) (1995)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12002-2_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:46:24Z","timestamp":1606185984000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12002-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120015","9783642120022"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12002-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}