Abstract
Time progress conditions in hybrid systems are usually specified in terms of invariants, predicates characterizing states where time can continuously progress or dually, deadline conditions, predicates characterizing states where time progress immediately stops. The aim of this work is the study of relationships between general time progress conditions and these generated by using state predicates. It is shown that using deadline conditions or invariants allows to characterize all practically interesting time progress conditions. The study is performed by using a Galois connection between the corresponding lattices. We provide conditions for the connection to be a homomorphism and apply the results to the compositional description of hybrid systems.
Partially supported by CNET Contract #95 7B.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.
O. Ore. Galois connections. Trans. Amer. Math. Society, 55:493–513, February 1944.
L.E. Sanchis. Data types as lattices: retractions, closures and projections. RAIRO, Theoretical Computer Science, 11, no 4:339–344, 1977.
P. Sénac, M. Diaz, and P. de Saqui-Sannes. Toward a formal specification of multimedia scenarios. Annals of telecomunications, 49(5–6):297–314, 1994.
J. Sifakis. Use of petri nets for performance evaluation. In H. Beilner and E. Gelenebe, editors, Measuring, modelling and evaluating computer systems, pages 75–93. North-Holland, 1977.
J. Sifakis and S. Yovine. Compositional specification of timed systems. In 13th Annual Symposium on Theoretical Aspects of Computer Science, STACS'96, pages 347–359, Grenoble, France, February 1996. Lecture Notes in Computer Science 1046, Spinger-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bornot, S., Sifakis, J. (1997). Relating time progress and deadlines in hybrid systems. 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/BFb0014733
Download citation
DOI: https://doi.org/10.1007/BFb0014733
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