Techniques for determining a trajectory for an autonomous vehicle are described herein. In general, determining a route can include utilizing a search algorithm such as Monte Carlo Tree Search (MCTS) to search for possible trajectories, while using temporal logic formulas, such as Linear Temporal Logic (LTL), to validate or reject the possible trajectories. Trajectories can be selected based on various costs and constraints optimized for performance. Determining a trajectory can include determining a current state of the autonomous vehicle, which can include determining static and dynamic symbols in an environment. A context of an environment can be populated with the symbols, features, predicates, and LTL formula. Rabin automata can be based on the LTL formula, and the automata can be used to evaluate various candidate trajectories. Nodes of the MCTS can be generated and actions can be explored based on machine learning implemented as, for example, a deep neural network.