Quantum Temporal Logic

Origin. Emerging area combining temporal logic with quantum systems (2010s-present). Baltazar, Chadha, Mateus, Sernadas and others. Verifying quantum protocols over time. Quantum Markov chains with temporal specifications. Connection to quantum model checking.

Models. Temporal properties of quantum systems. Quantum states evolve via unitaries and measurements. Verify: "eventually reaches target state with high probability." Quantum Markov chains: probabilistic + quantum. Temporal operators over quantum trajectories.

Formalism.

Quantum Markov chain: Q = (H, S, s₀, δ, L) where:

H: Hilbert space
S: classical states
s₀: initial state
δ: S × S → CP(H) (transition via completely positive maps)
L: S → 2^AP (labeling)

Quantum LTL (conceptual): Path through quantum states with measurements. P≥p[Fφ]: probability ≥ p of eventually satisfying φ.

Measurement outcomes: Temporal properties over measurement sequences. "If we measure repeatedly, eventually get outcome 1."

Quantum CTL: Branching over quantum superposition + measurement. ∃≥p(Fφ): exists path with prob ≥ p reaching φ.

Entanglement over time: Track entanglement through protocol steps. "After n steps, parties remain entangled."

Verification tasks:

Reachability: can system reach target state?
Safety: does system avoid bad states?
Liveness: does system eventually do something?

Symbols.

Symbol	Unicode	Name	Meaning
P≥p	—	Probability bound	Quantum probability
F	—	Eventually	Future operator
G	—	Always	Global operator
ρ	U+03C1	Rho / Density matrix	Quantum state
U	—	Unitary	Evolution
M	—	Measurement	Quantum measurement
⊗	U+2297	Circled times / Tensor	Composite system
≥	U+2265	Greater-than or equal	Probability threshold in P≥p
∃	U+2203	There exists	Path quantifier of the branching-time fragment
δ	U+03B4	Delta	Transition function into completely positive maps
φ	U+03C6	Phi	Formula variable
CP(H)	—	Completely positive maps on H	Codomain of the transition function
AP	—	Atomic propositions	Labels attached to classical states
s₀	—	Initial state	Start of a trajectory
L	—	Labelling function	Assigns atomic propositions to states

Metatheory. Baltazar, Chadha, and Mateus gave a quantum computation tree logic with a model-checking algorithm and a complete calculus (2008), building on the exogenous quantum propositional logic of Mateus and Sernadas (2006), which has a weakly complete axiomatization. The decidable results all come from restricting the model. Gay, Nagarajan, and Papanikolaou's QMC model checker verifies protocols expressed in the stabilizer fragment, which is decidable because stabilizer circuits are classically simulable in polynomial time by the Gottesman–Knill theorem, sharpened by Aaronson and Gottesman (2004). For quantum Markov chains in finite dimension, reachability and repeated reachability are decidable, and the analysis proceeds by decomposing the state space into bottom strongly connected components of the trace-preserving superoperator and computing its asymptotic average (Ying, Yu, Feng, and Duan). Outside these restrictions the state space is a continuum and the automata-theoretic constructions of classical model checking have no direct analogue.

Applies to. Quantum protocol verification. Quantum error correction. Quantum cryptography (BB84, etc.). Quantum algorithms. Quantum communication. Fault-tolerant quantum computing.

Limitations. Classical temporal logic presupposes a path can be observed without altering it; quantum measurement changes the state, so a trajectory records what was done rather than what was true, and the semantics must fix a measurement schedule before any path formula has meaning. Atomic propositions are projections or subspaces, and these form an orthomodular rather than a Boolean lattice, so the Boolean connectives of LTL and CTL are not available on them unless the projections commute — which is exactly when the model has already been made classical. Branching-time path quantification requires a basis the model does not determine. Decidability results are confined to the stabilizer fragment and to finite-dimensional quantum Markov chains; outside these, the state space is a continuum and no automata-theoretic construction applies. Cost is exponential in the number of qubits beyond the stabilizer case, and the several proposals use incompatible syntaxes, so results do not transfer.