TCTL inevitability analysis of dense-time systems

10Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free