Skip to main content
SpringerLink
Log in

Analysis of Slope-Parametric Rectangular Automata

  • Conference paper
  • First Online:
Hybrid Systems V (HS 1997)

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

Included in the following conference series:

Abstract

This paper presents reduction techniques from initialized rectangular automata with slope parameters to linear hybrid automata. The translations are correctness preserving, thereby yielding semialgorithms for the analysis of slope parameters. The automated analysis technique is used to synthesize new bounds on the independent clock drifts of processes in an audio control protocol. The emptiness problem for slope-parametric rectangular automata is proven undecidable.

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, N. Halbwachs, T. 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  MathSciNet  Google Scholar 

  2. R. Alur, T. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181–201, 1996.

    Article  Google Scholar 

  3. R. Alur, T. Henzinger, and M. Vardi. Parametric real-time reasoning. In Proceedings of the 25th Annual Symposium on Theory of Computing, pages 592–601. ACM Press, 1993.

    Google Scholar 

  4. F. Boniol, A. Burgueño, O. Roux, and V. Rusu. Analysis of slope-parametric hybrid automata. In O. Maler, editor, HART 97: Hybrid and Real-Time Systems, Lecture Notes in Computer Science 1201, pages 75–80. Springer-Verlag, 1997.

    Chapter  Google Scholar 

  5. D. Bosscher, I. Polak, and F. Vaandrager. Verification of an audio-control protocol. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, FTRTFT 94: Formal Techniques in Real-time and Fault-tolerant Systems, Lecture Notes in Computer Science 863, pages 170–192. Springer-Verlag, 1994.

    Chapter  Google Scholar 

  6. A. Burgueño and V. Rusu. Task-system analysis using slope-parametric hybrid automata. In C. Lengauer, M. Griebl, and S. Gorlatch, editors, Proc. of the Euro-Par’97 Workshop on Real-Time Systems and Constraints, Lecture Notes in Computer Science 1300, pages 1262–1273. Springer-Verlag, 1997.

    Google Scholar 

  7. K. Čerāns. Algorithmic Problems in Analysis of Real-time System Specifications. PhD thesis, University of Latvia, 1992.

    Google Scholar 

  8. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the Fifth Annual Symposium on Principles of Programming Languages, pages 84–97. ACM Press, 1978.

    Google Scholar 

  9. W. Griffoen. Proof-checking an audio control protocol with LP. Technical Report CS-R 9570, CWI, 1995.

    Google Scholar 

  10. T. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: the next generation. In Proceedings of the 16th Annual Real-time Systems Symposium, pages 56–65. IEEE Computer Society Press, 1995.

    Google Scholar 

  11. T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1(1):110–122, 1997.

    Article  Google Scholar 

  12. T. Henzinger, P. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? In Proceedings of the 27th Annual Symposium on Theory of Computing, pages 373–382. tACM Press, 1995. Full version to appear in Journal of Computer and System Sciences.

    Google Scholar 

  13. N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximation. In B. LeCharlier, editor, SAS 94: Static Analysis Symposium, Lecture Notes in Computer Science 864, pages 223–237. Springer-Verlag, 1994.

    Chapter  Google Scholar 

  14. J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

    Google Scholar 

  15. P.-H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In P. Wolper, editor, CAV 95: Computer-aided Verification, Lecture Notes in Computer Science 939, pages 381–394. Springer-Verlag, 1995.

    Chapter  Google Scholar 

  16. D. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings of 5th GI conference, Lecture Notes in Computer Science 104, pages 167–183. Springer-Verlag, 1981.

    Google Scholar 

  17. A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular differential inclusions. In D. L. Dill, editor, CAV 94: Computer-Aided Verification, Lecture Notes in Computer Science 818, pages 95–104. Springer-Verlag, 1994.

    Chapter  Google Scholar 

  18. V. Rusu and A. Burgueño. Analysis of slope-parametric hybrid automata. Submitted, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cadence Design Systems, Cadence Berkeley Laboratories, 2001 Addison St, Third Floor, Berkeley, CA, 94704-1103, USA

    Howard Wong-Toi

Authors
  1. Howard Wong-Toi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electrical Engineering, University of Notre Dame, Notre Dame, IN, 46556, USA

    Panos Antsaklis  & Michael Lemmon  & 

  2. Hynomics Corporation, 10632 NE 37th Circle, Building 23, Kirkland, WA, 98033, USA

    Wolf Kohn

  3. Department of Mathematics, Cornell University, 217, White Hall, Ithaca, NY, 14853, USA

    Anil Nerode

  4. Electronic Research Laboratory, University of California at Berkeley, 253 Cory Hall, Berkeley, CA, 94720, USA

    Shankar Sastry

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wong-Toi, H. (1999). Analysis of Slope-Parametric Rectangular Automata. In: Antsaklis, P., Lemmon, M., Kohn, W., Nerode, A., Sastry, S. (eds) Hybrid Systems V. HS 1997. Lecture Notes in Computer Science, vol 1567. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49163-5_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-49163-5_21

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65643-2

  • Online ISBN: 978-3-540-49163-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation