Skip to main content
Linear Time Logic Control of Discrete-Time Linear Systems
Departmental Papers (ESE)
  • Paulo Tabuada, University of California
  • George J Pappas, University of Pennsylvania

The control of complex systems poses new challenges that fall beyond the traditional methods of control theory. One of these challenges is given by the need to control, coordinate and synchronize the operation of several interacting submodules within a system. The desired objectives are no longer captured by usual control specifications such as stabilization or output regulation. Instead, we consider specifications given by linear temporal logic (LTL) formulas. We show that existence of controllers for discrete-time controllable linear systems and LTL specifications can be decided and that such controllers can be effectively computed. The closed-loop system is of hybrid nature, combining the original continuous dynamics with the automatically synthesized switching logic required to enforce the specification.

Document Type
Conference Paper
Date of this Version
Copyright 2006 IEEE. Reprinted from IEEE Transactions on Automatic Control, Volume 51, Issue 12, pages 1862-1877.

This material is posted here with permission of the IEEE. Such permission of the IEEE does not in any way imply IEEE endorsement of any of the University of Pennsylvania's products or services. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to By choosing to view this document, you agree to all provisions of the copyright laws protecting it.
  • automatic synthesis,
  • discrete-time,
  • linear control systems,
  • hybrid systems,
  • linear time logic
Citation Information
Paulo Tabuada and George J Pappas. "Linear Time Logic Control of Discrete-Time Linear Systems" (2006)
Available at: