{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T11:37:45Z","timestamp":1770982665162,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540249986","type":"print"},{"value":"9783540318569","type":"electronic"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31856-9_12","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T18:06:19Z","timestamp":1267553179000},"page":"145-157","source":"Crossref","is-referenced-by-count":41,"title":["On the Decidability of Temporal Properties of Probabilistic Pushdown Automata"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Br\u00e1zdil","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton\u00edn","family":"Ku\u010dera","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Old\u0159ich","family":"Stra\u017eovsk\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/3-540-44618-4_24","volume-title":"CONCUR 2000 - Concurrency Theory","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., Baier, C., Iyer, S.P., Jonsson, B.: Reasoning about probabilistic channel systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 320\u2013330. Springer, Heidelberg (2000)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-36576-1_3","volume-title":"Foundations of Software Science and Computational Structures","author":"P.A. Abdulla","year":"2003","unstructured":"Abdulla, P.A., Rabinovich, A.: Verification of probabilistic systems with faulty communication. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 39\u201353. Springer, Heidelberg (2003)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-44585-4_18","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 207\u2013220. Springer, Heidelberg (2001)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/3-540-48778-6_3","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"C. Baier","year":"1999","unstructured":"Baier, C., Engelen, B.: Establishing qualitative properties for probabilistic lossy channel systems: an algorithmic approach. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 34\u201352. Springer, Heidelberg (1999)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-36576-1_8","volume-title":"Foundations of Software Science and Computational Structures","author":"N. Bertrand","year":"2003","unstructured":"Bertrand, N., Schnoebelen, P.: Model checking lossy channel systems is probably decidable. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 120\u2013135. Springer, Heidelberg (2003)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-28644-8_13","volume-title":"CONCUR 2004 - Concurrency Theory","author":"T. Br\u00e1zdil","year":"2004","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Stra\u017eovsk\u00fd, O.: Deciding probabilistic bisimilarity over infinite-state probabilistic systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 193\u2013208. Springer, Heidelberg (2004)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Stra\u017eovsk\u00fd, O.: On the decidability of temporal properties of probabilistic pushdown automata. Technical report FIMU-RS-2005-01, Faculty of Informatics, Masaryk University (2005)","DOI":"10.1007\/978-3-540-31856-9_12"},{"key":"12_CR9","first-page":"460","volume-title":"Proceedings of STOC 1988","author":"J. Canny","year":"1988","unstructured":"Canny, J.: Some algebraic and geometric computations in PSPACE. In: Proceedings of STOC 1988, pp. 460\u2013467. ACM Press, New York (1988)"},{"issue":"4","key":"12_CR10","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. JACM\u00a042(4), 857\u2013907 (1995)","journal-title":"JACM"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-39813-4_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J.M. Couvreur","year":"2003","unstructured":"Couvreur, J.M., Saheb, N., Sutre, G.: An optimal automata approach to LTL model checking of probabilistic systems. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, pp. 361\u2013375. Springer, Heidelberg (2003)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 14\u201330. Springer, Heidelberg (1999)"},{"key":"12_CR13","first-page":"12","volume-title":"Proceedings of LICS 2004","author":"J. Esparza","year":"2004","unstructured":"Esparza, J., Ku\u010dera, A., Mayr, R.: Model-checking probabilistic pushdown automata. In: Proceedings of LICS 2004, pp. 12\u201321. IEEE, Los Alamitos (2004)"},{"issue":"2","key":"12_CR14","first-page":"355","volume":"186","author":"J. Esparza","year":"2003","unstructured":"Esparza, J., Ku\u010dera, A., Schwoon, S.: Model-checking LTL with regular valuations for pushdown systems. I&C\u00a0186(2), 355\u2013376 (2003)","journal-title":"I&C"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Etessami, K., Yannakakis, M.: Algorithmic verification of recursive probabilistic systems. Technical Report, School of Informatics, U. of Edinburgh (2005)","DOI":"10.1007\/978-3-540-31980-1_17"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-31856-9_28","volume-title":"STACS 2005","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of non-linear equations. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol.\u00a03404, pp. 340\u2013352. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"12_CR17","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0747-7171(88)80006-3","volume":"5","author":"D. Grigoriev","year":"1988","unstructured":"Grigoriev, D.: Complexity of deciding Tarski algebra. Journal of Symbolic Computation\u00a05(1-2), 65\u2013108 (1988)","journal-title":"Journal of Symbolic Computation"},{"key":"12_CR18","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06, 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"12_CR19","first-page":"1","volume-title":"Proceedings of POPL 1984","author":"S. Hart","year":"1984","unstructured":"Hart, S., Sharir, M.: Probabilistic temporal logic for finite and bounded models. In: Proceedings of POPL 1984, pp. 1\u201313. ACM Press, New York (1984)"},{"key":"12_CR20","first-page":"111","volume-title":"Proceedings of LICS 1997","author":"M. Huth","year":"1997","unstructured":"Huth, M., Kwiatkowska, M.Z.: Quantitative analysis and model checking. In: Proceedings of LICS 1997, pp. 111\u2013122. IEEE, Los Alamitos (1997)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/BFb0030633","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"S.P. Iyer","year":"1997","unstructured":"Iyer, S.P., Narasimha, M.: Probabilistic lossy channel systems. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 667\u2013681. Springer, Heidelberg (1997)"},{"key":"12_CR22","first-page":"351","volume-title":"Proceedings of LICS 2003","author":"M.Z. Kwiatkowska","year":"2003","unstructured":"Kwiatkowska, M.Z.: Model checking for probability and time: from theory to practice. In: Proceedings of LICS 2003, pp. 351\u2013360. IEEE, Los Alamitos (2003)"},{"key":"12_CR23","first-page":"165","volume":"53","author":"D. Lehman","year":"1982","unstructured":"Lehman, D., Shelah, S.: Reasoning with time and chance. I&C\u00a053, 165\u2013198 (1982)","journal-title":"I&C"},{"key":"12_CR24","volume-title":"Computation: Finite and Infinite Machines","author":"M.L. Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs (1967)"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1008","DOI":"10.1007\/3-540-45061-0_78","volume-title":"Automata, Languages and Programming","author":"A. Rabinovich","year":"2003","unstructured":"Rabinovich, A.: Quantitative analysis of probabilistic lossy channel systems. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 1008\u20131021. Springer, Heidelberg (2003)"},{"key":"12_CR26","first-page":"327","volume-title":"Proceedings of FOCS 1985","author":"M. Vardi","year":"1985","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of FOCS 1985, pp. 327\u2013338. IEEE, Los Alamitos (1985)"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-44450-5_10","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Science","author":"I. Walukiewicz","year":"2000","unstructured":"Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol.\u00a01974, pp. 127\u2013138. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","STACS 2005"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31856-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T17:30:03Z","timestamp":1558287003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31856-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540249986","9783540318569"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31856-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}