IEEE/CAA Journal of Automatica Sinica
Citation:  W. Ren, Z.R. Pan, W. Xia, and X.M. Sun, “Hierarchical controller synthesis under linear temporal logic specifications using dynamic quantization,” IEEE/CAA J. Autom. Sinica, vol. 11, no. 10, pp. 2082–2098, Oct. 2024. doi: 10.1109/JAS.2024.124473 
Linear temporal logic (LTL) is an intuitive and expressive language to specify complex control tasks, and how to design an efficient control strategy for LTL specification is still a challenge. In this paper, we implement the dynamic quantization technique to propose a novel hierarchical control strategy for nonlinear control systems under LTL specifications. Based on the regions of interest involved in the LTL formula, an accepting path is derived first to provide a highlevel solution for the controller synthesis problem. Second, we develop a dynamic quantization based approach to verify the realization of the accepting path. The realization verification results in the necessity of the controller design and a sequence of quantization regions for the controller design. Third, the techniques of dynamic quantization and abstractionbased control are combined together to establish the localtoglobal control strategy. Both abstraction construction and controller design are local and dynamic, thereby resulting in the potential reduction of the computational complexity. Since each quantization region can be considered locally and individually, the proposed hierarchical mechanism is more efficient and can solve much larger problems than many existing methods. Finally, the proposed control strategy is illustrated via two examples from the path planning and tracking problems of mobile robots.
[1] 
Z. Zuo, C. Liu, Q.L. Han, and J. Song, “Unmanned aerial vehicles: Control methods and future challenges,” IEEE/CAA J. Autom. Sinica, vol. 9, pp. 601–614, 2022.

[2] 
X. W. Guo, M. C. Zhou, A. Abusorrah, F. Alsokhiry, and K. Sedraoui, “Disassembly sequence planning: A survey,” IEEE/CAA J. Autom. Sinica, vol. 8, no. 7, pp. 1308–1324, 2020.

[3] 
C. Baier and J.P. Katoen, Principles of Model Checking. Cambridge, USA: MIT Press, 2008.

[4] 
E. M. Wolff, U. Topcu, and R. M. Murray, “Optimizationbased trajectory generation with linear temporal logic specifications,” in Proc. Int. Conf. Robotics and Automation, 2014, pp. 5319–5325.

[5] 
R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa’ar, “Synthesis of reactive (1) designs,” J. Computer and Syst. Sciences, vol. 78, no. 3, pp. 911–938, 2012. doi: 10.1016/j.jcss.2011.08.007

[6] 
T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R. M. Murray, “TuLiP: A software toolbox for receding horizon temporal logic planning,” in Proc. Int. Conf. Hybrid Syst.: Computation and Control, 2011, pp. 313–314.

[7] 
P. J. Antsaklis, M. Lemmon, and J. A. Stiver, “Hybrid system modeling and event identification,” the ISIS Group, the University of Notre Dame, South Bend, USA, Tech. Rep. ISIS93002, 1993, vol. 93, pp. 366–392.

[8] 
P. Tabuada, Verification and Control of Hybrid Systems: A Symbolic Approach. USA: Springer Science & Business Media, 2009.

[9] 
A. Girard, “Controller synthesis for safety and reachability via approximate bisimulation,” Automatica, vol. 48, no. 5, pp. 947–953, 2012. doi: 10.1016/j.automatica.2012.02.037

[10] 
P. Tabuada, “An approximate simulation approach to symbolic control,” IEEE Trans. Autom. Control, vol. 53, no. 6, pp. 1406–1418, 2008. doi: 10.1109/TAC.2008.925824

[11] 
G. Pola, A. Girard, and P. Tabuada, “Approximately bisimilar symbolic models for nonlinear control systems,” Automatica, vol. 44, no. 10, pp. 2508–2516, 2008. doi: 10.1016/j.automatica.2008.02.021

[12] 
M. Zamani, G. Pola, M. Mazo, and P. Tabuada, “Symbolic models for nonlinear control systems without stability assumptions,” IEEE Trans. Autom. Control, vol. 57, no. 7, pp. 1804–1809, 2012. doi: 10.1109/TAC.2011.2176409

[13] 
W. Ren and D. V. Dimarogonas, “Logarithmic quantization based symbolic abstractions for nonlinear control systems,” in Proc. European Control Conf., 2019, pp. 1312–1317.

[14] 
G. Pola, P. Pepe, M. D. Di Benedetto, and P. Tabuada, “Symbolic models for nonlinear timedelay systems using approximate bisimulations,” Syst. & Control Lett., vol. 59, no. 6, pp. 365–373, 2010.

