Stavros Tripakis
Checking Timed Buchi Automata Emptiness on Simulation Graphs (2006)
Checking Timed Buchi Automata Emptiness on Simulation Graphs (2006)
TR-2006-1.pdf
Keywords: formal methods, specification languages, model checking, timed Buchi automata, property-preserving abstractions.
Abstract: This paper completes previous work on checking language emptiness of timed Buchi automata efficiently. In previous work we showed how to check emptiness on the region-closed simulation graph. However, the latter is not used in practice, since its nodes are non-convex, thus, not easily representable. Using recent results of Bouyer on simulation-graph over-approximations that preserve convexity, we show that the previous result carries over to the zone-closed simulation graph. The nodes of the latter are convex and can be efficiently represented. The zone-closed simulation graph is used in the tools Kronos and Uppaal for checking reachability. Our result shows that these tools can be also used to check emptiness of timed Buchi automata with small modifications.
