Model checking LTL over controllable linear systems is decidableDepartmental Papers (ESE)
AbstractThe 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.
Document TypeConference Paper
Date of this Version4-3-2003
Citation InformationPaulo Tabuada and George J. Pappas. "Model checking LTL over controllable linear systems is decidable" (2003)
Available at: http://works.bepress.com/george_pappas/218/