Inevitability properties in branching temporal logics are of the syntax ∀◇ø, where ø is an arbitrary (timed) CTL formula. Such inevitability properties in dense-time logics can be analyzed with greatest fixpoint calculation. We present algorithms to model-check inevitability properties both with and without non-Zeno computation requirement. We discuss a technique for early decision on greatest fixpoint calculation. Our algorithms come with a d-parameter for the measurement of time-progress. We have experimented with various issues, which may affect the performance of TCTL inevitability analysis. Specifically, we report the performance of our implementation w.r.t. various d-parameter values and with or without the non-Zeno computation requirement in the evaluation of greatest fixpoints. We have also experimented with safe abstration techniques for model-checking TCTL inevitability properties. Analysis of experiment data helps clarify how various techniques can be used to improve verification of inevitability properties. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Wang, F., Hwang, G. D., & Yu, F. (2003). TCTL inevitability analysis of dense-time systems. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2759, 176–187. https://doi.org/10.1007/3-540-45089-0_17
Mendeley helps you to discover research relevant for your work.