Hoan VU
École Nationale Supérieure des Mines de Saint-Étienne - Thèse pour obtenir le grade de Docteur. Spécialité : Informatique

Logique temporelle linéaire LTL, Confiance au web

  1. Infrastructure de gestion de la confiance sur Internet
  2. Définitions: Contrôle, Transaction, Authentification et Certificat
  3. La confiance dans les domaines d’application Internet
  4. Risque, Réputation, Recommandation et domaine d’application Internet
  5. Sécurité, Négociation et Gestion de la confiance confiance sur Internet
  6. La gestion de la confiance sur Internet basée sur la politique
  7. Gestion de la confiance au web sémantique basée sur l’expérience
  8. Approches hybrides de la gestion de la confiance sur Internet
  9. Système de négociation de la confiance au web sémantique
  10. Prise en charge du risque pour la gestion de confiance sur Internet
  11. Comparaison des systèmes de gestion de confiance sur Internet
  12. Contraintes pour un système de gestion de la confiance
  13. Modèle global de gestion de la confiance sur Internet
  14. Modèle de confiance de SECURE
  15. Logique temporelle linéaire LTL, Confiance au web
  16. Framework logique pour les systèmes de réputation
  17. Architecture d’un système de gestion de la confiance
  18. Formalisation de la confiance aux applications
  19. Transaction dans le cadre du commerce électronique et la confiance
  20. Évaluation de la contribution d’un utilisateur à Wikipédia
  21. La notion de négociation, Modèle de la négociation de la confiance
  22. Architecture du système de négociation de la confiance
  23. Protocole de négociation, Système de négociation de la confiance
  24. Module de négociation de la confiance
  25. Transaction de e-commerce et Tiers de confiance pour le paiement
  26. Politique de confiance dans une transaction de e-commerce
  27. La gestion de la Stratégie de Négociation – Transaction en ligne
  28. Processus de gestion du risque, Système de gestion de la confiance
  29. Modèle du risque risque et le système de gestion de la confiance
  30. Politique du tiers de paiement, Transaction de commerce électronique
  31. Prototype de négociation de la confiance : Architecture
  32. Politique de confiance: Spécification de la politique en XML
  33. Réalisation du module de vérification de la politique de sécurité
  34. Le système de gestion de la confiance au web

