REVIEW 1 cited by
Quantum Temporal Logic
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Quantum Temporal Logic
read the original abstract
In this paper, we introduce a model of quantum concurrent program, which can be used to model the behaviour of reactive quantum systems and to design quantum compilers. We investigate quantum temporal logic, QTL, for the specification of quantum concurrent systems by suggesting the time-dependence of events. QTL employs the projections on subspaces as atomic propositions, which was established in the Birkhoff and von Neumann's classic treatise on quantum logic. For deterministic functional quantum program, We prove a quantum B\"{o}hm-Jacopini theorem which states that any such program is equivalent to a Q-While program. The decidability of basic QTL formulae for general quantum concurrent program is studied.
Forward citations
Cited by 1 Pith paper
-
Complex Bounded Operators in Isabelle/HOL
A comprehensive, machine-checked Isabelle/HOL formalization of complex Hilbert spaces and bounded operators, including adjoints, unitaries, projectors, the BLT extension theorem, Loewner order, and ℓ2 spaces.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.