Transition Systems.- Temporal Logics and Automata.- Model Checking.- Largest Finite Satisfying Region.- Finite Temporal Logic Control.- Discrete-Time Dynamical Systems.- Largest Satisfying Region.- Parameter Synthesis.- Temporal Logic Control.- Finite Bisimulations.- Language Guided Controller Synthesis.- Optimal Temporal Logic Control.- Background.