Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
Hostname: page-component-745bb68f8f-grxwn Total loading time: 0 Render date: 2025-02-06T19:03:44.714Z Has data issue: false hasContentIssue false

10 - Temporal Logics for Reasoning about Quantum Systems

Published online by Cambridge University Press:  05 July 2014

By
Paulo Mateus ,
Jaime Ramos ,
Amílcar Sernadas  and
Cristina Sernadas
Edited by
Simon Gay  and
Ian Mackie
Paulo Mateus
Affiliation:
Instituto Superior Técnico
Jaime Ramos
Affiliation:
Instituto Superior Técnico
Amílcar Sernadas
Affiliation:
Instituto Superior Técnico
Cristina Sernadas
Affiliation:
Instituto Superior Técnico
Simon Gay
Affiliation:
University of Glasgow
Ian Mackie
Affiliation:
Imperial College London
Get access

Summary

Abstract

Reasoning about quantum systems has gained prominence due to a big potential in applications such as information processing, security, distributed systems, and randomized algorithms. This fact has attracted research in formal reasoning about quantum states, programs, and processes. On the other hand, temporal logics have proved to be successful in the verification of classical distributed systems and security protocols. In this chapter we extend exogenous quantum propositional logic with temporal modalities, considering both linear and branching time. We provide a weakly complete Hilbert calculi for the proposed quantum temporal logics and study their SAT and model-checking problems.

10.1 Introduction

