Compositional Detection of Zeno Behavior in Timed Automata with

We present a compositional analysis to detect Zeno behavior in Timed Automata with Deadlines. A syntactic analysis is defined, based on Tripakis ’ strong non-Zenoness property, which identifies all elementary cycles where Zeno behavior may occur. This analysis is complemented by TCTL reachability properties, which characterize the occurrence Zeno behavior in potentially unsafe cycles.