TCTL Inevitability Analysis of Dense-time Systems

Inevitability properties in branching temporal logics are of the syntax forall eventually \phi, where \phi is an arbitrary (timed) CTL formula. In the sense that "good things will happen", they are parallel to the "liveness" properties in linear temporal logics. 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 requirement of non-Zeno computations. We discuss a technique for early decision on greatest fixpoints in the temporal logics, and experiment with the effect of non-Zeno computations on the evaluation of greatest fixpoints. We also discuss the TCTL subclass with only universal path quantifiers which allows for the safe abstraction analysis of inevitability properties. Finally, we report our implementation and experiments to show the plausibility of our ideas.