Efficient Emptiness Check for Timed B\"uchi Automata (Extended version)
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.
Keywords
Cite
@article{arxiv.1104.1540,
title = {Efficient Emptiness Check for Timed B\"uchi Automata (Extended version)},
author = {Frédéric Herbreteau and B. Srivathsan and Igor Walukiewicz},
journal= {arXiv preprint arXiv:1104.1540},
year = {2020}
}
Comments
Published in the Special Issue on Computer Aided Verification - CAV 2010; Formal Methods in System Design, 2011