Abstract
The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (the control funnels), that models behaviors of systems as timed automata. The main advantage of this method is that it allows automated verification of formal specifications and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient constructions are possible in the case of linear dynamics. We demonstrate the potential of our approach with two examples.
This work has been partly supported by ERC Starting grant EQualIS (FP7-308087) and by European FET project Cassting (FP7-601148).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Computer Science 126(2), 183–235 (1994)
Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. Theor. Computer Science 138(1), 35–65 (1995)
Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: SSSC 1998, pp. 469–474. Elsevier (1998)
Aubin, J.P.: Viability tubes. In: Byrnes, C.I., Kurzhanski, A.B. (eds.) Modelling and Adaptive Control. LNCIS, vol. 105, pp. 27–47. Springer, Heidelberg (1988)
Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007)
Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST 2006, pp. 125–126. IEEE, September 2006
Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Computer Science 321(2–3), 291–345 (2004)
David, A., Grunnet, J.D., Jessen, J.J., Larsen, K.G., Rasmussen, J.I.: Application of model-checking technology to controller synthesis. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 336–351. Springer, Heidelberg (2011)
DeCastro, J., Kress-Gazit, H.: Synthesis of nonlinear continuous controllers for verifiably-correct high-level, reactive behaviors. IJRR 34(3), 378–394 (2014)
Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: EMSOFT 2013, pp. 1–10. IEEE, September 2013
Frazzoli, E., Dahleh, M.A., Feron, E.: Maneuver-based motion planning for nonlinear systems with symmetries. IEEE Trans. Robotics 21(6), 1077–1091 (2005)
Fu, J., Topcu, U.: Computational methods for stochastic control with metric interval temporal logic specifications. Tech. Rep. 1503.07193, ArXiv, Mar 2015
Julius, A.A., Pappas, G.J.: Trajectory based verification using local finite-time invariance. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 223–236. Springer, Heidelberg (2009)
Koiran, P., Cosnard, M., Garzon, M.: Computability with low-dimensional dynamical systems. Theor. Computer Science 132(1), 113–128 (1994)
Le Ny, J., Pappas, G.J.: Sequential composition of robust controller specifications. In: ICRA 2012, pp. 5190–5195. IEEE, May 2012
Liu, J., Prabhakar, P.: Switching control of dynamical systems from metric temporal logic specifications. In: ICRA 2014, pp. 5333–5338. IEEE, May 2014
Majumdar, A., Ahmadi, A.A., Tedrake, R.: Control design along trajectories with sums of squares programming. In: ICRA 2013, pp. 4054–4061. IEEE, May 2013
Majumdar, A., Tedrake, R.: Robust online motion planning with regions of finite time invariance. In: WAFR 2012. STAR, vol. 86, pp. 543–558. Springer, Heidelberg (2013)
Maler, O., Batt, G.: Approximating continuous systems by timed automata. In: Fisher, J. (ed.) FMSB 2008. LNCS (LNBI), vol. 5054, pp. 77–89. Springer, Heidelberg (2008)
Maler, O., Manna, Z., Pnueli, A.: From timed to hybrid systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) Real-Time: Theory in Practice. LNCS, vol. 600, pp. 447–484. Springer, Heidelberg (1992)
Mason, M.T.: The mechanics of manipulation. In: ICRA 1985, vol. 2, pp. 544–548. IEEE , March 1985
Quottrup, M.M., Bak, T., Zamanabadi, R.I.: Multi-robot planning : a timed automata approach. In: ICRA 2004, vol. 5, pp. 4417–4422. IEEE, April 2004
Sloth, C., Wisniewski, R.: Timed game abstraction of control systems. Tech. Rep. 1012.5113, ArXiv, December 2010
Sloth, C., Wisniewski, R.: Complete abstractions of dynamical systems by timed automata. Nonlinear Analysis: Hybrid Systems 7(1), 80–100 (2013)
Sontag, E.D.: Mathematical control theory: deterministic finite dimensional systems. Springer (1998)
Tedrake, R., Manchester, I.R., Tobenkin, M., Roberts, J.W.: LQR-trees: Feedback motion planning via sums-of-squares verification. IJRR 29(8), 1038–1052 (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bouyer, P., Markey, N., Perrin, N., Schlehuber-Caissier, P. (2015). Timed-Automata Abstraction of Switched Dynamical Systems Using Control Funnels. In: Sankaranarayanan, S., Vicario, E. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2015. Lecture Notes in Computer Science(), vol 9268. Springer, Cham. https://doi.org/10.1007/978-3-319-22975-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-22975-1_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22974-4
Online ISBN: 978-3-319-22975-1
eBook Packages: Computer ScienceComputer Science (R0)