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	Density matrix	Quantum state
U	—	Unitary	Evolution
M	—	Measurement	Quantum measurement
⊗	U+2297	Tensor	Composite system

Metatheory. Decidability depends on model class. Finite-dimensional quantum systems: some properties decidable. Approximation often needed. Connections to QPCP (quantum probabilistic checking). Active research area.

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

Limitations. Immature compared to classical temporal logic. Continuous state space challenges. Measurement disturbs state (non-classical). Tool support minimal. Theory still developing. Complexity not well-characterized.