×

Augmented finite transition systems as abstractions for control synthesis. (English) Zbl 1379.93050

Summary: This work is motivated by the problem of synthesizing switching protocols for continuous switched systems described by differential or difference equations, in a way that guarantees that the resulting closed-loop trajectories satisfy certain high-level specifications expressed in linear temporal logic. We introduce augmented finite transition systems as an abstract representation of the continuous dynamics; the augmentation consists in encodings of liveness properties that can be used to enforce progress in accordance with the underlying continuous dynamics. Abstraction and refinement relations that induce a preorder on this class of finite transition systems are established, and, by construction, this preorder respects the feasibility (i.e., realizability) of the synthesis problem. Hence, the existence of a discrete strategy for one of these abstract finite transition systems guarantees the existence of a switching protocol for the continuous system that enforces the specification for all resulting trajectories. We show how abstractions and refinements can be computed for different classes of continuous systems through an incremental synthesis procedure that starts with a coarse abstraction and gradually refines it according to the established preorder relations. Finally, the incremental synthesis procedure is tailored to a class of temporal logic formulas by utilizing specific fixed-point structures to enable localized updates in the refinement steps. The procedure is not guaranteed to terminate in general but we illustrate its practical applicability on numerical examples.

MSC:

93B50 Synthesis problems
93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
03B44 Temporal logic

Software:

TuLiP; SPOTless; YALMIP
Full Text: DOI

References:

