Certifying Algorithms for Interactive Components and Distributed Systems

• Applicant: Professor Dr. Wolfgang Reisig
• Subject Area: Theoretical Computer Science
• Term: from 2014 to 2019
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 261369405

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.

• DFG Programme: Research Grants