{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:26:05Z","timestamp":1777519565635,"version":"3.51.4"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2007,11,8]],"date-time":"2007-11-08T00:00:00Z","timestamp":1194480000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We consider qualitative and quantitative verification problems for\ninfinite-state Markov chains. We call a Markov chain decisive w.r.t. a given\nset of target states F if it almost certainly eventually reaches either F or a\nstate from which F can no longer be reached. While all finite Markov chains are\ntrivially decisive (for every set F), this also holds for many classes of\ninfinite Markov chains. Infinite Markov chains which contain a finite attractor\nare decisive w.r.t. every set F. In particular, this holds for probabilistic\nlossy channel systems (PLCS). Furthermore, all globally coarse Markov chains\nare decisive. This class includes probabilistic vector addition systems (PVASS)\nand probabilistic noisy Turing machines (PNTM). We consider both safety and\nliveness problems for decisive Markov chains, i.e., the probabilities that a\ngiven set of states F is eventually reached or reached infinitely often,\nrespectively. 1. We express the qualitative problems in abstract terms for\ndecisive Markov chains, and show an almost complete picture of its decidability\nfor PLCS, PVASS and PNTM. 2. We also show that the path enumeration algorithm\nof Iyer and Narasimha terminates for decisive Markov chains and can thus be\nused to solve the approximate quantitative safety problem. A modified variant\nof this algorithm solves the approximate quantitative liveness problem. 3.\nFinally, we show that the exact probability of (repeatedly) reaching F cannot\nbe effectively expressed (in a uniform way) in Tarski-algebra for either PLCS,\nPVASS or (P)NTM.<\/jats:p>","DOI":"10.2168\/lmcs-3(4:7)2007","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T13:13:37Z","timestamp":1212498817000},"source":"Crossref","is-referenced-by-count":20,"title":["Decisive Markov Chains"],"prefix":"10.46298","volume":"Volume 3, Issue 4","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noomene Ben","family":"Henda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Mayr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2007,11,8]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/867\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/867\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:58:07Z","timestamp":1681243087000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/867"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11,8]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-3(4:7)2007","relation":{"is-same-as":[{"id-type":"arxiv","id":"0706.2585","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0706.2585","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1145\/2933575.2934574","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,11,8]]},"article-number":"867"}}