{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:13:30Z","timestamp":1725747210110},"publisher-location":"Berlin, Heidelberg","reference-count":51,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397172"},{"type":"electronic","value":"9783642397189"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39718-9_3","type":"book-chapter","created":{"date-parts":[[2013,8,30]],"date-time":"2013-08-30T03:01:54Z","timestamp":1377831714000},"page":"42-58","source":"Crossref","is-referenced-by-count":5,"title":["Advances in Quantitative Verification for Ubiquitous Computing"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"PRISM, \n                  \n                    http:\/\/www.prismmodelchecker.org"},{"key":"3_CR2","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering\u00a029, 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"3_CR4","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.cose.2011.02.001","volume":"30","author":"S. Basagiannis","year":"2011","unstructured":"Basagiannis, S., Petridou, S.G., Alexiou, N., Papadimitriou, G.I., Katsaros, P.: Quantitative analysis of a certified e-mail protocol in mobile environments: A probabilistic model checking approach. Computers & Security\u00a030(4), 257\u2013272 (2011)","journal-title":"Computers & Security"},{"issue":"10","key":"3_CR5","doi-asserted-by":"publisher","first-page":"1693","DOI":"10.1016\/j.jss.2011.04.054","volume":"84","author":"D. Bucur","year":"2011","unstructured":"Bucur, D., Kwiatkowska, M.: On software verification for TinyOS. Journal of Software and Systems\u00a084(10), 1693\u20131707 (2011)","journal-title":"Journal of Software and Systems"},{"issue":"9","key":"3_CR6","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/2330667.2330686","volume":"55","author":"R. Calinescu","year":"2012","unstructured":"Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Communications of the ACM\u00a055(9), 69\u201377 (2012)","journal-title":"Communications of the ACM"},{"issue":"3","key":"3_CR7","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1109\/TSE.2010.92","volume":"37","author":"R. Calinescu","year":"2011","unstructured":"Calinescu, R., Grunske, L., Kwiatkowska, M., Mirandola, R., Tamburrelli, G.: Dynamic QoS management and optimisation in service-based systems. IEEE Transactions on Software Engineering\u00a037(3), 387\u2013409 (2011)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-39176-7_9","volume-title":"Model Checking Software","author":"S. Chaki","year":"2013","unstructured":"Chaki, S., Giampapa, J.A.: Probabilistic verification of coordinated multi-robot missions. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol.\u00a07976, pp. 135\u2013153. Springer, Heidelberg (2013)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers. In: Proc. 33rd Real-Time Systems Symposium (RTSS). IEEE Computer Society (2012)","DOI":"10.1109\/RTSS.2012.77"},{"key":"3_CR10","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. In: Formal Methods in System Design (to appear, 2013)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-36742-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: A model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 185\u2013191. Springer, Heidelberg (2013)"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Proc. MFCS 2013. LNCS, Springer (2013)","DOI":"10.1007\/978-3-642-40313-2_25"},{"key":"3_CR13","unstructured":"Chen, T., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: Synthesis for multi-objective stochastic games: An application to autonomous urban driving. In: Proc. QEST 2013 (to appear, 2013)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M.Z., Mereacre, A.: A Simulink hybrid heart model for quantitative verification of cardiac pacemakers. In: Proc. HSCC 2013, pp. 131\u2013136. ACM (2013)","DOI":"10.1145\/2461328.2461351"},{"key":"3_CR15","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M.Z., Mereacre, A.: Symbolic model checking for probabilistic timed automata. In: ACM Transactions on Computational Logic (to appear, 2013)"},{"key":"3_CR16","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: Proc. TASE 2013. IEEE (to appear, 2013)"},{"issue":"6","key":"3_CR17","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M. Duflot","year":"2006","unstructured":"Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of Bluetooth device discovery. Int. Journal on Software Tools for Technology Transfer\u00a08(6), 621\u2013632 (2006)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Egami, K., Matsumoto, S., Nakamura, M.: Ubiquitous cloud: Managing service resources for adaptive ubiquitous computing. In: PerCom Workshops, pp. 123\u2013128 (2011)","DOI":"10.1109\/PERCOMW.2011.5766853"},{"issue":"4","key":"3_CR19","first-page":"1","volume":"4","author":"K. Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Logical Methods in Computer Science\u00a04(4), 1\u201321 (2008)","journal-title":"Logical Methods in Computer Science"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Feng, L., Kwiatkowska, M., Parker, D.: Compositional verification of probabilistic systems using learning. In: Proc. QEST 2010, pp. 133\u2013142. IEEE CS Press (2010)","DOI":"10.1109\/QEST.2010.24"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-19811-3_2","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Feng","year":"2011","unstructured":"Feng, L., Kwiatkowska, M., Parker, D.: Automated learning of probabilistic assumptions for compositional reasoning. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol.\u00a06603, pp. 2\u201317. Springer, Heidelberg (2011)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: Taylor, R.N., Gall, H., Medvidovic, N. (eds.) Proc. ICSE, pp. 341\u2013350. ACM (2011)","DOI":"10.1145\/1985793.1985840"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol.\u00a06659, pp. 53\u2013113. Springer, Heidelberg (2011)"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 112\u2013127. Springer, Heidelberg (2011)"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V. Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 317\u2013332. Springer, Heidelberg (2012)"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-642-35632-2_30","volume-title":"Runtime Verification","author":"V. Forejt","year":"2013","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D., Qu, H., Ujma, M.: Incremental runtime verification of probabilistic systems. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol.\u00a07687, pp. 314\u2013319. Springer, Heidelberg (2013)"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Fruth, M.: Probabilistic model checking of contention resolution in the IEEE 802.15.4 low-rate wireless personal area network protocol. In: Proc. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISOLA 2006 (2006)","DOI":"10.1109\/ISoLA.2006.34"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Gallina, L., Han, T., Kwiatkowska, M., Marin, A., Rossi, S., Spano, A.: Automatic energy-aware performance analysis of mobile ad-hoc networks. In: Proc. IFIP Wireless Days, WD 2012 (2012)","DOI":"10.1109\/WD.2012.6402864"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: Proc. NASA Formal Methods, pp. 146\u2013161 (2011)","DOI":"10.1007\/978-3-642-20398-5_12"},{"key":"3_CR30","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06, 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer (1976)","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Where\u2019s waldo? sensor-based temporal logic motion planning. In: Proc. ICRA 2007, pp. 3116\u20133121. IEEE (2007)","DOI":"10.1109\/ROBOT.2007.363946"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.: Quantitative verification: Models, techniques and tools. In: Proc. ESEC\/FSE 2007, pp. 449\u2013458. ACM Press (September 2007)","DOI":"10.1145\/1287624.1287688"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol.\u00a04486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M. Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol.\u00a05813, pp. 212\u2013227. Springer, Heidelberg (2009)"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-12002-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Kwiatkowska","year":"2010","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 23\u201337. Springer, Heidelberg (2010)"},{"key":"3_CR38","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design\u00a029, 33\u201378 (2006)","journal-title":"Formal Methods in System Design"},{"key":"3_CR39","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science\u00a0282, 101\u2013150 (2002)","journal-title":"Theoretical Computer Science"},{"issue":"7","key":"3_CR40","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., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Information and Computation\u00a0205(7), 1027\u20131077 (2007)","journal-title":"Information and Computation"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Parker, D., Simaitis, A.: Strategic analysis of trust models for user-centric networks. In: Proc. SR 2013. EPTCS, vol.\u00a0112, pp. 53\u201360 (2013)","DOI":"10.4204\/EPTCS.112.10"},{"key":"#cr-split#-3_CR42.1","unstructured":"Kwiatkowska, M., Rodden, T., Sassone, V. (eds.): From computers to ubiquitous computing, by 2020, vol.\u00a0366 (1881)"},{"key":"#cr-split#-3_CR42.2","unstructured":"Philosophical Transactions of the Royal Society A (2008)"},{"issue":"2","key":"3_CR43","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1109\/TRO.2011.2172150","volume":"28","author":"M. Lahijanian","year":"2012","unstructured":"Lahijanian, M., Andersson, S.B., Belta, C.: Temporal logic motion planning and control with probabilistic satisfaction guarantees. IEEE Transactions on Robotics\u00a028(2), 396\u2013409 (2012)","journal-title":"IEEE Transactions on Robotics"},{"issue":"72","key":"3_CR44","doi-asserted-by":"publisher","first-page":"1470","DOI":"10.1098\/rsif.2011.0800","volume":"9","author":"M. Lakin","year":"2012","unstructured":"Lakin, M., Parker, D., Cardelli, L., Kwiatkowska, M., Phillips, A.: Design and analysis of DNA strand displacement devices using probabilistic model checking. Journal of the Royal Society Interface\u00a09(72), 1470\u20131485 (2012)","journal-title":"Journal of the Royal Society Interface"},{"issue":"2","key":"3_CR45","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/s00165-005-0062-0","volume":"17","author":"G. Norman","year":"2005","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., Gupta, R.: Using probabilistic model checking for dynamic power management. Formal Aspects of Computing\u00a017(2), 160\u2013176 (2005)","journal-title":"Formal Aspects of Computing"},{"key":"3_CR46","doi-asserted-by":"crossref","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods in System Design (2012) (to appear)","DOI":"10.1007\/s10703-012-0177-x"},{"key":"3_CR47","doi-asserted-by":"crossref","unstructured":"Paparrizos, I.K., Basagiannis, S., Petridou, S.G.: Quantitative analysis for authentication of low-cost RFID tags. In: Proc. LCN, pp. 295\u2013298 (2011)","DOI":"10.1109\/LCN.2011.6115307"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Susu, A.E., Acquaviva, A., Atienza, D., Micheli, G.D.: Stochastic modeling and analysis for environmentally powered wireless sensor nodes. In: Proc. WiOpt, pp. 125\u2013134. IEEE (2008)","DOI":"10.4108\/ICST.WIOPT2008.3179"},{"issue":"3","key":"3_CR49","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/329124.329126","volume":"3","author":"M. Weiser","year":"1999","unstructured":"Weiser, M.: The computer for the 21st century. SIGMOBILE Mob. Comput. Commun. Rev.\u00a03(3), 3\u201311 (1999)","journal-title":"SIGMOBILE Mob. Comput. Commun. Rev."},{"issue":"11","key":"3_CR50","doi-asserted-by":"publisher","first-page":"2817","DOI":"10.1109\/TAC.2012.2195811","volume":"57","author":"T. Wongpiromsarn","year":"2012","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning. IEEE Trans. Automat. Contr.\u00a057(11), 2817\u20132830 (2012)","journal-title":"IEEE Trans. Automat. Contr."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2013"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39718-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:55:10Z","timestamp":1558317310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39718-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397172","9783642397189"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39718-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}