TCTL Inevitability Analysis of Dense-time Systems

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

Inevitability properties in branching temporal logics are of the syntax forall eventually ϕ, where ϕ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.
22 pages

Keywords

Symbolic Computation, B.1.2

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/31511

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/cs/0304003
 http://arxiv.org/abs/cs/0304003

Collections

arXiv