Notify me of new papers
via Email or RSS

ABSTRACT:
Inevitability properties in branching temporal logics are of the syntax AE f, where f is an arbitrary (timed) CTL (Computation Tree Logic) formula. Such inevitability properties in dense-time logics can be analyzed with the greatest fixpoint calculation. We present algorithms to model-check inevitability properties. We discuss a technique for early decision on greatest fixpoint calculation which has shown promising performance against several benchmarks. We have experimented with various issues which may affect the performance of TCTL inevitability analysis. Specifically, our algorithms come with a parameter for the measurement of timeprogress. We report the performance of our implementation with regard to various parameter values and with or without the non-Zeno computation requirement in the evaluation of greatest fixpoints. We have also experimented with safe abstraction techniques for model-checking TCTL inevitability properties. The experiment results help us in deducing rules for setting the parameter for verification performance. Finally, we summarize suggestions for configurations of efficient TCTL inevitability evaluation procedure.

SUGGESTED CITATION:
Farn Wang, G D. Huang, and Fang Yu, "TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering" (2006). IEEE TRANSACTIONS ON SOFTWARE ENGINEERING. 28 (7), pp. 510-526. Postprint available free at: http://repositories.cdlib.org/postprints/1937

REQUIRED PUBLISHER STATEMENT:
©2006 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.