Verifying Quantum Based Systems : What do we have to change?

Over the last decade quantum information technology emerged as a promising new field of research. The quantum algorithms and protocols developed in this context often exhibit non-intuitive behaviour, due to quantum specific properties–such as superposition, entanglement, and probabilistic outcomes–making it essential to build trust in these systems. Formal verification plays a key role in this process, and as such, research on verification and testing methods is as important as research on the quantum-based systems themselves.

In this thesis, we explore the changes needed to adapt existing formal verification and testing methods from classical, i.e., non-quantum based, to quantum based systems. As a part of this, we began by considering quantum based process calculi, as they are often used as a modelling language to specify the behaviour of a system in an abstract manner. In particular, encodings between different process calculi–used to compare their expressive power and suitability for different application areas–caught our interest. These encodings must satisfy specific quality criteria to rule out trivial or meaningless encodings. Gorla proposed one well-known set of quality criteria. Even though Gorla's framework is well-known, it was not designed for the quantum based setting; nevertheless we are able to prove its relevance in this context.

While still meaningful, these criteria may not be sufficient. Especially quantum specific principles push Gorla's criteria to their limits. Hence, in this thesis we define two new quantum specific criteria and adapt one of Gorla's most common and important criteria: operational correspondence. Our adaption leads to the new criterion probabilistic operational correspondence–a version of operational correspondence, that preserves and reflects the probabilistic nature of quantum processes. The three different variants we specify vary in the strength of the criterion. We also analyse the quality and relevance of each version by mapping them onto behavioural relations.

Since the specification of a formal testing theory for quantum based systems is another way of formal verification we also explore this possibility. After surveying the well-established foundations of formal testing for classical discrete and probabilistic processes, we identify the requirements and challenges for developing a testing theory for quantum based systems and outline a roadmap for its creation.

Im Verlaufe des letzten Jahrzehnts hat sich die Quanteninformationstechnologie als vielversprechendes neues Forschungsfeld abgezeichnet. Jedoch sollten wie bei jeder neuen technologischen Errungenschaft auch die Forschungsergebnisse in diesem Bereich mit Sorgfalt behandelt werden. Daher ist die Forschung an den Methoden zur Verifikation und dem Testen von quantenbasierten Systemen ebenso wichtig wie die Forschung an quantenbasierten Systemen selbst.

In dieser Arbeit gehen wir der Frage nach, welche Änderungen an den bestehenden Methoden zur formalen Verifikation und dem Testen erforderlich sind, wenn diese von nicht-quantenbasierten auf quantenbasierte Systeme übertragen werden. Im Rahmen dieser Fragestellung haben wir uns zunächst mit quantenbasierten Prozesskalkülen beschäftigt, da sie häufig als Modellierungssprache verwendet werden, um das Verhalten eines Systems in einer abstrakten Art und Weise zu spezifizieren. Besonders die Codierungen zwischen verschiedenen Prozesskalkülen, die zum Vergleich von deren Ausdruckskraft und Eignung für verschiedene Anwendungsbereiche verwendet werden, zogen hierbei unser Interesse auf sich. Derartige Codierungen müssen bestimmte Qualitätskriterien erfüllen, wodurch triviale oder bedeutungslose Codierungen verhindert werden. Wenngleich Gorlas renommiertes Framework an Qualitätskriterien nicht für die quantenbasierte Umgebung entwickelt wurde, sind wir in der Lage seine andauernde Relevanz in diesem Kontext nachzuweisen.

Obwohl diese Kriterien weiterhin sinnvoll sind, reichen sie möglicherweise nicht aus. Insbesondere bezüglich der quantenspezifischen Prinzipien stoßen Gorlas Kriterien an ihre Grenzen. Daher definieren wir in dieser Arbeit nicht nur zwei neue, quantenspezifische Kriterien, sondern passen auch eines der bekanntesten und wichtigsten Kriterien Gorlas an: operational correspondence. Unsere Anpassung führt zu dem neuen Kriterium probabilistic operational correspondence - einer Version von operational correspondence, die den probabilistischen Charakter der quantenmechanischen Prozesse bewahrt und widerspiegelt. Die drei verschiedenen Varianten dieses Kriteriums, die wir spezifizieren, unterscheiden sich in ihrer Striktheit. Zudem analysieren wir die Qualität und Relevanz jeder Version, indem wir sie auf Verhaltensrelationen abbilden.

Da die Entwicklung einer formalen Testtheorie für quantenbasierte Systeme eine weitere Möglichkeit der formalen Verifikation darstellt, untersuchen wir auch diese Option. Nach dem Verschaffen eines Überblickes über die bereits etablierten Grundlagen des formalen Testens für klassische diskrete und probabilistische Prozesse bestimmen wir die Anforderungen und Herausforderungen für die Entwicklung einer Testtheorie für quantenbasierte Systeme und skizzieren ein Konzept für deren Erstellung.