Efficient Emptiness Check for Timed B\"uchi Automata (Extended version)

TL;DR

This paper introduces a new, more efficient method for checking the non-emptiness of timed B"uchi automata by avoiding exponential blowups and using an on-the-fly approach that only applies complex checks when necessary.

Contribution

It proposes a construction that prevents exponential blowup in non-Zenoness checking and an on-the-fly algorithm that optimizes the non-emptiness verification process.

Findings

The new construction avoids exponential blowup in certain cases.

The on-the-fly algorithm reduces unnecessary complex checks.

Experimental results demonstrate improved efficiency over standard methods.

Abstract

The B\"uchi non-emptiness problem for timed automata refers to deciding if a given automaton has an infinite non-Zeno run satisfying the B\"uchi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, it is shown that this simple transformation may sometimes result in an exponential blowup. A construction avoiding this blowup is proposed. It is also shown that in many cases, non-Zenoness can be ascertained without extra construction. An on-the-fly algorithm for the non-emptiness problem, using non-Zenoness construction only when required, is proposed. Experiments carried out with a prototype implementation of the algorithm are reported.