Personal tools
You are here: Home Graduate Study Formal Verification Methods for Quantum Systems

Formal Verification Methods for Quantum Systems

Develop temporal logics and model checking techniques for quantum systems

It has been predicted that any large-scale overhaul of information science in the 21st century will have to include quantum information. The last decade has witnessed a quantum leap in both design and implementation of quantum protocols, which rely on various fundamental properties of quantum mechanics for their performance, security and correctness. The increasing complexity of these advanced quantum protocols demands a unified high-level approach to their formal verification, far beyond the currently available ad-hoc schemes based on matrix calculus.

The overall goal of the project is to develop temporal logics and model checking techniques for quantum systems, similarly to the development in the classical world. However the existing classical methods have to be properly extended to address fundamentally different concepts of quantum systems, such as entanglement which will affect the structure of the agent's local view in a protocol. The first approach would be based on characterising the class of  quantum properties that can be abstracted into similar classical properties  to be verified using classical model checking. This will pave the road to  develop the required logic which can explicitly express unique aspects of
the dynamics of quantum systems, and to develop model checking algorithms for it. The general aim is to bring logic-based formal reasoning techniques into the domain of quantum computation.

Potential Supervisors

Elham Kashefi

Richard Mayr

Document Actions