Linear temporal logic control of discrete-time linear systems