{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:39:15Z","timestamp":1767339555858,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":65,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031671135"},{"type":"electronic","value":"9783031671142"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-67114-2_4","type":"book-chapter","created":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:42:47Z","timestamp":1725507767000},"page":"71-102","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["PCSP# Denotational Semantics with\u00a0an\u00a0Application in\u00a0Sports Analytics"],"prefix":"10.1007","author":[{"given":"Zhaoyu","family":"Liu","sequence":"first","affiliation":[]},{"given":"Murong","family":"Ma","sequence":"additional","affiliation":[]},{"given":"Kan","family":"Jiang","sequence":"additional","affiliation":[]},{"given":"Zhe","family":"Hou","sequence":"additional","affiliation":[]},{"given":"Ling","family":"Shi","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,1]]},"reference":[{"key":"4_CR1","unstructured":"Bresciani, R., Butterfield, A.: Towards a UTP-style framework to deal with probabilities. Technical Report TCD-CS-2011-09, FMG, Trinity College Dublin, Ireland (2011)"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-030-51054-1_22","volume-title":"Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1\u20134, 2020, Proceedings, Part II","author":"H Bride","year":"2020","unstructured":"Bride, H., et al.: N-PAT: a nested model-checker: (System Description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1\u20134, 2020, Proceedings, Part II, pp. 369\u2013377. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_22"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Cavalcanti, A., Sampaio, A., Woodcock, J.: Refinement of actions in circus. In: Derrick, J., Boiten, E.A., Woodcock, J., von Wright, J. (eds.) BCS FACS Refinement Workshop 2002, Refine 2002, Satellite Event of FLoC 2002, Copenhagen, Denmark, July 20-21, 2002. Electronic Notes in Theoretical Computer Science, vol.\u00a070, pp. 132\u2013162. Elsevier (2002). https:\/\/doi.org\/10.1016\/S1571-0661(05)80489-X","DOI":"10.1016\/S1571-0661(05)80489-X"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11889229_6","volume-title":"Refinement Techniques in Software Engineering","author":"A Cavalcanti","year":"2006","unstructured":"Cavalcanti, A., Woodcock, J.: A Tutorial Introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) Refinement Techniques in Software Engineering, pp. 220\u2013268. Springer, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11889229_6"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-030-03044-5_13","volume-title":"Formal Methods: Foundations and Applications: 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26\u201330, 2018, Proceedings","author":"MS Conserva Filho","year":"2018","unstructured":"Conserva Filho, M.S., Marinho, R., Mota, A., Woodcock, J.: Analysing RoboChart with Probabilities. In: Massoni, T., Mousavi, M.R. (eds.) Formal Methods: Foundations and Applications: 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26\u201330, 2018, Proceedings, pp. 198\u2013214. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03044-5_13"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Davies, J.: Specification and proof in real-time CSP. Cambridge University Press (1993)","DOI":"10.1017\/CBO9780511569760"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Dong, J.S., et al.: Sports analytics using probabilistic model checking and deep learning. In: 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 7\u201311. IEEE (2023)","DOI":"10.1109\/ICECCS59891.2023.00011"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Dong, J.S., Shi, L., Jiang, K., Sun, J., et\u00a0al.: Sports strategy analytics using probabilistic reasoning. In: 20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, pp. 182\u2013185. IEEE (2015)","DOI":"10.1109\/ICECCS.2015.28"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Fernando, D., Dong, N., J\u00e9gourel, C., Dong, J.S.: Verification of Nash-equilibrium for probabilistic BAR systems. In: 21st International Conference on Engineering of Complex Computer Systems, ICECCS 2016, pp. 53\u201362. IEEE Computer Society (2016)","DOI":"10.1109\/ICECCS.2016.016"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-319-52228-9_3","volume-title":"Unifying Theories of Programming","author":"S Foster","year":"2017","unstructured":"Foster, S., Thiele, B., Cavalcanti, A., Woodcock, J.: Towards a UTP semantics for modelica. In: Bowen, J.P., Zhu, H. (eds.) Unifying Theories of Programming, pp. 44\u201364. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52228-9_3"},{"issue":"3","key":"4_CR11","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s11518-018-5395-3","volume":"28","author":"W Gu","year":"2019","unstructured":"Gu, W., Saaty, T.L.: Predicting the outcome of a tennis tournament: based on both data and judgments. J. Syst. Sci. Syst. Eng. 28(3), 317\u2013343 (2019)","journal-title":"J. Syst. Sci. Syst. Eng."},{"key":"4_CR12","unstructured":"Guo, C., Pleiss, G., Sun, Y., Weinberger, K.Q.: On calibration of modern neural networks. In: International Conference on Machine Learning, pp. 1321\u20131330. PMLR (2017)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-73210-5_19","volume-title":"Integrated Formal Methods","author":"H Jifeng","year":"2007","unstructured":"Jifeng, H.: UTP semantics for web services. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 353\u2013372. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73210-5_19"},{"issue":"1\u20132","key":"4_CR14","first-page":"109","volume":"365","author":"J He","year":"2006","unstructured":"He, J., Li, X., Liu, Z.: rCOS: a refinement calculus of object systems. Theor. Comput. Sci. 365(1\u20132), 109\u2013142 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR15","first-page":"171","volume":"28","author":"J He","year":"1999","unstructured":"He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Sci. Comput. Program. 28, 171\u2013192 (1999)","journal-title":"Sci. Comput. Program."},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Hoare, C.: Communicating Sequential Processes. Prentice-Hall (1985)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Hoare, C., He, J.: Unifying Theories of Programming. Prentice-Hall (1998)","DOI":"10.1007\/BFb0002714"},{"issue":"4","key":"4_CR18","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1515\/jqas-2018-0008","volume":"15","author":"M Ingram","year":"2019","unstructured":"Ingram, M.: A point-based Bayesian hierarchical model to predict the outcome of tennis matches. J. Quantit. Anal. Sports 15(4), 313\u2013325 (2019)","journal-title":"J. Quantit. Anal. Sports"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Jiang, K., Izadi, M., Liu, Z., Dong, J.S.: Deep learning application in broadcast tennis video annotation. In: 2020 25th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 53\u201362. IEEE (2020)","DOI":"10.1109\/ICECCS51672.2020.00014"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Jiang, K., Li, J., Liu, Z., Dong, C.: Court detection using masked perspective fields network. In: 2023 IEEE 28th Pacific Rim International Symposium on Dependable Computing (PRDC), pp. 342\u2013345. IEEE (2023)","DOI":"10.1109\/PRDC59308.2023.00055"},{"issue":"3","key":"4_CR21","first-page":"127","volume":"12","author":"SA Kovalchik","year":"2016","unstructured":"Kovalchik, S.A.: Searching for the goat of tennis win prediction. J. Quantit. Anal. Sports 12(3), 127\u2013138 (2016)","journal-title":"J. Quantit. Anal. Sports"},{"issue":"4","key":"4_CR22","first-page":"277","volume":"38","author":"C Leitner","year":"2009","unstructured":"Leitner, C., Zeileis, A., Hornik, K.: Is federer stronger in a tournamentwithout nadal? an evaluation of odds and seedings for wimbledon 2009. Austrian J. Stat. 38(4), 277\u2013286 (2009)","journal-title":"Austrian J. Stat."},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Liu, Z., Guo, J., Wang, M., Wang, R., Jiang, K., Dong, J.S.: Recognizing a sequence of events from tennis video clips: addressing timestep identification and subtle class differences. In: 2023 IEEE 28th Pacific Rim International Symposium on Dependable Computing (PRDC), pp. 337\u2013341. IEEE (2023)","DOI":"10.1109\/PRDC59308.2023.00054"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Liu, Z., Jiang, K., Dong, J.S.: Sports injury prediction in professional tennis. In: 2023 IEEE 28th Pacific Rim International Symposium on Dependable Computing (PRDC), pp. 304\u2013308. IEEE (2023)","DOI":"10.1109\/PRDC59308.2023.00048"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Liu, Z., Jiang, K., Hou, Z., Lin, Y., Dong, J.S.: Insight analysis for tennis strategy and tactics. In: 2023 IEEE International Conference on Data Mining (ICDM), pp. 1169\u20131174. IEEE (2023)","DOI":"10.1109\/ICDM58522.2023.00143"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-031-40436-8_3","volume-title":"Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday","author":"Z Liu","year":"2023","unstructured":"Liu, Z.: Linking formal methods in\u00a0software development: a reflection on the development of rCOS. In: Bowen, J.P., Li, Q., Xu, Q. (eds.) Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, pp. 52\u201384. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-40436-8_3"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Mahony, B., Dong, J.S.: Blending Object-Z and Timed CSP: an introduction to TCOZ. In: Proceedings of the 20th International Conference on Software Engineering, pp. 95\u2013104 (1998)","DOI":"10.1109\/ICSE.1998.671106"},{"issue":"2","key":"4_CR28","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1109\/32.841115","volume":"26","author":"B Mahony","year":"2000","unstructured":"Mahony, B., Dong, J.S.: Timed communicating object Z. IEEE Trans. Software Eng. 26(2), 150\u2013177 (2000)","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR29","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-1-4471-0851-1_5","volume-title":"IFM\u201999","author":"B Mahony","year":"1999","unstructured":"Mahony, B., Dong, J.S.: Overview of the semantics of TCOZ. In: Araki, K., Galloway, A., Taguchi, K. (eds.) IFM\u201999, pp. 66\u201385. Springer, London (1999). https:\/\/doi.org\/10.1007\/978-1-4471-0851-1_5"},{"key":"4_CR30","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18, 3097\u20133149 (2019). https:\/\/doi.org\/10.1007\/s10270-018-00710-z","journal-title":"Softw. Syst. Model."},{"issue":"6","key":"4_CR31","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/BF01213492","volume":"8","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Aspects Comput. 8(6), 617\u2013647 (1996)","journal-title":"Formal Aspects Comput."},{"key":"4_CR32","unstructured":"Morris, B., Bialik, C., Boice, J.: How we\u2019re forecasting the 2016 us open. https:\/\/fivethirtyeight.com\/features\/how-were-forecasting-the-2016-us-open\/. Search in (2016)"},{"key":"4_CR33","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-34281-3_28","volume-title":"Formal Methods and Software Engineering","author":"TK Nguyen","year":"2012","unstructured":"Nguyen, T.K., Sun, J., Liu, Y., Dong, J.S.: Symbolic model-checking of stateful timed CSP using BDD and digitization. In: Aoki, T., Taguchi, K. (eds.) Formal Methods and Software Engineering, pp. 398\u2013413. Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34281-3_28"},{"key":"4_CR34","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.entcs.2006.08.047","volume":"187","author":"M Oliveira","year":"2007","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A denotational semantics for circus. Electron. Notes Theor. Comput. Sci. 187, 107\u2013123 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"4_CR35","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"M Oliveira","year":"2009","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for circus. Formal Aspects Comput. 21(1\u20132), 3\u201332 (2009)","journal-title":"Formal Aspects Comput."},{"key":"4_CR36","unstructured":"Phillips, J.J.: Measuring return on investment, vol.\u00a02. American Society for Training and Development (1994)"},{"key":"4_CR37","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-540-45236-2_19","volume-title":"FME 2003: Formal Methods: International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003. Proceedings","author":"S Qin","year":"2003","unstructured":"Qin, S., Dong, J.S., Chin, W.-N.: A semantic foundation for TCOZ in unifying theories of programming. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: Formal Methods: International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003. Proceedings, pp. 321\u2013340. Springer, Berlin, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_19"},{"key":"4_CR38","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1997)"},{"key":"4_CR39","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"A Roscoe","year":"2010","unstructured":"Roscoe, A.: Understanding Concurrent Systems, 1st edn. Springer-Verlag, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-1-84882-258-0","edition":"1"},{"key":"4_CR40","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/3-540-45614-7_26","volume-title":"FME 2002:Formal Methods\u2014Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22\u201324, 2002 Proceedings","author":"A Sampaio","year":"2002","unstructured":"Sampaio, A., Woodcock, J., Cavalcanti, A.: Refinement in circus. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002:Formal Methods\u2014Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22\u201324, 2002 Proceedings, pp. 451\u2013470. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45614-7_26"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Sherif, A., Cavalcanti, A., Jifeng, H., Sampaio, A.: A process algebraic framework for specification and validation of real-time systems. Form. Asp. Comput. 22(2), 153\u2013191 (2010)","DOI":"10.1007\/s00165-009-0119-6"},{"key":"4_CR42","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-642-41202-8_15","volume-title":"Formal Methods and Software Engineering","author":"L Shi","year":"2013","unstructured":"Shi, L., Zhao, Y., Liu, Y., Sun, J., Dong, J.S., Qin, S.: A UTP semantics for communicating processes with shared variables. In: Groves, L., Sun, J. (eds.) Formal Methods and Software Engineering, pp. 215\u2013230. Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41202-8_15"},{"issue":"3\u20134","key":"4_CR43","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/s00165-018-0453-7","volume":"30","author":"L Shi","year":"2018","unstructured":"Shi, L., Zhao, Y., Liu, Y., Sun, J., Dong, J.S., Qin, S.: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS. Form. Asp. Comput. 30(3\u20134), 351\u2013380 (2018)","journal-title":"Form. Asp. Comput."},{"key":"4_CR44","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-63533-5_4","volume-title":"FME \u201997: Industrial Applications and Strengthened Foundations of Formal Methods: 4th International Symposium of Formal Methods Europe Graz, Austria, September 15\u201319, 1997 Proceedings","author":"G Smith","year":"1997","unstructured":"Smith, G.: A semantic integration of object-Z and CSP for the specification of concurrent systems. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds.) FME \u201997: Industrial Applications and Strengthened Foundations of Formal Methods: 4th International Symposium of Formal Methods Europe Graz, Austria, September 15\u201319, 1997 Proceedings, pp. 62\u201381. Springer, Berlin, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63533-5_4"},{"key":"4_CR45","doi-asserted-by":"crossref","unstructured":"Smith, G.: The Object-Z specification language. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"4_CR46","doi-asserted-by":"crossref","unstructured":"Song, S., Hao, J., Liu, Y., Sun, J., Leung, H., Dong, J.S.: Analyzing multi-agent systems with probabilistic model checking approach. In: 34th International Conference on Software Engineering, ICSE 2012, pp. 1337\u20131340. IEEE Computer Society (2012)","DOI":"10.1109\/ICSE.2012.6227085"},{"key":"4_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1007\/978-3-642-31424-7_53","volume-title":"Computer Aided Verification","author":"S Song","year":"2012","unstructured":"Song, S., Sun, J., Liu, Y., Dong, J.S.: A model checker for hierarchical probabilistic real-time systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 705\u2013711. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_53"},{"key":"4_CR48","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-88479-8_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"J Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: introducing a process analysis toolkit. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 307\u2013322. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88479-8_22"},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE\u201909), pp. 127\u2013135. IEEE Computer Society (2009)","DOI":"10.1109\/TASE.2009.32"},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Andr\u00e9, E.: Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. Softw. Eng. Methodol. 22(1), 3:1\u20133:29 (2013)","DOI":"10.1145\/2430536.2430537"},{"key":"4_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709\u2013714. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_59"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-16901-4_26","volume-title":"Formal Methods and Software Engineering","author":"J Sun","year":"2010","unstructured":"Sun, J., Song, S., Liu, Y.: Model checking hierarchical probabilistic systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 388\u2013403. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16901-4_26"},{"issue":"06","key":"4_CR53","doi-asserted-by":"publisher","first-page":"1355010","DOI":"10.1142\/S0218001413550100","volume":"27","author":"A Terroba","year":"2013","unstructured":"Terroba, A., Kosters, W., Varona, J., Manresa-Yee, C.S.: Finding optimal strategies in tennis from video sequences. Int. J. Pattern Recogn. Artif. Intell. 27(06), 1355010 (2013)","journal-title":"Int. J. Pattern Recogn. Artif. Intell."},{"key":"4_CR54","doi-asserted-by":"crossref","unstructured":"Thorp, E.O.: Portfolio choice and the Kelly criterion. In: Stochastic Optimization Models in Finance, pp. 599\u2013619. Elsevier (1975)","DOI":"10.1016\/B978-0-12-780850-5.50051-4"},{"key":"4_CR55","doi-asserted-by":"crossref","unstructured":"Wang, J., et al.: Tac-Valuer: knowledge-based stroke evaluation in table tennis. In: Proceedings of the 27th ACM SIGKDD Conference on Knowledge Discovery & Data Mining, pp. 3688\u20133696 (2021)","DOI":"10.1145\/3447548.3467104"},{"key":"4_CR56","doi-asserted-by":"crossref","unstructured":"Wang, W.Y., Chan, T.F., Yang, H.K., Wang, C.C., Fan, Y.C., Peng, W.C.: Exploring the long short-term dependencies to infer shot influence in badminton matches. In: 2021 IEEE International Conference on Data Mining (ICDM), pp. 1397\u20131402. IEEE (2021)","DOI":"10.1109\/ICDM51629.2021.00178"},{"key":"4_CR57","doi-asserted-by":"crossref","unstructured":"Wang, W.Y., Shuai, H.H., Chang, K.S., Peng, W.C.: ShuttleNet: position-aware fusion of rally progress and player styles for stroke forecasting in badminton. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a036, pp. 4219\u20134227 (2022)","DOI":"10.1609\/aaai.v36i4.20341"},{"key":"4_CR58","doi-asserted-by":"crossref","unstructured":"Wei, K., Woodcock, J., Burns, A.: Timed Circus: timed CSP with the miracle. In: 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011, pp. 55\u201364. IEEE Computer Society (2011)","DOI":"10.1109\/ICECCS.2011.13"},{"key":"4_CR59","unstructured":"Wei, X., Lucey, P., Morgan, S., Reid, M., Sridharan, S.: The thin edge of the wedge: accurately predicting shot outcomes in tennis using style and context priors. In: Proceedings of the 10th Annual MIT Sloan Sport Anal Conference, Boston, MA, USA, pp. 1\u201311 (2016)"},{"key":"4_CR60","doi-asserted-by":"crossref","unstructured":"Woodcock, J.: Software Engineering Mathematics. CRC Press (1988)","DOI":"10.1201\/9781315274744"},{"key":"4_CR61","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"J Woodcock","year":"2002","unstructured":"Woodcock, J., Cavalcanti, A.: The semantics of circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002:Formal Specification and Development in Z and B, pp. 184\u2013203. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45648-1_10"},{"key":"4_CR62","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-030-31038-7_5","volume-title":"Unifying Theories of Programming: 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings","author":"J Woodcock","year":"2019","unstructured":"Woodcock, J., Cavalcanti, A., Foster, S., Mota, A., Ye, K.: Probabilistic semantics for RoboChart: a weakest completion approach. In: Ribeiro, P., Sampaio, A. (eds.) Unifying Theories of Programming: 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Porto, Portugal, October 8, 2019, Proceedings, pp. 80\u2013105. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31038-7_5"},{"key":"4_CR63","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall Inc, USA (1996)"},{"issue":"2","key":"4_CR64","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/s10270-021-00916-8","volume":"21","author":"K Ye","year":"2022","unstructured":"Ye, K., Cavalcanti, A., Foster, S., Miyazawa, A., Woodcock, J.: Probabilistic modelling and verification using RoboChart and PRISM. Softw. Syst. Model. 21(2), 667\u2013716 (2022)","journal-title":"Softw. Syst. Model."},{"key":"4_CR65","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-35705-3_11","volume-title":"Unifying Theories of Programming","author":"H Zhu","year":"2013","unstructured":"Zhu, H., Sanders, J.W., He, J., Qin, S.: Denotational semantics for a probabilistic timed shared-variable language. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) Unifying Theories of Programming, pp. 224\u2013247. Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35705-3_11"}],"container-title":["Lecture Notes in Computer Science","The Application of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-67114-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T19:56:28Z","timestamp":1732737388000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-67114-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031671135","9783031671142"],"references-count":65,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-67114-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}