Abstract
We present a methodology for the synthesis of controllers, which exploits (explicit) model checking techniques. That is, we can cope with the systematic exploration of a very large state space. This methodology can be applied to systems where other approaches fail. In particular, we can consider systems with an highly non-linear dynamics and lacking a uniform mathematical description (model). We can also consider situations where the required control action cannot be specified as a local action, and rather a kind of planning is required. Our methodology individuates first a raw optimal controller, then extends it to obtain a more robust one. A case study is presented which considers the well known truck-trailer obstacle avoidance parking problem, in a parking lot with obstacles on it. The complex non-linear dynamics of the truck-trailer system, within the presence of obstacles, makes the parking problem extremely hard. We show how, by our methodology, we can obtain optimal controllers with different degrees of robustness.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Kautz, H., Thomas, W., Vardi, M.Y.: 05241 executive summary – synthesis and planning. In Kautz, H., Thomas, W., Vardi, M.Y., eds.: Synthesis and Planning. Number 05241 in Dagstuhl Seminar Proceedings (2006)
Lygeros, J., Tomlin, C., Sastry, S.: Controllers for reachability specifications for hybrid systems Special Issue on Hybrid Systems, 35 (1999)
Åstrom, K.J., Hägglund, T.: PID controllers - Theory, Design, and Tuning. International Society for Measurement and Con; 2nd edn (2005)
Li, H., Gupta, M.: Fuzzy Logic and Intelligent Systems. Kluwer Academic Publishers (1995)
Jin, J.: Advanced Fuzzy Systems Design and Applications. Physica-Verlag (2003)
Bertsekas, D.P.: Dynamic Programming and Optimal Control. Athena Scientific (2005)
Sniedovich, M.: Dynamic Programming. Marcel Dekker (1992)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98 (1992) 142–170
Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley (2003)
Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, IEEE Computer Society (1992) 522–525
Hu, A.J., York, G., Dill, D.L.: New techniques for efficient verification with implicitly conjoined bdds. In: DAC ’94: Proceedings of the 31st Annual Conference on Design Automation, New York, USA, ACM Press (1994) 276–282
http://www.dsi.uniroma1.it/∼tronci/cached.murphi.html (2006)
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Venturini Zilli, M.: Exploiting transition locality in automatic verification of finite state concurrent systems. STTT 6 (2004) 320–341
Murphi Web Page: http://sprout.stanford.edu/dill/murphi.html (2004)
Stern, U., Dill, D.: Using magnetic disk instead of main memory in the murϕ verifier. In Hu, A.J., Vardi, M.Y., eds.: Computer Aided Verification, 10th International Conference, CAV ’98, Vancouver, BC, Canada, June 28-July 2, Proceedings. Volume 1427 of Lecture Notes in Computer Science, Springer (1998) 172–183
Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: CHARME ’95: Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, London, UK, Springer-Verlag (1995) 206–224
Nguyen, D., Widrow, B.: The truck backer-upper: an example of self learning in neural networks. In: W.T. Miller, R.S. Sutton, and P.J. Werbos, eds.: Neural Networks For Control, Mit Press Series In Neural Network Modeling and Connectionism. MIT Press, Cambridge, MA (1990) 287–299
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Penna, G.D., Magazzeni, D., Tofani, A., Intrigila, B., Melatti, I., Tronci, E. (2008). Automated Generation of Optimal Controllers through Model Checking Techniques. In: Cetto, J.A., Ferrier, JL., Costa dias Pereira, J., Filipe, J. (eds) Informatics in Control Automation and Robotics. Lecture Notes Electrical Engineering, vol 15. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79142-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-79142-3_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79141-6
Online ISBN: 978-3-540-79142-3
eBook Packages: EngineeringEngineering (R0)