{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T19:06:32Z","timestamp":1763233592728,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_20","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T12:51:59Z","timestamp":1286196719000},"page":"278-293","source":"Crossref","is-referenced-by-count":12,"title":["Characterising Probabilistic Processes Logically"],"prefix":"10.1007","author":[{"given":"Yuxin","family":"Deng","sequence":"first","affiliation":[]},{"given":"Rob","family":"van Glabbeek","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/3-540-48224-5_31","volume-title":"Automata, Languages and Programming","author":"E. Bandini","year":"2001","unstructured":"Bandini, E., Segala, R.: Axiomatizations for Probabilistic Bisimulation. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 370\u2013381. Springer, Heidelberg (2001)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/BFb0039056","volume-title":"CONCUR \u201990","author":"I. Christoff","year":"1990","unstructured":"Christoff, I.: Testing equivalences and fully abstract models for probabilistic processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol.\u00a0458, pp. 126\u2013140. Springer, Heidelberg (1990)"},{"issue":"2-3","key":"20_CR3","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1016\/j.tcs.2005.03.048","volume":"342","author":"R. Cleaveland","year":"2005","unstructured":"Cleaveland, R., Purushothaman Iyer, S., Narasimha, M.: Probabilistic temporal logics via the modal mu-calculus. Theoretical Computer Science\u00a0342(2-3), 316\u2013350 (2005)","journal-title":"Theoretical Computer Science"},{"key":"20_CR4","first-page":"11","volume-title":"Proc. QEST 2009","author":"P.R. D\u2019Argenio","year":"2009","unstructured":"D\u2019Argenio, P.R., Wolovick, N., Terraf, P.S., Celayes, P.: Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization. In: Proc. QEST 2009, pp. 11\u201320. IEEE Computer Society, Los Alamitos (2009)"},{"key":"20_CR5","first-page":"401","volume-title":"Proc. FCST 2009","author":"Y. Deng","year":"2009","unstructured":"Deng, Y., Du, W.: A Local Algorithm for Checking Probabilistic Bisimilarity. In: Proc. FCST 2009, pp. 401\u2013407. IEEE Computer Society, Los Alamitos (2009)"},{"key":"20_CR6","unstructured":"Deng, Y., van Glabbeek, R.J.: Characterising Probabilistic Processes Logically, http:\/\/arxiv.org\/abs\/1007.5188 , Full version of this paper"},{"issue":"4","key":"20_CR7","doi-asserted-by":"publisher","first-page":"4","DOI":"10.2168\/LMCS-4(4:4)2008","volume":"4","author":"Y. Deng","year":"2008","unstructured":"Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.C.: Characterising Testing Preorders for Finite Probabilistic Processes. Logical Methods in Computer Science\u00a04(4), 4 (2008)","journal-title":"Logical Methods in Computer Science"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-04081-8_19","volume-title":"CONCUR 2009 - Concurrency Theory","author":"Y. Deng","year":"2009","unstructured":"Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.C.: Testing Finitary Probabilistic Processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009 - Concurrency Theory. LNCS, vol.\u00a05710, pp. 274\u2013288. Springer, Heidelberg (2009)"},{"key":"20_CR9","first-page":"359","volume":"172","author":"Y. Deng","year":"2007","unstructured":"Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.C., Zhang, C.: Remarks on Testing Probabilistic Processes. ENTCS\u00a0172, 359\u2013397 (2007)","journal-title":"ENTCS"},{"issue":"1-2","key":"20_CR10","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.tcs.2006.12.008","volume":"373","author":"Y. Deng","year":"2007","unstructured":"Deng, Y., Palamidessi, C.: Axiomatizations for probabilistic finite-state behaviors. Theoretical Computer Science\u00a0373(1-2), 92\u2013114 (2007)","journal-title":"Theoretical Computer Science"},{"key":"20_CR11","first-page":"478","volume-title":"Proc. LICS 1998","author":"J. Desharnais","year":"1998","unstructured":"Desharnais, J., Edalat, A., Panangaden, P.: A logical characterization of bisimulation for labelled Markov processes. In: Proc. LICS 1998, pp. 478\u2013489. IEEE Computer Society, Los Alamitos (1998)"},{"key":"20_CR12","unstructured":"Giacalone, A., Jou, C.-C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proc. IFIP TC 2 Working Conference on Programming Concepts and Methods, pp. 443\u2013458 (1990)"},{"key":"20_CR13","first-page":"278","volume-title":"Proc. RTSS 1990","author":"H. Hansson","year":"1990","unstructured":"Hansson, H., Jonsson, B.: A Calculus for Communicating Systems with Time and Probabilities. In: Proc. RTSS 1990, pp. 278\u2013287. IEEE Computer Society, Los Alamitos (1990)"},{"issue":"5","key":"20_CR14","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(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"20_CR15","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM\u00a032(1), 137\u2013161 (1985)","journal-title":"Journal of the ACM"},{"key":"20_CR16","first-page":"111","volume-title":"Proc. LICS 1997","author":"M. Huth","year":"1997","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proc. LICS 1997, pp. 111\u2013122. IEEE Computer Society, Los Alamitos (1997)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proc. LICS 1991, pp. 266\u2013277. Computer Society Press (1991)","DOI":"10.1109\/LICS.1991.151651"},{"issue":"1","key":"20_CR18","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/S0304-3975(01)00044-5","volume":"282","author":"B. Jonsson","year":"2002","unstructured":"Jonsson, B., Wang, Y.: Testing preorders for probabilistic processes can be characterized by simulations. Theoretical Computer Science\u00a0282(1), 33\u201351 (2002)","journal-title":"Theoretical Computer Science"},{"key":"20_CR19","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"20_CR20","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":"20_CR21","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/0304-3975(94)00171-E","volume":"138","author":"G. Lowe","year":"1995","unstructured":"Lowe, G.: Probabilistic and Prioritized Models of Timed CSP. Theoretical Computer Science\u00a0138, 315\u2013352 (1995)","journal-title":"Theoretical Computer Science"},{"key":"20_CR22","unstructured":"McIver, A.K., Morgan, C.C.: An expectation-based model for probabilistic temporal logic. Technical Report PRG-TR-13-97, Oxford University Computing Laboratory (1997)"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"McIver, A.K., Morgan, C.C.: Results on the Quantitative Mu-Calculus. ACM Transactions on Computational Logic\u00a08(1) (2007)","DOI":"10.1145\/1182613.1182616"},{"key":"20_CR24","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"20_CR25","first-page":"7","volume":"96","author":"M.W. Mislove","year":"2004","unstructured":"Mislove, M.W., Ouaknine, J., Worrell, J.: Axioms for Probability and Non-determinism. ENTCS\u00a096, 7\u201328 (2004)","journal-title":"ENTCS"},{"key":"20_CR26","first-page":"159","volume":"18","author":"M. M\u00fcller-Olm","year":"1998","unstructured":"M\u00fcller-Olm, M.: Derivation of Characteristic Formulae. ENTCS\u00a018, 159\u2013170 (1998)","journal-title":"ENTCS"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-71389-0_21","volume-title":"Foundations of Software Science and Computational Structures","author":"A. Parma","year":"2007","unstructured":"Parma, A., Segala, R.: Logical Characterizations of Bisimulations for Discrete Probabilistic Systems. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423, pp. 287\u2013301. Springer, Heidelberg (2007)"},{"key":"20_CR28","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes","author":"M.L. Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes. Wiley, Chichester (1994)"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/3-540-63141-0_2","volume-title":"Logical Foundations of Computer Science","author":"Y.S. Ramakrishna","year":"1997","unstructured":"Ramakrishna, Y.S., Smolka, S.A.: Partial-order reduction in the weak modal mu-calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) LFCS 1997. LNCS, vol.\u00a01234, pp. 5\u201324. Springer, Heidelberg (1997)"},{"key":"20_CR30","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Technical Report MIT\/LCS\/TR-676, PhD thesis, MIT, Dept. of EECS (1995)"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-540-48654-1_35","volume-title":"CONCUR \u201994: Concurrency Theory","author":"R. Segala","year":"1994","unstructured":"Segala, R., Lynch, N.A.: Probabilistic Simulations for Probabilistic Processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 481\u2013496. Springer, Heidelberg (1994)"},{"key":"20_CR32","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/inco.1994.1028","volume":"110","author":"B. Steffen","year":"1994","unstructured":"Steffen, B., Ing\u00f3lfsd\u00f3ttir, A.: Characteristic Formulae for Processes with Divergence. Information and Computation\u00a0110, 149\u2013163 (1994)","journal-title":"Information and Computation"},{"issue":"2","key":"20_CR33","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics\u00a05(2), 285\u2013309 (1955)","journal-title":"Pacific Journal of Mathematics"},{"key":"20_CR34","first-page":"1","volume":"129","author":"R. Tix","year":"2005","unstructured":"Tix, R., Keimel, K., Plotkin, G.D.: Semantic Domains for Combining Probability and Non-Determinism. ENTCS\u00a0129, 1\u2013104 (2005)","journal-title":"ENTCS"},{"key":"20_CR35","doi-asserted-by":"crossref","unstructured":"Wang, Y., Larsen, K.G.: Testing Probabilistic and Nondeterministic Processes. In: Proc. IFIP TC6\/WG6.1 PSTV\u201992, C-8, North-Holland, pp. 47\u201361 (1992)","DOI":"10.1016\/B978-0-444-89874-6.50010-6"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:32:47Z","timestamp":1740547967000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_20"}},"subtitle":["(Extended Abstract)"],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}