Hierarchical Controller Synthesis Under Linear Temporal Logic Specifications Using Dynamic Quantization

Wei Ren; Zhuo-Rui Pan; Weiguo Xia; Xi-Ming Sun

doi:10.1109/JAS.2024.124473

Volume 11 Issue 10

Oct. 2024

IEEE/CAA Journal of Automatica Sinica

JCR Impact Factor: 15.3, Top 1 (SCI Q1)

CiteScore: 23.5, Top 2% (Q1)
Google Scholar h5-index: 77， TOP 5

Turn off MathJax

Article Contents

Article Navigation > IEEE/CAA Journal of Automatica Sinica > 2024 > 11(10): 2082-2098

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

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

Citation:

PDF( 2465 KB)

Hierarchical Controller Synthesis Under Linear Temporal Logic Specifications Using Dynamic Quantization

doi: 10.1109/JAS.2024.124473

Funds: This work was supported by the Fundamental Research Funds for the Central Universities (DUT22RT(3)090), the National Natural Science Foundation of China (61890920, 61890921, 62122016, 08120003), and Liaoning Science and Technology Program (2023JH2/101700361)

More Information

Author Bio:
Wei Ren received the B.Sci. degree in information and computer science from Hubei University in 2011, and the Ph.D. degree in control science and engineering from the University of Science and Technology of China in 2018. From 2017 to 2018, he was a visiting student at the University of Melbourne, Australia. From 2018 to 2022, he was a Postdoctoral Researcher at the KTH Royal Institute of Technology, Sweden, and at Université Catholique de Louvain, Belgium. He is currently a Professor at Dalian University of Technology. His research interests include multi-agent systems, networked control systems, formal methods and hybrid systems

Zhuo-Rui Pan received the B.E. and M.E. degrees in automation from Dalian University of Technology, in 2019 and 2022, respectively. He is currently a Ph.D. candidate in navigation guidance and control at the School of Control Science and Engineering, Dalian University of Technology. His current research interests include electronic controller design and aeroengine control

Weiguo Xia received the B.Sc. and M.Sc. degrees in applied mathematics from Southeast University in 2006 and 2009, respectively, and the Ph.D. degree in systems and control from the Faculty of Science and Engineering, ENTEG, University of Groningen, the Netherland in 2013. He is currently a Professor with the School of Control Science and Engineering, Dalian University of Technology China. From 2013 to 2015, he was a Postdoctoral Researcher with the ACCESS Linnaeus Centre, KTH Royal Institute of Technology, Sweden. His current research interests include complex networks, social networks, and multiagent systems. He is an Associate Editor for Systems & Control Letters and IEEE Transactions on Cybernetics

Xi-Ming Sun received the M.S. degree in applied mathematics from Bohai University in 2003 and the Ph.D. degree in control theory and control engineering from Northeastern University in 2006. From 2006 to 2008, he was a Research Fellow with the Faculty of Advanced Technology, The University of South Wales, UK. He then visited the School of Electrical and Electronic Engineering, Melbourne University, Australia in 2009, and the Polytechnic Institute of New York University, USA in 2011. He is currently a Professor with the School of Control Science and Engineering, Dalian University of Technology. His current research interests include hybrid systems, networked control systems and control of aircraft engines. Prof. Sun was a recipient of the Most Cited Article (2006−2010) from the Journal Automatica in 2011. He is an Associate Editor of IEEE Transactions on Cybernetics and a Member of the Editorial Board of Scientia Sinica Informationis
Corresponding author: Wei Ren, e-mail: wei.ren@dlut.edu.cn
Received Date: 2024-01-29
Revised Date: 2024-03-26
Accepted Date: 2024-04-07

Available Online: 2024-08-13

Abstract

Abstract

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 high-level 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 abstraction-based control are combined together to establish the local-to-global 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.
- Abstraction-based control design,
- dynamic quantization,
- formal methods,
- linear temporal logic (LTL)

FullText(HTML)

References(50)

References

[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, “Optimization-based 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. ISIS-93-002, 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 time-delay 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 discretization-free 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. Computer-Aided Verification, 2010, pp. 566–569.
[22]	S. Mouelhi, A. Girard, and G. Gössler, “CoSyMA: A tool for controller synthesis using multi-scale 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. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Temporal-logic-based 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. Kress-Gazit, 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, “Multi-agent 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 abstraction-based 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 multi-robot 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. Kress-Gazit, “Analyzing unsynthesizable specifications for high-level robot behavior using LTLMoP,” in Proc. Int. Conf. Computer-Aided Verification, 2011, pp. 663–668.
[39]	Y. Zheng, A. Lai, X. Yu, and W. Lan, “Early-awareness collision avoidance in optimal multi-agent 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/S0005-1098(03)00151-1
[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, “Minimum-violation 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 tube-based 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 steady-state performance,” IEEE Trans. Control Syst. Technology, vol. 26, no. 1, pp. 299–304, 2017.
[48]	S. Karaman and E. Frazzoli, “Sampling-based 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 abstraction-based controller synthesis,” in Proc. Int. Symp. Automated Technology for Verification and Analysis, 2019, pp. 23–47.
[50]	K. Garg and D. Panagou, “Control-Lyapunov and control-barrier functions based quadratic program for spatio-temporal specifications,” in Proc. IEEE Conf. Decision and Control, 2019, pp. 1422–1429.

Supplements(0)

Cited By

Proportional views

Proportional views

通讯作者: 陈斌, bchen63@163.com

1.
沈阳化工大学材料科学与工程学院沈阳 110142

Figures(9) / Tables(1)

Get Citation

PDF

XML

Article Metrics

Article views (42) PDF downloads(11)

Highlights

Hierarchical control structure to connect high-level plan with local-level control
Dynamic quantization based realization verification for LTL specifications
A novel local-to-global control strategy to reduce computational complexity greatly

Hierarchical Controller Synthesis Under Linear Temporal Logic Specifications Using Dynamic Quantization

doi: 10.1109/JAS.2024.124473

Abstract

References

Proportional views

Catalog

通讯作者: 陈斌, bchen63@163.com

Article Metrics

Highlights

Export File

Citation

Format

Content