In this paper, we propose a new method for representing real-time systems symbolically : the TMTDGs (Timed Mirroring Typed Decision Graphs) representation, that is an evolved combination of TDGs that exploit the property of mirroring and timed constraints. It provides a considerable gain in memory space compared to the other structures. Hence the motivation of this paper is about the symbolic structure for the modeling of timed systems, based on the algorithms that we propose in this work.

Summary form only given. In symbolic model checking of untimed systems, the general approach is based on BDDs (Binary Decision Diagrams) representation. Concurrently, TDGs (typed Decision Graphs) were proposed in another context, bring a better profit of capacity memory. However, the symbolic method do not easily generalize to models that contain variables ranging over noncountable domains like for example real-time systems where time is modeled using continuous real variables and the behavior of a system is specified using constraints on these variables. To solve the reachability problem for a timed system, there are very few results on how model checking is efficient, such as the technique of DDDs (Difference Decision Diagrams) representing difference constraints on clocks. But, it remains an open problem to find algorithms and data structures that work just as well for timed systems as BDDs do for untimed systems. We present a methodology for the symbolic model checker using a new technique of representation of timed systems: the DTDGs, Difference Typed Decision Graphs that is a combination of TDGs and DDDs. Then, our approach consists in analyzing timed systems symbolically, and describe the corresponding data structure (DTDGs) for representing the state space of a timed system. For that, we use timed graphs for the modelling of timed systems. This result allows us to analyse timed systems with both the discrete part of states and the associated timing information. Hence the motivation is about symbolic model checking for timed systems based on difference typed decision graphs.

Summary form only given. Several applications generate complicated finite states systems as the design of the communications protocols and the design of circuits. When the number of states of a system is large, it is difficult to determine manually if such a system is correct or not. The checking or model checking proposed in parallel by both (Clarke and Emerson, Quielle and Sifakis) is a method to decide automatically if a finite states system satisfies or not its specifications. This algorithm is called model checking. In symbolic model checking of finite state systems, the general approach is based on BDDs (binary decision diagrams) representation, proposed by Bryant. However, the problem of the explosion of the space of states therefore is not solved in an effective way. Also, the construction of the BDDs proves sometimes difficult in some applications, in particular in software applications. For the static analysis of programs, another model of symbolic notation, the TDGs (typed decision graphs), was proposed by Mauborgne. We show that, in this context, the TDGs bring a considerable profit of capacity memory compared to the BDDs. This reduction of the complexity of the representation lets hope for an improvement of the execution times. Thus, we use this symbolic representation for our environment of verification and we attempt to improve executions time of verifications programs. We detail the approach of symbolic representation of the finite states systems: the set of states and the transition relation with our method of construction of TDGs from the logical operations. To specify the behaviour of a system according to the passing of the time, we are interested to the temporal logic CTL(computational tree logic), that allows the expression of the properties of the branching time. We apply that on the example of the 3-bit counter. Then, we illustrate the example of processes using a variable semaphore to implement mutual exclusion. Hence, the motivation of our- research which is about the development of an environment of symbolic model checking based on TDGs. In a future work, we are interested to apply this environment for the checking of the real applications and to compare its performances with the existing tools for checks.