Verification of Bounded Inclusion Problem for Timed Automata with Diagonal Constraints

The verification of the inclusion problem between two timed languages accepted by timed automata is undecidable in the general case. In the literature, there are several studies proposing decidable solutions for this problem under some restrictions. An interesting work, [4], proposes a theory of timed bounded verification applied to a non-Zeno timed automaton with an upper bound. The solution framework is based on a new discretization technique for timed automata without clocks reset and simple constraints restrictions. The first contribution in this paper aims at proposing an extension of this discretization technique to solve the non-diagonal constraints restriction applied to the timed automata without clocks reset. The proposed solution consists to integrate the Difference Bound Matrices DBM data structure to update the old discretized language. The second contribution focuses on designing all required algorithms relative to the generation of the timed bounded discretized language and the verification of the inclusion problem. In addition, we calculate the time complexity of each proposed algorithm.