Quantum computing is a rapidly growing technology that utilizes the laws of quantum physics to solve complex computational problems that are extremely difficult for classical computing. Researchers worldwide have developed many quantum algorithms to take advantage of quantum computing, demonstrating significant improvements over classical algorithms.

Quantum circuits, which are models of quantum computation, are crucial for developing these algorithms. They are used to design and implement quantum algorithms before actual deployment on quantum hardware.

Quantum circuits comprise a sequence of quantum gates, measurements, and initializations of qubits, among other actions. Quantum gates perform quantum computations by operating on qubits, which are the quantum counterparts of classical bits (0s and 1s), and by manipulating the quantum states of the system. Quantum states are the output of quantum circuits, which can be measured to obtain classical outcomes with probabilities, from which further actions can be done.

Since quantum computing is often counter-intuitive and dramatically different from classical computing, the probability of errors is much higher. Hence, it is necessary to verify that quantum circuits have the desired properties and function as intended. This can be done through model checking, a formal verification technique used to verify whether systems satisfy desired properties.

Although some model checkers are dedicated to quantum programs, there is a gap between model-checking quantum programs and quantum circuits due to different representations and no iterations in quantum circuits.

Addressing this gap, Assistant Professor Canh Minh Do and Professor Kazuhiro Ogata from Japan Advanced Institute of Science and Technology (JAIST) proposed a symbolic model checking approach.

Dr. Do explains, “Considering the success of model-checking methods for verification of classical circuits, model-checking of quantum circuits is a promising approach. We developed a symbolic approach for model checking of quantum circuits using laws of quantum mechanics and basic matrix operations using the Maude programming language.”

Their approach is detailed in a study published in the journal PeerJ Computer Science.

Maude is a high-level specification/programming language based on rewriting logic, which supports the formal specification and verification of complex systems. It is equipped with a Linear Temporal Logic (LTL) model checker, which checks whether systems satisfy the specified properties.

Additionally, Maude allows the creation of precise mathematical models of systems. The researchers formally specified quantum circuits in Maude, as a series of quantum gates and measurement applications, represented as basic matrix operations using laws of quantum mechanics with the Dirac notation. They specified the initial state and the desired properties of the system in LTL.

By using a set of quantum physics laws and basic matrix operations formalized in our specifications, quantum computation can be reasoned in Maude. They then used the built-in Maude LTL model checker to automatically verify whether quantum circuits satisfy the desired properties.

They used this approach to check several early quantum communication protocols, including Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, Entanglement Swapping, Quantum Gate Teleportation, Two Mirror-image Teleportation, and Quantum Network Coding, each with increasing complexity.

They found that the original version of Quantum Gate Teleportation did not satisfy its desired property. By using this approach, the researchers notably proposed a revised version and confirmed its correctness.

These findings signify the importance of the proposed innovative approach for the verification of quantum circuits. However, the researchers also point out some limitations of their method, requiring further research.

Dr. Do says, “In the future, we aim to extend our symbolic reasoning to handle more quantum gates and more complicated reasoning on complex number operations. We also would like to apply our symbolic approach to model-checking quantum programs and quantum cryptography protocols.”

Verifying the intended operation of quantum circuits will be highly valuable in the upcoming era of quantum computing. In this context, the present approach marks the first step toward a general framework for the verification and specification of quantum circuits, paving the way for error-free quantum computing.

Robots that can navigate various terrains both rapidly and efficiently could be highly advantageous, as they could successfully complete complex missions in challenging environments. For instance, these robots could help to monitor complex natural environments, such as forests, or could search for survivors after natural disasters.

One of the most common types of robots designed to navigate varying terrains are legged robots, whose bodies are often inspired by the body structure of animals. To move swiftly in varying terrains, legged robots should be able to adapt their movements and gait-styles based on detected changes in their environmental conditions.

Researchers at the Higher Institute for Applied Science and Technology in Damascus, Syria, recently developed a new method to facilitate a smooth transition between the different gaits of a hexapod robot.

Their proposed gait control technique, introduced in a paper published in Heliyon, is based on so-called central pattern generators (CPGs), computational approaches that mimic biological CPGs. These are the neural networks underpinning many rhythmic movements performed by humans and animals (i.e., walking, swimming, jogging, etc.).

“Our recent publication is a foundational component of a larger project that aims to revolutionize the locomotion control of hexapod robots,” Kifah Helal, corresponding author of the paper, told Tech Xplore.

“While machine learning techniques have not yet been integrated, the architecture we’ve designed lays the groundwork for such advanced applications. Our methodology is crafted with future machine learning integration in mind, ensuring that when implemented, it will significantly enhance malfunction compensation.”

Helal and his colleagues first set out to design and simulate a six-legged (hexapod) robot. This simulated robotic platform was then used to test their proposed control architecture based on CPGs.

“Our control method leverages the principles of CPGs where each leg of the hexapod robot is governed by a distinct rhythmic signal,” Helal explained. “The essence of different gaits lies in the phase differences between these signals. Our paper’s core contribution is the novel interaction design among the oscillators, ensuring seamless gait transitions.”

Helal and his colleagues also developed a workspace trajectory generator, a computational tool that translates the outputs of oscillators integrated in a hexapod robot into trajectories for its feet, ensuring that these trajectories remain effective during transitions. In initial tests, their proposed control architecture was found to enable stable, efficient and swift changes in gait in both a simulated and real hexapod robot.

“The most striking outcomes of our research are the harmonious blend of transition smoothness and speed,” Helal said. “Essentially, it’s the fusion of fluidity and quickness that sets our work apart from other previous efforts. We also validated a mapping function that ensures the robot’s foot trajectory remains effective throughout these transitions.”

The new architecture introduced by this team of researchers could soon be tested in further experiments and applied to other legged robots, to allow them to swiftly adapt to environmental changes while retaining their agility.

In their next studies, Helal and his colleagues plan to further improve their method, to tackle potential malfunctions and further boost its performance when robots encounter particularly challenging terrains.

“Looking ahead, we plan to delve deeper into machine learning to further refine our robot’s environmental adaptability,” Helal added. “We’re particularly excited about exploring malfunction compensation and integrating pain sensing as feedback mechanisms.

“These advancements will not only improve the robot‘s interaction with its surroundings but also pave the way for more autonomous and resilient robotic systems.”

© 2024 Science X Network