Opérateur « finalement » (losange temporel) en LaTeX (\Diamond p)

Où il est utilisé

Le « finalement » temporel : \Diamond p affirme que p est vrai à un instant présent ou futur.

La logique temporelle linéaire l'écrit aussi F p (futur), et on peut le définir à partir de « jusqu'à » par \Diamond p \equiv \top\,\mathcal{U}\,p. Les propriétés de vivacité ont typiquement cette forme, comme \Box(\mathit{req} \to \Diamond\mathit{grant}). \Diamond\Box p signifie que p finit par être vrai pour toujours. En logique modale aléthique, le même losange signifie « possiblement » : précisez donc la lecture temporelle. Utilisez \Diamond et non \diamond, qui est un opérateur binaire plus petit. En logique arborescente (CTL), il est préfixé d'un quantificateur de chemin, comme dans AF p ou EF p.

Exemple minimal compilable

Collez-le dans un fichier .tex vide et compilez avec pdfLaTeX, XeLaTeX ou LuaLaTeX.

\documentclass{article}
\usepackage{amssymb}
\begin{document}
Eventually (temporal diamond): $\Diamond p$

\[ \Diamond \Box p \to \Box \Diamond p \]
\end{document}

Symboles associés

• Opérateur « jusqu'à » (until)p \mathcal{U} q
• Opérateur « toujours » (boîte temporelle)\Box p
• Opérateur « suivant » (next)\bigcirc p
• Connaissance communeC_G p
• Relation d'accessibilitéw R v
• Opérateur de croyanceB_a p

Questions fréquentes

Comment écrire Opérateur « finalement » (losange temporel) en LaTeX ?

Tapez \Diamond p en mode mathématique, par exemple $\Diamond \Box p \to \Box \Diamond p$. Chargez d’abord amssymb avec \usepackage{amssymb}.

Quel paquet faut-il pour \Diamond p ?

\Diamond p nécessite amssymb : ajoutez \usepackage{amssymb} au préambule avant le début du document.

Peut-on utiliser \Diamond p en mode texte, ou seulement en mode mathématique ?

Seulement en mode mathématique. Hors de $...$, LaTeX s’arrête avec "Missing $ inserted" : dans le texte, écrivez $\Diamond p$.