La logique temporelle est une branche de la logique mathématique et plus précisément de la logique modale, qui est formalisée de plusieurs manières. La caractéristique commune de ces formalisations réside en l'ajout de modalités (autrement dit de « transformateurs de prédicats ») liées au temps ; par exemple, une formule typique de la logique modale est la formule , qui se lit : « la formule est satisfaite jusqu'à ce que la formule le soit » et qui signifie que l'on cherche à garantir qu'une certaine propriété (ici ) est satisfaite pendant tout le temps qui court avant qu'une autre formule (ici ) le soit. D'un point de vue sémantique, cela signifie que la notion de vérité dans ces logiques prend en compte l'évolution du monde. C'est-à-dire qu'une proposition peut être, à un moment, satisfaite, puis plus tard, ne plus l'être. Plusieurs formalisations de la logique temporelle ont été décrites, prenant en compte diverses modalités de base. La logique temporelle est très utilisée en vérification formelle, où la technique de base est essentiellement le model checking. On peut, par exemple, y exprimer le fait qu'un événement dangereux ne doit pas survenir tant qu'une certaine condition de sécurité n'est pas satisfaite. Dans cet article, seul est présenté le calcul des propositions temporel, autrement dit un calcul des propositions augmenté de modalités temporelles, qui sera néanmoins appelé « logique temporelle ». Ces logiques sont définies sur un ensemble de propositions atomiques P ou variables de propositions. Ces propositions atomiques sont combinées par un certain nombre de connecteurs logiques, dont les connecteurs usuels : et, ou, non, implication, ainsi que d'autres opérateurs que l'on appelle des modalités. La logique temporelle est donc une logique modale.

À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Cours associés (5)
CS-550: Formal verification
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
EE-554: Automatic speech processing
The goal of this course is to provide the students with the main formalisms, models and algorithms required for the implementation of advanced speech processing applications (involving, among others,
PHYS-101(f): General physics : mechanics
Le but du cours de physique générale est de donner à l'étudiant les notions de base nécessaires à la compréhension des phénomènes physiques. L'objectif est atteint lorsque l'étudiant est capable de pr
Afficher plus
Séances de cours associées (23)
ODEs linéaires de deuxième ordre
Couvre la solution des ODE linéaires de second ordre avec des coefficients constants et explore la méthode de variation des paramètres.
Muscles de la cavité orale: Anatomie et fonction
Explore l'anatomie et la fonction des muscles de la cavité buccale et leur rôle dans les mouvements hyoïdes et mandibules.
Impact Investissement : Technologies, Innovations et Marchés Émergents
Explore l'investissement d'impact, les objectifs sociaux, les résultats, les méthodes de mesure et les exercices pratiques d'évaluation d'impact.
Afficher plus
Publications associées (59)

Temporal aspects of feature integration in vision

Lukas Vogelsang

To fully comprehend visual perception, we need to necessarily understand its temporal dimension. Our visual environment is highly dynamic, requiring the processing and integration of temporal signals in order to make sense of it. Many processes, such as th ...
EPFL2024

Data-Driven Behaviour Estimation in Parametric Games

Anna Maria Maddux, Nicolò Pagan

A central question in multi-agent strategic games deals with learning the underlying utilities driving the agents' behaviour. Motivated by the increasing availability of large data-sets, we develop an unifying data-driven technique to estimate agents' util ...
Elsevier2023

Non-Hermitian time evolution: From static to parametric instability

Romain Christophe Rémy Fleury, Aleksi Antoine Bossart

Eigenmode coalescence imparts remarkable properties to non-Hermitian time evolution, culminating in a purely non-Hermitian spectral degeneracy known as an exceptional point (EP). Here, we revisit time evolution around EPs, looking at both static and period ...
2021
Afficher plus
Concepts associés (18)
Logique modale
En logique mathématique, une logique modale est un type de logique formelle qui étend la logique propositionnelle, la logique du premier ordre ou la logique d'ordre supérieur avec des modalités. Une modalité spécifie des . Par exemple, une proposition comme « il pleut » peut être précédée d'une modalité : Il est nécessaire qu'''il pleuve ; Demain, il pleut ; Christophe Colomb croit quil pleut ; Il est démontré qu'''il pleut ; Il est obligatoire quil pleuve.
Logique
La logique — du grec , qui est un terme dérivé de signifiant à la fois « raison », « langage » et « raisonnement » — est, dans une première approche, l'étude de l'inférence, c'est-à-dire des règles formelles que doit respecter toute argumentation correcte. Le terme aurait été utilisé pour la première fois par Xénocrate. La logique antique se décompose d'abord en dialectique et rhétorique. Elle est depuis l'Antiquité l'une des grandes disciplines de la philosophie, avec l'éthique (philosophie morale) et la physique (science de la nature).
Vérification de modèles
thumb|308x308px|Principe du model checking. En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique.
Afficher plus

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.