Coarse abstractions make Zeno behaviours difficult to detect

TL;DR

This paper investigates the difficulty of detecting Zeno behaviors in timed automata, showing that certain optimization techniques increase complexity and proposing a modified approach to improve efficiency.

Contribution

It analyzes the complexity of Zeno run detection under various extrapolation operators and introduces a weakened LU-extrapolation to enable more efficient checking.

Findings

NP-completeness of LU-extrapolation for Zeno detection

Conditions for polynomial complexity in extrapolation operators

A modified LU-extrapolation that improves Zeno detection efficiency

Abstract

An infinite run of a timed automaton is Zeno if it spans only a finite amount of time. Such runs are considered unfeasible and hence it is important to detect them, or dually, find runs that are non-Zeno. Over the years important improvements have been obtained in checking reachability properties for timed automata. We show that some of these very efficient optimizations make testing for Zeno runs costly. In particular we show NP-completeness for the LU-extrapolation of Behrmann et al. We analyze the source of this complexity in detail and give general conditions on extrapolation operators that guarantee a (low) polynomial complexity of Zenoness checking. We propose a slight weakening of the LU-extrapolation that satisfies these conditions.