Skip to main content
SpringerLink
Log in

Using Cylindrical Algebraic Decomposition for the Analysis of Slope Parametric Hybrid Automata

  • Conference paper
  • First Online:
Book cover Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1926))

Abstract

We address the ambitious problem of synthesizing the parameters which stand for the execution speeds in time constrained executions of a real-time system. The core of the paper is a new method based on the Gröbner bases and the so-called Cylindrical Algebraic Decomposition in order to design a simplification algorithm and a test inclusion upon sets of inequalities. The method is illustrated throughout the paper with a small example.

IRCCyN/CNRS UMR 6597 (1 rue de la Noë, BP 92101, 44321 Nantes cedex 03, France) e-mail: fMichael.Adelaide j Olivier.Rouxg@ircyn.ec-nantes.fr

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
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. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. of the 5th. Annual Symposium on Logic in Computer Science, LICS’90, pages 41–425. IEEE Computer Society Press, 1990.

    Google Scholar 

  2. R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  3. R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  4. e99]_M. AdélaÏde. Application des bases de gröbner à l’analyse paramétrique des systèmes hybrides. Master’s thesis, Ecole Centrale de Nantes, august 1999.

    Google Scholar 

  5. R. Alur and T. A. Henzinger. Real-time system = discrete system + clock variables. In T. Rus and C. Rattray, editors, Theories and Experiences for Real-Time System Development-Papers presented at First AMAST Workshop on Real-Time System Development, pages 1–29, Iowa City, Iowa, 1994. World Scientific Publishing. Also available as Cornell University technical report CSD-TR-94-1403.

    Google Scholar 

  6. R. Alur, T. A. Henzinger, and M. Y. Vardi. Parametric real-time reasoning. In Proc. of the 25th Annual ACM Symposium on Theory of Computing, STOC’93, pages 592–601, 1993.

    Google Scholar 

  7. E. Asarin, O. Maler, and A. Pnueli. Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science, 138:35–65, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  8. A. Burgueño Arajona. Vérification des Systèmes Temporisés par des Méthodes d’Observation et d’Analyse Paramétrique. PhD thesis, Ecole Nationale Supérieure de l’Aéronautique et de l’Espace, june 1998.

    Google Scholar 

  9. F. Boniol, A. Burgueño, O. Roux, and V. Rusu. Analysis of slope-parametric hybrid automata. In O. Maler, editor, Proc. of the International Workshop on Real time and Hybrid Systems, HART 97, pages 75–80. Springer-Verlag, March 26-28 1997.

    Google Scholar 

  10. A. Burgueño and V. Rusu. Task-system analysis using slope-parametric hybrid automata. In Proc. of the Euro-Par’97 Workshop on Real-Time Systems and Constraints, Passau, Germany, August 26-29 1997. Springer-Verlag’s Lecture Notes in Computer Science series No1300.

    Google Scholar 

  11. B. Buchberger. Gröbner Bases: an Algorithmic Method in Polynomial Ideal Theory, pages 184–232. Reidel.

    Google Scholar 

  12. T. Becker and V. Weispfenning. Gröbner Bases: A Computationnal Approach to Commutative Algebra. Springer Verlag, 1993.

    Google Scholar 

  13. A.M. Cohen. Gröbner base: a primer. Technical report, Computer Algebra Information Network, Europe, 1996.

    Google Scholar 

  14. George E. Collins. Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. In Proceedings of the 2nd GI Conference, volume 33 of Lecture Notes in Computer Science, pages 134–183, Kaiserslautern, 1975. Springer, Berlin.

    Google Scholar 

  15. J. Little D. Cox and D. O’Shea. Ideals, Varieties and Algorithms. Springer Verlag, 1992.

    Google Scholar 

  16. Laureano Gonzales-Vega, Fabrice Rouillier, Marie-FranÇoise Roy, and Guadalupe Trujillo. Some Tapas of Computer Algebra. Eindoven University of Technology, a.m. cohen and h. cuypers and h. sterk edition, 1995.

    Google Scholar 

  17. T. Henziger. The theroie of hybrid auromata. In IEEE Symposium on Logic In Computer Science, pages 278–282, 1996.

    Google Scholar 

  18. T.A. Henzinger and P.-H. Ho. HyTech: The Cornell Hybrid Technology Tool. In P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, editors, Hybrid Systems II, Lecture Notes in Computer Science 999, pages 265–293. Springer-Verlag, 1995.

    Google Scholar 

  19. O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In J. W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Proc. of the REX workshop ‘Real-Time: theory in practicers, volume 600 of Lecture Notes in Computer Science, pages 447–484, Berlin, New York, 1992. Springer-Verlag.

    Google Scholar 

  20. M. Jirstrand. Cylindrical algebraic decomposition — an introduction. Technical report, Computer Algebra Information Network, Europe, Departement of Electrical Engineering, Linköping university, S-581 83 Linköping. Sweden, October 1995.

    Google Scholar 

  21. G. Roda. Quantifier elimination — lecture notes based on a course by g.e. collins, risc-summer semester 96. Technical report, Computer Algebra Information Network, Europe, July 1996.

    Google Scholar 

  22. Farn Wang. Parametric timing analysis for real-time systems. 130(2):131–150, 1 November 1996.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut de Recherche en Communication et Cybernétique de Nantes, France

    Michaël AdélaÏde & Olivier Roux

Authors
  1. Michaël AdélaÏde
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Olivier Roux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Tata Research Development and Design Centre, 54B, Hadapsar Industrial Estate, Pune, 411013, India

    Mathai Joseph

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

AdélaÏde, M., Roux, O. (2000). Using Cylindrical Algebraic Decomposition for the Analysis of Slope Parametric Hybrid Automata. In: Joseph, M. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2000. Lecture Notes in Computer Science, vol 1926. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45352-0_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-45352-0_21

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41055-3

  • Online ISBN: 978-3-540-45352-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation