Comparing Two Inclusion Techniques in Timed Automata

Abstract

Verifying the correctness of real-time systems often involves checking language inclusion between timed automata. This problem determines if the language of a system implementation is a subset of the language specified by its design. While the general case is undecidable, recent advancements have proposed techniques for specific scenarios. This paper compares two such techniques: a zone-based semi-algorithm for non-Zeno runs and a time-bounded discretization approach. We analyze their strengths and weaknesses, highlighting cases where each method is advantageous. The comparison highlights the timed bounded discretized language approach's advantages in terms of guaranteed termination and lower memory usage.