{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:32:46Z","timestamp":1743035566265,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540231691"},{"type":"electronic","value":"9783540302339"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"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":[[2004]]},"DOI":"10.1007\/978-3-540-30233-9_12","type":"book-chapter","created":{"date-parts":[[2010,10,24]],"date-time":"2010-10-24T16:06:08Z","timestamp":1287936368000},"page":"156-169","source":"Crossref","is-referenced-by-count":2,"title":["Branching Time Equivalences for Interactive Markov Chains"],"prefix":"10.1007","author":[{"given":"Guangping","family":"Qin","sequence":"first","affiliation":[]},{"given":"Jinzhao","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-45694-5_23","volume-title":"CONCUR 2002 - Concurrency Theory","author":"C. Baier","year":"2002","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H., Haverkort, B.: Simulation for continuoustime Markov chains. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 338\u2013354. Springer, Heidelberg (2002)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/10722167_28","volume-title":"Computer Aided Verification","author":"C. Baier","year":"2000","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 358\u2013372. Springer, Heidelberg (2000)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1007\/3-540-45022-X_65","volume-title":"Automata, Languages and Programming","author":"C. Baier","year":"2000","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the logical characterization of performability properties. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 780\u2013792. Springer, Heidelberg (2000)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 146\u2013162. Springer, Heidelberg (1999)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-540-45187-7_32","volume-title":"CONCUR 2003 - Concurrency Theory","author":"C. Baier","year":"2003","unstructured":"Baier, C., Hermanns, H., Katoen, J.-P., Wolf, V.: Comparative branchingtime semantics for Markov chains. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 492\u2013507. Springer, Heidelberg (2003)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-63166-6_14","volume-title":"Computer Aided Verification","author":"C. Baier","year":"1997","unstructured":"Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 119\u2013130. Springer, Heidelberg (1997)"},{"key":"12_CR9","unstructured":"Bravetti, M.: Revisiting Interactive Markov Chains. 3rd Workshop on Models for Time-Critical Systems, BRICS Notes NP-02-3, pp. 68\u201388 (2002)"},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M. Brown","year":"1988","unstructured":"Brown, M., Clarke, E., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Th. Comp. Sci.\u00a059, 115\u2013131 (1988)","journal-title":"Th. Comp. Sci."},{"issue":"5","key":"12_CR11","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. on Programming Language and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. on Programming Language and Systems"},{"key":"12_CR12","unstructured":"Desharnais, J.: Logical characterisation of simulation for Markov chains. In: Proc. Workshop on Probabilistic Methods in Verification, Tech. Rep. CSR-99-8, Univ. of Birmingham (1999)"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Panangaden, P.: Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. J. of Logic and Algebraic Programming (2003)","DOI":"10.1016\/S1567-8326(02)00068-1"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/3-540-52559-9_68","volume-title":"Stepwise Refinement of Distributed Systems","author":"R. Glabbeek van","year":"1990","unstructured":"van Glabbeek, R.: The linear time - branching time spectrum I. The semantics of concrete, sequential processe. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol.\u00a0430, pp. 267\u2013300. Springer, Heidelberg (1990)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-57208-2_6","volume-title":"CONCUR\u201993","author":"R. Glabbeek van","year":"1993","unstructured":"van Glabbeek, R.: The linear time - branching time spectrum II. The semantics of sequential processes with silent moves. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 66\u201381. Springer, Heidelberg (1993)"},{"key":"12_CR16","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. Form. Asp. of Comp.\u00a06, 512\u2013535 (1994)","journal-title":"Form. Asp. of Comp."},{"key":"12_CR17","unstructured":"Hermanns, H.: Interactive Markov Chains. PhD thesis, Universit\u00e4t Erlangen- N\u00fcrnberg (1998)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-40911-4_24","volume-title":"Integrated Formal Methods","author":"H. Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: Towards model checking stochastic process algebra. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol.\u00a01945, pp. 420\u2013439. Springer, Heidelberg (2000)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specifcation and refnement of probabilistic processes. In: IEEE Symp. on Logic in Computer Science, pp. 266\u2013277 (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-54430-5_99","volume-title":"CONCUR \u201991","author":"B. Jonsson","year":"1991","unstructured":"Jonsson, B.: Simulations between specifications of distributed systems. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol.\u00a0527, pp. 346\u2013360. Springer, Heidelberg (1991)"},{"key":"12_CR21","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"issue":"2","key":"12_CR22","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. Nicola De","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. of ACM\u00a042(2), 458\u2013487 (1995)","journal-title":"J. of ACM"},{"issue":"2","key":"12_CR23","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nordic J. of Computing\u00a02(2), 250\u2013273 (1995)","journal-title":"Nordic J. of Computing"}],"container-title":["Lecture Notes in Computer Science","Applying Formal Methods: Testing, Performance, and M\/E-Commerce"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30233-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T04:53:27Z","timestamp":1740632007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30233-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231691","9783540302339"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30233-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}