Abstract
We provided a framework for the specification and the verification of hybrid systems. We introduced a general specification logic HATL which is an extension of the temporal logic allowing constraints on bounded trajectories expressed by means of hybrid automata. We have shown how to translate verification problems stated in the automata-logic-based or in the logic-based approaches into the automata-based approach in order to apply algorithmic analysis techniques on automata. These translations are based on effective constructions of timed or hybrid automata from formulas in some fragments of HATL. Using these translations, we proved the decidability of the verification problems of timed Büchi automata w.r.t. TATL+ formulas, and of pure-time CDF formulas w.r.t. simple RF formulas.
The fragment TATL+ is a fairly powerful specification language since it subsumes deterministic timed Muller automata, and allows the expression of response as well as invariance timed properties. Its sublanguage TPTL+ constitues a fragment of TPTL whose verification problem is decidable. Moreover. TATL+ (as well as TPTL+) is not comparable with the known logics whose verification problem is decidable. as MITL and EMITL.
Pure-time CDF and simple RF are more expressive than the fragments of CoD that have been suggested to specify control systems and requirements. Thus, our results show, in particular, that the verification of CoD control designs w.r.t. CoD requirement formulas is decidable. This is the first decidability result concerning fragments of (dense time) CoD that are not purely propositional.
This work has been performed while this author was visiting Verimag.
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. TCS. 138. 1995.
R. Alur, C. Courcoubetis, and T. Henzinger. Computing Accumulated Delays in Real-time Systems. In CAV'93. LNCS 697. 1993.
R. Alur, C. Courcoubetis, T. Henzinger, and P-H. Ho. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In Hybrid Systems. LNCS 736. 1993.
R. Alur and D. Dill. A Theory of Timed Automata. TCS, 126, 1994.
R. Alur, T. Feder, and T. Henzinger. The Benefits of Relaxing Punctuality. In PODC'91. 1991.
R. Alur and T. Henzinger. A Really Temporal Logic. In FOCS'89. IEEE, 1989.
A. Bouajjani, R. Echahed. and J. Sifakis. On Model Checking for Real-Time Properties with Durations. In LICS'93. IEEE. 1993.
A. Bouajjani and Y. Lakhnech. Temporal Logic + Timed Automata: Expressiveness and Decidability. In CONCUR'95. LNCS 962. 1995.
A. Bouajjani, Y. Lakhnech. and R. Robbana. From Duration Calculus to Linear Hybrid Automata. In CAV'95. LNCS 939, 1995.
Z. Chaochen, C.A.R. Hoare. and A.P. Ravn. A Calculus of Durations. IPL, 40, 1991.
J. He, C.A.R. Hoare, M. Fränzle, M. Müller-Olm, E.R. Olderog, M. Schenke, M.R. Hansen, A.P. Ravn. and H. Rishel. Provably Correct. Systems. In FTRTFT'94. LNCS 863, 1994.
Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine. Integration Graphs: A Class of Decidable Hybrid Systems. In Hybrid Systems. LNCS 736, 1993.
O. Maler, Z. Manna, and A. Pnueli. From Timed to Hybrid Systems. In REX workshop on Real-Time: Theory and Practice. LNCS 600, 1992.
X. Nicollin, J. Sifakis. and S. Yovine. From ATP to Timed Graphs and Hybrid Systems. In REX workshop on Real-Time: Theory and Practice. LNCS 600, 1992.
A. Pnueli. The Temporal Logic of Programs. In FOCS'77. IEEE, 1977.
W. Thomas. Automata on Infinite Objects. In Handbook of Theo. Comp. Sci. Elsevier Sci. Pub., 1990.
M.Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. In LICS'86. IEEE. 1986.
Th. Wilke. Specifying Timed State Sequences in Powerful Decidable Logics and Timed Automata. In FTRTFT'94. LNCS 863. 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouajjani, A., Lakhnech, Y. (1996). Logics vs. automata: The hybrid case. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds) Hybrid Systems III. HS 1995. Lecture Notes in Computer Science, vol 1066. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0020973
Download citation
DOI: https://doi.org/10.1007/BFb0020973
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61155-4
Online ISBN: 978-3-540-68334-6
eBook Packages: Springer Book Archive