[15] 
W. Ren and D. V. Dimarogonas, “Symbolic abstractions for nonlinear control systems via feedback refinement relation,” Automatica, vol. 114, p. 108828, 2020. doi: 10.1016/j.automatica.2020.108828

[16] 
A. Girard, G. Gössler, and S. Mouelhi, “Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models,” IEEE Trans. Autom. Control, vol. 61, no. 6, pp. 1537–1549, 2016. doi: 10.1109/TAC.2015.2478131

[17] 
M. Zamani, M. Mazo, M. Khaled, and A. Abate, “Symbolic abstractions of networked control systems,” IEEE Trans. Control of Network Systems, vol. 5, no. 4, pp. 1622–1634, 2017.

[18] 
M. Zamani, A. Abate, and A. Girard, “Symbolic models for stochastic switched systems: A discretization and a discretizationfree approach,” Automatica, vol. 55, pp. 183–196, 2015. doi: 10.1016/j.automatica.2015.03.004

[19] 
G. Reissig, A. Weber, and M. Rungger, “Feedback refinement relations for the synthesis of symbolic controllers,” IEEE Trans. Autom. Control, vol. 62, no. 4, pp. 1781–1796, 2017. doi: 10.1109/TAC.2016.2593947

[20] 
E. S. Kim, M. Arcak, and S. A. Seshia, “Symbolic control design for monotone systems with directed specifications,” Automatica, vol. 83, pp. 10–19, 2017. doi: 10.1016/j.automatica.2017.04.060

[21] 
M. Mazo, A. Davitian, and P. Tabuada, “PESSOA: A tool for embedded controller synthesis,” in Proc. Int. Conf. ComputerAided Verification, 2010, pp. 566–569.

[22] 
S. Mouelhi, A. Girard, and G. Gössler, “CoSyMA: A tool for controller synthesis using multiscale abstractions,” in Proc. Int. Conf. Hybrid Systems: Computation and Control, 2013, pp. 83–88.

[23] 
M. Rungger and M. Zamani, “SCOTS: A tool for the synthesis of symbolic controllers,” in Proc. Int. Conf. Hybrid Systems: Comput. and Control, 2016, pp. 99–104.

[24] 
J. Tůmová, B. Yordanov, C. Belta, I. Černá, and J. Barnat, “A symbolic approach to controlling piecewise affine systems,” in Proc. IEEE Conf. Decision and Control, 2010, pp. 4230–4235.

[25] 
P.J. Meyer and D. V. Dimarogonas, “Hierarchical decomposition of LTL synthesis problem for nonlinear control systems,” IEEE Trans. Autom. Control, vol. 64, no. 11, pp. 4676–4683, 2019. doi: 10.1109/TAC.2019.2902643

[26] 
D. F. Delchamps, “Stabilizing a linear system with quantized state feedback,” IEEE Trans. Autom. Control, vol. 35, no. 8, pp. 916–924, 1990. doi: 10.1109/9.58500

[27] 
W. Ren and J. Xiong, “Quantized feedback stabilization of nonlinear systems with external disturbance,” IEEE Trans. Autom. Control, vol. 63, no. 9, pp. 3167–3172, 2018. doi: 10.1109/TAC.2018.2791461

[28] 
C. Belta, A. Bicchi, M. Egerstedt, E. Frazzoli, E. Klavins, and G. J. Pappas, “Symbolic planning and control of robot motion,” IEEE Robotics & Automation Magazine, vol. 14, no. 1, pp. 61–70, 2007.

[29] 
H. KressGazit, G. E. Fainekos, and G. J. Pappas, “Temporallogicbased reactive mission and motion planning,” IEEE Trans. Robotics, vol. 25, no. 6, pp. 1370–1381, 2009. doi: 10.1109/TRO.2009.2030225

[30] 
G. E. Fainekos, A. Girard, H. KressGazit, and G. J. Pappas, “Temporal logic motion planning for dynamic robots,” Automatica, vol. 45, no. 2, pp. 343–352, 2009. doi: 10.1016/j.automatica.2008.08.008

[31] 
A. Girard and G. J. Pappas, “Approximation metrics for discrete and continuous systems,” IEEE Trans. Autom. Control, vol. 5, no. 52, pp. 782–798, 2007.

[32] 
A. Girard, G. Pola, and P. Tabuada, “Approximately bisimilar symbolic models for incrementally stable switched systems,” IEEE Trans. Autom. Control, vol. 55, no. 1, pp. 116–126, 2010. doi: 10.1109/TAC.2009.2034922