[1] Ahmadi AA, Majumdar A (2014) DSOS and SDSOS optimization: LP and SOCP-based alternatives to sum of squares optimization. In: Proceedings of the IEEE conference on decision and control, pp 394-401 · Zbl 1369.93355
[2] Ahmadi AA, Parrilo PA (2014) Towards scalable algorithms with formal guarantees for Lyapunov analysis of control systems via algebraic optimization · Zbl 1003.68069
[3] Baier C., Katoen J. (2008) Principles of model checking, MIT press · Zbl 1179.68076
[4] Batt G., Belta C., Weiss R. (2008) Temporal logic analysis of gene networks under parameter uncertainty. IEEE Trans Automatic Control 53(Special Issue):215-229 · Zbl 1366.92077 · doi:10.1109/TAC.2007.911330
[5] Belta C., Habets L. (2006) Controlling a class of nonlinear systems on rectangles. IEEE Trans Automatic Control 51(11):1749-1759 · Zbl 1366.93278 · doi:10.1109/TAC.2006.884957
[6] Bloem R, Jobstmann B, Piterman N, Pnueli A, Saar Y (2012) Synthesis of reactive (1) designs. J Comput System Sci 78:911-938 · Zbl 1247.68050 · doi:10.1016/j.jcss.2011.08.007
[7] Cámara J, Girard A, Gössler G (2011) Synthesis of switching controllers using approximately bisimilar multiscale abstractions. In: Proceeding of HSCC, pp 191-200 · Zbl 1362.93056
[8] Church A (1962) Logic, arithmetic and automata. In: Proceedings of the international congress of mathematicians, pp 23-35 · Zbl 0987.93072
[9] Clarke FH, Ledyaev YS, Stern RJ, Wolenski PR (1998) Nonsmooth analysis and control theory. Springer · Zbl 1047.49500
[10] Coogan S, Arcak M (2015) Efficient finite abstraction of mixed monotone systems. In: Proceedings of HSCC, pp 58-67 · Zbl 1364.93238
[11] Feuer A, Heymann M (1976) Ω-invariance in control systems with bounded controls. J Math Anal Appl 53(2):266-276 · Zbl 0326.49004 · doi:10.1016/0022-247X(76)90110-4
[12] Filippidis I, Dathathri S, Livingston SC, Ozay N, Murray RM (2016) Control design for hybrid systems with TuLiP: The temporal logic planning toolbox. In: Proceedings of MSC
[13] Girard A, Martin S (2012) Control synthesis for constrained nonlinear systems using hybridization and robust controllers on simplices. IEEE Trans Automatic Control 57:1046-1051 · Zbl 1369.93192 · doi:10.1109/TAC.2011.2168874
[14] Girard A, Pola G, Tabuada P (2010) Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans Automatic Control 55 (1):116-126 · Zbl 1144.93340 · doi:10.1109/TAC.2009.2034922
[15] Gol E, Ding X, Lazar M, Belta C (2012) Finite bisimulations for switched linear systems. In: Proceedings of IEEE CDC, pp 7632-7637 · Zbl 1360.93461
[16] Grädel E, Thomas W, Wilke T (eds.) (2002) Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science, vol. 2500. Springer · Zbl 1011.00037
[17] Gwerder M, Lehmann B, Tödtli J, Dorer V, Renggli F (2008) Control of thermally-activated building systems (tabs). Appl Energy 85(7):565-581. doi:10.1016/j.apenergy.2007.08.001 · doi:10.1016/j.apenergy.2007.08.001
[18] Habets L., Collins P., van Schuppen J. (2006) Reachability and control synthesis for piecewise-affine hybrid systems on simplices. IEEE Trans Automatic Control 51 (6):938-948 · Zbl 1366.93348
[19] Jiang ZP, Wang Y (2002) A converse Lyapunov theorem for discrete-time systems with disturbances. Syst Control Lett 45(1):49-58 · Zbl 0987.93072 · doi:10.1016/S0167-6911(01)00164-5
[20] Kesten Y, Pnueli A (2000) Verification by augmented finitary abstraction. Inf Comput 163(1):203-243 · Zbl 1003.68069 · doi:10.1006/inco.2000.3000
[21] Lin Y, Sontag ED, Wang Y (1996) A smooth converse Lyapunov theorem for robust stability. SIAM J Control Optimization 34(1):124-160 · Zbl 0856.93070 · doi:10.1137/S0363012993259981
[22] Liu J, Ozay N, Topcu U, Murray R (2013) Synthesis of reactive switching protocols from temporal logic specifications. IEEE Trans Automatic Control · Zbl 1369.93307
[23] Löfberg J (2004) Yalmip: a toolbox for modeling and optimization in matlab. In: Proceeding of IEEE CACSD, pp 284-289 · Zbl 1247.68050
[24] Mattila R, Mo Y, Murray RM (2015) An iterative abstraction algorithm for reactive correct-by-construction controller synthesis. In: Proceedings of IEEE CDC, pp 6147-+6152 · Zbl 1043.14018
[25] Nilsson P, Ozay N (2014) Incremental synthesis of switching protocols via abstraction refinement. In: Proceedings of CDC, pp 6246-6253
[26] Ozay N, Liu J, Prabhakar P, Murray R (2013) Computing augmented finite transition systems to synthesize switching protocols for polynomial switched systems. American Control Conference
[27] Parrilo P (2003) Semidefinite programming relaxations for semialgebraic problems. Math Program 96(2):293-320 · Zbl 1043.14018 · doi:10.1007/s10107-003-0387-5
[28] Piterman N, Pnueli A (2006) Faster solutions of rabin and streett games. In: Proceedings of IEEE LICS, pp 275-284
[29] Piterman N, Pnueli A, Sa’ar Y (2006) Synthesis of reactive (1) designs. In: Proceedings of VMCAI, pp 364-380 · Zbl 1176.68126
[30] Pnueli A, Rosner R (1989) On the synthesis of an asynchronous reactive module. In: Proceedings of ICALP, pp 652-671 · Zbl 0686.68015
[31] Romaní J, de Gracia A, Cabeza LF (2016) Simulation and control of thermally activated building systems (TABS). Energy & Buildings 127:22-42
[32] Sourbron M, Verhelst C, Helsen L (2013) Building models for model predictive control of office buildings with concrete core activation. J Build Perform Simul 6(3):175-198 · doi:10.1080/19401493.2012.680497
[33] Sun F, Ozay N, Wolff EM, Liu J, Murray RM (2014) Efficient control synthesis for augmented finite transition systems with an application to switching protocols. In: Proceedings of ACC · Zbl 0856.93070
[34] Svorenova M, Kretinsky J, Chmelik M, Chatterjee K, Cerna I, Belta C (2015) Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of HSCC, pp 259-268 · Zbl 1364.93751
[35] Tabuada P (2009) Verification and control of hybrid systems: a symbolic approach. Springer · Zbl 1195.93001
[36] Walter W, Thompson R (1998) Ordinary differential equations, 1 edn. Springer · Zbl 0991.34001
[37] Wolff E, Topcu U, Murray R (2013) Efficient reactive controller synthesis for a fragment of linear temporal logic. In: Proceedings of IEEE ICRA, pp. 5033-5040
[38] Yang L, Ozay N, Karnik A (2016) Synthesis of fault tolerant switching protocols for vehicle engine thermal management. In: Proceedings of ACC, pp 4213-4220 · Zbl 1247.68050
[39] Yordanov B, Tumova J, Cerna I, Barnat J, Belta C (2012) Temporal logic control of discrete-time piecewise affine systems. IEEE Trans Automatic Control 57(6):1491-1504 · Zbl 1257.93030 · doi:10.1109/TAC.2011.2178328
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.