Certifying Algorithms for Interactive Components and Distributed Systems

一个证明算法不仅产生一个结果，而且产生一个证明者，证明结果的正确性。在最好的情况下，证人是不言而喻的。否则，一个（相对简单的）检查器算法验证见证。自2000年代以来，已经开发了许多“经典”算法的认证变体。例如，MPI萨尔布吕肯的LEDA库包含许多认证算法。现代计算机集成系统和基础设施通常由交互组件构建，形成松散耦合和交互节点的分布式系统。交互式组件的算法通常不会终止。此外，分布式系统的组件通常不知道整个系统结构的布局。因此，这些组件和系统的算法的行为与经典算法根本不同。本计画研究认证的概念在何种程度上可以应用于互动式元件与分散式系统。这个问题特别有趣，因为这类系统经常被非计算机科学家使用，或者因为它们的内部细节是秘密，但它们使用的正确性仍然需要令人信服地证明。这个问题立即从不同的角度着手处理。我们开始与已知的数据结构的认证算法为基础，并试图将使用的建设原则，证人和他们的检查员，通用的交互式组件。特别是，这涉及到算法产生一个数据流作为证据的想法，检查器以很短的延迟进行验证，但仍然与运行的算法并发。分布式系统的算法通常由交互式组件的算法组成，这就产生了认证组件与认证系统的可组合性问题。由计算机节点和通信通道组成的网络是一种特殊的分布式系统。对于这样的网络，存在许多众所周知的算法-例如，纠正通信信道中可能的故障的通信协议。这就产生了这样一个问题，即这种协议是否可以以某种方式设计来证明。在网络中，每个节点只能与其直接邻居通信。这足以形成和使用网络的全局构造（例如，虚拟生成树）。已经存在用于此的合适算法，现在将其扩展以进行认证。另一个有趣的任务是将图上的已知证明算法转换为网络节点上的算法，以及证人和他们的检查员。

A certifying algorithm produces not only a result, but also a witness, who shows the result's correctness. In the best case, the witness is self-explanatory. Otherwise, a (comparatively simple) checker algorithm verifies the witness. Since the 2000s, certifying variants of numerous "classic" algorithms have been developed. The LEDA library of the MPI Saarbrücken, for instance, contains numerous certifying algorithms. Modern computer-integrated systems and infrastructures are often built from interactive components, forming a distributed system of loosely coupled and interactive nodes. Algorithms for interactive components generally do not terminate. Furthermore, the components of a distributed system usually do not know the layout of the entire system structure. Therefore, algorithms for such components and systems behave fundamentally differently than classic algorithms. This project researches, to what extend the concept of certification can be applied to interactive components and distributed systems. This question is particularly interesting because such systems are often used by non-computer scientists, or because their inner details are a secret, but the correctness of their usage still needs to be demonstrated convincingly. The problem is tackled from different angles at once. We start with known certifying algorithms for data structures as a basis and try to transfer the used construction principles for witnesses and their checkers to generic interactive components. In particular, this involves the idea that the algorithm produces a data stream as a witness, which the checker verifies with a short delay, but still concurrently to the running algorithm. Algorithms for distributed systems often consist of algorithms for interactive components, which gives rise to the question of the composability of certifying components to a certifying system. A network of computer nodes and communication channels is a special distributed system. For such networks, there exist numerous wellknown algorithms - for instance, communication protocols that correct a possible fault in the communication channels. This gives rise to the question, whether such protocols can be designed in a certain way to be certifying. In a network, each node can only communicate with its direct neighbors. This is sufficient to form and use global constructs of the network (for instance, a virtual spanning tree). There already exist suitable algorithms for this, which are now to be extended in order to be certifying. Another interesting task is the conversion of known certifying algorithms on graphs into algorithms on the nodes of a network, together with the witnesses and their checkers.