“Abstraction of Dynamical Systems by Timed Automata”
Authors: Rafael Wisniewski and Christoffer Sloth,Affiliation: Aalborg University
Reference: 2011, Vol 32, No 2, pp. 79-90.
Keywords: verification, stability, abstraction, timed automata
Abstract: To enable formal verification of a dynamical system, given by a set of differential equations, it is abstracted by a finite state model. This allows for application of methods for model checking. Consequently, it opens the possibility of carrying out the verification of reachability and timing requirements, which by classical control methods is impossible. We put forward a method for abstracting dynamical systems, where level sets of Lyapunov functions are used to generate the partitioning of the state space. We propose to partition the state space using an entire family of functions. The properties of these functions ensure that the discrete model captures the behaviors of a dynamical system by generating appropriate equivalence classes of the states. These equivalence classes make up the partition of the state space.
PDF (483 Kb)
DOI: 10.4173/mic.2011.2.3DOI forward links to this article:
| [1] Christoffer Sloth and Rafael Wisniewski (2013), doi:10.1016/j.nahs.2012.05.003 |
| [2] Christoffer Sloth and Rafael Wisniewski (2012), doi:10.3182/20120829-3-IT-4022.00049 |
| [3] Stefano Schivo and Rom Langerak (2017), doi:10.1007/978-3-319-68270-9_15 |
| [4] Nikola Bene , Lubo Brim, Jana Dra anová, Samuel Pastva and David afránek (2019), doi:10.1145/3302504.3311793 |
[1] Alur, R. (1999). Timed automata, In Computer aided verification.Trento, volume 1633 of Lecture Notes in Computer Science, pages 8--22. Springer, Berlin doi:10.1007/3-540-48683-63
[2] Alur, R., Courcoubetis, C., Dill, D. (1990). Model-checking for real-time systems, In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science. pp. 414--425 doi:10.1109/LICS.1990.113766
[3] Alur, R. Dill, D.L. (1994). A theory of timed automata, Theoretical Computer Science, 126(2):183--235 doi:10.1016/0304-3975(94)90010-8
[4] Asarin, E., Dang, T., Frehse, G., Girard, A., Guernic, C.L., Maler, O. (2006). Recent progress in continuous and hybrid reachability analysis, In Proceedings of the 2006 IEEE Conference on Computer Aided Control Systems Design. Munich, Germany, pp. 1582--1587 doi:10.1109/CACSD-CCA-ISIC.2006.4776877
[5] Behrmann, G., David, A., Larsen, K. (2004). A tutorial on Uppaal, In Formal Methods for the Design of Real-Time Systems, volume 3185 of Lecture Notes in Computer Science, pp. 200--236. Springer Berlin / Heidelberg doi:10.1007/978-3-540-30080-9_7
[6] Fahrenberg, U., Larsen, K., Thrane, C. (2010). Verification, performance analysis and controller synthesis for real-time systems, In Fundamentals of Software Engineering, volume 5961 of Lecture Notes in Computer Science, pp. 34--61. Springer Berlin / Heidelberg doi:10.1007/978-3-642-11623-0_2
[7] Frehse, G. (2005). Phaver: Algorithmic verification of hybrid systems past HyTech, In Hybrid Systems: Computation and Control, volume 3414 of Lecture Notes in Computer Science, pages 258--273. Springer Berlin / Heidelberg doi:10.1007/978-3-540-31954-2_17
[8] Girard, A. (2005). Reachability of uncertain linear systems using zonotopes, In Hybrid Systems: Computation and Control, volume 3414 of Lecture Notes in Computer Science, pages 291--305. Springer Berlin / Heidelberg doi:10.1007/978-3-540-31954-2_19
[9] Gueguen, H., Lefebvre, M.-A., Zaytoon, J., Nasri, O. (2009). Safety verification and reachability analysis for hybrid systems, Annual Reviews in Control, 3.1:1367--5788 doi:10.1016/j.arcontrol.2009.03.002
[10] Hirsch, M.W. (1976). Differential Topology, Springer, Heidelberg.
[11] Kurzhanski, A.B. Valyi, I. (1997). Ellipsoidal Calculus for Estimation and Control, Birkhäuser Boston.
[12] Maler, O. Batt, G. (2008). Approximating continuous systems by timed automata, In Formal Methods in Systems Biology, volume 5054 of Lecture Notes in Computer Science, pages 77--89. Springer Berlin / Heidelberg doi:10.1007/978-3-540-68413-8_6
[13] Matsumoto, Y. (2002). An Introduction to Morse Theory, American Mathematical Society.
[14] Meyer, K.R. (1968). Energy functions for Morse Smale systems, American Journal of Mathematics, 9.4:1031--1040 doi:10.2307/2373287
[15] Mitchell, I., Bayen, A., Tomlin, C. (2005). A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games, IEEE Transactions on Automatic Control, 5.7:947--957 doi:10.1109/TAC.2005.851439
[16] Prajna, S. (2006). Barrier certificates for nonlinear model validation, Automatica, 4.1:117 -- 126 doi:10.1016/j.automatica.2005.08.007
[17] Sloth, C. Wisniewski, R. (2011). Verification of continuous dynamical systems by timed automata, Formal Methods in System Design, s3.1:47--82 doi:10.1007/s10703-011-0118-0
[18] Tiwari, A. (2008). Abstractions for hybrid systems, Formal Methods in System Design, 3.1:57--83 doi:10.1007/s10703-007-0044-3
[19] Tu, L.W. (2008). An Introduction to Manifolds, Springer doi:10.1007/978-1-4419-7400-6
BibTeX:
@article{MIC-2011-2-3,
title={{Abstraction of Dynamical Systems by Timed Automata}},
author={Wisniewski, Rafael and Sloth, Christoffer},
journal={Modeling, Identification and Control},
volume={32},
number={2},
pages={79--90},
year={2011},
doi={10.4173/mic.2011.2.3},
publisher={Norwegian Society of Automatic Control}
};