A Scalable Synthesis-based Approach for Autonomous Airport Runway Management

As global air traffic increases, ensuring safe and efficient airport runway management becomes a critical challenge, with traditional Multi-Agent Path Finding (MAPF) approaches struggling to handle the dynamic, time-dependent nature of runway operations. This paper proposes a novel autonomous runway management system using discrete controller synthesis, a formal method that automatically generates controllers to enforce safety under complex temporal constraints. Additionally, to overcome the scalability limitations of controller synthesis, particularly the state explosion problem driven by the exponential growth of aircraft and runway variables, we introduce a state reduction technique based on information separation between movable and immovable aircraft. The experiment results demonstrate our method's capability in generating safe controllers and its effectiveness in reducing computational costs.