Model checking LTL over controllable linear systems is decidable

Paulo Tabuada, University of Pennsylvania
George J. Pappas, University of Pennsylvania

Article comments

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: http://springerlink.metapress.com/link.asp?id=eyk912mcngh0wppm

Abstract

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.