{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:23Z","timestamp":1750306763039,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004211","name":"Oxford Martin School, University of Oxford","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004211","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:p>\n            Stochastic modelling and algorithmic verification techniques have been proved useful in analysing and detecting unusual trends in performance and energy usage of systems such as power management controllers and wireless sensor devices. Many important properties are dependent on the cumulated time that the device spends in certain states, possibly intermittently. We study the problem of verifying\n            <jats:italic>continuous-time Markov Chains<\/jats:italic>\n            (CTMCs) against\n            <jats:italic>Linear Duration Properties<\/jats:italic>\n            (LDP), that is, properties stated as conjunctions of linear constraints over the total duration of time spent in states that satisfy a given property. We identify two classes of LDP properties,\n            <jats:italic>Eventuality Duration Properties<\/jats:italic>\n            (EDP) and\n            <jats:italic>Invariance Duration Properties<\/jats:italic>\n            (IDP), respectively referring to the reachability of a set of goal states, within a time bound; and the continuous satisfaction of a duration property over an execution path. The central question that we address is how to compute the probability of the set of infinite timed paths of the CTMC that satisfy a given LDP. We present algorithms to approximate these probabilities up to a given precision, stating their complexity and error bounds. The algorithms mainly employ an adaptation of uniformisation and the computation of volumes of multidimensional integrals under systems of linear constraints, together with different mechanisms to bound the errors.\n          <\/jats:p>","DOI":"10.1145\/2528935","type":"journal-article","created":{"date-parts":[[2013,12,4]],"date-time":"2013-12-04T14:04:47Z","timestamp":1386165887000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Verification of linear duration properties over continuous-time markov chains"],"prefix":"10.1145","volume":"14","author":[{"given":"Taolue","family":"Chen","sequence":"first","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Diciolla","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandru","family":"Mereacre","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,11,28]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1023\/A:1008626013578"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1145\/343369.343402"},{"key":"e_1_2_1_3_1","series-title":"Lecture Notes in Computer Science","volume-title":"-P","author":"Baier C.","year":"2000","unstructured":"Baier , C. , Haverkort , B. R. , Hermanns , H. , and Katoen , J . -P . 2000 . On the logical characterization of performability properties. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP'00). U. Montanari, J. D. P. Rolim, and E. Welzl, Eds., Lecture Notes in Computer Science , vol. 1853 , Springer , 780--792. Baier, C., Haverkort, B. R., Hermanns, H., and Katoen, J.-P. 2000. On the logical characterization of performability properties. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP'00). U. Montanari, J. D. P. Rolim, and E. Welzl, Eds., Lecture Notes in Computer Science, vol. 1853, Springer, 780--792."},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1109\/TSE.2003.1205180"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1145\/1810891.1810912"},{"key":"e_1_2_1_6_1","volume-title":"-P","author":"Baier C.","year":"2008","unstructured":"Baier , C. and Katoen , J . -P . 2008 . Principles of Model Checking. MIT Press . Baier, C. and Katoen, J.-P. 2008. Principles of Model Checking. MIT Press."},{"doi-asserted-by":"crossref","unstructured":"Barbot B. Chen T. Han T. Katoen J.-P. and \n      Mereacre A\n  . \n  2011\n  . Efficient CTMC model checking of linear real-time objectives. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Part of the Joint European Conferences on Theory and Practice of Software (TACAS\/ETAP'11). P. A. Abdulla and K. R. M. Leino Eds. Lecture Notes in Computer Science vol. \n  6605 Springer 128--142.   Barbot B. Chen T. Han T. Katoen J.-P. and Mereacre A. 2011. Efficient CTMC model checking of linear real-time objectives. In Proceedings of the 17 th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Part of the Joint European Conferences on Theory and Practice of Software (TACAS\/ETAP'11). P. A. Abdulla and K. R. M. Leino Eds. Lecture Notes in Computer Science vol. 6605 Springer 128--142.","key":"e_1_2_1_7_1","DOI":"10.1007\/978-3-642-19835-9_12"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1109\/LICS.2011.33"},{"volume-title":"Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS'93)","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Echahed , R. , and Sifakis , J . 1993. On model checking for real-time properties with durations . In Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS'93) . IEEE Computer Society, Los Alamitos, CA, 147--159. Bouajjani, A., Echahed, R., and Sifakis, J. 1993. On model checking for real-time properties with durations. In Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS'93). IEEE Computer Society, Los Alamitos, CA, 147--159.","key":"e_1_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1145\/1755952.1755963"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1007\/978-3-540-85778-5_4"},{"doi-asserted-by":"crossref","unstructured":"Chen T. Diciolla M. Kwiatkowska M. Z. and \n      Mereacre A\n  . \n  2011\n  a. Time-bounded verification of ctmcs against real-time specifications. In Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'11). U. Fahrenberg and S. Tripakis Eds. Lecture Notes in Computer Science vol. \n  6919 Springer 26--42.   Chen T. Diciolla M. Kwiatkowska M. Z. and Mereacre A. 2011a. Time-bounded verification of ctmcs against real-time specifications. In Proceedings of the 9 th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'11). U. Fahrenberg and S. Tripakis Eds. Lecture Notes in Computer Science vol. 6919 Springer 26--42.","key":"e_1_2_1_12_1","DOI":"10.1007\/978-3-642-24310-3_4"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1145\/2185632.2185672"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1109\/LICS.2009.21"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.2168\/LMCS-7(1:12)2011"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/210332.210339"},{"volume-title":"Markov Models and Optimization","author":"Davis M. H. A.","unstructured":"Davis , M. H. A. 1993. Markov Models and Optimization . Chapman and Hall . Davis, M. H. A. 1993. Markov Models and Optimization. Chapman and Hall.","key":"e_1_2_1_19_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1007\/978-3-642-31594-7_27"},{"doi-asserted-by":"crossref","unstructured":"Gribaudo M.\n     and \n      Telek M\n  . \n  2007\n  . Fluid models in performance analysis. In Proceedings of the 7th International Conference on Formal Methods for Performance Evaluation (SFM'07). M. Bernardo and J. Hillston Eds. Lecture Notes in Computer Science vol. \n  4486 Springer 271--317.   Gribaudo M. and Telek M. 2007. Fluid models in performance analysis. In Proceedings of the 7 th International Conference on Formal Methods for Performance Evaluation (SFM'07). M. Bernardo and J. Hillston Eds. Lecture Notes in Computer Science vol. 4486 Springer 271--317.","key":"e_1_2_1_21_1","DOI":"10.1007\/978-3-540-72522-0_7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1016\/j.entcs.2010.06.004"},{"volume-title":"Proceedings of the International Conference on Dependable Systems and Networks (DSN'02)","author":"Haverkort B. R.","unstructured":"Haverkort , B. R. , Cloth , L. , Hermanns , H. , Katoen , J.-P. , and Baier , C . 2002. Model checking performability properties . In Proceedings of the International Conference on Dependable Systems and Networks (DSN'02) . IEEE Computer Society, Los Alamitos, CA, 103--112. Haverkort, B. R., Cloth, L., Hermanns, H., Katoen, J.-P., and Baier, C. 2002. Model checking performability properties. In Proceedings of the International Conference on Dependable Systems and Networks (DSN'02). IEEE Computer Society, Los Alamitos, CA, 103--112.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","volume-title":"Accuracy and Stability of Numerical Algorithms","author":"Higham N. J.","unstructured":"Higham , N. J. 2002. Accuracy and Stability of Numerical Algorithms . 2 nd ed. Society for Industrial and Applied Mathematics , Philadelphia, PA . Higham, N. J. 2002. Accuracy and Stability of Numerical Algorithms. 2nd ed. Society for Industrial and Applied Mathematics, Philadelphia, PA.","edition":"2"},{"unstructured":"Horn R. A. and Johnson C. R. 1990. Matrix Analysis. Cambridge University Press.   Horn R. A. and Johnson C. R. 1990. Matrix Analysis. Cambridge University Press.","key":"e_1_2_1_25_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1016\/S0377-2217(97)00028-3"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1109\/RTCSA.2007.53"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1007\/s001650050034"},{"key":"e_1_2_1_29_1","first-page":"87","article-title":"Markoff chains as an aid in the study of markoff processes","volume":"36","author":"Jensen A.","year":"1953","unstructured":"Jensen , A. 1953 . Markoff chains as an aid in the study of markoff processes . Skand. Aktuarietidskrift 36 , 87 -- 91 . Jensen, A. 1953. Markoff chains as an aid in the study of markoff processes. Skand. Aktuarietidskrift 36, 87--91.","journal-title":"Skand. Aktuarietidskrift"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1006\/inco.1998.2774"},{"doi-asserted-by":"crossref","unstructured":"Kwiatkowska M. Norman G. and \n      Parker D\n  . \n  2007\n  . Stochastic model checking. In Proceedings of the 7th International Conference on Formal Methods for Performance Evaluation (SFM'07). M. Bernardo and J. Hillston Eds. Lecture Notes in Computer Science vol. \n  4486 Springer 220--270.   Kwiatkowska M. Norman G. and Parker D. 2007. Stochastic model checking. In Proceedings of the 7 th International Conference on Formal Methods for Performance Evaluation (SFM'07). M. Bernardo and J. Hillston Eds. Lecture Notes in Computer Science vol. 4486 Springer 220--270.","key":"e_1_2_1_31_1","DOI":"10.1007\/978-3-540-72522-0_6"},{"doi-asserted-by":"crossref","unstructured":"Kwiatkowska M. Norman G. and \n      Parker D\n  . \n  2011\n  . PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11). G. Gopalakrishnan and S. Qadeer Eds. Lecture Notes in Computer Science vol. \n  6806 Springer 585--591.   Kwiatkowska M. Norman G. and Parker D. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23 rd International Conference on Computer Aided Verification (CAV'11). G. Gopalakrishnan and S. Qadeer Eds. Lecture Notes in Computer Science vol. 6806 Springer 585--591.","key":"e_1_2_1_32_1","DOI":"10.1007\/978-3-642-22110-1_47"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1145\/504794.504796"},{"doi-asserted-by":"crossref","unstructured":"Li X. Hung D. V. and \n      Zheng T\n  . \n  1997\n  . Checking hybrid automata for linear duration invariants. In Proceedings of the 3rd Asian Computing Science Conference on Advances in Computing Science (ASIAN'97). R. K. Shyamasundar and K. Ueda Eds. Lecture Notes in Computer Science vol. \n  1345 Springer 166--180.   Li X. Hung D. V. and Zheng T. 1997. Checking hybrid automata for linear duration invariants. In Proceedings of the 3 rd Asian Computing Science Conference on Advances in Computing Science (ASIAN'97). R. K. Shyamasundar and K. Ueda Eds. Lecture Notes in Computer Science vol. 1345 Springer 166--180.","key":"e_1_2_1_34_1","DOI":"10.1007\/3-540-63875-X_51"},{"unstructured":"Meyn S. P. and Tweedie R. L. 1996. Markov Chains and Stochastic Stability. Springer.  Meyn S. P. and Tweedie R. L. 1996. Markov Chains and Stochastic Stability. Springer.","key":"e_1_2_1_35_1"},{"volume-title":"Matrix-Geometric Solutions in Stochastic Models: An Algorithmic Approach","author":"Neuts M.","unstructured":"Neuts , M. 1981. Matrix-Geometric Solutions in Stochastic Models: An Algorithmic Approach . John Hopkins University Press . Neuts, M. 1981. Matrix-Geometric Solutions in Stochastic Models: An Algorithmic Approach. John Hopkins University Press.","key":"e_1_2_1_36_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1109\/QEST.2010.10"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.1007\/s00165-005-0062-0"},{"volume-title":"2nd International Workshop on Performability Modeling of Computer and Communication Systems.","author":"Pattipati K. R.","unstructured":"Pattipati , K. R. , Mallubhatla , R. , Gopalakrishna , V. , and Viswanatham , N . 1993. Markov-reward models and hyperbolic systems . In 2nd International Workshop on Performability Modeling of Computer and Communication Systems. Pattipati, K. R., Mallubhatla, R., Gopalakrishna, V., and Viswanatham, N. 1993. Markov-reward models and hyperbolic systems. In 2nd International Workshop on Performability Modeling of Computer and Communication Systems.","key":"e_1_2_1_39_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1109\/43.952737"},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1016\/0166-5316(94)90061-2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_42_1","DOI":"10.1007\/978-3-540-31862-0_22"},{"doi-asserted-by":"publisher","key":"e_1_2_1_43_1","DOI":"10.2168\/LMCS-8(2:17)2012"},{"doi-asserted-by":"publisher","key":"e_1_2_1_44_1","DOI":"10.1007\/978-3-540-85762-4_27"},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94)","volume":"863","author":"Zhou C.","unstructured":"Zhou , C. , Zhang , J. , Yang , L. , and Li , X . 1994. Linear duration invariants . In Proceedings of the 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94) . H. Langmaack, W. P. de Roever, and J. Vytopil, Eds., Lecture Notes in Computer Science , vol. 863 , Springer, 86--109. Zhou, C., Zhang, J., Yang, L., and Li, X. 1994. Linear duration invariants. In Proceedings of the 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94). H. Langmaack, W. P. de Roever, and J. Vytopil, Eds., Lecture Notes in Computer Science, vol. 863, Springer, 86--109."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2528935","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2528935","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:45Z","timestamp":1750231725000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2528935"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":44,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1145\/2528935"],"URL":"https:\/\/doi.org\/10.1145\/2528935","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2013,11]]},"assertion":[{"value":"2012-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}