A Framework for Black-Box Controller Design to Automatically Satisfy Specifications Using Signal Temporal Logic

We present a framework for including humanreadable specifications in the design of black-box autonomous systems, or systems whose construct are prohibitively complex to analyze or intuit. By integrating parametric Signal Temporal Logic (pSTL), we can systematically evaluate and refine deep reinforcement learning policies to ensure compliance with predefined system specifications. Our approach is tested in a simulated autonomous driving environment, where we train a deep reinforcement learning agent in Mario Kart SNES using Proximal Policy Optimization. The agent is evaluated based on its ability to navigate a structured driving course while satisfying a set of a priori requirements; this evaluation is performed by writing and solving the parameters in a pSTL statement. This work contributes to the broader effort of bridging formal methods and data-driven learning, providing insights for researchers and operators alike in developing AIbased controllers for real-world autonomous systems.