Formalisation De La Logique Temporelle Dans Le Coq
Résumé: L'objectif de ce travail est de fournir une formalisation de la syntaxe ainsi que la sémantique de la logique temporelle linéaire propositionnelle(LTLP) en utilisant le langage de spécification GALLINA de l'assistant de preuves Coq. Par la suite, nous donnerons une vérification formelle de terminaison de l'algorithme du tableau sémantique por cette logique dans l'assistant de preuve Coq
Mots-clès:
Nos services universitaires et académiques
Thèses-Algérie vous propose ses divers services d’édition: mise en page, révision, correction, traduction, analyse du plagiat, ainsi que la réalisation des supports graphiques et de présentation (Slideshows).
Obtenez dès à présent et en toute facilité votre devis gratuit et une estimation de la durée de réalisation et bénéficiez d'une qualité de travail irréprochable et d'un temps de livraison imbattable!
Aucun fichier associé
Si le fichier est volumineux, l'affichage peut échouer. Vous pouvez obtenir le fichier directement en cliquant sur le bouton "Télécharger".
