Operatore temporale "sempre" in LaTeX (\Box p)

Dove si usa

"Sempre" temporale: \Box p afferma che p vale ora e in ogni istante futuro dell'esecuzione.

Nella logica temporale lineare \Box si scrive spesso G (globalmente), e le proprietà di safety hanno la forma \Box\neg\mathit{bad}. È il duale di "prima o poi", \Box p \leftrightarrow \neg\Diamond\neg p, e \Box\Diamond p esprime che p si verifica infinitamente spesso. Lo stesso quadrato indica la necessità nella logica modale aletica, quindi specificate quale lettura si applica. \Box e \square danno quadrati quasi identici; \Box è l'operatore modale convenzionale e lo spazio prima di p non viene aggiunto automaticamente. CTL lo fa precedere da un quantificatore di cammino, come in AG p.

Esempio minimo compilabile

Incollalo in un file .tex vuoto e compilalo con pdfLaTeX, XeLaTeX o LuaLaTeX.

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

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

Simboli correlati

• Operatore temporale "prima o poi"\Diamond p
• Conoscenza comuneC_G p
• Operatore untilp \mathcal{U} q
• Operatore di credenzaB_a p
• Operatore next\bigcirc p
• Operatore di conoscenzaK_a p

Domande frequenti

Come si scrive Operatore temporale "sempre" in LaTeX?

Scrivi \Box p in modalità matematica, per esempio $\Box(\mathit{req} \to \Diamond \mathit{grant})$. Carica prima amssymb con \usepackage{amssymb}.

Quale pacchetto serve per \Box p?

\Box p richiede amssymb: aggiungi \usepackage{amssymb} al preambolo prima dell'inizio del documento.

Posso usare \Box p in modalità testo o solo in modalità matematica?

Solo in modalità matematica. Fuori da $...$ LaTeX si ferma con "Missing $ inserted", quindi nel testo scrivi $\Box p$.