PLQP & Company: Decidable Logics for Quantum Algorithms

Alexandru Baltag, Jort Bergfeld, Kohei Kishida, Joshua Sack, Sonja Smets, Shengyang Zhong

Research output: Contribution to journalArticlepeer-review


We introduce a probabilistic modal (dynamic-epistemic) quantum logic PLQP for reasoning about quantum algorithms. We illustrate its expressivity by using it to encode the correctness of the well-known quantum search algorithm, as well as of a quantum protocol known to solve one of the paradigmatic tasks from classical distributed computing (the leader election problem). We also provide a general method (extending an idea employed in the decidability proof in Dunn et al. (J. Symb. Log. 70:353–359, 2005)) for proving the decidability of a range of quantum logics, interpreted on finite-dimensional Hilbert spaces. We give general conditions for the applicability of this method, and in particular we apply it to prove the decidability of PLQP.

Original languageEnglish (US)
Pages (from-to)3628-3647
Number of pages20
JournalInternational Journal of Theoretical Physics
Issue number10
StatePublished - Oct 1 2014
Externally publishedYes


  • Decidability
  • Modal logic
  • Quantum computation
  • Quantum logic

ASJC Scopus subject areas

  • Mathematics(all)
  • Physics and Astronomy (miscellaneous)


Dive into the research topics of 'PLQP & Company: Decidable Logics for Quantum Algorithms'. Together they form a unique fingerprint.

Cite this