{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:15Z","timestamp":1740109095387,"version":"3.37.3"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"3-4","license":[{"start":{"date-parts":[[2018,8,1]],"date-time":"2018-08-01T00:00:00Z","timestamp":1533081600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            In this work, we present a formal language, CTML, to reason over probabilistic systems. CTML extends stochastic temporal logics in a way that it takes a real value as input and output a real value in the range of\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo stretchy=\"false\">[<\/mml:mo>\n                    <mml:mn>0<\/mml:mn>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mi>\u221e<\/mml:mi>\n                    <mml:mo stretchy=\"false\">)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            , as opposed to 0\/1 values as input and output, and it can\n            <jats:italic>nest<\/jats:italic>\n            real values. This allows CTML to express a rich set of queries towards the unification of model checking and performance evaluation. In fact, CTML covers PCTL. It can express a nontrivial subset of PLTL formulas that cannot be expressed by PCTL. The significance of this result is that the overall complexity of CTML is linear, as opposed to exponential as it is with PLTL, in the size of the operators for a given formula, and polynomial in the size of a given model. Moreover, CTML can express real-valued performance queries such as: \u201cif a system encounters a failure, what is the expected time to reach a recovery state?\u201d that cannot be expressed by a probabilistic model checking logic, because they are \u201cprobabilistic\u201d at most. Along with the specification language, we present a set of algorithms for the evaluation of the language and show proofs for their correctness. Additionally, we include an application example and show experimental results.\n          <\/jats:p>","DOI":"10.1007\/s00165-018-0457-3","type":"journal-article","created":{"date-parts":[[2018,6,18]],"date-time":"2018-06-18T11:21:10Z","timestamp":1529320870000},"page":"443-462","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Computation tree measurement language (CTML)"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3042-0634","authenticated-orcid":false,"given":"Yaping","family":"Jing","sequence":"first","affiliation":[{"name":"Department of Math and Computer Science, Salisbury University, Salisbury, MD, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew S.","family":"Miner","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Iowa State University, Ames, IA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Andova S Hermanns H Katoen J-P (2003) Discrete-time rewards model-checked. In: Larsen KG Niebert P (eds) Formal modelling and analysis of timed systems volume 2791 of Lecture notes in computer science. Springer pp 88\u2013104","DOI":"10.1007\/978-3-540-40903-8_8"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Aziz A Singhal V Balarin F (1995) It usually works: The temporal logic of stochastic systems. In: Proceedings of the 7th international conference on computer aided verification London UK. Springer pp 155\u2013165","DOI":"10.1007\/3-540-60045-0_48"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.36"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bianco A de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Proceedings of the 15th conference on foundations of software technology and theoretical computer science Berlin Heidelberg. Springer pp 499\u2013513","DOI":"10.1007\/3-540-60692-0_70"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Beaudry DM (1978) Performance-related reliability measures for computing systems. IEEE Trans Comput C-27(6):540\u2013547","DOI":"10.1109\/TC.1978.1675145"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Borgerson BR Freitas RF (1975) A reliability model for gracefully degrading and standby-sparing systems. IEEE Trans Comput C-24(5):517\u2013525","DOI":"10.1109\/T-C.1975.224255"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Baier C Haverkort BR Hermanns H Katoen J-P (2000) On the logical characterisation of performability properties. In: Proceedings of the 27th international colloquium on automata languages and programming London UK. Springer pp 780\u2013792","DOI":"10.1007\/3-540-45022-X_65"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/2841997.2842006"},{"volume-title":"Introduction to stochastic processes","year":"1975","author":"\u00c7inlar E","key":"e_1_2_1_2_10_2"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Clark G Gilmore S Hillston J (1999) Specifying performance measures for PEPA. In: Proceedings of the 5th international AMAST workshop on formal methods for real-time and probabilistic systems London UK. Springer pp 211\u2013227","DOI":"10.1007\/3-540-48778-6_13"},{"volume-title":"Model checking","year":"1999","author":"Clarke EM","key":"e_1_2_1_2_12_2"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Chung KL (1979) Elementary probability theory with stochastic processes. Undergraduate texts in mathematics 3rd edn. Springer Orlando","DOI":"10.1007\/978-1-4684-9346-7"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2005.06.001"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4899-0399-0","volume-title":"Measure theory","author":"Cohn DL","year":"1980"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"de Alfaro L (1997) Temporal logics for the specification of performance and reliability. In: Proceedings of the 14th annual symposium on theoretical aspects of computer science London UK. Springer pp 165\u2013176","DOI":"10.1007\/BFb0023457"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"de Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Proceedings of the 10th international conference on concurrency theory London UK. Springer pp 66\u201381","DOI":"10.1007\/3-540-48320-9_7"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.033"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.108"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289519"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Emerson EA (1990) Temporal and modal logic. In: Handbook of theoretical computer science. Elsevier pp 995\u20131072","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1530873.1530878"},{"key":"e_1_2_1_2_24_2","unstructured":"Grinstead CM Snell JL (2003) Introduction to probability. American Mathematical Society"},{"key":"e_1_2_1_2_25_2","unstructured":"Haverkort BR Cloth L Hermanns H Katoen J-P (2002) Model checking performability properties. In: Proceedings of the 2002 international conference on dependable systems and networks Washington DC USA. IEEE Computer Society pp 103\u2013112"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/511399.511345"},{"key":"e_1_2_1_2_28_2","unstructured":"Jing Yaping (2015) A formal language towards the unification of model checking and performance evaluation. PhD thesis Iowa State University Ames IA"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1530873.1530882"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G Qadeer S (eds) Proceedings of 23rd international conference on computer aided verification volume 6806 of LNCS. Springer pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D Sproston J (2003) Performance analysis of probabilistic timed automata using digital clocks. In: Proceedings of formal modeling and analysis of timed systems volume 2791 of LNCS. Springer pp 105\u2013120","DOI":"10.1007\/978-3-540-40903-8_9"},{"volume-title":"Finite Markov Chains","year":"1960","author":"Kemeny JG","key":"e_1_2_1_2_32_2"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M (2007) Quantitative verification: models techniques and tools. In: Proceedings of the 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 ACM pp 449\u2013458","DOI":"10.1145\/1295014.1295018"},{"key":"e_1_2_1_2_34_2","first-page":"140","volume-title":"8th international conference on foundations of software science and computational structures","author":"Laroussinie F","year":"2005"},{"key":"e_1_2_1_2_35_2","unstructured":"Liu Y Trivedi KS (2004) A general framework for network survivability quantification. In: Peter B Ralf L Michal P (eds) MMB. VDE Verlag pp 369\u2013378"},{"key":"e_1_2_1_2_36_2","unstructured":"Muppala JK Ciardo G Trivedi KS (1993) Modeling using stochastic reward nets. In: Proceedings of the international workshop on modeling analysis and simulation on computer and telecommunication systems. Society for Computer Simulation pp 367\u2013372"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Meyer JF (1980) On evaluating the performability of degradable computing systems. IEEE Trans Comput C-29(8):720\u2013731","DOI":"10.1109\/TC.1980.1675654"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2003.07.005"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Miner AS Jing Y (2010) A formal language toward the unification of model checking and performance evaluation. In: Analytical and stochastic modeling techniques and applications pp 130\u2013144","DOI":"10.1007\/978-3-642-13568-2_10"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-5316(99)00010-3"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.5555\/1197141"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Suto T Bradley JT Knottenbelt WJ (2007) Performance trees: Expressiveness and quantitative semantics. In: Proceedings of the fourth international conference on quantitative evaluation of systems Washington DC USA. IEEE Computer Society pp 41\u201350","DOI":"10.1109\/QEST.2007.9"},{"key":"e_1_2_1_2_44_2","unstructured":"Schnoebelen P (2002) The complexity of temporal logic model checking. In: Advances in modal logic pp 393\u2013436"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Stewart WJ (1994) Introduction to the numerical solution of Markov Chains. Princeton University Press","DOI":"10.1515\/9780691223384"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1007\/BFb0013869","volume-title":"Performance evaluation of computer and communication systems, joint tutorial papers of performance\u201993 and Sigmetrics\u201993","author":"Trivedi KS","year":"1993"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-018-0457-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0457-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0457-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0457-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:13:01Z","timestamp":1641485581000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-018-0457-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8]]},"references-count":46,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["10.1007\/s00165-018-0457-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-018-0457-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2018,8]]},"assertion":[{"value":"7 February 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 May 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 June 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}