Implementing Differentiable SSTL in Julia for System Optimization

Project Description

This project focuses on building a Domain Specific Language (DSL) in Julia based on Signal Spatio-Temporal Logic (SSTL). SSTL allows us to verify if complex physical systems such as power grids or traffic networks meet safety requirements over time and space.

The student will design a flexible syntax allowing users to define these requirements independent of network topology. Crucially, the student will implement this logic with differentiable semantics. Unlike standard logic (which returns a simple True/False), this approach calculates a continuous robustness score. This allows the logical specifications to integrate directly with Julia’s gradient-based optimization solvers, enabling the software to automatically tune simulation parameters to maximize safety and performance.

We are looking for a highly motivated student to lead the design and implementation of this framework, bridging the gap between formal verification and differentiable programming.

Prerequisites

1. Software Design: Proficiency in Julia (preferred) or Python. Strong interest in compiler design, metaprogramming, or building clean APIs.
2. Mathematics: Understanding of calculus, specifically how derivatives and gradients are used in optimization.
3. Scientific Computing: Familiarity with Ordinary Differential Equations (ODEs) and numerical simulations.

For more information, please reach out to jonathan.hellwig@kit.edu.