Reasoning about quantum systems has gained prominence due to their potential applications in information processing, security, distributed systems and randomized algorithms. This has attracted research in formal reasoning about quantum states (see for instance van der Meyden and Patra 2003b, a; Mateus and Sernadas 2006; Chadha et al. 2009; Caleiro et al. 2006) and quantum programs (cf. Knill 1996; Sanders and Zuliani 2000; Abramsky and Coecke 2004; D'Hondt and Panangaden 2004; Altenkirch and Grattage 2005; Selinger and Valiron 2005; Baltag and Smets 2006; Baltazar et al. 2007; Chadha et al. 2006, 2007; Baltazar et al. 2008). On the other hand, formal methods have proved to be successful in design and verification of classical distributed systems and security protocols (e.g., Clarke and Wing 1996; Meadows 2003). Herein, we present branching and linear temporal logics for reasoning about evolution of quantum systems composed of a fixed finite set of qubits.

Type
Chapter
Information
Semantic Techniques in Quantum Computation , pp. 389 - 413
Publisher: Cambridge University Press
Print publication year: 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S., and Coecke, B. (2004) A categorical semantics of quantum protocols. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pages 415–125. IEEE Computer Society.Google Scholar
Altenkirch, T., and Grattage, J. (2005) A functional quantum programming language. In Proceedings ofthe 20th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 249–258. IEEE Computer Society.Google Scholar
Baltag, A., and Smets, S. (2006) LQP: The dynamic logic of quantum information. Mathematical Structures in Computer Science 16(3):491–525.CrossRefGoogle Scholar
Baltazar, P, Chadha, R., and Mateus, P. (2008) Quantum computation tree logic -model checking and complete calculus. International Journal of Quantum Information 6(2):219–236.CrossRefGoogle Scholar
Baltazar, P., Chadha, R., Mateus, P., and Sernadas, A. (2007) Towards model-checking quantum security protocols. In Dini, P., editor, Proceedings of the First Workshop on Quantum Security: QSec'07, page 0014. IEEE Press. Joint e-proceedings with Quantum, Nano, and Micro Technologies: ICQNM '07. 6 pages.Google Scholar
Baltazar, P., and Mateus, P. (2009) Temporalization of probabilistic propositional logic. In Logical Foundations of Computer Science 2009, volume 5407 of Lecture Notes in Computer Science, pages 46–60. Springer.Google Scholar
Basu, S., Pollack, R., and Roy, M.-F. (2003) Algorithms in Real Algebraic Geometry. Springer.CrossRefGoogle Scholar
Caleiro, C., Mateus, P., Sernadas, A., and Sernadas, C. (2006) Quantum institutions. In Futatsugi, K., Jouannaud, J.-P., and Meseguer, J., editors, Algebra, Meaning, and Computation - Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, volume 4060 of Lecture Notes in Computer Science, pages 50–64. Springer-Verlag.Google Scholar
Caleiro, C., Sernadas, C., and Sernadas, A. (1999) Parameterisation of logics. In Fiadeiro, J., editor, Recent Trends in Algebraic Development Techniques - Selected Papers, volume 1589 of Lecture Notes in Computer Science, pages 48–62. Springer-Verlag.Google Scholar
Chadha, R., Cruz-Filipe, L., Mateus, P., and Sernadas, A. (2007) Reasoning about probabilistic sequential programs. Theoretical Computer Science 379(1-2):142-165.CrossRefGoogle Scholar
Chadha, R., Mateus, P., and Sernadas, A. (2006) Reasoning about quantum imperative programs. Electronic Notes in Theoretical Computer Science 158:19–10. Invited talk at the Twenty-second Conference on the Mathematical Foundations of Programming Semantics.CrossRefGoogle Scholar
Chadha, R., Mateus, P., Sernadas, A., and Sernadas, C. (2009) Extending classical logic for reasoning about quantum systems. In Engesser, K., Gabbay, D. M., and Lehmann, D., editors, Handbook ofQuantum Logic and Quantum Structures: Quantum Logic, pages 325–372. Elsevier.Google Scholar
Clarke, E. M., and Emerson, E. A. (1981) Design and synthesis of synchronization skeletons using branching time temporal logics. In Proceeding of the Workshop on Logics of Programs, volume 131 of LNCS. Springer-Verlag.Google Scholar
Clarke, E. M., and Schlingloff, B.-H. (2001) Model checking. In Handbook of Automated Reasoning, pages 1635-1790.Google Scholar
Clarke, E. M., and Wing, J. M. (1996) Formal methods: state of the art and future directions. ACM Computing Surveys 28(4):626–643.CrossRefGoogle Scholar
D'Hondt, E., and Panangaden, P. (2004) Quantum weakest preconditions. In Selinger, P., editor, Proceedings ofthe 2nd International Workshop on Quantum Programming Languages, number 33 in TUCS General Publications, pages 75-90. Turku Centre for Computer Science.Google Scholar
Fagin, R., Halpern, J. Y., and Megiddo, N. (1990) A logic for reasoning about probabilities. Information and Computation 87(1-2):78-128.CrossRefGoogle Scholar
Gabbay, D., Pnueli, A., Shelah, S., and Stavi, J. (1980) The temporal analysis of fairness. In Proceedings 7th Symposium on Principles of Programming Languages, POPL'80, pages 163173. ACM.Google Scholar
Knill, E. (1996) Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National Laboratory.CrossRefGoogle Scholar
Mateus, P., and Sernadas, A. (2006) Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation 204(5):771–794.CrossRefGoogle Scholar
Mateus, P., Sernadas, A., and Sernadas, C. (2005) Exogenous semantics approach to enriching logics. In Sica, G., editor, Essays on the Foundations of Mathematics and Logic, volume 1 of Advanced Studies in Mathematics and Logic, pages 165–194. Polimetrica.Google Scholar
Meadows, C. (2003) Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE Journal on Selected Areas in Communications 21(1):44–54.CrossRefGoogle Scholar
Naur, P. (1963) Revised report on the algorithmic language Algol 60. The Computer Journal 5:349-367.Google Scholar
Sanders, J. W., and Zuliani, P. (2000) Quantum programming. In Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 80–99. Springer.Google Scholar
Selinger, P., and Valiron, B. (2005) A lambda calculus for quantum computation with classical control. In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA), volume 3461 of Lecture Notes in Computer Science, pages 354–368. Springer.Google Scholar
Shenvi, N., Kempe, J., and Whaley, K. B. (2003) Quantum random-walk search algorithm. Physical Review A 67(5):052307.CrossRefGoogle Scholar
Sistla, A. P., and Clarke, E. M. (1985) The complexity of propositional linear temporal logics. Journal of ACM 32(3):733–749.CrossRefGoogle Scholar
van der Meyden, R., and Patra, M. (2003a) Knowledge in quantum systems. In Tennenholtz, M., editor, Theoretical Aspects of Rationality and Knowledge, pages 104–117. ACM.Google Scholar
van der Meyden, R., and Patra, M. (2003b) A logic for probability in quantum systems. In Baaz, M., and Makowsky, J. A., editors, Computer Science Logic, volume 2803 of Lecture Notes in Computer Science, pages 427–440. Springer-Verlag.Google Scholar

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×