Skip to main content
SpringerLink
Log in

Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems

  • Conference paper
Book cover Theoretical Aspects of Computing – ICTAC 2012 (ICTAC 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7521))

Included in the following conference series:

Abstract

We show that the existence of a quantized controller for a given Discrete Time Linear Hybrid System (DTLHS) is undecidable. This is a relevant class of controllers since control software always implements a quantized controller. Furthermore, we investigate the relationship between dense time modelling and discrete time modelling by showing that any Rectangular Hybrid Automaton (and thus, any Timed Automaton) can be modelled as a DTLHS.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Agrawal, M., Thiagarajan, P.S.: The Discrete Time Behavior of Lazy Linear Hybrid Automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 55–69. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of Hybrid Systems. Theoretical Computer Science 138(1), 3–34 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R.: Timed Automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  4. Asarin, E., Bouajjani, A.: Perturbed Turing Machines and Hybrid Systems. In: LICS, pp. 269–278 (2001)

    Google Scholar 

  5. Bemporad, A., Morari, M.: Verification of Hybrid Systems via Mathematical Programming. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 31–45. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Brogan, W.L.: Modern Control Theory, 3rd edn. Prentice-Hall, Inc., Upper Saddle River (1991)

    MATH  Google Scholar 

  7. Cassez, F., Henzinger, T.A., Raskin, J.-F.: A Comparison of Control Problems for Timed and Hybrid Systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 134–148. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Cimatti, A., Roveri, M., Traverso, P.: Strong planning in non-deterministic domains via Model Checking. In: AIPS, pp. 36–43 (1998)

    Google Scholar 

  9. Frehse, G.: Phaver: algorithmic verification of Hybrid Systems past Hytech. Int. J. Softw. Tools Technol. Transf. 10(3), 263–279 (2008)

    Article  MathSciNet  Google Scholar 

  10. Fu, M., Xie, L.: The sector bound approach to quantized feedback control. IEEE Trans. on Automatic Control 50(11), 1698–1711 (2005)

    Article  MathSciNet  Google Scholar 

  11. Henzinger, T., Ho, P.H., Wong-Toi, H.: Hytech: A model checker for Hybrid Systems. STTT 1(1), 110–122 (1997)

    Article  MATH  Google Scholar 

  12. Henzinger, T.A., Kopke, P.W.: Discrete-time Control for Rectangular Hybrid Automata. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 582–593. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  13. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about Hybrid Automata? J. of Computer and System Sciences 57(1), 94–124 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  14. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal: Status & Developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 456–459. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  15. Mari, F., Melatti, I., Salvo, I., Tronci, E.: Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 180–195. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Minsky, M.L.: Recursive unsolvability of Post’s problem of ”tag” and other topics in theory of Turing Machines. The Annals of Mathematics 74(3), 437–455 (1961)

    Article  MathSciNet  MATH  Google Scholar 

  17. Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44(10), 2508–2516 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  18. Tronci, E.: Automatic synthesis of controllers from formal specifications. In: ICFEM, pp. 134–143. IEEE (1998)

    Google Scholar 

  19. Vidal, R., Schaffert, S., Shakernia, O., Lygeros, J., Sastry, S.: Decidable and semi-decidable controller synthesis for classes of Discrete Time Hybrid Systems. In: CDC, pp. 1243–1248. IEEE Computer Society (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Sapienza University of Rome, Italy

    Federico Mari, Igor Melatti, Ivano Salvo & Enrico Tronci

Authors
  1. Federico Mari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Igor Melatti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ivano Salvo
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Enrico Tronci
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. National University of Singapore, Computing Drive 13, 117417, Singapore, Singapore

    Abhik Roychoudhury

  2. International Institute of Information Technology, Eletronics City 26-C, 560100, Bangalore, India

    Meenakshi D’Souza

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mari, F., Melatti, I., Salvo, I., Tronci, E. (2012). Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems. In: Roychoudhury, A., D’Souza, M. (eds) Theoretical Aspects of Computing – ICTAC 2012. ICTAC 2012. Lecture Notes in Computer Science, vol 7521. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32943-2_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32943-2_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32942-5

  • Online ISBN: 978-3-642-32943-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation