{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T15:44:42Z","timestamp":1750347882143,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T00:00:00Z","timestamp":1503273600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,8,21]]},"DOI":"10.1145\/3106237.3106301","type":"proceedings-article","created":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T19:36:18Z","timestamp":1501702578000},"page":"454-464","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Probabilistic model checking of perturbed MDPs with applications to cloud computing"],"prefix":"10.1145","author":[{"given":"Yamilet R. Serrano","family":"Llerena","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guoxin","family":"Su","sequence":"additional","affiliation":[{"name":"University of Wollongong, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David S.","family":"Rosenblum","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,8,21]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Husain Aljazzar and Stefan Leue. 2009.  Husain Aljazzar and Stefan Leue. 2009."},{"key":"e_1_3_2_1_2_1","unstructured":"Generation of Counterexamples for Model Checking of Markov Decision Processes. In QEST. 197\u2013206.  Generation of Counterexamples for Model Checking of Markov Decision Processes. In QEST. 197\u2013206."},{"key":"e_1_3_2_1_3_1","unstructured":"Christel Baier and Joost-Pieter Katoen. 2007.  Christel Baier and Joost-Pieter Katoen. 2007."},{"key":"e_1_3_2_1_4_1","unstructured":"Principles of Model Checking. The MIT Press.  Principles of Model Checking. The MIT Press."},{"key":"e_1_3_2_1_5_1","volume-title":"International Conference on High Probabilistic Model Checking of Perturbed MDPs with Applications to Cloud Computing ESEC\/FSE\u201917, September 4\u20138","author":"Baldi Marco","year":"2017","unstructured":"Marco Baldi , Alessandro Cucchiarelli , Linda Senigagliesi , Luca Spalazzi , and Francesco Spegni . 2016. Parametric and Probabilistic Model Checking of Confidentiality in Data Dispersal Algorithms . In International Conference on High Probabilistic Model Checking of Perturbed MDPs with Applications to Cloud Computing ESEC\/FSE\u201917, September 4\u20138 , 2017 , Paderborn, Germany Performance Computing & Simulation, HPCS 2016, Innsbruck, Austria , July 18-22, 2016. 476\u2013483. Marco Baldi, Alessandro Cucchiarelli, Linda Senigagliesi, Luca Spalazzi, and Francesco Spegni. 2016. Parametric and Probabilistic Model Checking of Confidentiality in Data Dispersal Algorithms. In International Conference on High Probabilistic Model Checking of Perturbed MDPs with Applications to Cloud Computing ESEC\/FSE\u201917, September 4\u20138, 2017, Paderborn, Germany Performance Computing & Simulation, HPCS 2016, Innsbruck, Austria, July 18-22, 2016. 476\u2013483."},{"key":"e_1_3_2_1_6_1","unstructured":"Radu Calinescu Kenneth Johnson and Yasmin Rafiq. 2013.  Radu Calinescu Kenneth Johnson and Yasmin Rafiq. 2013."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693145"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.22"},{"key":"e_1_3_2_1_9_1","unstructured":"Taolue Chen Yuan Feng David S. Rosenblum and Guoxin Su. 2014.  Taolue Chen Yuan Feng David S. Rosenblum and Guoxin Su. 2014."},{"volume-title":"Analysis in Verification of Discrete-Time Markov Chains. In CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings. 218\u2013233","author":"Perturbation","key":"e_1_3_2_1_10_1","unstructured":"Perturbation Analysis in Verification of Discrete-Time Markov Chains. In CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings. 218\u2013233 . 978- 3- 662- 44584- 6_16 Perturbation Analysis in Verification of Discrete-Time Markov Chains. In CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings. 218\u2013233. 978- 3- 662- 44584- 6_16"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2008.45"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"e_1_3_2_1_13_1","volume-title":"Multi-Objective Model Checking of Markov Decision Processes. Logical Methods in Computer Science 4, 4","author":"Etessami Kousha","year":"2008","unstructured":"Kousha Etessami , Marta Z. Kwiatkowska , Moshe Y. Vardi , and Mihalis Yannakakis . 2008. Multi-Objective Model Checking of Markov Decision Processes. Logical Methods in Computer Science 4, 4 ( 2008 ). Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. 2008. Multi-Objective Model Checking of Markov Decision Processes. Logical Methods in Computer Science 4, 4 (2008)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Antonio Filieri and Giordano Tamburrelli. 2013. Probabilistic Verification at Runtime for Self-Adaptive Systems. In Assurances for Self-Adaptive Systems - Principles Models and Techniques. 30\u201359.  Antonio Filieri and Giordano Tamburrelli. 2013. Probabilistic Verification at Runtime for Self-Adaptive Systems. In Assurances for Self-Adaptive Systems - Principles Models and Techniques. 30\u201359.","DOI":"10.1007\/978-3-642-36249-1_2"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985840"},{"key":"e_1_3_2_1_16_1","unstructured":"Vojtech Forejt Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011.  Vojtech Forejt Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011."},{"key":"e_1_3_2_1_17_1","unstructured":"Automated Verification Techniques for Probabilistic Systems. In SFM. 53\u2013113.  Automated Verification Techniques for Probabilistic Systems. In SFM. 53\u2013113."},{"key":"e_1_3_2_1_18_1","unstructured":"Lin Gui Jun Sun Songzheng Song Yang Liu and Jin Song Dong. 2014.  Lin Gui Jun Sun Songzheng Song Yang Liu and Jin Song Dong. 2014."},{"volume-title":"ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings. 171\u2013186","author":"Reachability Based Improved","key":"e_1_3_2_1_19_1","unstructured":"SCC Based Improved Reachability Analysis for Markov Decision Processes . In Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods , ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings. 171\u2013186 . SCCBased Improved Reachability Analysis for Markov Decision Processes. In Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings. 171\u2013186."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Ernst Moritz Hahn Tingting Han and Lijun Zhang. 2011. Synthesis for PCTL in Parametric Markov Decision Processes. In NASA Formal Methods. 146\u2013161.   Ernst Moritz Hahn Tingting Han and Lijun Zhang. 2011. Synthesis for PCTL in Parametric Markov Decision Processes. In NASA Formal Methods. 146\u2013161.","DOI":"10.1007\/978-3-642-20398-5_12"},{"key":"e_1_3_2_1_21_1","unstructured":"Ernst Moritz Hahn Holger Hermanns and Lijun Zhang. 2009.  Ernst Moritz Hahn Holger Hermanns and Lijun Zhang. 2009."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02652-2_10"},{"key":"e_1_3_2_1_23_1","unstructured":"John Kemeny James Snell and Anthony Knapp. 1976.  John Kemeny James Snell and Anthony Knapp. 1976."},{"key":"e_1_3_2_1_24_1","unstructured":"Denumerable Markov Chains (2 ed.). Vol. 40. Springer-Verlag New York.  Denumerable Markov Chains (2 ed.). Vol. 40. Springer-Verlag New York."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Shinji Kikuchi and Yasuhide Matsumoto. 2011.  Shinji Kikuchi and Yasuhide Matsumoto. 2011.","DOI":"10.1002\/ejoc.201100517"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CLOUD.2011.48"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICC.2014.6883509"},{"key":"e_1_3_2_1_28_1","unstructured":"1350\u20131354.  1350\u20131354."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1059816.1059820"},{"key":"e_1_3_2_1_30_1","unstructured":"Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011.  Marta Z. Kwiatkowska Gethin Norman and David Parker. 2011."},{"key":"e_1_3_2_1_31_1","unstructured":"PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV. 585\u2013591.  PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV. 585\u2013591."},{"key":"e_1_3_2_1_32_1","unstructured":"Marta Z. Kwiatkowska David Parker and Hongyang Qu. 2011.  Marta Z. Kwiatkowska David Parker and Hongyang Qu. 2011."},{"key":"e_1_3_2_1_33_1","unstructured":"Incremental Quantitative Verification for Markov Decision Processes. In DSN. 359\u2013370.  Incremental Quantitative Verification for Markov Decision Processes. In DSN. 359\u2013370."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0015-2"},{"key":"e_1_3_2_1_35_1","unstructured":"Athanasios Naskos Emmanouela Stachtiari Anastasios Gounaris Panagiotis Katsaros Dimitrios Tsoumakos Ioannis Konstantinou and Spyros Sioutas. 2014.  Athanasios Naskos Emmanouela Stachtiari Anastasios Gounaris Panagiotis Katsaros Dimitrios Tsoumakos Ioannis Konstantinou and Spyros Sioutas. 2014."},{"key":"e_1_3_2_1_36_1","volume-title":"CoRR abs\/1405.4699","author":"Probabilistic Model Checking Cloud Elasticity","year":"2014","unstructured":"Cloud Elasticity using Probabilistic Model Checking . CoRR abs\/1405.4699 ( 2014 ). http:\/\/arxiv.org\/abs\/1405.4699 Cloud Elasticity using Probabilistic Model Checking. CoRR abs\/1405.4699 (2014). http:\/\/arxiv.org\/abs\/1405.4699"},{"key":"e_1_3_2_1_37_1","unstructured":"Athanasios Naskos Emmanouela Stachtiari Anastasios Gounaris Panagiotis Katsaros Dimitrios Tsoumakos Ioannis Konstantinou and Spyros Sioutas. 2015.  Athanasios Naskos Emmanouela Stachtiari Anastasios Gounaris Panagiotis Katsaros Dimitrios Tsoumakos Ioannis Konstantinou and Spyros Sioutas. 2015."},{"key":"e_1_3_2_1_38_1","volume-title":"Horizontal Scaling Based on Probabilistic Model Checking. In 15th IEEE\/ACM International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2015","author":"Dependable","year":"2015","unstructured":"Dependable Horizontal Scaling Based on Probabilistic Model Checking. In 15th IEEE\/ACM International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2015 , Shenzhen, China , May 4-7, 2015 . 31\u201340. Dependable Horizontal Scaling Based on Probabilistic Model Checking. In 15th IEEE\/ACM International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2015, Shenzhen, China, May 4-7, 2015. 31\u201340."},{"key":"e_1_3_2_1_39_1","unstructured":"91  91"},{"key":"e_1_3_2_1_40_1","volume-title":"RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings. 275\u2013280","author":"Naskos Athanasios","year":"2015","unstructured":"Athanasios Naskos , Emmanouela Stachtiari , Panagiotis Katsaros , and Anastasios Gounaris . 2015 . Probabilistic Model Checking at Runtime for the Provisioning of Cloud Resources. In Runtime Verification - 6th International Conference , RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings. 275\u2013280 . 1007\/978- 3- 319- 23820- 3_18 Athanasios Naskos, Emmanouela Stachtiari, Panagiotis Katsaros, and Anastasios Gounaris. 2015. Probabilistic Model Checking at Runtime for the Provisioning of Cloud Resources. In Runtime Verification - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings. 275\u2013280. 1007\/978- 3- 319- 23820- 3_18"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.9790\/0661\/0811422"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)90047-7"},{"volume-title":"CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. 527\u2013542","author":"Puggelli Alberto","key":"e_1_3_2_1_43_1","unstructured":"Alberto Puggelli , Wenchao Li , Alberto L. Sangiovanni-Vincentelli , and Sanjit A. Seshia . 2013. Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In Computer Aided Verification - 25th International Conference , CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. 527\u2013542 . 3- 642- 39799- 8_35 Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia. 2013. Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. 527\u2013542. 3- 642- 39799- 8_35"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_26"},{"key":"e_1_3_2_1_45_1","volume-title":"Rosenblum","author":"Su Guoxin","year":"2017","unstructured":"Guoxin Su , Taolue Chen , Yuan Feng , and David S . Rosenblum . 2017 . Guoxin Su, Taolue Chen, Yuan Feng, and David S. Rosenblum. 2017."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.51"},{"key":"e_1_3_2_1_47_1","volume-title":"Rosenblum","author":"Su Guoxin","year":"2013","unstructured":"Guoxin Su and David S . Rosenblum . 2013 . Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems. In ICFEM. 297\u2013312. Guoxin Su and David S. Rosenblum. 2013. Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems. In ICFEM. 297\u2013312."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568256"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/MNET.2013.6616110"},{"key":"e_1_3_2_1_50_1","first-page":"1","article-title":"Follow-Me Cloud: When Cloud Services Follow Mobile Users","volume":"99","author":"Taleb Tarik","year":"2016","unstructured":"Tarik Taleb , Adlen Ksentini , and Pantelis Frangoudis . 2016 . Follow-Me Cloud: When Cloud Services Follow Mobile Users . IEEE Transactions on Cloud Computing PP , 99 (2016), 1 \u2013 1 . Tarik Taleb, Adlen Ksentini, and Pantelis Frangoudis. 2016. Follow-Me Cloud: When Cloud Services Follow Mobile Users. IEEE Transactions on Cloud Computing PP, 99 (2016), 1\u20131.","journal-title":"IEEE Transactions on Cloud Computing PP"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/MILCOM.2014.145"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"crossref","unstructured":"Mahmood Zaigham. 2014.  Mahmood Zaigham. 2014.","DOI":"10.1155\/2014\/564136"},{"volume-title":"Challenges, Limitation and R &amp","author":"Computing Cloud","key":"e_1_3_2_1_53_1","unstructured":"Cloud Computing : Challenges, Limitation and R &amp ; D. Springer . Cloud Computing: Challenges, Limitation and R & D. Springer."}],"event":{"name":"ESEC\/FSE'17: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Paderborn Germany","acronym":"ESEC\/FSE'17"},"container-title":["Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106301","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3106237.3106301","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:37Z","timestamp":1750217437000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106301"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,21]]},"references-count":53,"alternative-id":["10.1145\/3106237.3106301","10.1145\/3106237"],"URL":"https:\/\/doi.org\/10.1145\/3106237.3106301","relation":{},"subject":[],"published":{"date-parts":[[2017,8,21]]},"assertion":[{"value":"2017-08-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}