{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:58Z","timestamp":1760202538173},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439134"},{"type":"electronic","value":"9783540456056"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45605-8_11","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T22:15:19Z","timestamp":1179267319000},"page":"169-187","source":"Crossref","is-referenced-by-count":57,"title":["Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol"],"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":"Jeremy","family":"Sproston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"issue":"2","key":"11_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"11_CR2","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1006\/inco.1995.1059","volume":"18","author":"R. Alur","year":"1995","unstructured":"R. Alur, A. Itai, R.P. Kurshan, and M. Yannakakis. Timing verification by successive approximation. Information and Computation, 18(1):142\u2013157, 1995.","journal-title":"Information and Computation"},{"key":"11_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-45251-6_18","volume-title":"Proc. FME\u201901","author":"D. Beyer","year":"2001","unstructured":"D. Beyer. Improvements in BDD-based reachability analysis of timed automata. In Proc. FME\u201901, volume 2021 of LNCS, pages 318\u2013343. Springer, 2001."},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1109\/49.840210","volume":"18","author":"G. Bianchi","year":"2000","unstructured":"G. Bianchi. Performance analysis of the IEEE 802.11 distributed coordination function. IEEE Journal on Selected Areas in Communication, 18:535\u2013547, 2000.","journal-title":"IEEE Journal on Selected Areas in Communication"},{"key":"11_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Proc. FSTTCS\u201995","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. FSTTCS\u201995, volume 1026 of LNCS, pages 499\u2013513. Springer, 1995."},{"key":"11_CR6","unstructured":"E.M. Clarke, M. Fujita, P. McGeer, K. McMillan, J. Yang, and X. Zhao. Multi-Terminal Binary Decision Diagrams: An efficient data structure for matrix representation. In Proc. IWLS\u201993, pages 6a:1\u201315, 1993. Also available in Formal Methods in System Design, 10(2\/3), 1997."},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"C. Daws and S. Yovine. Two examples of verification of multirate timed automata with Kronos. In Proc. RTSS\u201995, pages 66\u201375. IEEE Computer Society Press, 1995.","DOI":"10.1109\/REAL.1995.495197"},{"key":"11_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"Proc. CONCUR\u201999","author":"L. Alfaro de","year":"1999","unstructured":"L. de Alfaro. Computing minimum and maximum reachability times in probabilistic systems. In Proc. CONCUR\u201999, volume 1664 of LNCS, pages 66\u201381. Springer, 1999."},{"key":"11_CR9","unstructured":"C. Derman. Finite-State Markovian Decision Processes. Academic Press, 1970."},{"issue":"5","key":"11_CR10","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0166-5316(00)00053-5","volume":"44","author":"A. Heindl","year":"2001","unstructured":"A. Heindl and R. German. Performance modeling of IEEE 802.11 wireless LANs with stochastic Petri nets. Performance Evaluation, 44:139\u2013164, 2001.","journal-title":"Performance Evaluation"},{"key":"11_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-60630-0_3","volume-title":"Proc. TACAS\u201995","author":"T. Henzinger","year":"1995","unstructured":"T. Henzinger, P.-H. Ho, and H. Wong-Toi. A user guide to HyTech. In Proc. TACAS\u201995, volume 1019 of LNCS, pages 41\u201371. Springer, 1995."},{"key":"11_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-45352-0_4","volume-title":"Proc. FTRTFT 2000","author":"H. Jensen","year":"2000","unstructured":"H. Jensen, K. Larsen, and A. Skou. Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction. In Proc. FTRTFT 2000, volume 1926 of LNCS, pages 19\u201330. Springer, 2000."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"J. G. Kemeny, J. L. Snell, and A. W. Knapp. Denumerable Markov Chains. Graduate Texts in Mathematics. Springer, 2nd edition, 1976.","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"11_CR15","unstructured":"A. Koepsel, J.-P. Ebert, and A. Wolisz. A performance comparison of point and distributed coordination function of an IEEE 802.11 WLAN in the presence of real-time requirements. In Proc. MoMuC 2000, 2000."},{"key":"11_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Proc. TACAS 2002","author":"M. Kwiatkowska","year":"2002","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with Prism: A hybrid approach. In Proc. TACAS 2002, volume 2280 of LNCS, pages 52\u201366. Springer, 2002."},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 286, 2002. To appear.","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"11_CR18","unstructured":"M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Submitted. Extended abstract appears in Proc. Int. Workshop on Application of Formal Methods to IEEE 1394 Standard, 2001."},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. Technical Report CSR-02-05, School of Computer Science, University of Birmingham, 2002.","DOI":"10.1007\/3-540-45605-8_11"},{"issue":"1+2","key":"11_CR20","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1+2):134\u2013152, 1997.","journal-title":"Software Tools for Technology Transfer"},{"key":"11_CR21","unstructured":"Prism web page. http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/ ."},{"key":"11_CR22","unstructured":"R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995."},{"issue":"2","key":"11_CR23","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"R. Segala and N. A. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250\u2013273, 1995.","journal-title":"Nordic Journal of Computing"},{"issue":"4","key":"11_CR24","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s100090100059","volume":"3","author":"D. Simons","year":"2001","unstructured":"D. Simons and M. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Software Tools for Technology Transfer, 3(4):469\u2013485, 2001.","journal-title":"Software Tools for Technology Transfer"},{"key":"11_CR25","unstructured":"S. Tripakis. The formal analysis of timed systems in practice. PhD thesis, Universit\u00e9 Joseph Fourier, 1998."},{"key":"11_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/3-540-49059-0_5","volume-title":"Proc. TACAS\u201999","author":"S. Tripakis","year":"1999","unstructured":"S. Tripakis. Timed diagnostics for reachability properties. In Proc. TACAS\u201999, volume 1579 of LNCS, pages 59\u201373. Springer, 1999."},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. FOCS\u201985, pages 327\u2013338. IEEE Computer Society Press, 1985.","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Process Algebra and Probabilistic Methods: Performance Modeling and Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45605-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,21]],"date-time":"2020-04-21T21:26:33Z","timestamp":1587504393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45605-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439134","9783540456056"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-45605-8_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}