Skip to main content
SpringerLink
Log in

On Relation Between Linear Temporal Logic and Quantum Finite Automata

  • Published:
Journal of Logic, Language and Information Aims and scope Submit manuscript

Abstract

Linear temporal logic is a widely used method for verification of model checking and expressing the system specifications. The relationship between theory of automata and logic had a great influence in the computer science. Investigation of the relationship between quantum finite automata and linear temporal logic is a natural goal. In this paper, we present a construction of quantum finite automata on finite words from linear-time temporal logic formulas. Further, the relation between quantum finite automata and linear temporal logic is explored in terms of language recognition and acceptance probability. We have shown that the class of languages accepted by quantum finite automata are definable in linear temporal logic, except for measure-once one-way quantum finite automata.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Fig. 1
Fig. 2

Similar content being viewed by others

References

  • Ambainis, A., Beaudry, M., Golovkins, M., Kikusts, A., Mercer, M., & Thérien, D. (2006). Algebraic results on quantum automata. Theory of Computing Systems, 39(1), 165–188.

    Article  Google Scholar 

  • Bertoni, A., Mereghetti, C., & Palano, B. (2003). Quantum computing: 1-Way quantum automata. In International conference on developments in language theory. (pp. 1–20). Springer.

  • Bhatia, A. S., & Kumar, A. (2018). Modeling of RNA secondary structures using two-way quantum finite automata. Chaos, Solitons & Fractals, 116, 332–339.

    Article  Google Scholar 

  • Bhatia, A. S., & Kumar, A. (2019a). Quantum finite automata: Survey, status and research directions. arXiv preprint: arXiv:1901.07992.

  • Bhatia, A. S., & Kumar, A. (2019b). On the power of two-way multihead quantum finite automata. RAIRO-Theoretical Informatics and Applications, 53(1–2), 19–35.

    Article  Google Scholar 

  • Bhatia, A. S., & Kumar, A. (2019c). Quantum \(\omega \)-automata over infinite words and their relationships. International Journal of Theoretical Physics, 58(3), 878–889.

    Article  Google Scholar 

  • Brodsky, A., & Pippenger, N. (2002). Characterizations of 1-way quantum finite automata. SIAM Journal on Computing, 31(5), 1456–1478.

    Article  Google Scholar 

  • Büchi, J. R. (1960a). On a decision method in restricted second order arithmetic, In Proceedings of international congress on logic, method, and philosophy of science (pp. 425–435) Stanford, CA: Stanford University Press.

    Chapter  Google Scholar 

  • Büchi, J. R. (1960b). Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6(1–6), 66–92.

    Article  Google Scholar 

  • De Giacomo, G., & Vardi, M. Y. (2013). Linear temporal logic and linear dynamic logic on finite traces. In IJCAI-International joint conference on artificial intelligence (Vol. 13, pp. 854–860).

  • Dzelme-Bērziņa, I. (2009). Mathematical logic and quantum finite state automata. Theoretical Computer Science, 410(20), 1952–1959.

    Article  Google Scholar 

  • Elgot, C. C. (1961). Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98(1), 21–51.

    Article  Google Scholar 

  • Guan, J., Feng, Y., Turrini, A., & Ying, M. (2019). Model checking applied to quantum physics. arXi preprint arXiv:1902.03218.

  • Kamp, J. A. W. (1968). Tense logic and the theory of linear order. Ph.D. thesis, University of California, University Microfilms, Los Angeles.

  • Kondacs, A., & Watrous, J. (1997). On the power of quantum finite state automata. In Proceedings of 38th annual symposium on foundations of computer science (pp. 66–75). IEEE.

  • Leucker, M., & Sánchez, C. (2007). Regular linear temporal logic. In International colloquium on theoretical aspects of computing (pp. 291–305). Springer.

  • Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., & Zhan, N. (2019). Formal verification of quantum algorithms using quantum Hoare logic. In International conference on computer aided verification (pp. 187–207). Springer.

  • McNaughton, R. (1966). Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5), 521–530.

    Article  Google Scholar 

  • McNaughton, R. (1969). The loop complexity of regular events. Information Sciences, 1(3), 305–328.

    Article  Google Scholar 

  • McNaughton, R., & Papert, S. A. (1971). Counter-free automata (MIT research monograph no. 65). Cambridge: The MIT Press.

    Google Scholar 

  • Moore, C., & Crutchfield, J. P. (2000). Quantum automata and quantum grammars. Theoretical Computer Science, 237(1–2), 275–306.

    Article  Google Scholar 

  • Pnueli, A. (1977). The temporal logic of programs. In Proceedings of 18th annual symposium on foundations of computer science (pp. 46–57). IEEE.

  • Rabin, M. O. (1969). Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141, 1–35.

    Google Scholar 

  • Schützenberger, M. P. (1965). On finite monoids having only trivial subgroups. Information and Control, 8(2), 190–194.

    Article  Google Scholar 

  • Sistla, A. P., & Clarke, E. M. (1985). The complexity of propositional linear temporal logics. Journal of the ACM (JACM), 32(3), 733–749.

    Article  Google Scholar 

  • Wang, J. (2012). Handbook of finite state based models and applications. Boca Raton: CRC Press.

    Google Scholar 

  • Wilke, T. (1999). Classifying discrete temporal properties. In Annual symposium on theoretical aspects of computer science (pp. 32–46). Springer.

  • Zheng, S., Li, L., & Qiu, D. (2011). Two-tape finite automata with quantum and classical states. International Journal of Theoretical Physics, 50(4), 1262–1281.

    Article  Google Scholar 

  • Zheng, S., Qiu, D., Li, L., & Gruska, J. (2012). One-way finite automata with quantum and classical states. In Languages alive (pp. 273–290). Springer.

  • Zimmermann, M. (2013). Optimal bounds in parametric LTL games. Theoretical Computer Science, 493, 30–45.

    Article  Google Scholar 

  • Zuck, L. (1987). Past temporal logic. Ann Arbor, 1001(48106–1346), 49.

    Google Scholar 

Download references

Acknowledgements

Amandeep Singh Bhatia was supported by Maulana Azad National Fellowship (MANF), funded by Ministry of Minority Affairs, Government of India.

Author information

Authors and Affiliations

  1. Department of Computer Science, Thapar Institute of Engineering & Technology, Patiala, India

    Amandeep Singh Bhatia & Ajay Kumar

Authors
  1. Amandeep Singh Bhatia
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ajay Kumar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Amandeep Singh Bhatia.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Bhatia, A.S., Kumar, A. On Relation Between Linear Temporal Logic and Quantum Finite Automata. J of Log Lang and Inf 29, 109–120 (2020). https://doi.org/10.1007/s10849-019-09302-6

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10849-019-09302-6

Keywords

Search

Navigation