{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T02:54:04Z","timestamp":1760151244388,"version":"build-2065373602"},"reference-count":59,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2022,3,8]],"date-time":"2022-03-08T00:00:00Z","timestamp":1646697600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithms"],"abstract":"<jats:p>In this paper, we show that a basic fixed point method used to enclose the greatest fixed point in a Kleene algebra will allow us to compute inner and outer approximations of invariant-based sets for continuous-time nonlinear dynamical systems. Our contribution is to provide the definitions and theorems that will allow us to make the link between the theory of invariant sets and the Kleene algebra. This link has never be done before and will allow us to compute rigorously sets that can be defined as a combination of positive invariant sets. Some illustrating examples show the nice properties of the approach.<\/jats:p>","DOI":"10.3390\/a15030090","type":"journal-article","created":{"date-parts":[[2022,3,8]],"date-time":"2022-03-08T12:35:37Z","timestamp":1646742937000},"page":"90","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Kleene Algebra to Compute Invariant Sets of Dynamical Systems"],"prefix":"10.3390","volume":"15","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7165-4499","authenticated-orcid":false,"given":"Thomas","family":"Le M\u00e9zo","sequence":"first","affiliation":[{"name":"ENSTA Bretagne, Robex, LabSTICC, 2 Rue Fran\u00e7ois Verny, 29806 Brest, France"}]},{"given":"Luc","family":"Jaulin","sequence":"additional","affiliation":[{"name":"ENSTA Bretagne, Robex, LabSTICC, 2 Rue Fran\u00e7ois Verny, 29806 Brest, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4485-8936","authenticated-orcid":false,"given":"Damien","family":"Mass\u00e9","sequence":"additional","affiliation":[{"name":"Lab-STICC, UMR 6285, University of Brest, 29238 Brest, France"}]},{"given":"Benoit","family":"Zerr","sequence":"additional","affiliation":[{"name":"ENSTA Bretagne, Robex, LabSTICC, 2 Rue Fran\u00e7ois Verny, 29806 Brest, France"}]}],"member":"1968","published-online":{"date-parts":[[2022,3,8]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Jaulin, L. (2015). Automation for Robotics, ISTE.","DOI":"10.1002\/9781119081326"},{"key":"ref_2","unstructured":"Jaulin, L. (2015). Mobile Robotics, ISTE."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Blanchini, F., and Miani, S. (2007). Set-Theoretic Methods in Control, Springer Science & Business Media.","DOI":"10.1007\/978-0-8176-4606-6"},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"229","DOI":"10.14232\/actacyb.23.1.2017.14","article-title":"An Algebraic Approach to Energy Problems II, The Algebra of Energy Functions","volume":"23","author":"Esik","year":"2017","journal-title":"Acta Cybern."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/s10898-008-9334-6","article-title":"A numerical approach to design control invariant sets for constrained nonlinear discrete-time systems with guaranteed optimality","volume":"44","author":"Wan","year":"2009","journal-title":"J. Glob. Optim."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"2622","DOI":"10.1080\/00207179.2010.535215","article-title":"Positive invariant sets for fault tolerant multisensor control schemes","volume":"83","author":"Olaru","year":"2010","journal-title":"Int. J. Control"},{"key":"ref_7","unstructured":"Althoff, D., Althoff, M., and Scherer, S. (October, January 28). Online Safety Verification of Trajectories for Unmanned Flight with Offline Computed Robust Invariant Sets. Proceedings of the IEEE\/RSJ International Conference on Intelligent Robots and Systems, Hamburg, Germany."},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Asarin, E., Dang, T., and Maler, O. (2002, January 21\u201324). The d\/dt tool for verification of hybrid systems. Proceedings of the International Conference on Computer Aided Verification, Los Angeles, CA, USA.","DOI":"10.1007\/3-540-45657-0_30"},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Tabuada, P. (2009). Verification and Control of Hybrid Systems: A Symbolic Approach, Springer.","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"ref_10","unstructured":"Bemporad, A., Bicchi, A., and Buttazzo, G. (2007). Comparing forward and backward reachability as tools for safety analysis. Hybrid Systems: Computation and Control, Springer."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"1416","DOI":"10.1109\/TAC.2014.2352692","article-title":"Low-Complexity Polytopic Invariant Sets for Linear Systems Subject to Norm-Bounded Uncertainty","volume":"60","author":"Tahir","year":"2015","journal-title":"IEEE Trans. Autom. Control"},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Roux, P., Jobredeaux, R., Garoche, P., and Feron, E. (2012, January 17\u201319). A generic ellipsoid abstract domain for linear time invariant systems. Proceedings of the Hybrid Systems: Computation and Control, HSCC\u201912, Beijing, China.","DOI":"10.1145\/2185632.2185651"},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"604","DOI":"10.1109\/TAC.1972.1100085","article-title":"Infinite-time reachability of state-space regions by using feedback Control","volume":"17","author":"Bertsekas","year":"1972","journal-title":"IEEE Trans. Autom. Control"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1109\/LCSYS.2017.2714840","article-title":"Invariant Sets Analysis for Constrained Switching Systems","volume":"1","author":"Athanasopoulos","year":"2017","journal-title":"IEEE Control Syst. Lett."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3126502","article-title":"A fast method to compute disjunctive quadratic invariants of numerical programs","volume":"6","author":"Allamigeon","year":"2017","journal-title":"Acm Trans. Embed. Comput. Syst."},{"key":"ref_16","first-page":"250","article-title":"Reachability analysis of linear systems using support functions","volume":"4","author":"Guernic","year":"2009","journal-title":"Nonlinear Anal."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Touili, T., Cook, B., and Jackson, P. (2010). A logical product approach to zonotope intersection. Computer Aided Verification, CAV 2010, Springer.","DOI":"10.1007\/978-3-642-14295-6"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s00236-006-0035-7","article-title":"Hybridization methods for the analysis of non-linear systems","volume":"7","author":"Asarin","year":"2007","journal-title":"Acta Inform."},{"key":"ref_19","unstructured":"Girard, A. (2003, January 16\u201318). Computation and stability analysis of limit cycles in piecewise linear hybrid systems. Proceedings of the 1st IFAC Conference on Analysis and Design of Hybrid Systems, St Malo, France."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-540-78800-3_14","article-title":"Symbolic model checking of hybrid systems using template polyhedra","volume":"4963","author":"Sankaranarayanan","year":"2008","journal-title":"Tacas Lect. Notes Comput. Sci."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/BF01204182","article-title":"Approximation of the viability kernel","volume":"29","year":"1994","journal-title":"Appl. Math. Optim."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"3659","DOI":"10.1109\/TAC.2018.2797196","article-title":"Automated-Sampling-Based Stability Verification and DOA Estimation for Nonlinear Systems","volume":"63","author":"Bobiti","year":"2018","journal-title":"IEEE Trans. Autom. Control"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Goubault, E., Mullier, O., Putot, S., and Kieffer, M. (2014, January 15\u201317). Inner approximated reachability analysis. Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC\u201914, Berlin, Germany.","DOI":"10.1145\/2562059.2562113"},{"key":"ref_24","first-page":"9","article-title":"Cr-Lohner algorithm","volume":"20","author":"Wilczak","year":"2011","journal-title":"Schedae Inform."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Goubault, E., and Putot, S. (2017, January 18\u201320). Forward Inner-Approximated Reachability of Non-Linear Continuous Systems. Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, Pittsburgh, PA, USA.","DOI":"10.1145\/3049797.3049811"},{"key":"ref_26","first-page":"2291","article-title":"Review on computational methods for Lyapunov functions","volume":"8","author":"Giesl","year":"2015","journal-title":"Discret. Contin. Dyn. Syst."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1109\/TAC.2013.2283095","article-title":"Convex computation of the region of attraction of polynomial control systems","volume":"59","author":"Henrion","year":"2013","journal-title":"IEEE Trans. Autom. Control"},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"4377","DOI":"10.1137\/090749955","article-title":"Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-like Functions","volume":"48","author":"Ratschan","year":"2010","journal-title":"SIAM J. Control Optim."},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1109\/LCSYS.2019.2916256","article-title":"Inner approximations of the maximal positively invariant set for polynomial dynamical systems","volume":"3","author":"Oustry","year":"2019","journal-title":"IEEE Control Syst. Lett."},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"2501","DOI":"10.1016\/j.topol.2006.04.033","article-title":"Polygonal approximation of flows","volume":"154","author":"Boczko","year":"2007","journal-title":"Topol. Its Appl."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"4236","DOI":"10.1109\/TAC.2017.2685241","article-title":"An interval approach to compute invariant sets","volume":"62","author":"Jaulin","year":"2017","journal-title":"IEEE Trans. Autom. Control"},{"key":"ref_32","unstructured":"Conley, C. (1991). Isolated Invariant Sets and the Morse Index, American Mathematical Society."},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/s10009-007-0062-x","article-title":"PHAVer: Algorithmic Verification of Hybrid Systems","volume":"10","author":"Frehse","year":"2008","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., and Maler, O. (2011, January 14\u201320). SpaceEx: Scalable Verification of Hybrid Systems. Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), Snowbird, UT, USA.","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"LaValle, S. (2006). Planning Algorithm, Cambridge University Press.","DOI":"10.1017\/CBO9780511546877"},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"1151","DOI":"10.1007\/s10208-015-9272-x","article-title":"Lattice Structures for Attractors","volume":"16","author":"Kalies","year":"2016","journal-title":"Found. Comput. Math."},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Davey, B.A., and Priestley, H.A. (2002). Introduction to Lattices and Order, Cambridge University Press.","DOI":"10.1017\/CBO9780511809088"},{"key":"ref_38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1353445.1353446","article-title":"The pitfalls of verifying floating-point computations","volume":"30","author":"Monniaux","year":"2008","journal-title":"Acm Trans. Program. Lang. Syst."},{"key":"ref_39","first-page":"70","article-title":"Bracketing the solutions of an ordinary differential equation with uncertain initial conditions","volume":"318","author":"Jaulin","year":"2018","journal-title":"Appl. Math. Comput."},{"key":"ref_40","first-page":"2528","article-title":"Bracketing backward reach sets of a dynamical system","volume":"93","author":"Jaulin","year":"2019","journal-title":"Int. J. Control"},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Kozen, D. (1990). On Kleene algebras and closed semirings. International Symposium on Mathematical Foundations of Computer Science, Springer.","DOI":"10.1007\/BFb0029594"},{"key":"ref_42","unstructured":"Kozen, D. (1991, January 15\u201318). A completeness theorem for Kleene algebras and the algebra of regular events. Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, LICS, Amsterdam, The Netherlands."},{"key":"ref_43","unstructured":"Moore, R.E. (1966). Interval Analysis, Prentice-Hall."},{"key":"ref_44","doi-asserted-by":"crossref","first-page":"1923","DOI":"10.1016\/j.automatica.2004.05.013","article-title":"Interval Analysis and Dioid: Application to Robust Controller Design for Timed Event Graphs","volume":"40","author":"Lhommeau","year":"2004","journal-title":"Automatica"},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1016\/j.robot.2017.03.020","article-title":"Guaranteed Computation of Robots Trajectories","volume":"93","author":"Rohou","year":"2017","journal-title":"Robot. Auton. Syst."},{"key":"ref_46","first-page":"138","article-title":"Computing an inner and an outer approximation of the viability kernel","volume":"22","author":"Monnet","year":"2016","journal-title":"Reliab. Comput."},{"key":"ref_47","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1002\/acs.1195","article-title":"Capture Basin Approximation using Interval Analysis","volume":"25","author":"Lhommeau","year":"2011","journal-title":"Int. J. Adapt. Control Signal Process."},{"key":"ref_48","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-642-03845-7_9","article-title":"Computing reachable states for nonlinear biological models","volume":"5688","author":"Dang","year":"2009","journal-title":"Comput. Methods Syst. Biol."},{"key":"ref_49","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.nahs.2010.05.010","article-title":"Computing Reachable Sets for Uncertain Nonlinear Hybrid Systems using Interval Constraint Propagation Techniques","volume":"5","author":"Ramdani","year":"2011","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"ref_50","unstructured":"Chen, X. (2015). Reachability Analysis of Non-LinearHybrid Systems Using Taylor Models. [Ph.D. Thesis, University of Aachen]."},{"key":"ref_51","first-page":"257","article-title":"Efficient computation of reachable sets of linear time-invariant systems with inputs","volume":"3927","author":"Girard","year":"2006","journal-title":"Hybrid Syst. Comput. Control"},{"key":"ref_52","doi-asserted-by":"crossref","first-page":"3623","DOI":"10.1002\/rnc.4103","article-title":"Using set invariance to design robust interval observers for discrete time linear systems","volume":"28","author":"Meslem","year":"2018","journal-title":"Int. J. Robust Nonlinear Control"},{"key":"ref_53","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1109\/TAC.2005.843854","article-title":"Invariant approximations of the minimal robust positively invariant set","volume":"50","author":"Rakovic","year":"2005","journal-title":"IEEE Trans. Autom. Control"},{"key":"ref_54","first-page":"108","article-title":"Spatial Planning: A Configuration Space Approach","volume":"32","year":"1983","journal-title":"IEEE Trans. Comput."},{"key":"ref_55","doi-asserted-by":"crossref","unstructured":"Rungger, M., and Zamani, M. (2016, January 12\u201314). SCOTS: A Tool for the Synthesis of Symbolic Controllers. Proceedings of the HSCC 2016, Vienna, Austria.","DOI":"10.1145\/2883817.2883834"},{"key":"ref_56","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1011400431065","article-title":"Path Planning Using Intervals and Graphs","volume":"7","author":"Jaulin","year":"2001","journal-title":"Reliab. Comput."},{"key":"ref_57","doi-asserted-by":"crossref","first-page":"413","DOI":"10.2478\/v10006-009-0034-2","article-title":"Reliable Robust Path Planning with Application to Mobile Robots","volume":"19","author":"Pepy","year":"2009","journal-title":"Int. J. Appl. Math. Comput. Sci."},{"key":"ref_58","unstructured":"Cr\u00e9pon, P., Panchea, A., and Chapoutot, A. (February, January 31). Reliable Motion Plannning for a Mobile Robot. Proceedings of the IEEE International Conference on Robotic Computing, Laguna Hills, CA, USA."},{"key":"ref_59","doi-asserted-by":"crossref","unstructured":"Belta, C., Yordanov, B., and Gol, E. (2017). Formal Methods for Discrete-Time Dynamical Systems, Springer International Publishing. Studies in Systems, Decision and Control.","DOI":"10.1007\/978-3-319-50763-7"}],"container-title":["Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-4893\/15\/3\/90\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T22:34:14Z","timestamp":1760135654000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-4893\/15\/3\/90"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,8]]},"references-count":59,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2022,3]]}},"alternative-id":["a15030090"],"URL":"https:\/\/doi.org\/10.3390\/a15030090","relation":{},"ISSN":["1999-4893"],"issn-type":[{"type":"electronic","value":"1999-4893"}],"subject":[],"published":{"date-parts":[[2022,3,8]]}}}