{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,20]],"date-time":"2024-09-20T04:25:35Z","timestamp":1726806335019},"reference-count":110,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,3,2]],"date-time":"2022-03-02T00:00:00Z","timestamp":1646179200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,3,2]],"date-time":"2022-03-02T00:00:00Z","timestamp":1646179200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Singapore-UK Cyber Security of EPSRC","award":["EP\/N020170\/1"],"award-info":[{"award-number":["EP\/N020170\/1"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2022,5]]},"DOI":"10.1007\/s10515-022-00327-z","type":"journal-article","created":{"date-parts":[[2022,3,2]],"date-time":"2022-03-02T07:02:51Z","timestamp":1646204571000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A three-valued model abstraction framework for PCTL* stochastic model checking"],"prefix":"10.1007","volume":"29","author":[{"given":"Yang","family":"Liu","sequence":"first","affiliation":[]},{"given":"Yan","family":"Ma","sequence":"additional","affiliation":[]},{"given":"Yongsheng","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,2]]},"reference":[{"key":"327_CR1","doi-asserted-by":"crossref","unstructured":"Abraham, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.P., Wimmer, R.: Counterexample generation for discrete-time Markov models: an introductory survey. In: Proceedings of the 14th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Executable Software Models (SFM-14:ESM), Springer, vol. 8483 of LNCS, pp. 65\u2013121 (2014)","DOI":"10.1007\/978-3-319-07317-0_3"},{"issue":"8","key":"327_CR2","doi-asserted-by":"publisher","first-page":"1429","DOI":"10.1109\/TMM.2008.2010417","volume":"10","author":"M Albanese","year":"2008","unstructured":"Albanese, M., Chellappa, R., Moscato, V., Picariello, A., et al.: A Constrained probabilistic petri net framework for human activity detection in video. IEEE Trans. Multimedia 10(8), 1429\u20131443 (2008)","journal-title":"IEEE Trans. Multimedia"},{"key":"327_CR3","doi-asserted-by":"crossref","unstructured":"Alfaro, L., Roy, P.: Magnifying-lens abstraction for Markov decision processes. In: Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). Springer, vol. 4590 of LNCS, pp. 325\u2013338 (2007)","DOI":"10.1007\/978-3-540-73368-3_38"},{"key":"327_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"327_CR5","doi-asserted-by":"crossref","unstructured":"Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Proceedings of the 9th International Conference on Computer Aided Verification. Springer-Verlag, Berlin, Heidelberg, pp. 119\u2013130 (1997)","DOI":"10.1007\/3-540-63166-6_14"},{"key":"327_CR6","doi-asserted-by":"crossref","unstructured":"Baier, C., Groser, M., Ciesinski, F.: Partial order reduction for probabilistic systems. In: Proceedings of the 1st International Conference on Quantitative Evaluation of Systems. IEEE Computer Society Press, Washington, pp. 230\u2013239 (2004)","DOI":"10.1109\/QEST.2004.1348037"},{"issue":"2","key":"327_CR7","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.ic.2005.03.001","volume":"200","author":"C Baier","year":"2005","unstructured":"Baier, C., Katoen, J.P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149\u2013214 (2005a)","journal-title":"Inf. Comput."},{"issue":"2","key":"327_CR8","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.entcs.2005.10.034","volume":"153","author":"C Baier","year":"2005","unstructured":"Baier, C., D\u2019Argenio, P., Groesser, M.: Partial order reduction for probabilistic branching time. Electron. Notes Theor. Comput. Sci. 153(2), 97\u2013116 (2005b)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"327_CR9","doi-asserted-by":"crossref","unstructured":"Belardinelli, F., Lomuscio, A., Malvone, V.: An abstraction-based method for verifying strategic properties in multi-agent systems with imperfect information. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 33, no. 01, pp. 6030\u20136037 (2019)","DOI":"10.1609\/aaai.v33i01.33016030"},{"key":"327_CR10","unstructured":"Bernemann, R., Cabrera, B., Heckel, R., K\u00f6nig, B.: Uncertainty reasoning for probabilistic petri nets via Bayesian networks, pp. 1\u201326 (2020) available: https:\/\/arxiv.org\/abs\/2009.14817"},{"issue":"1","key":"327_CR11","doi-asserted-by":"publisher","first-page":"59","DOI":"10.2307\/3215235","volume":"31","author":"P Buchholz","year":"1994","unstructured":"Buchholz, P.: Exact and ordinary lumpability infinite Markov chains. J. Appl. Probab. 31(1), 59\u201375 (1994)","journal-title":"J. Appl. Probab."},{"issue":"1","key":"327_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1838552.1838553","volume":"12","author":"R Chadha","year":"2010","unstructured":"Chadha, R., Viswanathan, M.: A counterexample guided abstraction-refinement framework for Markov decision processes. ACM Trans. Comput. Logic 12(1), 1\u201349 (2010)","journal-title":"ACM Trans. Comput. Logic"},{"key":"327_CR13","doi-asserted-by":"publisher","first-page":"805","DOI":"10.1007\/s11276-017-1593-z","volume":"25","author":"T Chi","year":"2019","unstructured":"Chi, T., Chen, M.: A frequency hopping method for spatial RFID\/WiFi\/Bluetooth scheduling in agricultural IoT. Wirel. Netw. 25, 805\u2013817 (2019)","journal-title":"Wirel. Netw."},{"key":"327_CR14","doi-asserted-by":"crossref","unstructured":"Christian, D., Katoen, J.P., Parker, D.: SMT-based bisimulation minimization of Markov models. In: Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer-Verlag, Berlin, Heidelberg, pp. 28\u201347 (2013)","DOI":"10.1007\/978-3-642-35873-9_5"},{"key":"327_CR15","unstructured":"Christopher P.: Probabilistic symmetry reduction [Ph.D. Thesis]. University of Glasgow, Scotland (2012)"},{"key":"327_CR16","unstructured":"Ciesinski, F.: High-Level modelling and efficient analysis of randomized protocols [Ph.D. Thesis]. Dresden University of Technology, Dresden (2011)"},{"issue":"5","key":"327_CR17","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994a)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"5","key":"327_CR18","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994b)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1\u20132","key":"327_CR19","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1\u20132), 77\u2013104 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"327_CR20","doi-asserted-by":"crossref","unstructured":"Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Proceedings of Conference on Computer-Aided Verification, Copenhagen, Denmark (2002)","DOI":"10.1007\/3-540-45657-0_20"},{"issue":"5","key":"327_CR21","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"issue":"11","key":"327_CR22","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"EM Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74\u201384 (2009)","journal-title":"Commun. ACM"},{"key":"327_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R., et al.: Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"327_CR24","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P.R., Niebert, P.: Partial order reduction on concurrent probabilistic programs. In: Proceedings of the 1st International Conference on Quantitative Evaluation of Systems. IEEE Computer Society Press, Washington, pp. 240\u2013249 (2004)","DOI":"10.1109\/QEST.2004.1348038"},{"key":"327_CR25","volume-title":"Handbook of Model Checking","author":"D Dams","year":"2018","unstructured":"Dams, D., Grumberg, O.: Abstraction and abstraction refinement. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"327_CR26","unstructured":"Dehnert C.: The probabilistic model checker storm: symbolic methods for probabilistic model checking. PhD Thesis at RWTH Aachen University (2018)"},{"key":"327_CR27","doi-asserted-by":"crossref","unstructured":"Derisavi, S.: A symbolic algorithm for optimal Markov chain lumping. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, pp. 139\u2013154 (2007)","DOI":"10.1007\/978-3-540-71209-1_13"},{"key":"327_CR28","doi-asserted-by":"crossref","unstructured":"Dey, D., Dansana, J., Behura, A.: A survey of datalink layer protocol for IoT. In: Smys, S., Senjyu, T., Lafata, P. (eds) Second International Conference on Computer Networks and Communication Technologies, pp. 459\u2013466 (2020)","DOI":"10.1007\/978-3-030-37051-0_52"},{"key":"327_CR29","doi-asserted-by":"crossref","unstructured":"Didier, F., Henzinger, T., Mateescu, M., Wolf, V.: Sabre: a tool for stochastic analysis of biochemical reaction networks. In: Proceedings of the 7th International Conference on the Quantitative Evaluation of Systems (QEST'10), pp. 193\u2013194. IEEE CS Press (2010)","DOI":"10.1109\/QEST.2010.33"},{"key":"327_CR30","doi-asserted-by":"crossref","unstructured":"Donaldson, A., Miller, A.: Symmetry reduction for probabilistic model checking using generic representatives. In: Proceedings of the 4th International Conference on Automated Technology for Verification and Analysis. Springer-Verlag, Berlin, Heidelberg, pp. 9\u201323 (2006)","DOI":"10.1007\/11901914_4"},{"key":"327_CR31","doi-asserted-by":"crossref","unstructured":"Donaldson, A., Miller, A., Parker, D.: Language-level symmetry reduction for probabilistic model checking. In: Proceedings of the 6th International Conference on Quantitative Evaluation of Systems. IEEE Computer Science Press, Washington, pp. 289\u2013298 (2009)","DOI":"10.1109\/QEST.2009.21"},{"issue":"5","key":"327_CR32","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1109\/MS.2019.2921037","volume":"36","author":"C Ebert","year":"2019","unstructured":"Ebert, C., Weyrich, M.: Validation of autonomous systems. IEEE Softw. 36(5), 15\u201323 (2019)","journal-title":"IEEE Softw."},{"key":"327_CR33","doi-asserted-by":"publisher","first-page":"46646","DOI":"10.1109\/ACCESS.2019.2909356","volume":"7","author":"S Ejaz","year":"2019","unstructured":"Ejaz, S., Iqbal, Z., Azmat Shah, P., Bukhari, B.H., Ali, A., Aadil, F.: Traffic load balancing using software defined networking (SDN) controller as virtualized network function. IEEE Access 7, 46646\u201346658 (2019)","journal-title":"IEEE Access"},{"key":"327_CR34","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Wahl, T.: On combining symmetry reduction and symbolic representation for efficient model checking. In: Proceedings of the 12th IFIP WG Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Springer-Verlag, Berlin, Heidelberg, pp. 216\u2013230 (2003)","DOI":"10.1007\/978-3-540-39724-3_20"},{"issue":"1\u20132","key":"327_CR35","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"EA Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.: Symmetry and model checking. Form. Methods Syst. Des. 9(1\u20132), 105\u2013131 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"327_CR36","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1016\/j.entcs.2005.03.019","volume":"130","author":"EA Emerson","year":"2005","unstructured":"Emerson, E.A., Wahl, T.: Efficient reduction techniques for systems with many components. Electron. Notes Theor. Comput. Sci. 130, 379\u2013399 (2005a)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"327_CR37","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, Berlin, Heidelberg, pp. 382\u2013396 (2005b)","DOI":"10.1007\/978-3-540-31980-1_25"},{"key":"327_CR38","unstructured":"Evangelidis A.: Verified control and estimation for cloud computing. Ph.D. thesis, School of Computer Science, University of Birmingham (2020)"},{"key":"327_CR39","doi-asserted-by":"crossref","unstructured":"Fecher, H., Leucker, M., Wolf, V.: Don\u2019t know in probabilistic systems. In: Proceedings of the 13th International Conference on Model Checking Software. Springer-Verlag, Berlin, Heidelberg, pp. 71\u201388 (2006)","DOI":"10.1007\/11691617_5"},{"key":"327_CR40","doi-asserted-by":"crossref","unstructured":"Fernandez-Diaz, A., Baier, C., Benac-Earle, C., Fredlund, L.A.: Static partial order reduction for probabilistic concurrent systems. In: Proceedings of the 9th International Conference on Quantitative Evaluation of Systems. IEEE Computer Science Press, Washington, pp. 104\u2013113 (2012)","DOI":"10.1109\/QEST.2012.22"},{"key":"327_CR41","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s00165-016-0356-4","volume":"28","author":"FLM Ferrer","year":"2016","unstructured":"Ferrer, F.L.M., Hashemi, V., Hermanns, H., Turrini, A.: Deciding probabilistic automata weak bisimulation: theory and practice. Form. Asp. Comput. 28, 109\u2013143 (2016)","journal-title":"Form. Asp. Comput."},{"key":"327_CR42","doi-asserted-by":"crossref","unstructured":"Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: Proceedings of the 33rd ACM\/IEEE International Conference on Software Engineering. Honolulu, HI, USA, pp. 341\u2013350 (2011)","DOI":"10.1145\/1985793.1985840"},{"key":"327_CR43","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Chiu, J., Margineantu, D.D., Osipychev, D., Seshia, S.A.: Formal analysis and redesign of a neural network-based aircraft taxiing system with VerifAI. In: 32nd International Conference on Computer Aided Verification (CAV), July (2020)","DOI":"10.1007\/978-3-030-53288-8_6"},{"key":"327_CR44","doi-asserted-by":"crossref","unstructured":"Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. In: Proceedings of the 3rd Israel Symposium on the Theory of Computing Systems. IEEE Computer Society Press, Washington, pp. 130\u2013139 (1995)","DOI":"10.1109\/ISTCS.1995.377038"},{"key":"327_CR45","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.J.: PASS: abstraction refinement for infinite probabilistic models. In: Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, Berlin, Heidelberg, pp. 353\u2013357 (2010)","DOI":"10.1007\/978-3-642-12002-2_30"},{"key":"327_CR46","doi-asserted-by":"crossref","unstructured":"Hansen, H., Wang, X.: Compositional analysis for weak stubborn sets. In: Proceedings of the International Conference on Application of Concurrency to System Design. IEEE Computer Science Press, Washington, pp. 36\u201343 (2011)","DOI":"10.1109\/ACSD.2011.25"},{"key":"327_CR47","doi-asserted-by":"crossref","unstructured":"Hansen, H., Kwiatkowska, M., Qu, H.: Partial order reduction for model checking Markov decision processes under unconditional fairness. In: Proceedings of the 8th International Conference on Quantitative Evaluation of SysTems. IEEE Computer Science Press, Washington, pp. 203\u2013212 (2011)","DOI":"10.1109\/QEST.2011.35"},{"key":"327_CR48","doi-asserted-by":"crossref","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.P.: Aiming low is harder: induction for lower bounds in probabilistic program verification. In: Proceedings of the ACM Programming Language, POPL, Article 37, vol. 4, pp. 1\u201328 (2020)","DOI":"10.1145\/3371105"},{"key":"327_CR49","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Junges, S., Katoen, J.P., Quatmann, T.: Multi-cost bounded reachability in MDPs. In: Proceedings of the of TACAS, vol 10805 of LNCS (2018)","DOI":"10.1007\/978-3-319-89963-3_19"},{"key":"327_CR50","doi-asserted-by":"publisher","DOI":"10.14279\/tuj.eceasst.66.895","author":"V Hashemi","year":"2013","unstructured":"Hashemi, V., Hermanns, H., Turrini, A.: On the efficiency of deciding probabilistic automata weak bisimulation. Electron. Commun. EASST (2013). https:\/\/doi.org\/10.14279\/tuj.eceasst.66.895","journal-title":"Electron. Commun. EASST"},{"issue":"1","key":"327_CR51","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TC.2009.105","volume":"59","author":"F He","year":"2010","unstructured":"He, F., Song, X., Hung, W.N.N., et al.: Integrating evolutionary computation with abstraction refinement for model checking. IEEE Trans. Comput. 59(1), 116\u2013126 (2010)","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"327_CR52","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/2907943","volume":"25","author":"F He","year":"2016","unstructured":"He, F., Gao, X., Wang, M., Wang, B.Y., Zhang, L.J.: Learning weighted assumptions for compositional verification of Markov decision processes. ACM Trans. Softw. Eng. Methodol. 25(3), 39 (2016)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"1","key":"327_CR53","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/S0167-6423(99)00019-2","volume":"36","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program. 36(1), 97\u2013127 (2000)","journal-title":"Sci. Comput. Program."},{"key":"327_CR54","unstructured":"Hermanns, H., Turrini, A.: Deciding probabilistic automata weak bisimulation in polynomial time. In: Proceedings of the 32nd International Conference on Foundations of Software Technology and Theoretical Computer Science. Saarbr\u00fccken\/Wadern: Dagstuhl Publishing, pp. 435\u2013447 (2012)"},{"key":"327_CR55","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Proceedings of 2008 the 20th International Conference on Computer Aided Verification. Springer-Verlag, Berlin, Heidelberg, pp. 162\u2013175 (2007)","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"327_CR56","doi-asserted-by":"publisher","first-page":"104431","DOI":"10.1016\/j.ic.2019.05.004","volume":"268","author":"M Huang","year":"2019","unstructured":"Huang, M., Fu, H., Katoen, J.P.: Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems. Inf. Comput. 268, 104431 (2019)","journal-title":"Inf. Comput."},{"issue":"3","key":"327_CR57","doi-asserted-by":"publisher","first-page":"211","DOI":"10.3233\/FI-1992-17304","volume":"17","author":"T Huynh","year":"1992","unstructured":"Huynh, T., Tian, L.: On some equivalence relations for probabilistic processes. Fundam. Inform. 17(3), 211\u2013234 (1992)","journal-title":"Fundam. Inform."},{"key":"327_CR58","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Washington, pp. 266\u2013277 (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"327_CR59","unstructured":"Kamaleson, N.: Model reduction techniques for probabilistic verification of Markov chains. Ph.D. thesis, University of Birmingham (2018)"},{"key":"327_CR60","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Sher, F.: Modal stochastic games: abstraction-refinement of probabilistic automata. In: Models, Algorithms, Logics and Tools (Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday). LNCS, Springer, vol. 10460, pp. 426\u2013448 (2017)","DOI":"10.1007\/978-3-319-63121-9_21"},{"issue":"4","key":"327_CR61","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1016\/j.jlap.2012.03.007","volume":"81","author":"JP Katoen","year":"2012","unstructured":"Katoen, J.P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for probabilistic systems. J. Logic Algebraic Program. 81(4), 356\u2013389 (2012)","journal-title":"J. Logic Algebraic Program."},{"issue":"3","key":"327_CR62","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/s10703-010-0097-6","volume":"36","author":"M Kattenbelt","year":"2010","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction refinement framework for Markov decision processes. Form. Methods Syst. Des. 36(3), 246\u2013280 (2010)","journal-title":"Form. Methods Syst. Des."},{"key":"327_CR63","doi-asserted-by":"crossref","unstructured":"Kennedy, J., Eberhart, R.: Particle swarm optimization. In: Proceedings IEEE International Conference on Neural Networks, pp. 1942\u20131948 (1995)","DOI":"10.1109\/ICNN.1995.488968"},{"key":"327_CR64","unstructured":"Kwiatkowska, M.: Safety verification for deep neural networks with provable guarantees. In: Proceedings of the 30th International Conference on Concurrency Theory, pp. 1\u20135 (2019)"},{"key":"327_CR65","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Proceedings of the 18th International Conference on Computer Aided Verification. Springer-Verlag, Berlin, Heidelberg, pp. 234\u2013248 (2006a)","DOI":"10.1007\/11817963_23"},{"key":"327_CR66","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: Proceedings of the 3rd International Conference on Quantitative Evaluation of Systems. IEEE Computer Science Press, Washington, pp. 157\u2013166 (2006b)","DOI":"10.1109\/QEST.2006.19"},{"key":"327_CR67","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Proceedings of the 23rd International Conference on Computer Aided Verification. Springer-Verlag, Berlin, Heidelberg, pp. 585\u2013591 (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"327_CR68","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-319-63121-9_15","volume-title":"Models, Algorithms, Logics and Tools","author":"M Kwiatkowska","year":"2017","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symbolic verification and strategy synthesis for linearly-priced probabilistic timed automata. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools, vol. 10460, pp. 289\u2013309. Springer, Cham (2017)"},{"key":"327_CR69","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Proceedings of the 32nd International Conference on Computer Aided Verification (CAV'20), Springer, vol. 12225 of LNCS, pp. 475\u2013487 (2020)","DOI":"10.1007\/978-3-030-53291-8_25"},{"key":"327_CR70","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-020-00356-y","author":"M Kwiatkowska","year":"2021","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automatic verification of concurrent stochastic systems. Form. Methods Syst. Des. (2021). https:\/\/doi.org\/10.1007\/s10703-020-00356-y","journal-title":"Form. Methods Syst. Des."},{"key":"327_CR71","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1146\/annurev-control-042820-010947","volume":"5","author":"M Kwiatkowska","year":"2022","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking and autonomy. Annu. Rev. Control Robot. Auton. Syst. 5, 1\u201326 (2022)","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"issue":"9","key":"327_CR72","doi-asserted-by":"publisher","first-page":"1098","DOI":"10.1177\/0278364919856695","volume":"38","author":"B Lacerda","year":"2019","unstructured":"Lacerda, B., Faruq, F., Parker, D., Hawes, N.: Probabilistic planning with formal performance guarantees for mobile service robots. Int. J. Robot. Res. 38(9), 1098\u20131123 (2019)","journal-title":"Int. J. Robot. Res."},{"issue":"1","key":"327_CR73","doi-asserted-by":"publisher","first-page":"1","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(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"327_CR74","doi-asserted-by":"crossref","unstructured":"Liu, Y.: Secure deep learning engineering: a road towards quality assurance of intelligent systems. In: The 21st International Conference on Formal Engineering Methods, November 5th\u20139th (2019)","DOI":"10.1007\/978-3-030-32409-4_1"},{"key":"327_CR75","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: PAT 3: an extensible architecture for building multi-domain model checkers. In: The 22nd annual International Symposium on Software Reliability Engineering (ISSRE 2011), Hiroshima, Japan, pp. 190\u2013199, Nov 29\u2013Dec 2 (2011)","DOI":"10.1109\/ISSRE.2011.19"},{"issue":"8","key":"327_CR76","first-page":"1853","volume":"26","author":"Y Liu","year":"2015","unstructured":"Liu, Y., Li, X.D., Ma, Y.: Model abstraction for stochastic model checking. Ruan Jian Xue Bao\/J. Softw. 26(8), 1853\u20131870 (2015)","journal-title":"Ruan Jian Xue Bao\/J. Softw."},{"issue":"1","key":"327_CR77","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/s11390-016-1621-y","volume":"31","author":"Y Liu","year":"2016","unstructured":"Liu, Y., Li, X.D., Ma, Y.: A game-based approach for PCTL* stochastic model checking with evidence. J. Comput. Sci. Technol. 31(1), 198\u2013216 (2016)","journal-title":"J. Comput. Sci. Technol."},{"key":"327_CR78","doi-asserted-by":"crossref","unstructured":"Luisa, V.L., Loreti, M., Nenzi, L., Hillston, J., Marion, G.: Three-valued spatio-temporal logic: a further analysis on spatio-temporal properties of stochastic systems. In: Proceedings 14th International Conference on Quantitative Evaluation of Systems, pp. 317\u2013332 (2017)","DOI":"10.1007\/978-3-319-66335-7_22"},{"key":"327_CR79","doi-asserted-by":"publisher","first-page":"83839","DOI":"10.1109\/ACCESS.2019.2924639","volume":"7","author":"Y Ma","year":"2019","unstructured":"Ma, Y., Cao, Z., Liu, Y.: A Probabilistic assume-guarantee reasoning framework based on genetic algorithm. IEEE Access 7, 83839\u201383851 (2019a)","journal-title":"IEEE Access"},{"issue":"10","key":"327_CR80","doi-asserted-by":"publisher","first-page":"1465","DOI":"10.1142\/S0218194019500463","volume":"29","author":"Y Ma","year":"2019","unstructured":"Ma, Y., Cao, Z., Liu, Y.: A PSO-based CEGAR framework for stochastic model checking. Int. J. Softw. Eng. Knowl. Eng. 29(10), 1465\u20131495 (2019b)","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"issue":"3","key":"327_CR81","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/1132960.1132962","volume":"38","author":"A Miller","year":"2006","unstructured":"Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3), 8 (2006)","journal-title":"ACM Comput. Surv."},{"key":"327_CR82","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of the 2nd International Joint Conference on Artificial Intelligence. William Kaufmann Inc., London, pp. 481\u2013489 (1971)"},{"key":"327_CR83","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer-Verlag, Berlin, Heidelberg (1980)"},{"key":"327_CR84","volume-title":"Intelligent and Evolutionary Systems. Proceedings in Adaptation, Learning and Optimization","author":"BH Nguyen","year":"2017","unstructured":"Nguyen, B.H., Xue, B., Andreae, P.: A novel binary particle swarm optimization algorithm and its applications on knapsack and feature selection problems. In: Leu, G., Singh, H., Elsayed, S. (eds.) Intelligent and Evolutionary Systems. Proceedings in Adaptation, Learning and Optimization, vol. 8. Springer, Cham (2017)"},{"issue":"2","key":"327_CR85","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1109\/TCYB.2019.2944141","volume":"51","author":"BH Nguyen","year":"2021","unstructured":"Nguyen, B.H., Xue, B., Andreae, P., Zhang, M.: A new binary particle swarm optimization approach: momentum and dynamic balance between exploration and exploitation. IEEE Trans. Cybern. 51(2), 589\u2013603 (2021)","journal-title":"IEEE Trans. Cybern."},{"issue":"1\u20132","key":"327_CR86","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"IPC Norris","year":"1996","unstructured":"Norris, I.P.C., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1\u20132), 41\u201375 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"327_CR87","doi-asserted-by":"crossref","unstructured":"Oxford, M., Parker, D., Ryan, M.: Quantitative verification of certificate transparency gossip protocols. In: Proceedings of the IEEE Conference on Communications and Network Security, France, June 29\u2013July 1, pp. 1\u20139 (2020)","DOI":"10.1109\/CNS48642.2020.9162197"},{"issue":"6","key":"327_CR88","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"issue":"108","key":"327_CR89","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1007\/s11225-019-09876-z","volume":"4","author":"F Paoli","year":"2020","unstructured":"Paoli, F., Prabaldi, M.: Proof theory of paraconsistent weak Kleene logic. Stud. Logica 4(108), 779\u2013802 (2020)","journal-title":"Stud. Logica"},{"key":"327_CR90","doi-asserted-by":"crossref","unstructured":"Park D.: Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science. Springer-Verlag, Berlin, Heidelberg, pp. 167\u2013183 (1981)","DOI":"10.1007\/BFb0017309"},{"key":"327_CR91","doi-asserted-by":"crossref","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Proceedings of the 5th International Conference on Computer Aided Verification. Springer-Verlag, Berlin, Heidelberg, pp. 409\u2013423 (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"key":"327_CR92","doi-asserted-by":"crossref","unstructured":"Peled, D.: Partial order reduction: linear and branching temporal logics and process algebras. In: Proceedings of the DIMACS Workshop on Partial Order Methods in Verification. AMS Press, New York, pp. 79\u201388 (1996)","DOI":"10.1090\/dimacs\/029\/13"},{"key":"327_CR93","doi-asserted-by":"crossref","unstructured":"Peled, D., Pratt, V., Holzmann, G.: Partial order methods in verification. In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science. (1997)","DOI":"10.1090\/dimacs\/029"},{"key":"327_CR94","first-page":"1","volume-title":"Lecture Notes in Computer Science 84","author":"CA Petri","year":"1979","unstructured":"Petri, C.A.: Introduction to general net theory. In: Brauer, W. (ed.) Lecture Notes in Computer Science 84, pp. 1\u201319. Springer-Verlag, Berlin, Heidelberg (1979)"},{"issue":"2","key":"327_CR95","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1109\/MS.2018.2886815","volume":"36","author":"A Pfeffer","year":"2019","unstructured":"Pfeffer, A., Wu, C., Fry, G., Lu, K., et al.: Software adaptation for an unmanned undersea vehicle. IEEE Softw. 36(2), 91\u201396 (2019)","journal-title":"IEEE Softw."},{"key":"327_CR96","doi-asserted-by":"crossref","unstructured":"Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Proceedings of the 11th International Conference on Concurrency Theory. Springer-Verlag, Berlin, Heidelberg, pp. 334\u2013349 (2000)","DOI":"10.1007\/3-540-44618-4_25"},{"issue":"2","key":"327_CR97","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250\u2013273 (1995)","journal-title":"Nord. J. Comput."},{"key":"327_CR98","doi-asserted-by":"crossref","unstructured":"Shivakumar, S., Torfah, H., Desai, A., Seshia, S.A.: SOTER on ROS: a run-time assurance framework on the robot operating system. In: 20th International Conference on Runtime Verification (RV), October (2020)","DOI":"10.1007\/978-3-030-60508-7_10"},{"issue":"1","key":"327_CR99","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1297658.1297659","volume":"9","author":"S Shoham","year":"2007","unstructured":"Shoham, S., Grumberg, O.: Game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Logic (TOCL) 9(1), 1 (2007)","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"issue":"4","key":"327_CR100","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Form. Methods Syst. Des. 1(4), 297\u2013322 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"327_CR101","doi-asserted-by":"crossref","unstructured":"Wachter, B., Zhang, L.J.: Best probabilistic transformers. In: Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer-Verlag, Berlin, Heidelberg, pp. 362\u2013379 (2010)","DOI":"10.1007\/978-3-642-11319-2_26"},{"key":"327_CR102","doi-asserted-by":"crossref","unstructured":"Wahl, T., Blanc, N., Emerson, E.A.: SVISS: symbolic verification of symmetric systems. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, Berlin, Heidelberg, pp. 459\u2013462 (2008)","DOI":"10.1007\/978-3-540-78800-3_34"},{"issue":"3","key":"327_CR103","doi-asserted-by":"publisher","first-page":"1472","DOI":"10.1109\/COMST.2020.2965856","volume":"22","author":"J Wang","year":"2020","unstructured":"Wang, J., Jiang, C., Zhang, H., Ren, Chen K C., Hanzo, L.: Thirty years of machine learning: the road to pareto-optimal wireless networks. IEEE Commun. Surv. Tutor. 22(3), 1472\u20131514 (2020)","journal-title":"IEEE Commun. Surv. Tutor."},{"key":"327_CR104","doi-asserted-by":"crossref","unstructured":"Winterer, L., Junges, S., Wimmer, R., Jansen, N., Topcu, U., Katoen, J.P., Becker, B.: Motion planning under partial observability using game-based abstraction. In: IEEE 56th Annual Conference on Decision and Control (CDC), pp. 2201\u20132208, IEEE (2017)","DOI":"10.1109\/CDC.2017.8263971"},{"issue":"3","key":"327_CR105","doi-asserted-by":"publisher","first-page":"1040","DOI":"10.1109\/TAC.2020.2990140","volume":"66","author":"L Winterer","year":"2020","unstructured":"Winterer, L., Junges, S., Wimmer, R., Jansen, N., Topcu, U., Katoen, J.P., Becker, B.: Strategy synthesis for POMDPs in robot planning via game-based abstractions. IEEE Trans. Autom. Control 66(3), 1040\u20131054 (2020)","journal-title":"IEEE Trans. Autom. Control"},{"key":"327_CR106","doi-asserted-by":"crossref","unstructured":"Younes, H.: Ymer: a statistical model checker. In: Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05), Springer, vol. 3576 of LNCS, pp. 429\u2013433 (2005)","DOI":"10.1007\/11513988_43"},{"key":"327_CR107","unstructured":"Zhang, L.J.: Decision algorithms for probabilistic simulations [Ph.D. Thesis]. Saarland University, Saarbr\u00fccken (2008)"},{"key":"327_CR108","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1016\/j.ic.2016.04.002","volume":"249","author":"LJ Zhang","year":"2016","unstructured":"Zhang, L.J., David, N.J.: A space-efficient simulation algorithm on probabilistic automata. Inf. Comput. 249, 138\u2013159 (2016)","journal-title":"Inf. Comput."},{"key":"327_CR109","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/s00236-018-0313-1","volume":"55","author":"LJ Zhang","year":"2018","unstructured":"Zhang, L.J., Yang, P., Song, L., et al.: Probabilistic bisimulation for realistic schedulers. Acta Inform. 55, 461\u2013488 (2018)","journal-title":"Acta Inform."},{"key":"327_CR110","doi-asserted-by":"crossref","unstructured":"Zhang, X., Zhou, Y., Han, T., Chen, T.: Training deep code comment generation models via data augmentation. In: Internetware, pp. 185\u2013188 (2020)","DOI":"10.1145\/3457913.3457937"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-022-00327-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10515-022-00327-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-022-00327-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T16:47:01Z","timestamp":1726764421000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10515-022-00327-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,2]]},"references-count":110,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,5]]}},"alternative-id":["327"],"URL":"https:\/\/doi.org\/10.1007\/s10515-022-00327-z","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[2022,3,2]]},"assertion":[{"value":"30 July 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 January 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 March 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"29"}}