A Quantum Computing Approach to Model Checking for Advanced Manufacturing Problems

Abstract

This project studied the feasibility of integrating the capabilities of the D-Wave adiabatic quantum annealing processor into a Model Checking (MC) approach based on Counter-example Guided Abstraction Refinement (CEGAR). The computational bottleneck of this approach is the solution of certain combinatorial optimization problems for which the D-Wave processor was specifically designed. We developed a set of tools to sidestep the restrictions imposed by the limited connectivity of the processor, performed a set of benchmarking tests of the device, and implemented a proof of concept example that integrated the quantum processor with regular model checking techniques.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 2014
Accession Number
ADA605962

Entities

People

  • Federico M. Spedalieri
  • John Damoulakis

Organizations

  • University of Southern California

Tags

Communities of Interest

  • Energy and Power Technologies
  • Materials and Manufacturing Processes
  • Sensors

DTIC Thesaurus Topics

  • Advanced Manufacturing
  • Air Force
  • Air Force Research Laboratories
  • Algorithms
  • Computer Programming
  • Computer Programs
  • Computers
  • Control Systems
  • Information Science
  • Integer Programming
  • Linear Programming
  • Lisp Programming Language
  • Magnetometers
  • Manufacturing
  • Optimization
  • Quantum Computers
  • Quantum Computing

Readers

  • Image Processing and Computer Vision.
  • Mathematical Modeling and Probability Theory.
  • Neural Network Machine Learning.

Technology Areas

  • Quantum Computing