{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T03:20:09Z","timestamp":1725852009310},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496299"},{"type":"electronic","value":"9783662496305"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49630-5_18","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T09:04:32Z","timestamp":1458551072000},"page":"303-318","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Trace Refinement in Labelled Markov Decision Processes"],"prefix":"10.1007","author":[{"given":"Nathana\u00ebl","family":"Fijalkow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Kiefer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mahsa","family":"Shirmohammadi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Full version. ArXiv CoRR: http:\/\/arxiv.org\/abs\/1510.09102 (2015)"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Arora, S., Ge, R., Kannan, R., Moitra, A.: Computing a nonnegative matrix factorization - provably. In: STOC, pp. 145\u2013162. ACM (2012)","DOI":"10.1145\/2213977.2213994"},{"issue":"3","key":"18_CR3","first-page":"231","volume":"36","author":"VD Blondel","year":"2003","unstructured":"Blondel, V.D., Canterini, V.: Undecidable problems for probabilistic automata of fixed dimension. Theor. Comput. Sci. 36(3), 231\u2013245 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Canny, J.: Some algebraic and geometric computations in PSPACE. In: STOC, pp. 460\u2013467 (1988)","DOI":"10.1145\/62212.62257"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0024-3795(93)90224-C","volume":"190","author":"J Cohen","year":"1993","unstructured":"Cohen, J., Rothblum, U.: Nonnegative ranks, decompositions, and factorizations of nonnegative matrices. Linear Algebra Appl. 190, 149\u2013168 (1993)","journal-title":"Linear Algebra Appl."},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Condon, A., Lipton, R.: On the complexity of space bounded interactive proofs (extended abstract). In: FOCS, pp. 462\u2013467 (1989)","DOI":"10.1109\/SFCS.1989.63519"},{"key":"18_CR7","volume-title":"Introduction to Algorithms","author":"T Cormen","year":"2001","unstructured":"Cormen, T., Stein, C., Rivest, R., Leiserson, C.E.: Introduction to Algorithms, 2nd edn. McGraw-Hill Higher Education, New York (2001)","edition":"2"},{"issue":"3","key":"18_CR8","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1142\/S0129054108005814","volume":"19","author":"L Doyen","year":"2008","unstructured":"Doyen, L., Henzinger, T.A., Raskin, J.-F.: Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci. 19(3), 549\u2013563 (2008)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"18_CR9","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.ic.2014.12.004","volume":"243","author":"J Fearnley","year":"2015","unstructured":"Fearnley, J., Jurdzinski, M.: Reachability in two-clock timed automata is PSPACE-complete. Inf. Comput. 243, 26\u201336 (2015)","journal-title":"Inf. Comput."},{"key":"18_CR10","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195085914.001.0001","volume-title":"Limits to Parallel Computation: P-completeness Theory","author":"R Greenlaw","year":"1995","unstructured":"Greenlaw, R., Hoover, H.J., Ruzzo, W.L.: Limits to Parallel Computation: P-completeness Theory. Oxford University Press, Oxford (1995)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-3-662-44584-6_18","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"H Hermanns","year":"2014","unstructured":"Hermanns, H., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J.: Probabilistic bisimulation: naturally on distributions. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 249\u2013265. Springer, Heidelberg (2014). Technical report at http:\/\/arxiv.org\/abs\/1404.5084"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-642-22110-1_42","volume-title":"Computer Aided Verification","author":"S Kiefer","year":"2011","unstructured":"Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Language equivalence for probabilistic automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 526\u2013540. Springer, Heidelberg (2011)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/978-3-642-31424-7_51","volume-title":"Computer Aided Verification","author":"S Kiefer","year":"2012","unstructured":"Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: $${\\sf APEX}$$ APEX : an analyzer for open probabilistic programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 693\u2013698. Springer, Heidelberg (2012)"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.ic.2015.07.001","volume":"244","author":"L Li","year":"2015","unstructured":"Li, L., Feng, Y.: Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties. Inf. Comput. 244, 229\u2013244 (2015)","journal-title":"Inf. Comput."},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-36563-8_8","volume-title":"Engineering Secure Software and Systems","author":"TM Ngo","year":"2013","unstructured":"Ngo, T.M., Stoelinga, M., Huisman, M.: Confidentiality for probabilistic multi-threaded programs and its verification. In: J\u00fcrjens, J., Livshits, B., Scandariato, R. (eds.) ESSoS 2013. LNCS, vol. 7781, pp. 107\u2013122. Springer, Heidelberg (2013)"},{"key":"18_CR16","volume-title":"Introduction to Probabilistic Automata","author":"A Paz","year":"1971","unstructured":"Paz, A.: Introduction to Probabilistic Automata. Academic Press, Cambridge (1971)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-32943-2_18","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"S Peyronnet","year":"2012","unstructured":"Peyronnet, S., De Rougemont, M., Strozecki, Y.: Approximate verification and enumeration problems. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 228\u2013242. Springer, Heidelberg (2012)"},{"issue":"3","key":"18_CR18","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0747-7171(10)80003-3","volume":"13","author":"J Renegar","year":"1992","unstructured":"Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals. Parts I-III. J. Symbolic Comput. 13(3), 255\u2013352 (1992)","journal-title":"J. Symbolic Comput."},{"key":"18_CR19","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/S0019-9958(61)80020-X","volume":"4","author":"M-P Sch\u00fctzenberger","year":"1961","unstructured":"Sch\u00fctzenberger, M.-P.: On the definition of a family of automata. Inf. Control 4, 245\u2013270 (1961)","journal-title":"Inf. Control"},{"issue":"2","key":"18_CR20","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1137\/0221017","volume":"21","author":"W Tzeng","year":"1992","unstructured":"Tzeng, W.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM J. Comput. 21(2), 216\u2013227 (1992)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"18_CR21","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0020-0190(96)00039-7","volume":"58","author":"W Tzeng","year":"1996","unstructured":"Tzeng, W.: On path equivalence of nondeterministic finite automata. Inf. Process. Lett. 58(1), 43\u201346 (1996)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"18_CR22","doi-asserted-by":"publisher","first-page":"1364","DOI":"10.1137\/070709967","volume":"20","author":"S Vavasis","year":"2009","unstructured":"Vavasis, S.: On the complexity of nonnegative matrix factorization. SIAM J. Optim. 20(3), 1364\u20131377 (2009)","journal-title":"SIAM J. Optim."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49630-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,15]],"date-time":"2022-06-15T19:21:01Z","timestamp":1655320861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49630-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496299","9783662496305"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}