4.4 Logique temporelle linéaire LTL
Nous présentons dans cette section une logique temporelle linéaire (LTL). Cette présentation nous permet d’introduire une variante de cette logique, PP-LTL (Pure Past Linear Temporal Logic) qui est dédiée aux faits passés. Une présentation plus détaillée peut être trouvée dans [57].
Une logique temporelle est une extension de la logique conventionnelle : elle intègre de nouveaux opérateurs qui expriment la notion du temps. La logique classique ne peut pas exprimer une assertion liée au comportement d’un système par exemple, « après exécution d’une instruction I, le système se bloque ». Dans une telle assertion, les actions s’exécutent en suivant l’axe du temps : à l’instant t l’instruction I est exécutée et à l’instant t+1 le système est bloqué. Les logiques temporelles ont été proposées pour modéliser ce type d’assertion, en fournissant des opérateurs pour exprimer les comportements passés et futurs du système.
La logique LTL permet de représenter le comportement des systèmes réactifs au moyen de propriétés. Les propriétés spécifient le comportement du système à un moment de son exécution.
Le système fonctionne de manière linéaire dans le temps. Les exécutions du système peuvent être modélisées par un système de transition ST qui se compose de plusieurs états, et permet de passer de l’un à l’autre. Chaque état de ST correspond à un état du système à un instant t. À chaque état, nous pouvons observer les propriétés, si elles existent, pour identifier le comportement du système. Le comportement global du système est spécifié par l’observation des propriétés dans tous les états concernés.
L’activité du système se déroule de manière chronologique (figure 4.2). Elle se décompose en une séquence d’états représentant les actions de l’entité dans le temps.
Déroulement temporel d’un système en logique LTL
Fig. 4.2 Déroulement temporel d’un système en logique LTL
4.4.1 Syntaxe
Les formules de la logique LTL peuvent être définies de la manière suivante :
-Propositions atomiques :
true | f alse | (x = v) sont des formules ((x = v) se lit x a pour valeur v).
-Connecteurs booléens :
Soit φ, ψ ∈ LT L, toutes les formules de la forme suivante appartiennent à LTL :
¬φ | φ ∧ ψ | φ ∨ ψ | φ → ψ | φ ↔ ψ
-Connecteurs temporels :
Soit φ, ψ ∈ LT L, toutes les formules de la forme suivante appartiennent à LTL :
Gφ | F φ | φ U ψ | X φ
4.4.2 Sémantique
Soit Π = s0, s1, s2 . . ., une séquence d’états du système de transition, et soit φ une formule en logique LTL. On définit « φ est satisfaite pour Π », noté Π |= φ de la manière suivante : pour tout i = 0, 1 . . ., on désigne par Πi la séquence d’états si, si+1 , si+2 . . . (on note que Π = Π0), soit φ et ψ des formules en logique LTL.
1. Π |= true et Π 2 f alse
2. Π |= (x = v) ssi s0 |= (x = v).
3. Π |= φ ∧ ψ ssi Π |= φ et Π |= ψ
Π |= φ ∨ ψ ssi Π |= φ ou Π |= ψ
4. Π |= ¬φ ssi Π 2 φ
5. Π |= φ → ψ ssi Π 2 φ ou Π |= ψ
Π |= φ ↔ ψ ssi Π 2 φ et Π 2 ψ à la fois, ou Π |= φ et Π |= ψ à la fois.
6. Π |= X φ si Π1 |= φ
Π |= F φ si ∃i ∈ (0, 1, . . .) tel que Πi |= φ
Π |= Gφ si ∀i ∈ (0, 1, . . .) tel que Πi |= φ
Π |= φU ψ si ∃k ∈ (0, 1, . . .) tel que j < k, Πj |= φ et j ≥ k, Πj |= ψ
Nous explicitons la sémantique des opérateurs temporels X , F , G et U avec les figures suivantes (les états en noir indiquent que la formule est vérifiée) :
framework-logique-systemes-reputation
framework-logique-systemes-reputation
Notons que l’état hachuré indique à partir de quel moment ψ est vérifiée.
Nous pouvons remarquer que la logique LTL est utilisée pour spécifier des faits (le comportement d’une entité) dans le temps (passé et futur). Pourtant, de par les particularités de notre modèle de gestion de la confiance, nous n’avons besoin que d’exprimer des comportements passés. Nous utiliserons donc dans la suite de nos travaux une logique temporelle qui ne s’intéresse qu’aux faits passés : PP-LTL (Pure-Past LTL). Nous présenterons à la section 4.5.3 les détails de PP-LTL.
4.4.3 Exemple
Supposons un système de transactions qui modélise le système téléphonique. Nous avons les deux événements signal et réponse qui représentent la signalisation d’un appel (sonnerie) et l’actions d’y répondre. Pour exprimer le fait que tout signal est suivi d’une réponse, nous pouvons utiliser la formule suivante :
G(signal → F reponse)
4.4.4 Vérification
Les techniques du model checking [17] sont traditionnellement utilisées pour la vérification des formules de logique LTL. Les algorithmes de vérification connus sont NPcomplet.
Lire le mémoire complet ==> (Infrastructure de gestion de la confiance sur Internet )
Thèse pour obtenir le grade de Docteur – Spécialité : Informatique
École Nationale Supérieure des Mines de Saint-Étienne

Cliquez sur suivant article pour lire la suivante partie de ce mémoire:

Abonnez-vous!
Inscrivez-vous gratuitement à la Newsletter et accédez à des milliers des mémoires de fin d’études !
Publier son mémoire!
WikiMemoires - Publier son mémoire de fin d’études !

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *