“Abstraction of Dynamical Systems by Timed Automata” Authors: Rafael Wisniewski and Christoffer Sloth Affiliation: Aalborg University, Denmark 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.3

DOI forward links to this article:
[1] Christoffer Sloth Rafael Wisniewski, (2013), doi:10.1016/j.nahs.2012.05.003



References:
[1] Alur, R. Timed automata. In Computer aided verification (Trento, 1999), volume 1633 of Lecture Notes in Computer Science, pages 8--22. Springer, Berlin, 1999. doi:10.1007/3-540-48683-63.
[2] Alur, R., Courcoubetis, C., and Dill, D. Model-checking for real-time systems. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science. pages 414--425, 1990. doi:10.1109/LICS.1990.113766.
[3] Alur, R. and Dill, D.L. A theory of timed automata. Theoretical Computer Science, 1994. 126(2):183--235. doi:10.1016/0304-3975(94)90010-8.
[4] Asarin, E., Dang, T., Frehse, G., Girard, A., Guernic, C.L., and Maler, O. Recent progress in continuous and hybrid reachability analysis. In Proceedings of the 2006 IEEE Conference on Computer Aided Control Systems Design. Munich, Germany, pages 1582--1587, 2006. doi:10.1109/CACSD-CCA-ISIC.2006.4776877.
[5] Behrmann, G., David, A., and Larsen, K. A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems, volume 3185 of Lecture Notes in Computer Science, pages 200--236. Springer Berlin / Heidelberg, 2004. doi:10.1007/978-3-540-30080-9_7.
[6] Fahrenberg, U., Larsen, K., and Thrane, C. Verification, performance analysis and controller synthesis for real-time systems. In Fundamentals of Software Engineering, volume 5961 of Lecture Notes in Computer Science, pages 34--61. Springer Berlin / Heidelberg, 2010. doi:10.1007/978-3-642-11623-0_2.
[7] Frehse, G. 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, 2005. doi:10.1007/978-3-540-31954-2_17.
[8] Girard, A. 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, 2005. doi:10.1007/978-3-540-31954-2_19.
[9] Gueguen, H., Lefebvre, M.-A., Zaytoon, J., and Nasri, O. Safety verification and reachability analysis for hybrid systems. Annual Reviews in Control, 2009. 33(1):1367--5788. doi:10.1016/j.arcontrol.2009.03.002.
[10] Hirsch, M.W. Differential Topology. Springer, Heidelberg, 1976.
[11] Kurzhanski, A.B. and Valyi, I. Ellipsoidal Calculus for Estimation and Control. Birkhäuser Boston, 1997.
[12] Maler, O. and Batt, G. 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, 2008. doi:10.1007/978-3-540-68413-8_6.
[13] Matsumoto, Y. An Introduction to Morse Theory. American Mathematical Society, 2002.
[14] Meyer, K.R. Energy functions for Morse Smale systems. American Journal of Mathematics, 1968. 90(4):1031--1040. doi:10.2307/2373287.
[15] Mitchell, I., Bayen, A., and Tomlin, C. A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Transactions on Automatic Control, 2005. 50(7):947--957. doi:10.1109/TAC.2005.851439.
[16] Prajna, S. Barrier certificates for nonlinear model validation. Automatica, 2006. 42(1):117 -- 126. doi:10.1016/j.automatica.2005.08.007.
[17] Sloth, C. and Wisniewski, R. Verification of continuous dynamical systems by timed automata. Formal Methods in System Design, 2011. 39(1):47--82. doi:10.1007/s10703-011-0118-0.
[18] Tiwari, A. Abstractions for hybrid systems. Formal Methods in System Design, 2008. 32(1):57--83. doi:10.1007/s10703-007-0044-3.
[19] Tu, L.W. An Introduction to Manifolds. Springer, 2008. doi:10.1007/978-1-4419-7400-6.


BibTeX:
@article{MIC-2011-2-3,
  title={{Abstraction of Dynamical Systems by Timed Automata}},
  author={Rafael Wisniewski and Christoffer Sloth},
  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}
};