Sergio Montenegro

Sergio Montenegro

Public confidence in democratic institutions has declined across many OECD countries over recent decades, while political participation and policy influence remain unevenly distributed across socioeconomic groups. Concurrently, democratic backsliding, declining electoral participation, and persistent concerns regarding institutional transparency and accountability have raised questions about whether existing governance structures are capable of sustaining broad-based legitimacy in complex modern societies. These developments motivate a central institutional design question: can governance systems be restructured to expand participation, improve transparency, and strengthen accountability without undermining stability or decision quality? This thesis proposes Programmable Participatory Governance (PPG), a formal governance framework designed to address these institutional deficits through the integration of democratic theory, institutional economics, and cryptographically verifiable distributed systems. PPG synthesises insights from deliberative and participatory democracy, collective action theory, direct democratic governance, and distributed computation to define a programmable architecture for transparent, verifiable, and scalable civic coordination. The framework is formally specified and evaluated through simulation and systems-oriented architectural analysis. The thesis examines how programmable governance mechanisms can support participatory decision-making while preserving procedural integrity, auditability, and institutional resilience under conditions of large-scale coordination. The objective is not to replace existing democratic institutions outright, but to explore how computationally mediated governance structures may augment or improve contemporary democratic processes in contexts where conventional institutions exhibit persistent structural limitations.

Kirill Djebko, Tom Baumann, Erik Dilger et al.

Attitude control is essential for many satellite missions. Classical controllers, however, are time-consuming to design and sensitive to model uncertainties and variations in operational boundary conditions. Deep Reinforcement Learning (DRL) offers a promising alternative by learning adaptive control strategies through autonomous interaction with a simulation environment. Overcoming the Sim2Real gap, which involves deploying an agent trained in simulation onto the real physical satellite, remains a significant challenge. In this work, we present the first successful in-orbit demonstration of an AI-based attitude controller for inertial pointing maneuvers. The controller was trained entirely in simulation and deployed to the InnoCube 3U nanosatellite, which was developed by the Julius-Maximilians-Universität Würzburg in cooperation with the Technische Universität Berlin, and launched in January 2025. We present the AI agent design, the methodology of the training procedure, the discrepancies between the simulation and the observed behavior of the real satellite, and a comparison of the AI-based attitude controller with the classical PD controller of InnoCube. Steady-state metrics confirm the robust performance of the AI-based controller during repeated in-orbit maneuvers.

Frank Flederer, Ludwig Ostermayer, Dietmar Seipel et al.

System relevant embedded software needs to be reliable and, therefore, well tested, especially for aerospace systems. A common technique to verify programs is the analysis of their abstract syntax tree (AST). Tree structures can be elegantly analyzed with the logic programming language Prolog. Moreover, Prolog offers further advantages for a thorough analysis: On the one hand, it natively provides versatile options to efficiently process tree or graph data structures. On the other hand, Prolog's non-determinism and backtracking eases tests of different variations of the program flow without big effort. A rule-based approach with Prolog allows to characterize the verification goals in a concise and declarative way. In this paper, we describe our approach to verify the source code of a flash file system with the help of Prolog. The flash file system is written in C++ and has been developed particularly for the use in satellites. We transform a given abstract syntax tree of C++ source code into Prolog facts and derive the call graph and the execution sequence (tree), which then are further tested against verification goals. The different program flow branching due to control structures is derived by backtracking as subtrees of the full execution sequence. Finally, these subtrees are verified in Prolog. We illustrate our approach with a case study, where we search for incorrect applications of semaphores in embedded software using the real-time operating system RODOS. We rely on computation tree logic (CTL) and have designed an embedded domain specific language (DSL) in Prolog to express the verification goals.