Abstract
The evaluation of successor or predecessor state spaces through time progress is a central component in the model-checking algorithm of dense-time automata. The definition of the time progress operator takes into consideration of the path condition of time progress and usually results in high complexity in the evaluation. Previous algorithms in this aspect usually assume that the original location invariance conditions of an automaton are convex in the dense-time state space. Based on this assumption, efficient algorithms for convex path conditions can be designed for reachability analysis. However, it is not clear whether the path conditions are still convex in the general setting of TCTL model-checking. In this work, we discuss the concept of time-convexity that allows us to relax the restrictions on the application of time-progress evaluation algorithm for convex path conditions. Then we give examples in TCTL model-checking that engenders time-concave path conditions even when the original automaton location invariance conditions are time-convex. Then we present two techniques that allow us to apply the evaluation algorithms for time-convex path conditions to time-concave path conditions. Finally, we report our experiment with the techniques. For some benchmarks, our techniques may enhance the performance of model-checking by an order of magnitude.
The work is partially supported by NSC, Taiwan, ROC under grants NSC 95-2221-E-002-067 and NSC 95-2221-E-002-072.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Courcoubetis, C., Dill, D.L.: Model Checking for Real-Time Systems. In: IEEE LICS (1990)
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid Automata: an Algorithmic Approach to the Specification and Verification of Hybrid Systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)
Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems. In: Hybrid Control System Symposium. LNCS. Springer, Heidelberg (1996)
Dill, D.L.: Timing Assumptions and Verification of Finite-state Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)
Fourier, J.B.: (reported in:) Analyse des travaux de l’Académie Royale des Sciences pendant l’année 1824, Partie Mathématique (1827)
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for Real-Time Systems. IEEE LICS (1992)
Wang, F.: Efficient Verification of Timed Automata with BDD-like Data-Structures, STTT (Software Tools for Technology Transfer). vol. 6(1) (June 2004) In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 189–205. Springer, Heidelberg (2002)
Wang, F.: Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-like Data-Structures. IEEE Transactions on Software Engineering 31(1), 38–51 (2005); A preliminary version. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 38–51. Springer, Heidelberg (2004)
Wang, F., Huang, G.-D., Yu, F.: TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering. IEEE Transactions on Software Engineering 32(7) (2006)
Yovine, S.: Kronos: A Verification Tool for Real-Time Systems. International Journal of Software Tools for Technology Transfer 1(1/2) (October 1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, F. (2008). Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions. In: Cha, S.(., Choi, JY., Kim, M., Lee, I., Viswanathan, M. (eds) Automated Technology for Verification and Analysis. ATVA 2008. Lecture Notes in Computer Science, vol 5311. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88387-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-88387-6_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88386-9
Online ISBN: 978-3-540-88387-6
eBook Packages: Computer ScienceComputer Science (R0)