Application of Model-Checking Technology to Controller Synthesis

  • Alexandre David
  • Jacob Deleuran Grunnet
  • Jan Jakob Jessen
  • Kim Guldstrand Larsen
  • Jacob Illum Rasmussen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6957)


In this paper we present two frameworks that have been implemented to link traditional model-checking techniques to the domain of control. The techniques are based on solving a timed game and using the resulting solution (a strategy) as a controller. The obtained discrete controller must fit within its continuous environment, which is modelled and taken care of in our frameworks. Our first technique does it by using Matlab to discretise the problem and then Uppaal-tiga to solve the obtained timed game. This is implemented as a toolbox. The second technique relies on the user defining a timed game model in Uppaal-tiga. Then the strategy is automatically imported in Simulink as an S-function for simulation and validation purposes. We demonstrate the effectiveness of these frameworks in different case-studies.


Hybrid System Linear Matrix Inequality Control Objective Winning Strategy Controller Synthesis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 192–206. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
    Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic synthesis of robust and optimal controllers – an industrial case study. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 90–104. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  5. 5.
    Chatain, T., David, A., Larsen, K.G.: Playing games with timed games. In: Giua, A., Mahulea, C., Silva, M., Zaytoon, J. (eds.) Preprints of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems, pp. 238–243 (2009)Google Scholar
  6. 6.
    Grunnet, J.D., Bak, T., Bendtsen, J.D., Ankersen, F.: PAHSCTRL - a control synthesis toolbox for piecewise-affine hybrid systems. In: Proceedings of the 2009 European Control Conference. IEEE, Los Alamitos (2009)Google Scholar
  7. 7.
    Grunnet, J.D., Bak, T., Bendtsen, J.D., Larsen, J.A.: Discrete game abstraction for fault tolerant control synthesis. In: Proceedings of IEEE CACSD 2008 (2008)Google Scholar
  8. 8.
    Grunnet, J.D., Bendtsen, J.D., Bak, T.: Automated fault tolerant control synthesis based on discrete games. In: Proceedings of the 48th IEEE Conference on Decision and Control. IEEE, Los Alamitos (2009)Google Scholar
  9. 9.
    Habets, L., van Schuppen, J.H.: Control to facet problems for affine systems on simplices and polytopes - with applications to control of hybrid systems. In: Proc. 44th IEEE CDC (2005)Google Scholar
  10. 10.
    Habets, L.C.G.J.M., Collins, P.J., van Schuppen, J.H.: Reachability and control synthesis for piecewise-affine hybrid systems on simplices. IEEE Transactions on Automatic Control 51, 938–948 (2006)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Jessen, J.J., Rasmussen, J.I., Larsen, K.G., David, A.: Guided controller synthesis for climate controller using uppaal tiga. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 227–240. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  13. 13.
    Mathworks. Simulink (2010)Google Scholar
  14. 14.
    Tabuada, P., Pappas, G.J.: Linear time logic control of discrete-time linear systems. IEEE Transactions on Automatic Control 51, 1862–1877 (2006)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Alexandre David
    • 1
  • Jacob Deleuran Grunnet
    • 2
  • Jan Jakob Jessen
    • 1
  • Kim Guldstrand Larsen
    • 1
  • Jacob Illum Rasmussen
    • 3
  1. 1.Department of Computer ScienceAalborg UniversityDenmark
  2. 2.LAC EngineeringHinnerupDenmark
  3. 3.Sanddru R&DNørresundbyDenmark

Personalised recommendations