{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:09:58Z","timestamp":1776373798293,"version":"3.51.2"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present QReach, the first reachability analysis tool for quantum Markov chains based on decision diagrams CFLOBDD (presented at <jats:italic>CAV<\/jats:italic> 2023). QReach provides a novel framework for finding reachable subspaces, as well as a series of model-checking subprocedures like image computation. Experiments indicate its practicality in verification of quantum circuits and algorithms. QReach is expected to play a central role in future quantum model checkers.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_23","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"520-532","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["QReach: A Reachability Analysis Tool for\u00a0Quantum Markov Chains"],"prefix":"10.1007","author":[{"given":"Aochu","family":"Dai","sequence":"first","affiliation":[]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"RI Bahar","year":"1997","unstructured":"Bahar, R.I., et al.: Algebric decision diagrams and their applications. Formal Methods Syst. Des. 10, 171\u2013206 (1997)","journal-title":"Formal Methods Syst. Des."},{"issue":"02","key":"23_CR2","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1142\/S0219749908003530","volume":"6","author":"P Baltazar","year":"2008","unstructured":"Baltazar, P., Chadha, R., Mateus, P.: Quantum computation tree logic-model checking and complete calculus. Int. J. Quantum Inform. 6(02), 219\u2013236 (2008)","journal-title":"Int. J. Quantum Inform."},{"issue":"9","key":"23_CR3","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is np-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996)","journal-title":"IEEE Trans. Comput."},{"issue":"4","key":"23_CR4","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"JR Burch","year":"1994","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4), 401\u2013424 (1994)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"23_CR5","doi-asserted-by":"publisher","unstructured":"Chen, Y.F., Chung, K.M., Leng\u00e1l, O., Lin, J.A., Tsai, W.L.: AUTOQ: an automata-based quantum circuit verifier. In: Enea, C., Lal, A. (eds.) International Conference on Computer Aided Verification, pp. 139\u2013153. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_7","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., Chung, K.M., Leng\u00e1l, O., Lin, J.A., Tsai, W.L., Yen, D.D.: An automata-based framework for verification and bug hunting in quantum circuits. Proc. ACM Program. Lang. 7(PLDI), 1218\u20131243 (2023)","DOI":"10.1145\/3591270"},{"issue":"3","key":"23_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3505636","volume":"3","author":"A Cross","year":"2022","unstructured":"Cross, A., et al.: OpenQASM 3: a broader and deeper quantum assembly language. ACM Trans. Quantum Comput. 3(3), 1\u201350 (2022)","journal-title":"ACM Trans. Quantum Comput."},{"issue":"19","key":"23_CR8","doi-asserted-by":"publisher","first-page":"4329","DOI":"10.1103\/PhysRevLett.80.4329","volume":"80","author":"LK Grover","year":"1998","unstructured":"Grover, L.K.: Quantum computers can search rapidly by using almost any transformation. Phys. Rev. Lett. 80(19), 4329 (1998)","journal-title":"Phys. Rev. Lett."},{"issue":"6","key":"23_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3514355","volume":"27","author":"X Hong","year":"2022","unstructured":"Hong, X., Zhou, X., Li, S., Feng, Y., Ying, M.: A tensor network based decision diagram for representation of quantum circuits. ACM Trans. Des. Autom. Electron. Syst. (TODAES) 27(6), 1\u201330 (2022)","journal-title":"ACM Trans. Des. Autom. Electron. Syst. (TODAES)"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Mateus, P., Ramos, J., Sernadas, A., Sernadas, C.: Temporal logics for reasoning about quantum systems. Semantic Tech. Quantum Comput., 389\u2013413 (2009)","DOI":"10.1017\/CBO9781139193313.011"},{"issue":"5","key":"23_CR11","doi-asserted-by":"publisher","first-page":"771","DOI":"10.1016\/j.ic.2006.02.001","volume":"204","author":"P Mateus","year":"2006","unstructured":"Mateus, P., Sernadas, A.: Weakly complete axiomatization of exogenous quantum propositional logic. Inf. Comput. 204(5), 771\u2013794 (2006)","journal-title":"Inf. Comput."},{"issue":"1","key":"23_CR12","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/TCAD.2015.2459034","volume":"35","author":"P Niemann","year":"2015","unstructured":"Niemann, P., Wille, R., Miller, D.M., Thornton, M.A., Drechsler, R.: QMDDs: efficient quantum function representation and manipulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 35(1), 86\u201399 (2015)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Paetznick, A., Svore, K.M.: Repeat-until-success: Non-deterministic decomposition of single-qubit unitaries. Quantum Info. Comput. 14(15\u201316), 1277\u20131301 (2014)","DOI":"10.26421\/QIC14.15-16-2"},{"key":"23_CR14","doi-asserted-by":"publisher","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: Symbolic quantum simulation with Quasimodo. In: International Conference on Computer Aided Verification. pp. 213\u2013225. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_11","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Sistla, M.A., Chaudhuri, S., Reps, T.: CFLOBDDs: context-free-language ordered binary decision diagrams. ACM Trans. Program. Lang. Syst. (2023)","DOI":"10.1145\/3651157"},{"issue":"5","key":"23_CR16","doi-asserted-by":"publisher","first-page":"1015","DOI":"10.1007\/s11128-012-0432-5","volume":"11","author":"SE Venegas-Andraca","year":"2012","unstructured":"Venegas-Andraca, S.E.: Quantum walks: a comprehensive review. Quantum Inf. Process. 11(5), 1015\u20131106 (2012)","journal-title":"Quantum Inf. Process."},{"key":"23_CR17","doi-asserted-by":"publisher","first-page":"1108","DOI":"10.22331\/q-2023-09-11-1108","volume":"7","author":"L Vinkhuijzen","year":"2023","unstructured":"Vinkhuijzen, L., Coopmans, T., Elkouss, D., Dunjko, V., Laarman, A.: LIMDD: a decision diagram for simulation of quantum computing including stabilizer states. Quantum 7, 1108 (2023)","journal-title":"Quantum"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Ying, M., Feng, Y.: Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press (2021)","DOI":"10.1017\/9781108613323"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-32940-1_7","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"N Yu","year":"2012","unstructured":"Yu, N., Ying, M.: Reachability and termination analysis of concurrent quantum programs. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 69\u201383. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_7"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Zulehner, A., Hillmich, S., Wille, R.: How to efficiently handle complex values? Implementing decision diagrams for quantum computing. In: 2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp.\u00a01\u20137. IEEE (2019)","DOI":"10.1109\/ICCAD45719.2019.8942057"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:08:07Z","timestamp":1721891287000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}