Abstract
This paper addresses the analysis of slope-parametric hybrid automata: finding conditions on the slopes of the automaton variables, for some safety property to be verified. The problem is shown decidable in some practical situations (e.g. finding the running speeds of tasks in a real time application, for all tasks to respect their deadlines). The resolution technique generalizes polyhedral-based symbolic analysis and it involves reasoning about polyhedra with parametric shapes.
Supported by Research Grant of the Spanish Ministry of Education. This research was carried out while the author was visiting the LAN.
Preview
Unable to display preview. Download preview PDF.
References
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.
R. Alur, T. A. Henzinger, and P-H. Ho. Automatic symbolic verification of embedded systems. In Proc. 14th Annual Real-time Systems Symposium, RTSS'93, pages 2–11. IEEE Computer Society Press, 1993.
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.
T. A. Henzinger and P.-H. Ho. HyTech: the cornell HYbrid TECHnology tool. In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, volume 999 of Lecture Notes in Computer Science, pages 265–294. Springer-Verlag, 1994.
T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. What's decidable about hybrid automata? In Proc. of the 27th Annual ACM Symposium on Theory of Computing, STOC'95, pages 373–382, 1995.
O. Roux and V. Rusu. Uniformity for the decidability of hybrid automata. In Internat. Static Analysis Symposium, LNCS 1145, pages 301–316, 1996.
G. M. Ziegler. Lectures on Polytopes, volume 152 of Graduate Texts in Mathematics. Springer-Verlag, 1995.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boniol, F., Burgueño, A., Roux, O., Rusu, V. (1997). Analysis of slope-parametric hybrid automata. In: Maler, O. (eds) Hybrid and Real-Time Systems. HART 1997. Lecture Notes in Computer Science, vol 1201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014715
Download citation
DOI: https://doi.org/10.1007/BFb0014715
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62600-8
Online ISBN: 978-3-540-68330-8
eBook Packages: Springer Book Archive