{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:32Z","timestamp":1750306532196,"version":"3.41.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,12,12]],"date-time":"2014-12-12T00:00:00Z","timestamp":1418342400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["SFRH\/BD\/73315\/2010 and SFRH\/BD\/51846\/2012"],"award-info":[{"award-number":["SFRH\/BD\/73315\/2010 and SFRH\/BD\/51846\/2012"]}],"id":[{"id":"10.13039\/501100001871","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":[[2015,3]]},"abstract":"<jats:p>When studying probabilistic dynamical systems, temporal logic has typically been used to analyze path properties. Recently, there has been some interest in analyzing the dynamical evolution of state probabilities of these systems. In this article, we show that verifying linear temporal properties concerning the state evolution induced by a Markov chain is equivalent to the decidability of the Skolem problem -- a long-standing open problem in Number Theory. However, from a practical point of view, usually it is enough to check properties up to some acceptable error bound \u03f5. We show that an approximate version of the Skolem problem is decidable, and that it can be applied to verify, up to arbitrarily small \u03f5, linear temporal properties of the state evolution induced by a Markov chain.<\/jats:p>","DOI":"10.1145\/2666772","type":"journal-article","created":{"date-parts":[[2014,12,16]],"date-time":"2014-12-16T13:39:54Z","timestamp":1418737194000},"page":"1-17","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Decidability of Approximate Skolem Problem and Applications to Logical Verification of Dynamical Properties of Markov Chains"],"prefix":"10.1145","volume":"16","author":[{"given":"M.","family":"Biscaia","sequence":"first","affiliation":[{"name":"Instituto de Telecomunica\u00e7\u00f5es, Universidade de Lisboa, Lisbon"}]},{"given":"D.","family":"Henriques","sequence":"additional","affiliation":[{"name":"Instituto de Telecomunica\u00e7\u00f5es, Universidade de Lisboa, Lisbon, Carnegie Mellon University, Pittsburgh, PA"}]},{"given":"P.","family":"Mateus","sequence":"additional","affiliation":[{"name":"Instituto de Telecomunica\u00e7\u00f5es, Universidade de Lisboa, Lisbon"}]}],"member":"320","published-online":{"date-parts":[[2014,12,12]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"M. Agrawal S. Akshay B. Genest and P. S. Thiagarajan. 2014. Approximate verification of the symbolic dynamics of Markov chains. Journal of the ACM (JACM) Accepted for publication 2014.  M. Agrawal S. Akshay B. Genest and P. S. Thiagarajan. 2014. Approximate verification of the symbolic dynamics of Markov chains. Journal of the ACM (JACM) Accepted for publication 2014."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.17"},{"key":"e_1_2_1_3_1","volume-title":"ICALP. Lecture Notes in Computer Science","volume":"1256","author":"Baier C.","unstructured":"C. Baier , E. M. Clarke , V. Hartonas-Garmhausen , M. Z. Kwiatkowska , and M. Ryan . 1997. Symbolic model checking for probabilistic processes . In ICALP. Lecture Notes in Computer Science , Vol. 1256 . Springer, 430--440. C. Baier, E. M. Clarke, V. Hartonas-Garmhausen, M. Z. Kwiatkowska, and M. Ryan. 1997. Symbolic model checking for probabilistic processes. In ICALP. Lecture Notes in Computer Science, Vol. 1256. Springer, 430--440."},{"volume-title":"Principles of Model Checking","author":"Baier C.","key":"e_1_2_1_4_1","unstructured":"C. Baier and J.-P. Katoen . 2008. Principles of Model Checking . MIT Press . I--XVII. C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press. I--XVII."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92687-0_4"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl004"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.24033\/bsmf.1823"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.25"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"F. Ciesinski and M. Gr\u00f6\u00dfer. 2004. On probabilistic computation tree logic. In Validation of Stochastic Systems. 147--188.  F. Ciesinski and M. Gr\u00f6\u00dfer. 2004. On probabilistic computation tree logic. In Validation of Stochastic Systems. 147--188.","DOI":"10.1007\/978-3-540-24611-4_5"},{"key":"e_1_2_1_10_1","unstructured":"T. H. Cormen C. E. Leiserson R. L. Rivest and C. Stein. 2001. Introduction to Algorithms (2nd ed.). MIT Press and McGraw-Hill.   T. H. Cormen C. E. Leiserson R. L. Rivest and C. Stein. 2001. Introduction to Algorithms (2nd ed.). MIT Press and McGraw-Hill."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2009.11"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.35"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska G. Norman and D. Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In CAV\u201911 (LNCS) Vol. 6806. Springer 585--591.   M. Kwiatkowska G. Norman and D. Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In CAV\u201911 (LNCS) Vol. 6806. Springer 585--591.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_14_1","volume-title":"ICFEM (LNCS)","volume":"3308","author":"Kwon Y.","unstructured":"Y. Kwon and G. Agha . 2004. Linear inequality LTL (iLTL): A model checker for discrete time Markov chains . In ICFEM (LNCS) , Vol. 3308 . Springer, 194--208. Y. Kwon and G. Agha. 2004. Linear inequality LTL (iLTL): A model checker for discrete time Markov chains. In ICFEM (LNCS), Vol. 3308. Springer, 194--208."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100030966"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/2406808.2406811"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"J. Ouaknine and J. Worrell. 2013. Positivity problems for low-order linear recurrence sequences. Computing Research Repository abs\/1307.2779 (2013).  J. Ouaknine and J. Worrell. 2013. Positivity problems for low-order linear recurrence sequences. Computing Research Repository abs\/1307.2779 (2013).","DOI":"10.1137\/1.9781611973402.27"},{"key":"e_1_2_1_18_1","first-page":"163","article-title":"Ein Verfahren zur Behandlung gewisser exponentialer Gleichungen und diophantischer Gleichungen. 8. Skand. Mat. Kongr","volume":"1934","author":"Skolem T.","year":"1934","unstructured":"T. Skolem . 1934 . Ein Verfahren zur Behandlung gewisser exponentialer Gleichungen und diophantischer Gleichungen. 8. Skand. Mat. Kongr ., Stockholm , 1934 , 163 -- 188 . T. Skolem. 1934. Ein Verfahren zur Behandlung gewisser exponentialer Gleichungen und diophantischer Gleichungen. 8. Skand. Mat. Kongr., Stockholm, 1934, 163--188.","journal-title":"Stockholm"},{"volume-title":"ARTS. Lecture Notes in Computer Science","author":"Vardi M. Y.","key":"e_1_2_1_19_1","unstructured":"M. Y. Vardi . 1999. Probabilistic linear-time model checking: An overview of the automata-theoretic approach . In 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 ARTS. Lecture Notes in Computer Science, Vol. 1601. Springer, 265--276."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2666772","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2666772","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:12:15Z","timestamp":1750227135000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2666772"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,12]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["10.1145\/2666772"],"URL":"https:\/\/doi.org\/10.1145\/2666772","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,12,12]]},"assertion":[{"value":"2014-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-12-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}