{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:24Z","timestamp":1760202624076,"version":"3.40.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642279393"},{"type":"electronic","value":"9783642279409"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-27940-9_26","type":"book-chapter","created":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T07:29:29Z","timestamp":1326958169000},"page":"396-411","source":"Crossref","is-referenced-by-count":11,"title":["A General Framework for Probabilistic Characterizing Formulae"],"prefix":"10.1007","author":[{"given":"Joshua","family":"Sack","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Ingolfsdottir, A., Levy, P., Sack, J.: Characteristic formulae for fixed-point semantics: a general approach. To appear in Mathematical Structures in Computer Science (2010)","DOI":"10.4204\/EPTCS.8.1"},{"issue":"1","key":"26_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jctb.2010.08.002","volume":"101","author":"R. Aharonia","year":"2011","unstructured":"Aharonia, R., Bergerb, E., Georgakopoulosc, A., Perlsteina, A., Spr\u00fcssel, P.: The Max-Flow Min-Cut theorem for countable networks. Journal of Combinatorial Theory, Series B\u00a0101(1), 1\u201317 (2011)","journal-title":"Journal of Combinatorial Theory, Series B"},{"issue":"2","key":"26_CR3","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.entcs.2005.10.034","volume":"153","author":"C. Baier","year":"2006","unstructured":"Baier, C., D\u2019Argenio, P.R., Gr\u00f6\u00dfer, M.: Partial order reduction for probabilistic branching time. Electr. Notes Theor. Comput. Sci.\u00a0153(2), 97\u2013116 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"26_CR4","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.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci.\u00a060(1), 187\u2013231 (2000)","journal-title":"J. Comput. Syst. Sci."},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model Checking of Probabilistic and Nondeterministic Systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"26_CR6","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Transactions on Dependable and Secure Computing\u00a099(1) (2009)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-16242-8_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Y. Deng","year":"2010","unstructured":"Deng, Y., van Glabbeek, R.: Characterising Probabilistic Processes Logically. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 278\u2013293. Springer, Heidelberg (2010)"},{"key":"26_CR8","unstructured":"Desharnais, J.: Labelled Markov processes. Ph.D. thesis, McGill University (1999)"},{"issue":"2","key":"26_CR9","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.ic.2009.11.002","volume":"208","author":"J. Desharnais","year":"2010","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Weak bisimulation is sound and complete for pctl*. Inf. Comput.\u00a0208(2), 203\u2013219 (2010)","journal-title":"Inf. Comput."},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: Logic, simulation and games. In: QEST, pp. 264\u2013273 (2008)","DOI":"10.1109\/QEST.2008.42"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351 (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-04081-8_23","volume-title":"CONCUR 2009 - Concurrency Theory","author":"S. Giro","year":"2009","unstructured":"Giro, S., D\u2019Argenio, P.R., Ferrer Fioriti, L.M.: Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 338\u2013353. Springer, Heidelberg (2009)"},{"issue":"1-2","key":"26_CR13","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/S1567-8326(02)00066-8","volume":"56","author":"H. Hermanns","year":"2003","unstructured":"Hermanns, H., Kwiatkowska, M.Z., Norman, G., Parker, D., Siegle, M.: On the use of mtbdds for performability analysis and verification of stochastic systems. J. Log. Algebr. Program\u00a056(1-2), 23\u201367 (2003)","journal-title":"J. Log. Algebr. Program"},{"issue":"2","key":"26_CR14","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1016\/j.ic.2010.11.024","volume":"209","author":"H. Hermanns","year":"2011","unstructured":"Hermanns, H., Parma, A., Segala, R., Wachter, B., Zhang, L.: Probabilistic logical characterization. Inf. Comput.\u00a0209(2), 154\u2013172 (2011)","journal-title":"Inf. Comput."},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Game-based abstraction for markov decision processes. In: QEST, pp. 157\u2013166 (2006)","DOI":"10.1109\/QEST.2006.19"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K., Yi, W.: Probabilistic Extensions of Process Algebras. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) The Handbook of Process Algebra, pp. 685\u2013710. Elsevier (2001)","DOI":"10.1016\/B978-044482830-9\/50029-1"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.: Specification and Refinement of Probabilistic Processes. In: LICS, pp. 266\u2013277 (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"26_CR18","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/s10992-007-9052-4","volume":"36","author":"L. Moss","year":"2007","unstructured":"Moss, L.: Finite Models Constructed from Canonical Formulas. Journal of Philosophical Logic\u00a036, 605\u2013740 (2007)","journal-title":"Journal of Philosophical Logic"},{"key":"26_CR19","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":"26_CR20","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Realtime Systems. PhD thesis, MIT (1995)"},{"issue":"2","key":"26_CR21","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput.\u00a02(2), 250\u2013273 (1995)","journal-title":"Nord. J. Comput."},{"key":"26_CR22","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 Applications. Pacific Journal of Mathematics\u00a05, 285\u2013309 (1955)","journal-title":"Pacific Journal of Mathematics"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, L.: Decision Algorithms for Probabilistic Simulations. PhD thesis, Universit\u00e4t des Saarlandes (2008)","DOI":"10.2168\/LMCS-4(4:6)2008"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27940-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,18]],"date-time":"2025-03-18T23:25:00Z","timestamp":1742340300000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27940-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642279393","9783642279409"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27940-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}