Чтобы устранить этот пробел, доцент Кан Мин До вместе с доцентом Цубасой Такаги и профессором Казухиро Огатой из Японского передового института науки и технологий (JAIST), Япония, разработали автоматизированный подход к проверке квантовых программ, основанный на базовой динамической квантовой логике (BDQL). BDQL точно отражает квантовую эволюцию и измерения в квантовой механике, обеспечивая логическую основу для формализации и проверки квантовых протоколов на соответствие их желаемым свойствам. Несмотря на свою эффективность, BDQL имел ограничения, в частности, неспособность обрабатывать взаимодействия между участниками квантовых протоколов.

Чтобы преодолеть эти ограничения, команда разработала новую логику, известную как Concurrent Dynamic Quantum Logic (CDQL), которая расширяет возможности BDQL для управления параллелизмом в квантовых протоколах. В своем недавнем исследовании, опубликованном 12 декабря в журнале ACM Transactions on Software Engineering and Methodology, доктор До объясняет: "CDQL эффективно формализует параллельное поведение и коммуникацию между участниками квантовых протоколов. Наша логическая структура также обеспечивает переход от моделей CDQLs к моделям BDQL, обеспечивая совместимость с семантикой BDQL, и внедряет стратегию отложенной перезаписи для быстрой проверки". Это усовершенствование не только повышает выразительность логики, но и ускоряет процесс верификации, делая его применимым к более широкому спектру проверенных практических квантовых приложений.

Одним из основных преимуществ CDQL перед BDQL является его способность обрабатывать параллельные действия. В то время как BDQL был ограничен последовательными действиями, CDQL может моделировать квантовые протоколы, которые требуют одновременного выполнения нескольких действий, что делает его более подходящим для решения реальных задач. Кроме того, наша логическая структура обеспечивает стратегию отложенной перезаписи для повышения эффективности процесса проверки. В частности, эта стратегия устраняет ненужные переходы с предыдущих этапов и повторно использует результаты, чтобы избежать ненужных вычислений. Это повышает скорость и масштабируемость проверки квантовых протоколов. Несмотря на свои преимущества, наш фреймворк имеет некоторые ограничения, такие как неспособность обрабатывать квантовый обмен данными по квантовым каналам. Однако доктор До и его команда планируют устранить это ограничение в будущем, чтобы повысить универсальность CDQL.

Для улучшения моделирования и верификации квантовых протоколов был разработан CDQL как расширение BDQL. Исследовательская группа успешно формализовала и верифицировала различные протоколы квантовой связи как в BDQL, так и в CDQL. "Наш автоматизированный подход к формальной верификации, использующий как BDQL, так и CDQL, обеспечивает строгую основу для верификации как последовательных, так и параллельных моделей квантовых протоколов. Это способствует повышению надежности основополагающих технологий, таких как квантовая коммуникация, квантовая криптография и распределенные квантовые вычислительные системы", - объясняет доктор До. Эта работа подчеркивает важность обеспечения корректности квантовых протоколов до их развертывания в критически важных приложениях.

В заключение, CDQL более эффективен, чем BDQL, для формализации квантовых протоколов с параллельными действиями. "В этой работе представлен автоматизированный подход с использованием CDQL для проверки корректности квантовых протоколов, обеспечивающий их надежность перед развертыванием в приложениях, критически важных для безопасности", - заключает доктор До. Далее он добавляет: "Обеспечивая корректность квантовых протоколов, эта работа способствует разработке надежных, защищенных от ошибок приложений".- свободные квантовые технологии, особенно в области квантовой коммуникации и криптографии, в ближайшие 5-10 лет".