{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T13:54:26Z","timestamp":1764251666224,"version":"3.41.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2020,10,14]],"date-time":"2020-10-14T00:00:00Z","timestamp":1602633600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2020,10,31]]},"abstract":"<jats:p>We investigate the decidability of model checking logics of time, knowledge, and probability, with respect to two epistemic semantics: the clock and synchronous perfect recall semantics in partially observable discrete-time Markov chains. Decidability results are known for certain restricted logics with respect to these semantics, subject to a variety of restrictions that are either unexplained or involve a longstanding unsolved mathematical problem. We show that mild generalizations of the known decidable cases suffice to render the model checking problem definitively undecidable. In particular, for the synchronous perfect recall semantics, a generalization from temporal operators with finite reach to operators with infinite reach renders model checking undecidable. The case of the clock semantics is closely related to a monadic second-order logic of time and probability that is known to be decidable, except on a set of measure zero. We show that two distinct extensions of this logic make model checking undecidable. One of these involves polynomial combinations of probability terms, the other involves monadic second-order quantification into the scope of probability operators. These results explain some of the restrictions in previous work.<\/jats:p>","DOI":"10.1145\/3409250","type":"journal-article","created":{"date-parts":[[2020,10,14]],"date-time":"2020-10-14T08:27:12Z","timestamp":1602664032000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic"],"prefix":"10.1145","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9243-0571","authenticated-orcid":false,"given":"Ron Van Der","family":"Meyden","sequence":"first","affiliation":[{"name":"UNSW Sydney, Sydney, NSW, Australia"}]},{"given":"Manas K.","family":"Patra","sequence":"additional","affiliation":[{"name":"Central University of Rajasthan, Dist-Ajme, Rajasthan, India"}]}],"member":"320","published-online":{"date-parts":[[2020,10,14]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2014.08.013"},{"volume-title":"Proc. of the Symposium on Logic in Computer Science (LICS). 414--425","author":"Alur R.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl004"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_2_1_5_1","unstructured":"J. Cassaigne V. Halava T. Harju and F. Nicolas. 2014. Tighter undecidability bounds for matrix mortality zero-in-the-corner problems and more. arXiv abs\/1404.0644 (2014).  J. Cassaigne V. Halava T. Harju and F. Nicolas. 2014. Tighter undecidability bounds for matrix mortality zero-in-the-corner problems and more. arXiv abs\/1404.0644 (2014)."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"volume-title":"Proc. of the IEEE Symp. on Foundations of Computer Science (FOCS). 462--467","year":"1989","author":"Condon A.","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","first-page":"1","article-title":"Dynamic epistemic modelling","volume":"0424","author":"Eijck J.N.","year":"2004","journal-title":"CWI. Software Engineering SENE"},{"volume-title":"Proc. of the Int. Symp. on Logical Foundations of Computer Science (LFCS). 195--211","author":"Engelhardt K.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"G. Everest I. Shparlinski A. J. van der Poorten and T. Ward. 2003. Recurrence Sequences. Amer. Math. Soc. Providence RI.  G. Everest I. Shparlinski A. J. van der Poorten and T. Ward. 2003. Recurrence Sequences. Amer. Math. Soc. Providence RI.","DOI":"10.1090\/surv\/104"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/174652.174658"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90060-U"},{"volume-title":"Proc. Conf. on Computer-Aided Verification (CAV). 479--483","author":"Gammie P.","key":"e_1_2_1_14_1"},{"volume-title":"Technical Report 683. Turku Centre for Computer Science","year":"2005","author":"Halava V.","key":"e_1_2_1_16_1"},{"volume-title":"Reasoning About Uncertainty","author":"Halpern J. Y.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"J. Y. Halpern and M. R. Tuttle. 1993. Knowledge probability and adversaries. J. ACM 40 (September 1993) 917--960. Issue 4. DOI:https:\/\/doi.org\/10.1145\/153724.153770  J. Y. Halpern and M. R. Tuttle. 1993. Knowledge probability and adversaries. J. ACM 40 (September 1993) 917--960. Issue 4. DOI:https:\/\/doi.org\/10.1145\/153724.153770","DOI":"10.1145\/153724.153770"},{"volume-title":"Proc. of the Int. Conf. on Principles of Knowledge Representation and Reasoning. 325--334","author":"Halpern J. Y.","key":"e_1_2_1_19_1"},{"volume-title":"Proc. of the Conf. on Theoretical Aspects of Rationality and Knowledge (TARK). 177--186","author":"Huang X.","key":"e_1_2_1_21_1"},{"volume-title":"European Conf. on Artificial Intelligence (ECAI). 549--554","author":"Huang X.","key":"e_1_2_1_22_1"},{"volume-title":"Proc. AAAI Conf. on Artificial Intelligence. 765--771","author":"Huang X.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1516165.1516187"},{"volume-title":"Probability Theory I","author":"Lo\u00e8ve M.","key":"e_1_2_1_26_1"},{"volume-title":"Proc. Conf. on Computer-Aided Verification (CAV). 682--688","author":"Lomuscio A.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"O. Maler D. Nickovic and A. Pnueli. 2008. Checking temporal properties of discrete timed and continuous behaviors. In Pillars of Computer Science Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. 475--505.  O. Maler D. Nickovic and A. Pnueli. 2008. Checking temporal properties of discrete timed and continuous behaviors. In Pillars of Computer Science Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday. 475--505.","DOI":"10.1007\/978-3-540-78127-1_26"},{"volume-title":"Hilbert\u2019s Tenth Problem","author":"Matiyasevich Y. V.","key":"e_1_2_1_29_1"},{"volume-title":"Proc. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 432--445","author":"van der Meyden R.","key":"e_1_2_1_30_1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026181001368"},{"volume-title":"Proc. ACM-SIAM Symp. on Discrete Algorithms. 366--379","author":"Ouaknine J.","key":"e_1_2_1_32_1"},{"volume-title":"Introduction to Probabilistic Automata","author":"Paz A.","key":"e_1_2_1_33_1"},{"volume":"23","volume-title":"Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. CRM Monograph Series","author":"Rutten J.","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1949.tb00928.x"},{"key":"e_1_2_1_36_1","unstructured":"T. Skolem. 1934. Ein Verfahren zur Behandlung Gewisser Exponentialer Gleichungen und Diophatischer Gleighungen. In Comptes Rendus du Congr\u00e8s des Math\u00e9maticiens Scandinaves.  T. Skolem. 1934. Ein Verfahren zur Behandlung Gewisser Exponentialer Gleichungen und Diophatischer Gleighungen. In Comptes Rendus du Congr\u00e8s des Math\u00e9maticiens Scandinaves."},{"edition":"2","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"Tarski A.","key":"e_1_2_1_37_1"},{"key":"e_1_2_1_38_1","first-page":"63","article-title":"The distance between terms of an algebraic recurrence sequence","volume":"349","author":"Tijdeman R.","year":"1984","journal-title":"Journal f\u00fcr die Reine und Angewandte Mathematik"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3409250","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3409250","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:32Z","timestamp":1750197692000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3409250"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,14]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,10,31]]}},"alternative-id":["10.1145\/3409250"],"URL":"https:\/\/doi.org\/10.1145\/3409250","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2020,10,14]]},"assertion":[{"value":"2019-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-10-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}