Résumé de l'exposé :
Nous proposons une structure symbolique pour la vérification (model
checking)
des systèmes temporisés temps-réel : Les TMTDGs (Timed
Mirroring Typed Decision
Graphs), qui représente, d’une part, structurellement, une version
réduite des BDDs, en
exploitant la propriété du « miroir » et d’autre
part, sémantiquement, les contraintes
temporelles du système. Cette approche permet d’aboutir à des
gains considérables en
espace mémoire.