[33] 
M. Guo and D. V. Dimarogonas, “Multiagent plan reconfiguration under local LTL specifications,” Int. J. Robotics Research, vol. 34, no. 2, pp. 218–235, 2015. doi: 10.1177/0278364914546174

[34] 
K. Hsu, R. Majumdar, K. Mallik, and A.K. Schmuck, “Lazy abstractionbased control for safety specifications,” in Proc. IEEE Conf. Decision and Control, 2018, pp. 4902–4907.

[35] 
W. Ren and D. V. Dimarogonas, “Dynamic quantization based symbolic abstractions for nonlinear control systems,” in Proc. IEEE Conf. Decision and Control, 2019, pp. 4343–4348.

[36] 
D. Angeli, “A Lyapunov approach to incremental stability properties,” IEEE Trans. Autom. Control, vol. 47, no. 3, pp. 410–421, 2002. doi: 10.1109/9.989067

[37] 
L. Lindemann, J. Nowak, L. Schönbächler, M. Guo, J. Tumova, and D. V. Dimarogonas, “Coupled multirobot systems under linear temporal logic and signal temporal logic tasks,” IEEE Trans. Control Syst. Technology, vol. 29, no. 2, pp. 858–865, 2019.

[38] 
V. Raman and H. KressGazit, “Analyzing unsynthesizable specifications for highlevel robot behavior using LTLMoP,” in Proc. Int. Conf. ComputerAided Verification, 2011, pp. 663–668.

[39] 
Y. Zheng, A. Lai, X. Yu, and W. Lan, “Earlyawareness collision avoidance in optimal multiagent path planning with temporal logic specifications,” IEEE/CAA J. Autom. Sinica, vol. 10, no. 5, pp. 1346–1348, 2022.

[40] 
D. Liberzon, “Hybrid feedback stabilization of systems with quantized signals,” Automatica, vol. 39, no. 9, pp. 1543–1554, 2003. doi: 10.1016/S00051098(03)001511

[41] 
L. Zou, Z. Wang, J. Hu, and D. Zhou, “Moving horizon estimation with unknown inputs under dynamic quantization effects,” IEEE Trans. Autom. Control, vol. 65, no. 12, pp. 5368–5375, 2020. doi: 10.1109/TAC.2020.2968975

[42] 
Z. Zhao, Z. Wang, L. Zou, Y. Chen, and W. Sheng, “Zonotopic distributed fusion for nonlinear networked systems with bit rate constraint,” Information Fusion, vol. 90, pp. 174–184, 2023. doi: 10.1016/j.inffus.2022.09.014

[43] 
R. W. Brockett and D. Liberzon, “Quantized feedback stabilization of linear systems,” IEEE Trans. Autom. Control, vol. 45, no. 7, pp. 1279–1289, 2000. doi: 10.1109/9.867021

[44] 
J. Tůmová, L. I. R. Castro, S. Karaman, E. Frazzoli, and D. Rus, “Minimumviolation LTL planning with conflicting specifications,” in Proc. American Control Conf., 2013, pp. 200–205.

[45] 
L. Lindemann and D. V. Dimarogonas, “Funnel control for fully actuated systems under a fragment of signal temporal logic specifications,” Nonlinear Analysis: Hybrid Systems, vol. 39, p. 100973, 2021. doi: 10.1016/j.nahs.2020.100973

[46] 
A. Nikou and D. V. Dimarogonas, “Decentralized tubebased model predictive control of uncertain nonlinear multiagent systems,” Int. J. Robust Nonlinear Control, vol. 29, no. 10, pp. 2799–2818, 2019. doi: 10.1002/rnc.4522

[47] 
C. K. Verginis, C. P. Bechlioulis, D. V. Dimarogonas, and K. J. Kyriakopoulos, “Robust distributed control protocols for large vehicular platoons with prescribed transient and steadystate performance,” IEEE Trans. Control Syst. Technology, vol. 26, no. 1, pp. 299–304, 2017.

[48] 
S. Karaman and E. Frazzoli, “Samplingbased algorithms for optimal motion planning,” Int. J. Robotics Research, vol. 30, no. 7, pp. 846–894, 2011. doi: 10.1177/0278364911406761

[49] 
K. Hsu, R. Majumdar, K. Mallik, and A.K. Schmuck, “Lazy abstractionbased controller synthesis,” in Proc. Int. Symp. Automated Technology for Verification and Analysis, 2019, pp. 23–47.

[50] 
K. Garg and D. Panagou, “ControlLyapunov and controlbarrier functions based quadratic program for spatiotemporal specifications,” in Proc. IEEE Conf. Decision and Control, 2019, pp. 1422–1429.
