{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T11:14:01Z","timestamp":1753182841405,"version":"3.28.0"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1109\/lics.2004.1319596","type":"proceedings-article","created":{"date-parts":[[2004,11,13]],"date-time":"2004-11-13T00:14:14Z","timestamp":1100304854000},"page":"12-21","source":"Crossref","is-referenced-by-count":49,"title":["Model checking probabilistic pushdown automata"],"prefix":"10.1109","author":[{"given":"J.","family":"Esparza","sequence":"first","affiliation":[]},{"given":"A.","family":"Kucera","sequence":"additional","affiliation":[]},{"given":"R.","family":"Mayr","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614940"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/800057.808660"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00139-1"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80006-3"},{"key":"13","first-page":"232","article-title":"Efficient algorithms for model checking pushdown systems","volume":"1855","author":"esparza","year":"2000","journal-title":"Proceedings of CAV 2000 Vol 1855 of Lecture Notes in Computer Science"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319596"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"12","first-page":"361","article-title":"An optimal automata approach to LTL model checking of probabilistic systems","volume":"2850","author":"couvreur","year":"2003","journal-title":"Proceedings of LPAR 2003 Vol 2850 of Lecture Notes in Computer Science"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705645"},{"key":"20","first-page":"667","article-title":"Probabilistic lossy channel systems","volume":"1214","author":"lyer","year":"1997","journal-title":"Proc TAPSOFT 97 Lecture Notes in Computer Science 1214"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)91022-1"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00059-0"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_78"},{"key":"25","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","author":"tarski","year":"1951","journal-title":"A decision method for elementary algebra and geometry"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2894"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.3115\/1034678.1034759"},{"key":"2","first-page":"39","article-title":"Verification of probabilistic systems with faulty communication","volume":"2620","author":"abdulla","year":"2003","journal-title":"Proceedings of FoSSaCS 2003 Vol 2620 of Lecture Notes in Computer Science"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21950"},{"key":"1","first-page":"320","article-title":"Reasoning about probabilistic channel systems","volume":"1877","author":"abdulla","year":"2000","journal-title":"Proceedings of CONCUR 2000 Vol 1877 of Lecture Notes in Computer Science"},{"key":"7","first-page":"34","article-title":"Establishing qualitative properties for probabilistic lossy channel systems: An algorithmic approach","volume":"1601","author":"baier","year":"1999","journal-title":"Proceedings of 5th International AMAST Workshop on Real-time and Probabilistic Systems (ARTS'99) Vol 1601 of Lecture Notes in Computer Science"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624193"},{"key":"5","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","article-title":"It usually works: The temporal logic of stochastic systems","volume":"939","author":"aziz","year":"1995","journal-title":"Proceedings of CAV'95 Vol 939 of Lecture Notes in Computer Science"},{"key":"4","first-page":"207","article-title":"Analysis of recursive state machines","volume":"2102","author":"alur","year":"2001","journal-title":"Proceedings of CAV 2001 Vol 2102 of Lecture Notes in Computer Science"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63165-8_198"},{"key":"8","first-page":"120","article-title":"Model checking lossy channel systems is probably decidable","volume":"2620","author":"bertrand","year":"2003","journal-title":"Proceedings of FoSSaCS 2003 Vol 2620 of Lecture Notes in Computer Science"}],"event":{"name":"Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.","start":{"date-parts":[[2004,7,17]]},"location":"Turku, Finland","end":{"date-parts":[[2004,7,17]]}},"container-title":["Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9221\/29239\/01319596.pdf?arnumber=1319596","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,28]],"date-time":"2021-06-28T09:05:15Z","timestamp":1624871115000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1319596\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/lics.2004.1319596","relation":{},"subject":[],"published":{"date-parts":[[2004]]}}}