Logique temporelle

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.

Publications associées (10)

Personnes associées (6)

Concepts associés (25)

Cours associés (4)

Séances de cours associées (29)

Robust Articulated-ICP for Real-Time Hand Tracking

Mark Pauly, Sofien Bouaziz, Andrea Tagliasacchi, Anastasia Tkach

We present a robust method for capturing articulated hand motions in realtime using a single depth camera. Our system is based on a realtime registration process that accurately reconstructs hand pose

Wiley-Blackwell2015

Verifying real-time systems goes beyond the verification of functional properties: it also requires the checking of real-time properties. This makes traditional contract-frameworks partially inept for

2014

A class of Neumann type systems and its application

Jinbing Chen

A class of Neumann type systems are derived separating the spatial and temporal variables for the 2+1 dimensional Caudrey-Dodd-Gibbon-Kotera-Sawada (CDGKS) equation and the modified Korteweg-de Vries

International Press2012

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).

Logique temporelle

Protocoles : Description officielle et types de séances

Couvre les protocoles, les descriptions officielles avec les types de session, les types de message et la logique linéaire.

Résoudre les jeux de parité dans la pratique

Explore les aspects pratiques de la résolution des jeux de parité, y compris les stratégies gagnantes, les algorithmes, la complexité, le déterminisme et les approches heuristiques.

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.

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

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

This course focuses on the physical mechanisms at the origin of the transition of a flow from laminar to turbulent using the hydrodynamic instability theory.