**Page description appears here**

“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.

     Valid XHTML 1.0 Strict

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 PDF (483 Kb)        DOI: 10.4173/mic.2011.2.3

DOI 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

[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

  title={{Abstraction of Dynamical Systems by Timed Automata}},
  author={Wisniewski, Rafael and Sloth, Christoffer},
  journal={Modeling, Identification and Control},
  publisher={Norwegian Society of Automatic Control}


May 2016: MIC reaches 2000 DOI Forward Links. The first 1000 took 34 years, the next 1000 took 2.5 years.

July 2015: MIC's new impact factor is now 0.778. The number of papers published in 2014 was 21 compared to 15 in 2013, which partially explains the small decrease in impact factor.

Aug 2014: For the 3rd year in a row MIC's impact factor increases. It is now 0.826.

Dec 2013: New database-driven web-design enabling extended statistics. Article number 500 is published and MIC reaches 1000 DOI Forward Links.

Jan 2012: Follow MIC on your smartphone by using the RSS feed.


July 2011: MIC passes 1000 ISI Web of Science citations.

Mar 2010: MIC is now indexed by DOAJ and has received the Sparc Seal seal for open access journals.

Dec 2009: A MIC group is created at LinkedIn and Twitter.

Oct 2009: MIC is now fully updated in ISI Web of Knowledge.