Termination of nondeterministic quantum programs
From MaRDI portal
Publication:2453979
Abstract: We define a language-independent model of nondeterministic quantum programs in which a quantum program consists of a finite set of quantum processes. These processes are represented by quantum Markov chains over the common state space. An execution of a nondeterministic quantum program is modeled by a sequence of actions of individual processes. These actions are described by super-operators on the state Hilbert space. At each step of an execution, a process is chosen nondeterministically to perform the next action. A characterization of reachable space and a characterization of diverging states of a nondeterministic quantum program are presented. We establish a zero-one law for termination probability of the states in the reachable space of a nondeterministic quantum program. A combination of these results leads to a necessary and sufficient condition for termination of nondeterministic quantum programs. Based on this condition, an algorithm is found for checking termination of nondeterministic quantum programs within a fixed finite-dimensional state space. A striking difference between nondeterministic classical and quantum programs is shown by example: it is possible that each of several quantum programs simulates the same classical program which terminates with probability 1, but the nondeterministic program consisting of them terminates with probability 0 due to the interference carried in the execution of them.
Recommendations
Cites work
- scientific article; zbMATH DE number 1579275 (Why is no real title available?)
- scientific article; zbMATH DE number 1612487 (Why is no real title available?)
- scientific article; zbMATH DE number 5162350 (Why is no real title available?)
- scientific article; zbMATH DE number 5708042 (Why is no real title available?)
- Bisimulation for quantum processes
- Communicating quantum processes
- Compiling quantum programs
- Counterfactual computation
- DYNAMIC QUANTUM LOGIC FOR QUANTUM PROGRAMS
- Functional and Logic Programming
- LQP: the dynamic logic of quantum information
- Proof rules for the correctness of quantum programs
- Quantum loop programs
- Quantum programming languages: survey and bibliography
- Quantum walks on graphs
- Quantum weakest preconditions
- Reasoning about imperative quantum programs
- Simulating and compiling code for the sequential quantum random access machine
- Termination of Probabilistic Concurrent Program
- Towards a quantum programming language
Cited in
(6)- Reachability and termination analysis of concurrent quantum programs
- Quantum Büchi automata
- Quantum temporal logic and reachability problems of matrix semigroups
- Semantic Analysis of a Linear Temporal Extension of Quantum Logic and Its Dynamic Aspect
- Toward automatic verification of quantum programs
- Quantum loop programs
This page was built for publication: Termination of nondeterministic quantum programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2453979)