Termination of nondeterministic quantum programs

DOI10.1007/S00236-013-0185-3zbMATH Open1359.68092arXiv1201.0891OpenAlexW2016769804MaRDI QIDQ2453979FDOQ2453979

Authors: Yangjia Li, Nengkun Yu, Mingsheng Ying 

Publication date: 12 June 2014

Published in: Acta Informatica (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1201.0891

Recommendations

• Reachability and termination analysis of concurrent quantum programs
• Quantum loop programs
• Reachability analysis of quantum Markov decision processes
• Proof rules for the correctness of quantum programs
• Quantum programs with classical output streams (extended abstract)

Mathematics Subject Classification ID

Quantum algorithms and complexity in the theory of computing (68Q12)

Cites Work

• Compiling quantum programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Towards a quantum programming language
• Quantum walks on graphs
• Quantum programming languages: survey and bibliography
• LQP: the dynamic logic of quantum information
• Quantum weakest preconditions
• Bisimulation for quantum processes
• DYNAMIC QUANTUM LOGIC FOR QUANTUM PROGRAMS
• Proof rules for the correctness of quantum programs
• Reasoning about imperative quantum programs
• Communicating quantum processes
• Quantum loop programs
• Termination of Probabilistic Concurrent Program
• Counterfactual computation
• Functional and Logic Programming
• Title not available (Why is that?)
• Simulating and compiling code for the sequential quantum random access machine

Cited In (5)

• 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

Uses Software

• QPL
• qGCL
• QML

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)