Skip to main content
Model checking LTL over controllable linear systems is decidable
Departmental Papers (ESE)
  • Paulo Tabuada, University of Pennsylvania
  • George J. Pappas, University of Pennsylvania
Document Type
Conference Paper
Date of this Version
Postprint version. Published in Lecture Notes in Computer Science, Volume 2623, Hybrid Systems: Computation and Control: 6th International Workshop, HSCC 2003, Prague, Czech Republic, April 3, 2003, pages 498-513.
Publisher URL:

The use of algorithmic verification and synthesis tools for hybrid systems is currently limited to systems exhibiting simple continuous dynamics such as timed automata or rectangular hybrid systems. In this paper we enlarge the class of systems amenable to algorithmic analysis and synthesis by showing decidability of model checking Linear Temporal Logic (LTL) formulas over discrete time, controllable, linear systems. This result follows from the construction of a language equivalent, finite abstraction of a control system based on a set of finite observations which correspond to the atomic propositions appearing in a given LTL formula. Furthermore, the size of this abstraction is shown to be polynomial in the dimension of the control system and the number of observations. These results open the doors for verification and synthesis of continuous and hybrid control systems from LTL specifications.

Citation Information
Paulo Tabuada and George J. Pappas. "Model checking LTL over controllable linear systems is decidable" (2003)
Available at: