TY - GEN
T1 - Translating temporal logic to controller specifications
AU - Fainekos, Georgias E.
AU - Loizou, Savvas G.
AU - Pappas, George J.
PY - 2006
Y1 - 2006
N2 - The problem of designing hybrid controllers in order to satisfy safety or liveness specifications has received much attention in the past decade. Much more recently, there is an increased interest in designing hybrid controllers in order to achieve more sophisticated discrete specifications, such as those expressible in temporal logics. A great challenge is how to compose safety and liveness controllers in order to achieve more complex specifications. Existing approaches are predominantly bottom-up, in the sense that the overall control and composition (or switching) logic requires verification of the integrated closed-loop hybrid system. In this paper, we advocate and develop a top-down approach for this problem by synthesizing controllers which satisfy the specification by construction. Given a flat linear temporal logic specification as an input, we develop an algorithm that translates the temporal logic specification into a hybrid automaton where in each discrete mode we impose controller specifications for the continuous dynamics. In addition to achieving the desired specification by construction, our methodology provides a very natural interface between high level logic design and low level control design.
AB - The problem of designing hybrid controllers in order to satisfy safety or liveness specifications has received much attention in the past decade. Much more recently, there is an increased interest in designing hybrid controllers in order to achieve more sophisticated discrete specifications, such as those expressible in temporal logics. A great challenge is how to compose safety and liveness controllers in order to achieve more complex specifications. Existing approaches are predominantly bottom-up, in the sense that the overall control and composition (or switching) logic requires verification of the integrated closed-loop hybrid system. In this paper, we advocate and develop a top-down approach for this problem by synthesizing controllers which satisfy the specification by construction. Given a flat linear temporal logic specification as an input, we develop an algorithm that translates the temporal logic specification into a hybrid automaton where in each discrete mode we impose controller specifications for the continuous dynamics. In addition to achieving the desired specification by construction, our methodology provides a very natural interface between high level logic design and low level control design.
UR - http://www.scopus.com/inward/record.url?scp=34147138966&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34147138966&partnerID=8YFLogxK
U2 - 10.1109/cdc.2006.377825
DO - 10.1109/cdc.2006.377825
M3 - Conference contribution
AN - SCOPUS:34147138966
SN - 1424401712
SN - 9781424401710
T3 - Proceedings of the IEEE Conference on Decision and Control
SP - 899
EP - 904
BT - Proceedings of the 45th IEEE Conference on Decision and Control 2006, CDC
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 45th IEEE Conference on Decision and Control 2006, CDC
Y2 - 13 December 2006 through 15 December 2006
ER -