{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:00:58Z","timestamp":1779087658242,"version":"3.51.4"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,3,2]],"date-time":"2015-03-02T00:00:00Z","timestamp":1425254400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Department of Science and Technology, India","award":["IFA12-MA-17"],"award-info":[{"award-number":["IFA12-MA-17"]}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-13-BS02-0011-01, ANR-2010-BLAN-0317"],"award-info":[{"award-number":["ANR-13-BS02-0011-01, ANR-2010-BLAN-0317"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001459","name":"Ministry of Education - Singapore","doi-asserted-by":"publisher","award":["MOE2011-T2-2-012"],"award-info":[{"award-number":["MOE2011-T2-2-012"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2015,3,2]]},"abstract":"<jats:p>\n            A finite-state Markov chain\n            <jats:italic>M<\/jats:italic>\n            can be regarded as a linear transform operating on the set of probability distributions over its node set. The iterative applications of\n            <jats:italic>M<\/jats:italic>\n            to an initial probability distribution \u03bc\n            <jats:sub>0<\/jats:sub>\n            will generate a trajectory of probability distributions. Thus, a set of initial distributions will induce a set of trajectories. It is an interesting and useful task to analyze the dynamics of\n            <jats:italic>M<\/jats:italic>\n            as defined by this set of trajectories. The novel idea here is to carry out this task in a\n            <jats:italic>symbolic<\/jats:italic>\n            framework. Specifically, we discretize the probability value space [0,1] into a finite set of intervals\n            <jats:italic>I<\/jats:italic>\n            = {\n            <jats:italic>I<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            ,\n            <jats:italic>\n              I\n              <jats:sub>2<\/jats:sub>\n            <\/jats:italic>\n            ,...,\n            <jats:italic>\n              I\n              <jats:sub>m<\/jats:sub>\n            <\/jats:italic>\n            }. A concrete probability distribution \u03bc over the node set {1, 2,...,\n            <jats:italic>n<\/jats:italic>\n            } of\n            <jats:italic>M<\/jats:italic>\n            is then symbolically represented as\n            <jats:italic>D<\/jats:italic>\n            , a tuple of intervals drawn from\n            <jats:italic>I<\/jats:italic>\n            where the\n            <jats:italic>i<\/jats:italic>\n            th component of\n            <jats:italic>D<\/jats:italic>\n            will be the interval in which \u03bc(\n            <jats:italic>i<\/jats:italic>\n            ) falls. The set of discretized distributions\n            <jats:italic>D<\/jats:italic>\n            is a finite alphabet. Hence, the trajectory, generated by repeated applications of\n            <jats:italic>M<\/jats:italic>\n            to an initial distribution, will induce an infinite string over this alphabet. Given a set of initial distributions, the symbolic dynamics of\n            <jats:italic>M<\/jats:italic>\n            will then consist of a language of infinite strings\n            <jats:italic>L<\/jats:italic>\n            over the alphabet\n            <jats:italic>D<\/jats:italic>\n            .\n          <\/jats:p>\n          <jats:p>\n            Our main goal is to verify whether\n            <jats:italic>L<\/jats:italic>\n            meets a specification given as a linear-time temporal logic formula \u03c6. In our logic, an atomic proposition will assert that the current probability of a node falls in the interval\n            <jats:italic>I<\/jats:italic>\n            from\n            <jats:italic>I<\/jats:italic>\n            . If\n            <jats:italic>L<\/jats:italic>\n            is an \u03c9-regular language, one can hope to solve our model-checking problem (whether\n            <jats:italic>L<\/jats:italic>\n            \u22a7 \u03c6?) using standard techniques. However, we show that, in general, this is not the case. Consequently, we develop the notion of an \u03f5-approximation, based on the transient and long-term behaviors of the Markov chain\n            <jats:italic>M<\/jats:italic>\n            . Briefly, the symbolic trajectory \u03be' is an \u03f5-approximation of the symbolic trajectory \u03be iff (1) \u03be' agrees with \u03be during its transient phase; and (2) both \u03be and \u03be' are within an \u03f5-neighborhood at all times after the transient phase. Our main results are that one can effectively check whether (i) for each infinite word in\n            <jats:italic>L<\/jats:italic>\n            , at least one of its \u03f5-approximations satisfies the given specification; (ii) for each infinite word in\n            <jats:italic>L<\/jats:italic>\n            , all its \u03f5-approximations satisfy the specification. These verification results are strong in that they apply to all finite state Markov chains.\n          <\/jats:p>","DOI":"10.1145\/2629417","type":"journal-article","created":{"date-parts":[[2015,3,3]],"date-time":"2015-03-03T14:08:19Z","timestamp":1425391699000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Approximate Verification of the Symbolic Dynamics of Markov Chains"],"prefix":"10.1145","volume":"62","author":[{"given":"Manindra","family":"Agrawal","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Kanpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Akshay","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Bombay, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Blaise","family":"Genest","sequence":"additional","affiliation":[{"name":"CNRS, UMR IRISA, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. S.","family":"Thiagarajan","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,3,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.17"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/646251.685846"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1059816.1059819"},{"key":"e_1_2_1_5_1","first-page":"482","article-title":"Comparative branching-time semantics for Markov chains. In Proceedings of CONCUR'03","volume":"2761","author":"Baier C.","year":"2003","unstructured":"C. Baier , H. Hermanns , J.-P. Katoen , and V. Wolf . 2003 . Comparative branching-time semantics for Markov chains. In Proceedings of CONCUR'03 . Lecture Notes in Computer Science , vol. 2761 , Spring er, 482 -- 497 . C. Baier, H. Hermanns, J.-P. Katoen, and V. Wolf. 2003. Comparative branching-time semantics for Markov chains. In Proceedings of CONCUR'03. Lecture Notes in Computer Science, vol. 2761, Springer, 482--497.","journal-title":"Lecture Notes in Computer Science"},{"key":"e_1_2_1_6_1","volume-title":"Principles of Model Checking","author":"Baier C.","unstructured":"C. Baier and J.-P. Katoen . 2008. Principles of Model Checking . MIT Press . C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/647852.737551"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_3"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the International Congress for Logic, Methodology and Philosophy of Science","author":"B\u00fcchi J.","year":"1962","unstructured":"J. B\u00fcchi . 1962 . On a decision method in restricted second order arithmetic . In Proceedings of the International Congress for Logic, Methodology and Philosophy of Science . Stanford University Press, 1--11. J. B\u00fcchi. 1962. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress for Logic, Methodology and Philosophy of Science. Stanford University Press, 1--11."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.05.010"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the International Conference on Mathematical Foundations of Programming Semantics. Springer, 554--566","author":"Calbrix H.","unstructured":"H. Calbrix , M. Nivat , and A. Podelski . 1994. Ultimately periodic words of rational omega-languages . In Proceedings of the International Conference on Mathematical Foundations of Programming Semantics. Springer, 554--566 . H. Calbrix, M. Nivat, and A. Podelski. 1994. Ultimately periodic words of rational omega-languages. In Proceedings of the International Conference on Mathematical Foundations of Programming Semantics. Springer, 554--566."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.22"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792825"},{"key":"e_1_2_1_14_1","volume-title":"Theory of Algebraic Integers","author":"Dedekind R.","unstructured":"R. Dedekind . 1996. Theory of Algebraic Integers . Cambridge Mathematical Library, Cambridge University Press . R. Dedekind. 1996. Theory of Algebraic Integers. Cambridge Mathematical Library, Cambridge University Press."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/2022896.2022919"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2009.42"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_19_1","unstructured":"G. Hardy and E. Wright. 1960. An Introduction to the Theory of Numbers. Clarendon Press Oxford.  G. Hardy and E. Wright. 1960. An Introduction to the Theory of Numbers. Clarendon Press Oxford."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788803"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of LICS. IEEE Computer Society Press, 111--122","author":"Huth M.","unstructured":"M. Huth and M. Z. Kwiatkowska . 1997. Quantitative analysis and model checking . In Proceedings of LICS. IEEE Computer Society Press, 111--122 . M. Huth and M. Z. Kwiatkowska. 1997. Quantitative analysis and model checking. In Proceedings of LICS. IEEE Computer Society Press, 111--122."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of LICS. IEEE Computer Society Press. 266--277","author":"Jonsson B.","unstructured":"B. Jonsson and K. G. Larsen . 1991. Specification and refinement of probabilistic processes . In Proceedings of LICS. IEEE Computer Society Press. 266--277 . B. Jonsson and K. G. Larsen. 1991. Specification and refinement of probabilistic processes. In Proceedings of LICS. IEEE Computer Society Press. 266--277."},{"key":"e_1_2_1_23_1","unstructured":"J. G. Kemeny and J. L. Snell. 1960. Finite Markov Chains. Princeton University Press.  J. G. Kemeny and J. L. Snell. 1960. Finite Markov Chains. Princeton University Press."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.35"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014745904458"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032352"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_21"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.80"},{"key":"e_1_2_1_29_1","unstructured":"S. Lalley. 2010. Course notes: Basic Markov chain theory. http:\/\/galton.uchicago.edu\/~lalley\/Courses\/312\/MarkovChains.pdf.  S. Lalley. 2010. Course notes: Basic Markov chain theory. http:\/\/galton.uchicago.edu\/~lalley\/Courses\/312\/MarkovChains.pdf."},{"key":"e_1_2_1_30_1","volume-title":"Algebraic Number Theory (Graduate Texts in Mathematics)","author":"Lang S.","unstructured":"S. Lang . 1994. Algebraic Number Theory (Graduate Texts in Mathematics) . Springer . S. Lang. 1994. Algebraic Number Theory (Graduate Texts in Mathematics). Springer."},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"D. Lind and B. Marcus. 1995. An Introduction to Symbolic Dynamics and Coding. Cambridge University Press Cambridge UK.   D. Lind and B. Marcus. 1995. An Introduction to Symbolic Dynamics and Coding. Cambridge University Press Cambridge UK.","DOI":"10.1017\/CBO9780511626302"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"S. Meyn and R. Tweedie. 1993. Markov Chains and Stochastic Stability. Springer-Verlag London.   S. Meyn and R. Tweedie. 1993. Markov Chains and Stochastic Stability. Springer-Verlag London.","DOI":"10.1007\/978-1-4471-3267-7"},{"key":"e_1_2_1_33_1","volume-title":"Performance Analysis of Communications Networks and Systems","author":"Mieghem P. V.","unstructured":"P. V. Mieghem . 2006. Performance Analysis of Communications Networks and Systems . Cambridge University Press . P. V. Mieghem. 2006. Performance Analysis of Communications Networks and Systems. Cambridge University Press."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.2307\/2371264"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810633"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33512-9_3"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0024-3795(02)00414-7"},{"key":"e_1_2_1_38_1","series-title":"Springer Series in Statistics","volume-title":"Non-Negative Matrices and Markov Chains","author":"Seneta E.","unstructured":"E. Seneta . 1981. Non-Negative Matrices and Markov Chains . Springer Series in Statistics . Springer . E. Seneta. 1981. Non-Negative Matrices and Markov Chains. Springer Series in Statistics. Springer."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2009.06.007"},{"key":"e_1_2_1_40_1","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"Tarski A.","unstructured":"A. Tarski . 1951. A Decision Method for Elementary Algebra and Geometry . University of California Press. A. Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(68)90360-4"},{"key":"e_1_2_1_42_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of ARTS","author":"Vardi M. Y.","unstructured":"M. Y. Vardi . 1999. Probabilistic linear-time model checking: An overview of the automata-theoretic approach . In Proceedings of ARTS . Lecture Notes in Computer Science , vol. 1601 , Springer , 265--276. M. Y. Vardi. 1999. Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In Proceedings of ARTS. Lecture Notes in Computer Science, vol. 1601, Springer, 265--276."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0888-613X(00)00032-3"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02230720"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1186\/1752-0509-4-42"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629417","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629417","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:30Z","timestamp":1750231170000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629417"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,2]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3,2]]}},"alternative-id":["10.1145\/2629417"],"URL":"https:\/\/doi.org\/10.1145\/2629417","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,2]]},"assertion":[{"value":"2013-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}