{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T16:55:01Z","timestamp":1781283301045,"version":"3.54.1"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2023,3,17]],"date-time":"2023-03-17T00:00:00Z","timestamp":1679011200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JSPS","award":["22J23575"],"award-info":[{"award-number":["22J23575"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,7,31]]},"abstract":"<jats:p>Although various dynamic or temporal logics have been proposed to verify quantum protocols and systems, these two viewpoints have not been studied comprehensively enough. We propose Linear Temporal Quantum Logic (LTQL), a linear temporal extension of quantum logic with a quantum implication, and extend it to Dynamic Linear Temporal Quantum Logic (DLTQL). This logic has temporal operators to express transitions by unitary operators (quantum gates) and dynamic ones to express those by projections (projective measurement). We then prove some logical properties of the relationship between these two transitions expressed by LTQL and DLTQL. A drawback in applying LTQL to the verification of quantum protocols is that these logics cannot express the future operator in linear temporal logic. We propose a way to mitigate this drawback by using a translation from (D)LTQL to Linear Temporal Modal Logic (LTML) and a simulation. This translation reduces the satisfiability problem of (D)LTQL formulas to that of LTML with the classical semantics over quantum states.<\/jats:p>","DOI":"10.1145\/3576926","type":"journal-article","created":{"date-parts":[[2022,12,16]],"date-time":"2022-12-16T13:20:25Z","timestamp":1671196825000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9890-1015","authenticated-orcid":false,"given":"Tsubasa","family":"Takagi","sequence":"first","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Nomi, Ishikawa, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,3,17]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-642-39992-3_9","volume-title":"International Workshop on Logic, Language, Information, and Computation","author":"Baltag A.","year":"2013","unstructured":"A. Baltag, J. M. Bergfeld, K. Kishida, J. Sack, S. J. L. Smets, and S. Zhong. 2013. Quantum probabilistic dyadic second-order logic. In International Workshop on Logic, Language, Information, and Computation. Springer, 64\u201380."},{"issue":"12","key":"e_1_3_1_3_2","doi-asserted-by":"crossref","first-page":"2267","DOI":"10.1007\/s10773-005-8022-2","article-title":"Complete axiomatizations for quantum actions","volume":"44","author":"Baltag A.","year":"2005","unstructured":"A. Baltag and S. Smets. 2005. Complete axiomatizations for quantum actions. International Journal of Theoretical Physics 44, 12 (2005), 2267\u20132282.","journal-title":"International Journal of Theoretical Physics"},{"issue":"3","key":"e_1_3_1_4_2","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1017\/S0960129506005299","article-title":"LQP: The dynamic logic of quantum information","volume":"16","author":"Baltag A.","year":"2006","unstructured":"A. Baltag and S. Smets. 2006. LQP: The dynamic logic of quantum information. Mathematical Structures in Computer Science 16, 3 (2006), 491\u2013525.","journal-title":"Mathematical Structures in Computer Science"},{"issue":"2","key":"e_1_3_1_5_2","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/s11229-010-9783-6","article-title":"Quantum logic as a dynamic logic","volume":"179","author":"Baltag A.","year":"2011","unstructured":"A. Baltag and S. Smets. 2011. Quantum logic as a dynamic logic. Synthese 179, 2 (2011), 285\u2013306.","journal-title":"Synthese"},{"issue":"3","key":"e_1_3_1_6_2","doi-asserted-by":"crossref","first-page":"753","DOI":"10.1007\/s11229-011-9915-7","article-title":"The dynamic turn in quantum logic","volume":"186","author":"Baltag A.","year":"2012","unstructured":"A. Baltag and S. Smets. 2012. The dynamic turn in quantum logic. Synthese 186, 3 (2012), 753\u2013773.","journal-title":"Synthese"},{"issue":"2","key":"e_1_3_1_7_2","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1142\/S0219749908003530","article-title":"Quantum computation tree logic: Model checking and complete calculus","volume":"6","author":"Baltazar P.","year":"2008","unstructured":"P. Baltazar, R. Chadha, and P. Mateus. 2008. Quantum computation tree logic: Model checking and complete calculus. International Journal of Quantum Information 6, 2 (2008), 219\u2013236.","journal-title":"International Journal of Quantum Information"},{"key":"e_1_3_1_8_2","first-page":"14","volume-title":"International Conference on Quantum, Nano, and Micro Technologies","author":"Baltazar P.","year":"2007","unstructured":"P. Baltazar, R. Chadha, P. Mateus, and A. Sernadas. 2007. Towards model-checking quantum security protocols. In International Conference on Quantum, Nano, and Micro Technologies. IEEE, 14."},{"issue":"4","key":"e_1_3_1_9_2","doi-asserted-by":"crossref","first-page":"781","DOI":"10.1007\/s11225-014-9592-x","article-title":"Duality for the logic of quantum actions","volume":"103","author":"Bergfeld J. M.","year":"2015","unstructured":"J. M. Bergfeld, K. Kishida, J. Sack, and S. Zhong. 2015. Duality for the logic of quantum actions. Studia Logica 103, 4 (2015), 781\u2013805.","journal-title":"Studia Logica"},{"issue":"4","key":"e_1_3_1_10_2","doi-asserted-by":"crossref","first-page":"823","DOI":"10.2307\/1968621","article-title":"The logic of quantum mechanics","volume":"57","author":"Birkhoff G.","year":"1936","unstructured":"G. Birkhoff and J. von Neumann. 1936. The logic of quantum mechanics. Annals of Mathematics 57, 4 (1936), 823\u2013843.","journal-title":"Annals of Mathematics"},{"key":"e_1_3_1_11_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"Blackburn P.","year":"2001","unstructured":"P. Blackburn, M. de Rijke, and Y. Venema. 2001. Modal Logic. Cambridge University Press."},{"issue":"1","key":"e_1_3_1_12_2","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1142\/S0219749904000067","article-title":"Dynamic quantum logic for quantum programs","volume":"2","author":"Brunet O.","year":"2004","unstructured":"O. Brunet and P. Jorrand. 2004. Dynamic quantum logic for quantum programs. International Journal of Quantum Information 2, 1 (2004), 45\u201354.","journal-title":"International Journal of Quantum Information"},{"key":"e_1_3_1_13_2","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"International Conference on Integrated Formal Methods","author":"Chaki S.","year":"2004","unstructured":"S. Chaki, E. M. Clarke, J. Ouaknine, N. Sharygina, and N. Sinha. 2004. State\/event-based software model checking. In International Conference on Integrated Formal Methods. Springer, 128\u2013147."},{"issue":"1","key":"e_1_3_1_14_2","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/BF02120818","article-title":"Semantics of the minimal logic of quantum mechanics","volume":"30","author":"Dishkant H.","year":"1972","unstructured":"H. Dishkant. 1972. Semantics of the minimal logic of quantum mechanics. Studia Logica 30, 1 (1972), 23\u201330.","journal-title":"Studia Logica"},{"issue":"2","key":"e_1_3_1_15_2","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0097-3165(71)90040-9","article-title":"Lexicographic orthogonality","volume":"11","author":"Foulis D. J.","year":"1971","unstructured":"D. J. Foulis and C. H. Randall. 1971. Lexicographic orthogonality. Journal of Combinatorial Theory, Series A 11, 2 (1971), 157\u2013162.","journal-title":"Journal of Combinatorial Theory, Series A"},{"key":"e_1_3_1_16_2","first-page":"39","article-title":"Eine Interpretation des intuitionischen Aussagenkalk\u00fcls","volume":"4","author":"G\u00f6del K.","year":"1933","unstructured":"K. G\u00f6del. 1933. Eine Interpretation des intuitionischen Aussagenkalk\u00fcls. Ergebnisse Eines Mathematischen Kolloquiumus 4 (1933), 39\u201340.","journal-title":"Ergebnisse Eines Mathematischen Kolloquiumus"},{"key":"e_1_3_1_17_2","volume-title":"Logics of Time and Computation (second ed.)","author":"Goldblatt R.","year":"1987","unstructured":"R. Goldblatt. 1987. Logics of Time and Computation (second ed.). Center for the Study of Language and Information."},{"key":"e_1_3_1_18_2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/BF00652069","article-title":"Semantic analysis of orthologic","volume":"3","author":"Goldblatt R. I.","year":"1974","unstructured":"R. I. Goldblatt. 1974. Semantic analysis of orthologic. Journal of Philosophical Logic 3 (1974), 19\u201335.","journal-title":"Journal of Philosophical Logic"},{"key":"e_1_3_1_19_2","doi-asserted-by":"crossref","unstructured":"G. M. Hardegree. 1974. The conditional in quantum logic. Synthese 29 (1974) 63\u201380.","DOI":"10.1007\/BF00484952"},{"key":"e_1_3_1_20_2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"Harel D.","year":"2000","unstructured":"D. Harel, D. Kozen, and J. Tiuryn. 2000. Dynamic Logic. MIT Press."},{"issue":"3","key":"e_1_3_1_21_2","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1305\/ndjfl\/1093891789","article-title":"Implication connectives in orthomodular lattices","volume":"16","author":"Herman L.","year":"1975","unstructured":"L. Herman, E. L. Marsden, and R. Piziak. 1975. Implication connectives in orthomodular lattices. Notre Dame Journal of Formal Logic 16, 3 (1975), 305\u2013328.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"e_1_3_1_22_2","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-662-57669-4_14","volume-title":"International Workshop on Logic, Language, Information, and Computation","author":"Kawano T.","year":"2018","unstructured":"T. Kawano. 2018. Advanced Kripke frame for quantum logic. In International Workshop on Logic, Language, Information, and Computation. 237\u2013249."},{"issue":"1","key":"e_1_3_1_23_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s00236-013-0185-3","article-title":"Termination of nondeterministic quantum programs","volume":"51","author":"Li Y.","year":"2014","unstructured":"Y. Li, N. Yu, and M. Ying. 2014. Termination of nondeterministic quantum programs. Acta Informatica 51, 1 (2014), 1\u201324.","journal-title":"Acta Informatica"},{"key":"e_1_3_1_24_2","doi-asserted-by":"crossref","unstructured":"P. Mateus J. Ramos A. Sernadas and C. Sernadas. 2009. Temporal logics for reasoning about quantum systems. In Semantic techniques in quantum computation S. Gay and I. Mackie (Eds.). Cambridge University Press 389\u2013413.","DOI":"10.1017\/CBO9781139193313.011"},{"key":"e_1_3_1_25_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2268135","article-title":"Some theorems about the sentential calculi of Lewis and Heyting","volume":"13","author":"McKinsey J. C. C.","year":"1933","unstructured":"J. C. C. McKinsey and A. Tarski. 1933. Some theorems about the sentential calculi of Lewis and Heyting. Journal of Symbolic Logic 13 (1933), 1\u201315.","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_3_1_26_2","series-title":"Fundamental Theories of Physics","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9026-6","volume-title":"Quantum Logic in Algebraic Approach","author":"R\u00e9dei M.","year":"1998","unstructured":"M. R\u00e9dei. 1998. Quantum Logic in Algebraic Approach. Fundamental Theories of Physics, Vol. 91. Springer."},{"key":"e_1_3_1_27_2","first-page":"293","article-title":"Orthocomplemented lattices satisfying the exchange axiom","volume":"17","author":"Sasaki U.","year":"1954","unstructured":"U. Sasaki. 1954. Orthocomplemented lattices satisfying the exchange axiom. Journal of Science Hiroshima University A 17 (1954), 293\u2013302.","journal-title":"Journal of Science Hiroshima University A"},{"key":"e_1_3_1_28_2","doi-asserted-by":"crossref","unstructured":"C. Stirling. 1992. Modal and temporal logics. In Handbook of Logic in Computer Science S. Abramsky D. M. Gabbay and T. S. E. Maibaum (Eds.). Vol. 2. Clarendon 478\u2013563.","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"issue":"5","key":"e_1_3_1_29_2","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1023\/A:1025693128153","article-title":"Extended quantum logic","volume":"32","author":"Tokuo K.","year":"2003","unstructured":"K. Tokuo. 2003. Extended quantum logic. Journal of Philosophical Logic 32, 5 (2003), 549\u2013563.","journal-title":"Journal of Philosophical Logic"},{"key":"e_1_3_1_30_2","article-title":"Quantum B\u00fcchi automata","author":"Wang Q.","year":"2018","unstructured":"Q. Wang and M. Ying. 2018. Quantum B\u00fcchi automata. arXiv preprint arXiv:1804.08982 (2018).","journal-title":"arXiv preprint arXiv:1804.08982"},{"key":"e_1_3_1_31_2","unstructured":"N. Yu. 2019. Quantum temporal logic. (2019). arXiv preprint arXiv:1908.00158."},{"issue":"2","key":"e_1_3_1_32_2","first-page":"112","article-title":"A formal state-property duality in quantum logic","volume":"10","author":"Zhong S.","year":"2017","unstructured":"S. Zhong. 2017. A formal state-property duality in quantum logic. Studies in Logic 10, 2 (2017), 112\u2013133.","journal-title":"Studies in Logic"},{"issue":"1","key":"e_1_3_1_33_2","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/s11225-017-9733-0","article-title":"Correspondence between Kripke frames and projective geometries","volume":"106","author":"Zhong S.","year":"2018","unstructured":"S. Zhong. 2018. Correspondence between Kripke frames and projective geometries. Studia Logica 106, 1 (2018), 167\u2013189.","journal-title":"Studia Logica"},{"issue":"2","key":"e_1_3_1_34_2","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/s10849-017-9262-2","article-title":"On the modal logic of the non-orthogonality relation between quantum states","volume":"27","author":"Zhong S.","year":"2018","unstructured":"S. Zhong. 2018. On the modal logic of the non-orthogonality relation between quantum states. Journal of Logic, Language and Information 27, 2 (2018), 157\u2013173.","journal-title":"Journal of Logic, Language and Information"},{"key":"e_1_3_1_35_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s11229-021-03453-5","article-title":"Quantum states: An analysis via the orthogonality relation","volume":"199","author":"Zhong S.","year":"2021","unstructured":"S. Zhong. 2021. Quantum states: An analysis via the orthogonality relation. Synthese 199 (2021), 1\u201328.","journal-title":"Synthese"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576926","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3576926","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:24Z","timestamp":1750178184000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576926"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,17]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,7,31]]}},"alternative-id":["10.1145\/3576926"],"URL":"https:\/\/doi.org\/10.1145\/3576926","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,17]]},"assertion":[{"value":"2022-01-31","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-30","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-03-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}