{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:40:03Z","timestamp":1737006003459,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48778-6_3","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T10:18:07Z","timestamp":1178014687000},"page":"34-52","source":"Crossref","is-referenced-by-count":20,"title":["Establishing Qualitative Properties for Probabilistic Lossy Channel Systems"],"prefix":"10.1007","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bettina","family":"Engelen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"3_CR1","first-page":"305","volume":"1427","author":"P. Abdulla","year":"1998","unstructured":"P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. LNCS, 1427:305\u2013318, 1998.","journal-title":"LNCS"},{"key":"3_CR2","first-page":"160","volume":"127","author":"P. Abdulla","year":"1993","unstructured":"P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Proc. LICS\u201993, pages 160\u2013170, 1993. The full version with the same title has been published in Information and Computation, 127:91\u2013101, 1996.","journal-title":"Information and Computation"},{"key":"3_CR3","first-page":"316","volume":"820","author":"P. Abdulla","year":"1994","unstructured":"P. Abdulla and B. Jonsson. Undecidable verification problems for programs with unreliable channels. LNCS, 820:316\u2013327, 1994. The full version with the same title has been published in Information and Computation, 130:71\u201390, 1996.","journal-title":"LNCS"},{"key":"3_CR4","first-page":"333","volume":"962","author":"P. Abdulla","year":"1995","unstructured":"P. Abdulla and M. Kindahl. Decidability of simulation and bisimulation between lossy channel systems and finite state systems. LNCS, 962:333\u2013347, 1995.","journal-title":"LNCS"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"P. Abdulla, M. Kindahl, and D. Peled. An improved search strategy for lossy channel systems. In PSTV\/FORTE. Chapman-Hall, 1997.","DOI":"10.1007\/978-0-387-35271-8_16"},{"key":"3_CR6","first-page":"155","volume":"939","author":"A. Aziz","year":"1995","unstructured":"A. Aziz, V. Singhal, R. Brayton, and A. Sangiovanni-Vincentelli. It usually works: The temporal logic of stochastic systems. Proc. CAV\u201995, 939:155\u2013165, 1995.","journal-title":"Proc. CAV\u201995"},{"key":"3_CR7","first-page":"472","volume":"630","author":"J. Baeten","year":"1992","unstructured":"J. Baeten, J. Bergstra, and S. Smolka. Axiomatizing probabilistic processes: ACP with generative probabilities (extended abstract). CONCUR\u201992, 630:472\u2013485, 1992. The full version with the same title has been published in Information and Computation, 122:234\u2013255, 1995.","journal-title":"CONCUR\u201992"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M. Browne","year":"1988","unstructured":"M. Browne, E. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115\u2013131, 1988.","journal-title":"Theoretical Computer Science"},{"key":"3_CR9","first-page":"499","volume":"1026","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. LNCS, 1026:499\u2013513, 1995.","journal-title":"LNCS"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"C. Baier, B. Engelen, and M. Roggenbach. Establishing Qualitative Properties for Probabilistic Lossy Channel Systems. Technical Report 3\/99, Universit\u00e4t Mannheim, Fakult\u00e4t f\u00fcr Mathematik und Informatik, 1999.","DOI":"10.1007\/3-540-48778-6_3"},{"key":"3_CR11","first-page":"119","volume":"1254","author":"C. Baier","year":"1997","unstructured":"C. Baier and H. Hermanns. Weak bisimulation for fully probabilistic processes. LNCS, 1254:119\u2013130, 1997.","journal-title":"LNCS"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125\u2013155, 1998.","journal-title":"Distributed Computing"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"A. Bouajjani and R. Mayr. Model checking lossy vector addition systems. 1998. To appear in Proc. STACS\u201999, LNCS.","DOI":"10.1007\/3-540-49116-3_30"},{"key":"3_CR14","unstructured":"L. Breiman. Probability. Addison-Wesley Publishing Company, 1968."},{"issue":"5","key":"3_CR15","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"K. Bartlett","year":"1969","unstructured":"K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5):260\u2013261, 1969.","journal-title":"Communications of the ACM"},{"issue":"2","key":"3_CR16","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323\u2013342, 1983.","journal-title":"Journal of the ACM"},{"key":"3_CR17","series-title":"Lect Notes Comput Sci","first-page":"310","volume-title":"Proc. CAV\u201991","author":"L. Christoff","year":"1991","unstructured":"L. Christoff and I. Christoff. Efficient algorithms for verification of equivalences for probabilistic processes. Proc. CAV\u201991, LNCS, 575:310\u2013321, 1991."},{"key":"3_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-56287-7_117","volume-title":"Proc. 12th Conference on Foundations of Software Technology and Theoretical Computer Science","author":"L. Christoff","year":"1992","unstructured":"L. Christoff and I. Christoff. Reasoning about safety and liveness properties for probabilistic processes. Proc. 12th Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS, 652:342\u2013355, 1992."},{"issue":"2","key":"3_CR19","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"3_CR20","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1006\/inco.1996.0003","volume":"124","author":"G. C\u00e9c\u00e9","year":"1996","unstructured":"G. C\u00e9c\u00e9, A. Finkel, and S. Iyer. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20\u201331, 1996.","journal-title":"Information and Computation"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. Proc. FOCS\u201988, pages 338\u2013345, 1988.","DOI":"10.1109\/SFCS.1988.21950"},{"issue":"4","key":"3_CR22","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857\u2013907, 1995.","journal-title":"Journal of the ACM"},{"key":"3_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BFb0023457","volume-title":"Proc. STACS\u201997","author":"L. Alfaro de","year":"1997","unstructured":"L. de Alfaro. Temporal logics for the specification of performance and reliability. Proc. STACS\u201997, LNCS, 1200:165\u2013176, 1997."},{"key":"3_CR24","first-page":"995","volume":"B","author":"E. Emerson","year":"1990","unstructured":"E. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, B:995\u20131072, 1990.","journal-title":"Handbook of Theoretical Computer Science"},{"key":"3_CR25","volume-title":"An Introduction to Probability Theory and its Application","author":"W. Feller","year":"1968","unstructured":"W. Feller. An Introduction to Probability Theory and its Application. John Wiley and Sons, New York, 1968."},{"issue":"3","key":"3_CR26","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BF02277857","volume":"7","author":"A. Finkel","year":"1994","unstructured":"A. Finkel. Decidability of the termination problem for completely specified protocols. Distributed Computing, 7(3):129\u2013135, 1994.","journal-title":"Distributed Computing"},{"issue":"5","key":"3_CR27","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"issue":"2\/3","key":"3_CR28","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/S0019-9958(86)80001-8","volume":"70","author":"S. Hart","year":"1986","unstructured":"S. Hart and M. Sharir. Probabilistic propositional temporal logics. Information and Control, 70(2\/3):97\u2013155, 1986. This is the extended version of \u201cProbabilistic Temporal Logics for Finite and Bounded Models\u201d. In Proc. STOCS\u201984, 1\u201313, 1984.","journal-title":"Information and Control"},{"issue":"3","key":"3_CR29","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/2166.357214","volume":"5","author":"S. Hart","year":"1983","unstructured":"S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent program. ACM Transactions on Programming Languages and Systems, 5(3):356\u2013380, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR30","doi-asserted-by":"crossref","first-page":"211","DOI":"10.3233\/FI-1992-17304","volume":"17","author":"T. Huynh","year":"1992","unstructured":"T. Huynh and L. Tian. On some equivalence relations for probabilistic processes. Fundamenta Informaticae, 17:211\u2013234, 1992.","journal-title":"Fundamenta Informaticae"},{"key":"3_CR31","unstructured":"P. Iyer and M. Narasimha. \u201cAlmost always\u201d and \u201csometime definitely\u201d are not enough: Probabilistic quantifiers and probabilistic model-checking. Technical Report TR-96-16, Department of Computer Science, North Carolina State University, 1996."},{"key":"3_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1007\/BFb0030633","volume-title":"Proc. TAPSOFT\u201997","author":"P. Iyer","year":"1997","unstructured":"P. Iyer and M. Narasimha. Probabilistic lossy channel systems. Proc. TAPSOFT\u201997, LNCS, 1214:667\u2013681, 1997."},{"key":"3_CR33","unstructured":"ISO. Data communications-HDLC procedures-elements of procedures. Technical Report TR-ISO-4335, International Standards Organization, Geneva, 1979."},{"key":"3_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/BFb0039071","volume-title":"Proc. CONCUR\u201990","author":"C. Jou","year":"1990","unstructured":"C. Jou and S. Smolka. Equivalences, congruences, and complete axiomatizations for probabilistic processes. In Proc. CONCUR\u201990, LNCS, 458:367\u2013383, 1990."},{"issue":"3","key":"3_CR35","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"D. Lehmann","year":"1982","unstructured":"D. Lehmann and S. Shelah. Reasoning about time and chance. Information and Control, 53(3):165\u2013198, 1982.","journal-title":"Information and Control"},{"key":"3_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/BFb0084809","volume-title":"CONCUR\u201992","author":"K. Larsen","year":"1992","unstructured":"K. Larsen and A. Skou. Compositional verification of probabilistic processes. In CONCUR\u201992, LNCS, 630:456\u2013471, 1992."},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"N. Lynch and M. Tuttle. Hierarchical Correctness Proofs For Distributed Algorithms. PODC\u201987, pages 137\u2013151, 1987.","DOI":"10.1145\/41840.41852"},{"key":"3_CR38","unstructured":"N. Lynch. Distributed Algorithms. Morgan Kaufmann Series in Data Management Systems. Morgan Kaufmann Publishers, 1995."},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems-Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"1","key":"3_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"A. Pnueli and L. Zuck. Probabilistic Verification. Information and Computation, 103(1):1\u201329, 1993. This is the extended version of \u201cProbabilistic Verification by Tableaux\u201d. In Proc. LICS\u201986, 322\u2013331, 1986.","journal-title":"Information and Computation"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"S. Safra. On the complexity of \u03c9-automata. FOCS\u201988, pages 319\u2013327, 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"3_CR42","unstructured":"R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995."},{"key":"3_CR43","first-page":"133","volume":"B","author":"W. Thomas","year":"1990","unstructured":"W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, B:133\u2013191, 1990.","journal-title":"Handbook of Theoretical Computer Science"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. FOCS\u201985, pages 327\u2013338, 1985.","DOI":"10.1109\/SFCS.1985.12"},{"key":"3_CR45","first-page":"238","volume":"1043","author":"M. Vardi","year":"1996","unstructured":"M. Vardi. An automata-theoretic approach to linear temporal logic. LNCS, 1043:238\u2013266, 1996.","journal-title":"LNCS"},{"key":"3_CR46","unstructured":"M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. LICS\u2019 86, pages 332\u2013345, 1986."},{"issue":"1","key":"3_CR47","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"M. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, 1994.","journal-title":"Information and Computation"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"P. Wolper, M. Vardi, and A. Sistla. Reasoning about infinite computation paths (extended abstract). FOCS\u201983, pages 185\u2013194, 1983.","DOI":"10.1109\/SFCS.1983.51"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:07:36Z","timestamp":1736986056000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}