{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:08:36Z","timestamp":1725548916261},"publisher-location":"Berlin, Heidelberg","reference-count":103,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540222651"},{"type":"electronic","value":"9783540246114"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24611-4_12","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T19:01:10Z","timestamp":1267124470000},"page":"419-444","source":"Crossref","is-referenced-by-count":8,"title":["An Abstraction Framework for Mixed Non-deterministic and Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Michael","family":"Huth","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"S. Abramsky","year":"1994","unstructured":"Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol.\u00a03, pp. 1\u2013168. Oxford Univ. Press, Oxford (1994)"},{"key":"12_CR2","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511608841","volume-title":"Process Algebra","author":"J.C.M. Baeten","year":"1990","unstructured":"Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge Tracts in Theoretical Computer Science, vol.\u00a018. Cambridge University Press, Cambridge (1990)"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1006\/jcss.1999.1683","volume":"60","author":"C. Baier","year":"2000","unstructured":"Baier, C., Engelen, B., Majster-Cederbaum, M.: Deciding Bisimilarity and Similarity for Probabilistic Processes. Journal of Computer and System Sciences\u00a060, 187\u2013231 (2000)","journal-title":"Journal of Computer and System Sciences"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46432-8_1","volume-title":"Foundation of Software Science and Computation Structures","author":"C. Baier","year":"2000","unstructured":"Baier, C., Stoelinga, M.I.A.: Norm functions for probabilistic bisimulations with delays. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol.\u00a01784, pp. 1\u201316. Springer, Heidelberg (2000)"},{"key":"12_CR5","volume-title":"Electronic Notes in Theoretical Computer Science","author":"C. Baier","year":"2000","unstructured":"Baier, C., Kwiatkowska, M., Norman, G.: Computing probability bounds for linear time formulas over concurrent probabilistic systems. In: Kwiatkowska, M., Baier, C., Huth, M., Ryan, M. (eds.) Electronic Notes in Theoretical Computer Science, vol.\u00a022. Elsevier Science Publishers, Amsterdam (2000)"},{"key":"12_CR6","volume-title":"Verifying Temporal Properties Of Systems","author":"J.C. Bradfield","year":"1991","unstructured":"Bradfield, J.C.: Verifying Temporal Properties Of Systems. Birkh\u00e4user, Boston (1991)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G. Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 274\u2013287. Springer, Heidelberg (1999)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-44618-4_14","volume-title":"CONCUR 2000 - Concurrency Theory","author":"G. Bruns","year":"2000","unstructured":"Bruns, G., Godefroid, P.: Generalized Model Checking: Reasoning about Partial State Spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 168\u2013182. Springer, Heidelberg (2000)"},{"issue":"3","key":"12_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.R. Bryant","year":"1992","unstructured":"Bryant, R.R.: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"key":"12_CR10","unstructured":"Burch, J.R., Clarke, E.M., Dill, D.L., McMillan, K.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science (June 1990)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-45694-5_25","volume-title":"CONCUR 2002 - Concurrency Theory","author":"S. Cattani","year":"2002","unstructured":"Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 371\u2013385. Springer, Heidelberg (2002)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Cerans, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification - theory and tools. In: Computer Aided Verification, pp. 253\u2013267 (1993)","DOI":"10.1007\/3-540-56922-7_21"},{"key":"12_CR13","first-page":"414","volume-title":"Proceedings of the Sixth European Software Engineering Conference (ESEC\/FSE 1997)","author":"Y.-F. Chen","year":"1997","unstructured":"Chen, Y.-F., Gansner, E.R., Koutsofios, E.: A C++ data model supporting reachability analysis and dead code detection. In: Jazayeri, M., Schauer, H. (eds.) Proceedings of the Sixth European Software Engineering Conference (ESEC\/FSE 1997), pp. 414\u2013431. Springer, Heidelberg (1997)"},{"key":"12_CR14","unstructured":"Clark, D., Hankin, C., Hunt, S., Nagarajan, R.: Possibilistic Information Flow is safe for Probabilistic Non-Interference. In: Workshop on Issues in the Theory of Security WITS 2000, Geneva, Switzerland, July 7-8 (2000)"},{"issue":"1","key":"12_CR15","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"12_CR16","first-page":"93","volume-title":"Representations of discrete functions, chapter Multi-terminal binary decision diagrams and hybrid decision diagrams","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Fujita, M., Zhao, X.: Representations of discrete functions, chapter Multi-terminal binary decision diagrams and hybrid decision diagrams, pp. 93\u2013108. Kluwer academic publishers, Dordrecht (1996)"},{"key":"12_CR17","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"issue":"5","key":"12_CR18","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"708","DOI":"10.1007\/3-540-55719-9_116","volume-title":"Automata, Languages and Programming","author":"R. Cleaveland","year":"1992","unstructured":"Cleaveland, R., Smolka, S.A., Zwarico, A.E.: Testing preorders for probabilistic processes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 708\u2013719. Springer, Heidelberg (1992)"},{"issue":"4","key":"12_CR20","doi-asserted-by":"crossref","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. Journal of the Association of Computing Machinery\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the Association of Computing Machinery"},{"key":"12_CR21","first-page":"238","volume-title":"Proc. 4th ACM Symp. on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs. In: Proc. 4th ACM Symp. on Principles of Programming Languages, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"12_CR22","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/325694.325699","volume-title":"Conference Record of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"2000","unstructured":"Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Conference Record of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Mass, pp. 12\u201325. ACM Press, New York (2000)"},{"key":"12_CR23","unstructured":"Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands (July 1996)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"P.R. D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability Analysis of Probabilistic Systems by Successive Refinements. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 39\u201356. Springer, Heidelberg (2001)"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45605-8_5","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"P.R. D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and Refinement Strategies for Probabilistic Analysis. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 57\u201376. Springer, Heidelberg (2002)"},{"issue":"5","key":"12_CR26","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D. Denning","year":"1976","unstructured":"Denning, D.: A Lattice Model of Secure Information Flow. Communications of the ACM\u00a019(5), 236\u2013243 (1976)","journal-title":"Communications of the ACM"},{"issue":"7","key":"12_CR27","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D. Denning","year":"1977","unstructured":"Denning, D.: Certification of Programs for Secure Information Flow. Communications of the ACM\u00a020(7), 504\u2013513 (1977)","journal-title":"Communications of the ACM"},{"issue":"2","key":"12_CR28","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1006\/inco.2001.2962","volume":"179","author":"J. Desharnais","year":"2002","unstructured":"Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for Labelled Markov Processes. Journal of Information and Computation\u00a0179(2), 163\u2013193 (2002)","journal-title":"Journal of Information and Computation"},{"key":"12_CR29","volume-title":"15th Annual IEEE Symposium on Logic in Computer Science LICS 2000","author":"J. Desharnais","year":"2000","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Approximating Labeled Markov Processes. In: 15th Annual IEEE Symposium on Logic in Computer Science LICS 2000, Santa Barbara, California. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/3-540-45694-5_24","volume-title":"CONCUR 2002 - Concurrency Theory","author":"J. Desharnais","year":"2002","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Weak bisimulation is sound and complete for PCTL*. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 355\u2013370. Springer, Heidelberg (2002)"},{"key":"12_CR31","unstructured":"Dwyer, M.B., Schmidt, D.A.: Limiting State Explosion with Filter-Based Refinement. In: Proceedings of the ILPS 1997 Workshop on Verification, Model Checking, and Abstraction (1997)"},{"key":"12_CR32","unstructured":"http:\/\/www.fsel.com\/fdr2_download.html"},{"key":"12_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-67678-9","volume-title":"A Compendium of Continuous Lattices","author":"G. Gierz","year":"1980","unstructured":"Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: A Compendium of Continuous Lattices. Springer, Heidelberg (1980)"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Gilmore, S., Ryan, M. (eds.): Language Constructs for Describing Features. In: Proc. of the FIREworks workshop. Springer, Heidelberg (2001)","DOI":"10.1007\/978-1-4471-0287-8"},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages, Paris, January 1997, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"Graf, S., Sifakis, J.: Readiness Semantics for Regular Processes with Silent Actions. In: Proc. of ICALP 1987, pp. 115\u2013125 (1987)","DOI":"10.1007\/3-540-18088-5_10"},{"key":"12_CR37","volume-title":"Graduate Texts in Mathematics 18","author":"P.R. Halmos","year":"1950","unstructured":"Halmos, P.R.: Measure Theory. In: Graduate Texts in Mathematics 18. Springer, Heidelberg (1950)"},{"key":"12_CR38","unstructured":"Hansson, H.: Time and Probability in Formal Design of Distributed Systems. PhD thesis, Department of Computer Science, Uppsala University, Uppsala, Sweden (1991)"},{"issue":"5","key":"12_CR39","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H.A. Hansson","year":"1994","unstructured":"Hansson, H.A., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"12_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/3-540-47813-2_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Harding","year":"2002","unstructured":"Harding, A., Ryan, M., Schobbens, P.-Y.: Approximating ATL* in ATL. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 289\u2013301. Springer, Heidelberg (2002)"},{"key":"12_CR41","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Corbett, J.C., Dwyer, M.B., Sokolowski, S., Zheng, H.: A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In: Static Analysis Symposium, pp. 1\u201318 (1999)","DOI":"10.1007\/3-540-48294-6_1"},{"issue":"1\u20132","key":"12_CR42","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0304-3975(00)00305-4","volume":"274","author":"H. Hermanns","year":"2002","unstructured":"Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theoretical Computer Science\u00a0274(1\u20132), 43\u201387 (2002)","journal-title":"Theoretical Computer Science"},{"key":"12_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/3-540-44685-0_6","volume-title":"CONCUR 2001 - Concurrency Theory","author":"H. Hermanns","year":"2001","unstructured":"Hermanns, H., Katoen, J.-P.: Performance Evaluation :\u2009= (Process Algebra + Model Checking) \u00d7 Markov Chains. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 59\u201381. Springer, Heidelberg (2001)"},{"key":"12_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains","author":"H. Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains. LNCS, vol.\u00a02428, p. 57. Springer, Heidelberg (2002)"},{"key":"12_CR45","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569951","volume-title":"A Compositional Approach to Performance Modelling","author":"J. Hillston","year":"1996","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)"},{"key":"12_CR46","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"12_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-46691-6_30","volume-title":"Proceedings of the 19th International Conference on the Foundations of Software Technology & Theoretical Computer Science","author":"M. Huth","year":"1999","unstructured":"Huth, M.: A Unifying Framework for Model Checking Labeled Kripke Structures, Modal Transition Systems, and Interval Transition Systems. In: Proceedings of the 19th International Conference on the Foundations of Software Technology & Theoretical Computer Science, IIT Chennai, India. LNCS, pp. 369\u2013380. Springer, Heidelberg (1999)"},{"key":"12_CR48","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/978-94-010-0654-5_10","volume-title":"Domains and Processes","author":"M. Huth","year":"2001","unstructured":"Huth, M.: Domains of view: a foundation for specification and analysis. In: Domains and Processes, pp. 183\u2013218. Kluwer Academic Publishers, Dordrecht (2001)"},{"key":"12_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-45605-8_8","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M. Huth","year":"2002","unstructured":"Huth, M.: Probabilistic Abstraction-Based Model Checking. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 115\u2013134. Springer, Heidelberg (2002)"},{"key":"12_CR50","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1109\/LICS.1997.614940","volume-title":"Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science","author":"M. Huth","year":"1997","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, pp. 111\u2013122. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"12_CR51","volume-title":"Electronic Notes in Theoretical Computer Science","author":"M. Huth","year":"2000","unstructured":"Huth, M.: The interval domain: A matchmaker for aCTL and aPCTL. In: Mislove, M., Cleaveland, R., Mulry, P. (eds.) Electronic Notes in Theoretical Computer Science, vol.\u00a014. Elsevier Science Publishers, Amsterdam (2000)"},{"key":"12_CR52","doi-asserted-by":"crossref","first-page":"211","DOI":"10.3233\/FI-1992-17304","volume":"17","author":"T. Huynh","year":"1992","unstructured":"Huynh, T., Tian, L.: On some Equivalence Relations for Probabilistic Processes. Fundamenta Informaticae\u00a017, 211\u2013234 (1992)","journal-title":"Fundamenta Informaticae"},{"issue":"2\u20133","key":"12_CR53","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","volume":"28","author":"H. Jifeng","year":"1997","unstructured":"Jifeng, H., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Science of Computer Programming\u00a028(2\u20133), 171\u2013192 (1997)","journal-title":"Science of Computer Programming"},{"key":"12_CR54","unstructured":"Jones, C.: Probabilistic Nondeterminism. PhD thesis, Laboratory for the Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland, Monograph ECS-LFCS-90-105 (1990)"},{"key":"12_CR55","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1109\/LICS.1989.39173","volume-title":"Proceedings of the IEEE 4th Annual Symposium on Logic in Computer Science","author":"C. Jones","year":"1989","unstructured":"Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: Proceedings of the IEEE 4th Annual Symposium on Logic in Computer Science, pp. 186\u2013195. IEEE Computer Society Press, Los Alamitos (1989)"},{"key":"12_CR56","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1109\/LICS.1991.151651","volume-title":"6th Annual IEEE Symposium on Logic in Computer Science","author":"B. Jonsson","year":"1991","unstructured":"Jonsson, B., Larsen, K.G.: Specification and Refinement of Probabilistic Processes. In: 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, July 15-18, pp. 266\u2013277. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"12_CR57","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P. Kannelakis","year":"1990","unstructured":"Kannelakis, P., Smolka, S.: CCS Expressions, Finite State Processes and Three Problems of Equivalence. Journal of Information and Computation\u00a086, 43\u201368 (1990)","journal-title":"Journal of Information and Computation"},{"key":"12_CR58","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"12_CR59","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D. Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of Probabilistic Programs. Computer and System Sciences\u00a022, 328\u2013350 (1981)","journal-title":"Computer and System Sciences"},{"issue":"2","key":"12_CR60","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"22","author":"D. Kozen","year":"1985","unstructured":"Kozen, D.: A Probabilistic PDL. Computer and System Sciences\u00a022(2), 162\u2013178 (1985)","journal-title":"Computer and System Sciences"},{"key":"12_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-45605-8_11","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 169\u2013187. Springer, Heidelberg (2002)"},{"key":"12_CR62","series-title":"Lecture Notes in Computer Science","first-page":"232","volume-title":"Automatic Verification Methods for Finite State Systems","author":"K.G. Larsen","year":"1989","unstructured":"Larsen, K.G.: Modal Specifications. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. International Workshop, Grenoble, France. LNCS, vol.\u00a0407, pp. 232\u2013246. Springer, Heidelberg (1989)"},{"issue":"1","key":"12_CR63","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation\u00a094(1), 1\u201328 (1991)","journal-title":"Information and Computation"},{"key":"12_CR64","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/LICS.1988.5119","volume-title":"Third Annual Symposium on Logic in Computer Science","author":"K.G. Larsen","year":"1988","unstructured":"Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: Third Annual Symposium on Logic in Computer Science, pp. 203\u2013210. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"12_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45605-8_16","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"R. Lassaigne","year":"2002","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate Verification of Probabilistic Systems. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 213\u2013214. Springer, Heidelberg (2002)"},{"key":"12_CR66","doi-asserted-by":"crossref","unstructured":"Martin, K.: The measurement process in domain theory. In: Proc. of Automata, Languages and Programming ICALP 2000, pp. 116\u2013126 (2000)","DOI":"10.1007\/3-540-45022-X_11"},{"key":"12_CR67","volume-title":"Electronic Notes in Theoretical Computer Science","author":"A. McIver","year":"2001","unstructured":"McIver, A., Morgan, C.: Almost-certain eventualities and abstract probabilities in quantitative temporal logic. In: Fidge, C. (ed.) Electronic Notes in Theoretical Computer Science, vol.\u00a042. Elsevier Science Publishers, Amsterdam (2001)"},{"key":"12_CR68","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-36078-6_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. McIver","year":"2002","unstructured":"McIver, A., Morgan, C.: Games, probability and the quantitative \u03bc-calculus qM\u03bc. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 292\u2013310. Springer, Heidelberg (2002)"},{"key":"12_CR69","first-page":"481","volume-title":"2nd International Joint Conference on Artificial Intelligence","author":"R. Milner","year":"1971","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: 2nd International Joint Conference on Artificial Intelligence, pp. 481\u2013489. British Computer Society, London (1971)"},{"key":"12_CR70","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"12_CR71","volume-title":"Communicating and Mobile Systems: the \u03c0-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"12_CR72","unstructured":"Monniaux, D.: Abstract interpretation of programs as Markov decision processes. Technical report, D\u00e9partment d\u2019Informatique,\u00c9cole Normale Sup\u00e9rieure, 45, rue d\u2019Ulm, 75230 Paris cedex 5, France (2001)"},{"key":"12_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/3-540-45309-1_24","volume-title":"Programming Languages and Systems","author":"D. Monniaux","year":"2001","unstructured":"Monniaux, D.: Backwards abstract interpretation of probabilistic programs. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, p. 367. Springer, Heidelberg (2001)"},{"key":"12_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45099-3_17","volume-title":"Static Analysis","author":"D. Monniaux","year":"2000","unstructured":"Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 322\u2013340. Springer, Heidelberg (2000)"},{"key":"12_CR75","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"D. Monniaux","year":"2001","unstructured":"Monniaux, D.: An abstract analysis of the probabilistic termination of programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, Springer, Heidelberg (2001)"},{"key":"12_CR76","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: An abstract Monte-Carlo method for the analysis of probabilistic programs (extended abstract). In: 28th Symposium on Principles of Programming Languages POPL 2001, pp. 93\u2013101. Association for Computer Machinery (2001)","DOI":"10.1145\/360204.360211"},{"key":"12_CR77","unstructured":"Monniaux, D.: Analyse de programmes probabilistes par interpr\u00e9tation abstraite. R\u00e9sum\u00e9 \u00e9tendu en fran\u00e7ais. Contents in English,R\u00e9sum\u00e9 \u00e9tendu en fran\u00e7ais. Contents in English (2001)"},{"issue":"6","key":"12_CR78","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/BF01213492","volume":"8","author":"C. Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Aspects of Computing\u00a08(6), 617\u2013647 (1996)","journal-title":"Formal Aspects of Computing"},{"issue":"6","key":"12_CR79","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1093\/jigpal\/7.6.779","volume":"7","author":"C. Morgan","year":"1999","unstructured":"Morgan, C., McIver, A.: An expectation-based model for probabilistic temporal logic. Logic Journal of the IGPL\u00a07(6), 779\u2013804 (1999)","journal-title":"Logic Journal of the IGPL"},{"issue":"3","key":"12_CR80","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C. Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems\u00a018(3), 325\u2013353 (1996)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR81","volume-title":"Randomized Algorithms","author":"R. Motvani","year":"1995","unstructured":"Motvani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)"},{"key":"12_CR82","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"key":"12_CR83","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/0022-0000(85)90045-5","volume":"31","author":"C.H. Papadimitriou","year":"1985","unstructured":"Papadimitriou, C.H.: Games against nature. Journal of Computer and System Sciences\u00a031, 288\u2013301 (1985)","journal-title":"Journal of Computer and System Sciences"},{"key":"12_CR84","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"12_CR85","series-title":"Lecture Notes in Computer Science","first-page":"167","volume-title":"Proc. of the 5th GI Conference","author":"D.M.R. Park","year":"1989","unstructured":"Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1989)"},{"key":"12_CR86","unstructured":"Pasareanu, C.S.: DEOS kernel: Environment modeling using LTL assumptions. Technical Report #NASA-ARC-IC-2000-196, NASA Ames (July 2000)"},{"key":"12_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-44618-4_25","volume-title":"CONCUR 2000 - Concurrency Theory","author":"A. Phillipou","year":"2000","unstructured":"Phillipou, A., Lee, I., Sokolsky, O.: Weak Bisimulation for Probabilistic Systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 334\u2013349. Springer, Heidelberg (2000)"},{"key":"12_CR88","doi-asserted-by":"crossref","unstructured":"Di Pierro, A., Hankin, C., Wiklicky, H.: Approximate Non-interference. In: CSFW 2002 15th IEEE Computer Security Foundation Workshop, June 2002, pp. 1\u201315 (2002)","DOI":"10.1109\/CSFW.2002.1021803"},{"key":"12_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-45605-8_15","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"A. Pierro Di","year":"2002","unstructured":"Di Pierro, A., Wicklicky, H.: Probabilistic Abstract Interpretation and Statistical Testing. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 211\u2013212. Springer, Heidelberg (2002)"},{"key":"#cr-split#-12_CR90.1","unstructured":"Plotkin, G.D.: A Structural Approach to Operational Semantics. Technical Report FN-19, DAIMI, Computer Science Department, Aarhus University, Ny Munkegade, Building 540, DK-8000 Aarhus, Denmark (September 1981);"},{"key":"#cr-split#-12_CR90.2","unstructured":"Reprinted April 1991"},{"key":"12_CR91","volume-title":"Wiley Series in Probability and Mathematical Statistics","author":"M.L. Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov decision processes: discrete stochastic dynamic programming. In: Wiley Series in Probability and Mathematical Statistics. John Wiley & Sons, Chichester (1994)"},{"key":"12_CR92","first-page":"188","volume-title":"IEEE \/ACM International Conference on CAD","author":"R.I. Bahar","year":"1993","unstructured":"Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic Decision Diagrams and Their Applications. In: IEEE \/ACM International Conference on CAD, Santa Clara, California, pp. 188\u2013191. IEEE Computer Society Press, Los Alamitos (1993)"},{"key":"12_CR93","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages, San Antonio, Texas, January 20-22, pp. 105\u2013118 (1999)","DOI":"10.1145\/292540.292552"},{"key":"12_CR94","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BFb0073967","volume-title":"Toposes, Algebraic Geometry and Logic","author":"D. Scott","year":"1972","unstructured":"Scott, D.: Continuous lattices. In: Lawvere, F.W. (ed.) Toposes, Algebraic Geometry and Logic. Lecture Notes in Mathematics, vol.\u00a0274, pp. 97\u2013136. Springer, Heidelberg (1972)"},{"key":"12_CR95","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Laboratory for Computer Science, Massachusetts Institute of Technology, Available as Technical Report MIT\/LCS\/TR-676 (June 1995)"},{"issue":"2","key":"12_CR96","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"Segala, R., Lynch, N.: Probabilistic Simulations for Probabilistic Processes. Nordic Journal of Computing\u00a02(2), 250\u2013273 (Summer 1995)","journal-title":"Nordic Journal of Computing"},{"key":"12_CR97","doi-asserted-by":"crossref","unstructured":"Seidel, K., Morgan, C., McIver, A.: An introduction to probabilistic predicate transformers. Technical Report PRG-TR-6-96, Programming Research Group, Oxford Computing Laboratory, Wolfson Building, Parks Road, Oxford OX1 3QD (1996)","DOI":"10.1145\/229542.229547"},{"key":"12_CR98","doi-asserted-by":"crossref","unstructured":"Selic, B.: Physical programming: Beyond mere logic. In: ETAPS 2001 (2001) (Invited Talk)","DOI":"10.1007\/3-540-45314-8_1"},{"issue":"3","key":"12_CR99","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J. Glabbeek van","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM\u00a043(3), 555\u2013600 (1996)","journal-title":"Journal of the ACM"},{"key":"12_CR100","doi-asserted-by":"crossref","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. 26th IEEE Symp. on Foundations of Computer Science, Portland, Oregon, October 1985, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"12_CR101","doi-asserted-by":"crossref","unstructured":"Volpano, D.: Provably secure programming languages for remote evaluation. ACM Computing Surveys: electronic\u00a028A(2) (December 1996)","DOI":"10.21236\/ADA486684"},{"key":"12_CR102","unstructured":"Waszkiewicz, P.: Quantitative Continuous Domains. PhD thesis, School of Computer Science, University of Birmingham, United Kingdom (July 2002)"}],"container-title":["Lecture Notes in Computer Science","Validation of Stochastic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24611-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,24]],"date-time":"2021-10-24T03:30:32Z","timestamp":1635046232000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24611-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540222651","9783540246114"],"references-count":103,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24611-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}