Operatore until in LaTeX (p \mathcal{U} q)

Dove si usa

Operatore until della logica temporale: p \mathcal{U} q vale se q prima o poi vale e p vale in ogni istante precedente.

L'until forte richiede che q si verifichi; l'until debole p \mathcal{W} q ammette anche che p valga per sempre. "Prima o poi" si ricava come \Diamond q \equiv \top \mathcal{U} q. Scritto semplicemente, \mathcal{U} è un simbolo ordinario, quindi p\mathcal{U}q viene composto senza spazio attorno alla U; racchiudetelo come p \mathbin{\mathcal{U}} q per ottenere la spaziatura da operatore binario, oppure definite \newcommand{\until}{\mathbin{\mathcal{U}}}. Molti articoli di LTL usano invece una U in tondo, \mathbin{\mathsf{U}}, al posto della lettera calligrafica. Le logiche del passato aggiungono since, la sua immagine speculare rivolta all'indietro.

Esempio minimo compilabile

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

\documentclass{article}
\usepackage{amssymb}
\begin{document}
Until: $p \mathcal{U} q$

\[ \Diamond q \leftrightarrow \top \mathbin{\mathcal{U}} q \]
\end{document}

Simboli correlati

• Operatore next\bigcirc p
• Operatore temporale "prima o poi"\Diamond p
• Relazione di accessibilitàw R v
• Operatore temporale "sempre"\Box p
• Modello di Kripke\mathcal{M}, w \models p
• Conoscenza comuneC_G p

Domande frequenti

Come si scrive Operatore until in LaTeX?

Scrivi p \mathcal{U} q in modalità matematica, per esempio $\Diamond q \leftrightarrow \top \mathbin{\mathcal{U}} q$. Funziona in LaTeX standard senza caricare alcun pacchetto.

Quale pacchetto serve per p \mathcal{U} q?

Nessuno. p \mathcal{U} q fa parte di LaTeX standard, quindi compila con la sola classe del documento nel preambolo.

Posso usare p \mathcal{U} q in modalità testo o solo in modalità matematica?

Solo in modalità matematica. Fuori da $...$ LaTeX si ferma con "Missing $ inserted", quindi nel testo scrivi $p \mathcal{U} q$.