Paper Info
Title
A fully automated framework for control of linear systems from LTL specifications
Abstract
We consider the following problem: given a linear system and an LTL−−X formula over a set of linear predicates in its state variables, find a feedback control law with polyhedral bounds and a set of initial states so that all trajectories of the closed loop system satisfy the formula. Our solution to this problem consists of three main steps. First, we partition the state space in accordance with the predicates in the formula and construct a transition system over the partition quotient, which captures our capability of designing controllers. Second, using model checking, we determine runs of the transition system satisfying the formula. Third, we generate the control strategy. Illustrative examples are included.
Year
DOI
Venue
2006
10.1007/11730637_26
HSCC
Keywords
Field
DocType
automated framework,partition quotient,following problem,closed loop system,ltl specification,initial state,linear system,feedback control law,x formula,transition system,linear predicate,control strategy,state space,model checking,satisfiability
Transition system,Model checking,Linear system,Algebra,Algorithm,Linear temporal logic,State variable,Linear logic,Hybrid system,State space,Mathematics
Conference
Volume
ISSN
ISBN
3927
0302-9743
3-540-33170-0
Citations 
PageRank 
References 
36
2.55
21
Authors
2
Name
Order
Citations
PageRank
Marius Kloetzer147629.21
Calin Belta22197153.54