Sciweavers

Share
ATVA
2008
Springer

Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions

11 years 7 months ago
Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions
The evaluation of successor or predecessor state spaces through time progress is a central component in the model-checking algorithm of dense-time automata. The definition of the time progress operator takes into consideration of the path condition of time progress and usually results in high complexity in the evaluation. Previous algorithms in this aspect usually assume that the original location invariance conditions of an automaton are convex in the dense-time state space. Based on this assumption, efficient algorithms for convex path conditions can be designed for reachability analysis. However, it is not clear whether the path conditions are still convex in the general setting of TCTL model-checking. In this work, we discuss the concept of time-convexity that allows us to relax the restrictions on the application of time-progress evaluation algorithm for convex path conditions. Then we give examples in TCTL model-checking that engenders time-concave path conditions even when the o...
Farn Wang
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where ATVA
Authors Farn Wang
Comments (0)
books