{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:51:34Z","timestamp":1740099094928,"version":"3.37.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319991535"},{"type":"electronic","value":"9783319991542"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99154-2_12","type":"book-chapter","created":{"date-parts":[[2018,8,14]],"date-time":"2018-08-14T14:14:35Z","timestamp":1534256075000},"page":"190-206","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Action and State Based Computation Tree Measurement Language and Algorithms"],"prefix":"10.1007","author":[{"given":"Yaping","family":"Jing","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew S.","family":"Miner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,15]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-13568-2_10","volume-title":"Analytical and Stochastic Modeling Techniques and Applications","author":"AS Miner","year":"2010","unstructured":"Miner, A.S., Jing, Y.: A formal language toward the unification of model checking and performance evaluation. In: Al-Begain, K., Fiems, D., Knottenbelt, W.J. (eds.) ASMTA 2010. LNCS, vol. 6148, pp. 130\u2013144. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13568-2_10"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0166-5316(93)90026-Q","volume":"18","author":"G Ciardo","year":"1993","unstructured":"Ciardo, G., Trivedi, K.S.: A decomposition approach for stochastic reward net models. Perform. Eval. 18, 37\u201359 (1993)","journal-title":"Perform. Eval."},{"issue":"5","key":"12_CR3","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 Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"issue":"4","key":"12_CR4","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1109\/TSE.2007.36","volume":"33","author":"C Baier","year":"2007","unstructured":"Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE Trans. Softw. Eng. 33, 209\u2013224 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF00289519","volume":"1","author":"EW Dijkstra","year":"1971","unstructured":"Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informatica 1, 115\u2013138 (1971)","journal-title":"Acta Informatica"},{"issue":"3\u20134","key":"12_CR7","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/S0166-5316(99)00010-3","volume":"35","author":"WD Obal","year":"1999","unstructured":"Obal, W.D., Sanders, W.H.: State-space support for path-based reward variables. Perform. Eval. 35(3\u20134), 233\u2013251 (1999)","journal-title":"Perform. Eval."},{"key":"12_CR8","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"WJ Stewart","year":"1994","unstructured":"Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)"},{"key":"12_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-0399-0","volume-title":"Measure Theory","author":"DL Cohn","year":"1980","unstructured":"Cohn, D.L.: Measure Theory. Birkh\u00e4user, Boston (1980)"},{"issue":"2","key":"12_CR10","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1109\/TSE.2008.108","volume":"35","author":"S Donatelli","year":"2009","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL$$^{\\text{ TA }}$$. IEEE Trans. Softw. Eng. 35(2), 224\u2013240 (2009)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-48778-6_13","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"G Clark","year":"1999","unstructured":"Clark, G., Gilmore, S., Hillston, J.: Specifying performance measures for PEPA. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 211\u2013227. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48778-6_13"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, New York, NY, USA, pp. 449\u2013458. ACM (2007)","DOI":"10.1145\/1287624.1287688"},{"key":"12_CR13","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. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"12_CR14","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput. Sci. 13, 45\u201360 (1981)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR15","first-page":"393","volume":"4","author":"P Schnoebelen","year":"2002","unstructured":"Schnoebelen, P.: The complexity of temporal logic model checking. Adv. Modal Log. 4, 393\u2013436 (2002)","journal-title":"Adv. Modal Log."},{"issue":"4\u20136","key":"12_CR16","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/s00165-012-0227-6","volume":"24","author":"M Kwiatkowska","year":"2012","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic verification of Herman\u2019s self-stabilisation algorithm. Formal Aspects Comput. 24(4\u20136), 661\u2013670 (2012)","journal-title":"Formal Aspects Comput."},{"key":"12_CR17","volume-title":"Finite Markov Chains","author":"JG Kemeny","year":"1960","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. D. Van Nostrand Company Inc., Princeton (1960)"},{"key":"12_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4374-8","volume-title":"Probability","author":"J Pitman","year":"1993","unstructured":"Pitman, J.: Probability. Springer, New York (1993). https:\/\/doi.org\/10.1007\/978-1-4612-4374-8"},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-40903-8_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Andova","year":"2004","unstructured":"Andova, S., Hermanns, H., Katoen, J.P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) Formal Modeling and Analysis of Timed Systems, pp. 88\u2013104. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-40903-8_8"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1007\/3-540-45022-X_65","volume-title":"Automata, Languages and Programming","author":"C Baier","year":"2000","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: On the logical characterisation of performability properties. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 780\u2013792. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45022-X_65"},{"issue":"6","key":"12_CR21","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 Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-40911-4_24","volume-title":"Integrated Formal Methods","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: Towards model checking stochastic process algebra. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 420\u2013439. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40911-4_24"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Suto, T., Bradley, J.T., Knottenbelt, W.J.: Performance trees: expressiveness and quantitative semantics. In: Proceedings of the 4th International Conference on Quantitative Evaluation of Systems, Washington DC, USA, pp. 41\u201350. IEEE Computer Society (2007)","DOI":"10.1109\/QEST.2007.9"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99154-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T05:07:02Z","timestamp":1571720822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99154-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319991535","9783319991542"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99154-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}