SpecTRM-RL State explosion prevented by dividing components into parallel state machines Traffic Density Schedule Slot [1...90 LOW Available Average Aircraft Scheduled High Blocked Unknown Unknown Complete state space is the cross productSpecTRM-RL State explosion prevented by dividing components into parallel state machines. Aircraft Scheduled Available Blocked Unknown Traffic Density Schedule Slot [1...90] High Unknown Low Average Complete state space is the cross product. ✄