Opérateur « toujours » (boîte temporelle) en LaTeX (\Box p)

Où il est utilisé

Le « toujours » temporel : \Box p affirme que p est vrai maintenant et à chaque instant futur de l'exécution.

En logique temporelle linéaire, \Box s'écrit souvent G (globalement), et les propriétés de sûreté prennent la forme \Box\neg\mathit{bad}. Il est dual de « finalement », \Box p \leftrightarrow \neg\Diamond\neg p, et \Box\Diamond p exprime que p se produit infiniment souvent. La même boîte désigne la nécessité en logique modale aléthique : précisez donc quelle lecture s'applique. \Box et \square donnent des carrés presque identiques ; \Box est l'opérateur modal conventionnel, et aucune espace n'est ajoutée automatiquement avant p. CTL le préfixe d'un quantificateur de chemin, comme dans AG p.

Exemple minimal compilable

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

\documentclass{article}
\usepackage{amssymb}
\begin{document}
Always (temporal box): $\Box p$

\[ \Box(\mathit{req} \to \Diamond \mathit{grant}) \]
\end{document}

Symboles associés

• Opérateur « finalement » (losange temporel)\Diamond p
• Connaissance communeC_G p
• Opérateur « jusqu'à » (until)p \mathcal{U} q
• Opérateur de croyanceB_a p
• Opérateur « suivant » (next)\bigcirc p
• Opérateur de connaissanceK_a p

Questions fréquentes

Comment écrire Opérateur « toujours » (boîte temporelle) en LaTeX ?

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

Quel paquet faut-il pour \Box p ?

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

Peut-on utiliser \Box 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 $\Box p$.