Checking Timed Buechi Automata Emptiness Using LU-Abstractions

摘要

This paper shows that the zone-based LU-extrapolation of Behrmann et al, that preserves reachability of timed automata, also preserves emptiness of timed Buechi automata. This improves the previous results by Tripakis et al who showed that the k-extrapolation preserves timed Buechi automata emptiness. The LU-extrapolation is coarser than k-extrapolation, allowing better state space reductions. A tool with LU-extrapolation for emptiness checking of timed Buechi automata has been implemented, and some experiments are reported.