Finite abstractions with robustness margins for temporal logic-based control synthesis. (English) Zbl 1344.93046

Summary: This paper introduces a notion of finite abstractions that can be used to synthesize robust controllers for dynamical systems from temporal logic specifications. These finite abstractions, equipped with certain robustness margins, provide a unified approach to various issues commonly encountered in implementing control systems, such as inter-sample behaviors of a sampled-data system, effects of imperfect state measurements and unmodeled dynamics. The main results of this paper demonstrate that the robustness margins can effectively account for the mismatches between a control system and its finite abstractions used for control synthesis. The quantitative nature of the robustness margins also makes it possible to study the trade-offs between the performance of controllers and their robustness against various types of adversaries (e.g., delays, measurement errors, or modeling uncertainties). We use a simple Adaptive Cruise Control (ACC) example to illustrate such robustness-performance trade-offs.


93B50 Synthesis problems
93B35 Sensitivity (robustness)
93C57 Sampled-data control/observation systems
93C41 Control/observation systems with incomplete information
93C40 Adaptive control/observation systems


CoSyma; TuLiP
Full Text: DOI


[1] Fainekos, G. E.; Girard, A.; Kress-Gazit, H.; Pappas, G. J., Temporal logic motion planning for dynamic robots, Automatica, 45, 343-352, (2009) · Zbl 1158.93369
[2] Kloetzer, M.; Belta, C., A fully automated framework for control of linear systems from temporal logic specifications, IEEE Trans. Automat. Control, 53, 287-297, (2008) · Zbl 1367.93202
[3] Kress-Gazit, H.; Fainekos, G. E.; Pappas, G. J., Temporal-logic-based reactive mission and motion planning, IEEE Trans. Robot., 25, 1370-1381, (2009)
[4] Liu, J.; Ozay, N.; Topcu, U.; Murray, R., Synthesis of reactive switching protocols from temporal logic specifications, IEEE Trans. Automat. Control, 58, 7, 1771-1785, (2013) · Zbl 1369.93307
[5] J. Liu, U. Topcu, N. Ozay, R.M. Murray, Reactive controllers for differentially flat systems with temporal logic constraints, in: Proc. of CDC, 2012, pp. 7664-7670.
[6] N. Ozay, J. Liu, P. Prabhakar, R.M. Murray, Computing augmented finite transition systems to synthesize switching protocols for polynomial switched systems, in: Proc. of ACC, 2013, pp. 6237-6244.
[7] S. Mouelhi, A. Girard, G. Gössler, Cosyma: a tool for controller synthesis using multi-scale abstractions, in: Proc. of HSCC, 2013, pp. 83-88.
[8] Tabuada, P., Verification and control of hybrid systems: A symbolic approach, (2009), Springer · Zbl 1195.93001
[9] Tabuada, P.; Pappas, G. J., Linear time logic control of discrete-time linear systems, IEEE Trans. Automat. Control, 51, 1862-1877, (2006) · Zbl 1366.93413
[10] Wongpiromsarn, T.; Topcu, U.; Murray, R. M., Receding horizon temporal logic planning, IEEE Trans. Automat. Control, 57, 2817-2830, (2012) · Zbl 1369.93392
[11] Zamani, M.; Pola, G.; Mazo, M.; Tabuada, P., Symbolic models for nonlinear control systems without stability assumptions, IEEE Trans. Automat. Control, 57, 1804-1809, (2012) · Zbl 1369.93002
[12] Reiszig, G., Computing abstractions of nonlinear systems, IEEE Trans. Automat. Control, 56, 2583-2598, (2011) · Zbl 1368.93178
[13] Tazaki, Y.; Imura, J., Discrete abstractions of nonlinear systems based on error propagation analysis, IEEE Trans. Automat. Control, 57, 550-564, (2012) · Zbl 1369.93121
[14] S. Karaman, E. Frazzoli, Sampling-based algorithms for optimal motion planning with deterministic \(\mu\)-calculus specifications, in: Proc. of ACC, 2012, pp. 735-742.
[15] E.M. Wolff, R.M. Murray, Optimal control of nonlinear systems with temporal logic specifications, in: Proc. of ISRR, 2013.
[16] J. Liu, N. Ozay, Abstraction, discretization, and robustness in temporal logic control of dynamical systems, in: Proc. of HSCC, 2014, pp. 293-302. · Zbl 1362.93058
[17] Baier, C.; Katoen, J.-P., Principles of model checking, (2008), MIT Press
[18] Clarke, E. M.; Grumberg, O.; Peled, D., Model checking, (1999), MIT Press
[19] Angeli, D.; Sontag, E. D., Forward completeness, unboundedness observability, and their Lyapunov characterizations, Systems Control Lett., 38, 4, 209-217, (1999) · Zbl 0986.93036
[20] R. Alur, T.A. Henzinger, O. Kupferman, M.Y. Vardi, Alternating refinement relations, in: Proc. of CONCUR, 1998, pp. 163-178. · Zbl 1070.68524
[21] Pola, G.; Tabuada, P., Symbolic models for nonlinear control systems: alternating approximate bisimulations, SIAM J. Control Optim., 48, 719-733, (2009) · Zbl 1194.93020
[22] Fainekos, G. E.; Pappas, G. J., Robustness of temporal logic specifications for continuous-time signals, Theoret. Comput. Sci., 410, 42, 4262-4291, (2009) · Zbl 1186.68287
[23] Angeli, D., A Lyapunov approach to incremental stability properties, IEEE Trans. Automat. Control, 47, 3, 410-421, (2002) · Zbl 1364.93552
[24] Pola, G.; Girard, A.; Tabuada, P., Approximately bisimilar symbolic models for nonlinear control systems, Automatica, 44, 10, 2508-2516, (2008) · Zbl 1155.93322
[25] Y. Li, J. Liu, N. Ozay, Computing finite abstractions with robustness margins via local reachable set over-approximation, in: IFAC Conference on Analysis and Design of Hybrid Systems, ADHS, 2015.
[26] Bloem, R.; Jobstmann, B.; Piterman, N.; Pnueli, A.; Sa’ar, Y., Synthesis of reactive (1) designs, J. Comput. System Sci., 78, 911-938, (2012) · Zbl 1247.68050
[27] Ehlers, R., Generalized rabin (1) synthesis with applications to robust system synthesis, (NASA Formal Methods, (2011), Springer), 101-115
[28] T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, R.M. Murray, TuLiP: a software toolbox for receding horizon temporal logic planning, in: Proc. of HSCC, 2011.
[29] A. Cervin, B. Lincoln, J. Eker, K.-E. Arzén, G. Buttazzo, The jitter margin and its application in the design of real-time control systems, in: Proceedings of the 10th International Conference on Real-Time and Embedded Computing Systems and Applications. Gothenburg, Sweden, 2004, pp. 1-9.
[30] Hale, J. K., Introduction to functional differential equations. vol. 99, (1993), Springer
[31] Franklin, G. F.; Workman, M. L.; Powell, D., Digital control of dynamic systems, (1997), Addison-Wesley Longman Publishing Co., Inc.
[32] P. Nilsson, O. Hussien, Y. Chen, A. Balkan, M. Rungger, A. Ames, J. Grizzle, N. Ozay, H. Peng, P. Tabuada, Preliminary results on correct-by-construction control software synthesis for adaptive cruise control, in: Proc. of CDC, 2014, pp. 816-823.
[33] O. Mickelin, N. Ozay, R.M. Murray, Synthesis of correct-by-construction control protocols for hybrid systems using partial state information, in: Proc. of ACC, 2014, pp. 2305-2311.
[34] Pola, G.; Pepe, P.; Di Benedetto, M. D.; Tabuada, P., Symbolic models for nonlinear time-delay systems using approximate bisimulations, Systems Control Lett., 59, 6, 365-373, (2010) · Zbl 1197.93090
[35] Girard, A.; Pappas, G., Approximation metrics for discrete and continuous systems, IEEE Trans. Automat. Control, 52, 782-798, (2007) · Zbl 1366.93032
[36] U. Topcu, N. Ozay, J. Liu, R.M. Murray, On synthesizing robust discrete controllers under modeling uncertainty, in: Proc. of HSCC, 2012, pp. 85-94. · Zbl 1362.68190
[37] R. Majumdar, E. Render, P. Tabuada, Robust discrete synthesis against unspecified disturbances, in: Proc. of HSCC, 2011, pp. 211-220. · Zbl 1362.68175
[38] Tarraf, D.; Megretski, A.; Dahleh, M. A., A framework for robust stability of systems over finite alphabets, IEEE Trans. Automat. Control, 53, 5, 1133-1146, (2008) · Zbl 1367.93482
[39] Tarraf, D. C., A control-oriented notion of finite state approximation, IEEE Trans. Automat. Control, 57, 12, 3197-3202, (2012) · Zbl 1369.93352
[40] M. Rungger, P. Tabuada, Abstracting and refining robustness for cyber-physical systems, in: Proc. of HSCC, 2014, pp. 223-232. · Zbl 1362.93132
[41] A. Borri, G. Pola, M.D. Di Benedetto, A symbolic approach to the design of nonlinear networked control systems, in: Proc. of HSCC, 2012, pp. 255-264. · Zbl 1361.68018
[42] M. Zamani, M. Mazo Jr., A. Abate, Finite abstractions of networked control systems, in: Proc. of CDC, 2014, pp. 95-100.
[43] D. Liberzon, Limited-information control of hybrid systems via reachable set propagation, in: Proc. of HSCC, 2013, pp. 11-20. · Zbl 1362.93081
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.