Logiques temporelles pour la vérification : expressivité, complexité, algorithmes
Ce travail s'inscrit dans le cadre de la vérification formelle de programmes: le model checking est une technique qui permet de s'assurer qu'une propriété, exprimée en logique temporelle, est vérifiée par le modèle d'un système. Cette thèse étudie plusieurs logiques temporelles,...
Kaydedildi:
| Yazar: | |
|---|---|
| Diğer Yazarlar: | |
| Materyal Türü: | Thèse et Mémoire papier |
| Dil: | Français |
| Baskı/Yayın Bilgisi: |
[S.l.] :
[s.n.]
2003.
|
| Konular: | |
| Not: |
Publication autorisée par le jury |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Temporal logics geared to verification :, expressivesness, complexity, algorithms |
| LEADER | 02503nam a22002897a 4500 | ||
|---|---|---|---|
| 001 | 195870 | ||
| 008 | 030711s2002 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN073426598 | ||
| 041 | 0 | |a fre |b fre |b eng | |
| 084 | |a 004 | ||
| 100 | 1 | |a Markey, Nicolas, |d 1976- | |
| 240 | 1 | 0 | |a Temporal logics geared to verification : |b expressivesness, complexity, algorithms |
| 245 | 1 | 0 | |a Logiques temporelles pour la vérification : |b expressivité, complexité, algorithmes |c par Nicolas Markey ; [sous la dir. de] François Le Berre,... |
| 260 | |a [S.l.] : |b [s.n.], |c 2003. | ||
| 300 | |a 176 p. : |b graph. ; |c 30 cm. | ||
| 500 | |a Publication autorisée par le jury | ||
| 502 | |a Thèse de doctorat. Informatique. Orléans. 2003 | ||
| 504 | |a Bibliogr. p. 163-176. Index | ||
| 520 | |a Ce travail s'inscrit dans le cadre de la vérification formelle de programmes: le model checking est une technique qui permet de s'assurer qu'une propriété, exprimée en logique temporelle, est vérifiée par le modèle d'un système. Cette thèse étudie plusieurs logiques temporelles, du point de vue de l'expressivité et de la complexité. Nous étudions trois grands types de logiques temporelles : - concernant la logique temporelle du temps linéaire, nous prouvons que l'ajout de modalités du passé permet de simplifier l'écriture des formules sans augmenter la complexité des problèmes de model checking. Nous étudions également l'impact de l'ajout de la modalité Now ; - concernant la logique temporelle du temps arborescent, nous établissons la complexité du model checking pour plusieurs extensions classiques de CTL ; - enfin, nous montrons qu'il est possible, sous certaines conditions, de vérifier efficacement des propriétés quantitatives sur la durée séparant deux évènements. | ||
| 650 | |a Temps réel (informatique) | ||
| 650 | |a Logique temporelle | ||
| 650 | |a Complexité de calcul (informatique) | ||
| 650 | |a Thèses et écrits académiques | ||
| 700 | 1 | |a Le Berre, François, |d 1932- |4 ths | |
| 710 | 2 | |a Université d'Orléans. |4 dgg | |
| 787 | 0 | 8 | |i Reproduced as: |0 246688726 |t Logiques temporelles pour la vérification |o expressivité, complexité, algorithmes |f par Nicolas Markey |c Lille |n Atelier national de reproduction des thèses |d 2003 |p Microfiches |s Lille-Thèses |
| 997 | |0 195870 |1 Thèse et Mémoire papier |a Ressource papier |c 0/Orléans/ |c 1/Orléans/BU Sciences, Technologies, STAPS/ |z Orléans, BU Sciences, Technologies, STAPS, TS 19-2003-4 |z Orléans, BU Sciences, Technologies, STAPS, TS 19-2003-4 b | ||