A Quantum Computing Approach to Model Checking for Advanced Manufacturing Problems
Federico M. Spedalieri, J. N. Damoulakis · 2014
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.