Comparing Two Inclusion Techniques in Timed Automata

Main Article Content

Hafedh Mahmoud Zayani, Refka Ghodhbani, Taoufik Saidani


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.

Article Details

How to Cite
Taoufik Saidani, H. M. Z. R. G. (2024). Comparing Two Inclusion Techniques in Timed Automata. International Journal on Recent and Innovation Trends in Computing and Communication, 12(2), 85–90. Retrieved from