diff options
Diffstat (limited to 'Assignment1/syntax.tex')
| -rw-r--r-- | Assignment1/syntax.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 833144b..81c1844 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -18,7 +18,7 @@ The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2 \[ \phi ::= - \left.\raisebox{0pt}[5pt][5pt]{} \text{true} + \left.\raisebox{0pt}[5pt][5pt]{} \top \enspace\middle|\enspace a \enspace\middle|\enspace \phi_1 \land \phi_2 \enspace\middle|\enspace \lnot \phi @@ -32,7 +32,7 @@ The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2 \end{definition} \camil -We additionally define $\lor, \rightarrow, \leftrightarrow, \text{false}$ using this syntax as usual. +We additionally define $\lor, \rightarrow, \leftrightarrow, \bot$ using this syntax as usual. The precedence order of the operators borrowed from LTL remains the same. $\Pop$ binds equally strong as $\Xop$ and $\lnot$. @@ -48,7 +48,7 @@ In discourse, it can be helpful to distinguish different kinds of PLTL formulas. \wffp\ (pure past \wff) inductively as the smallest classes conforming to the following rules: \begin{itemize} \item - Atomic propositions and $\text{true}$ are \wffn. + Atomic propositions and $\top$ are \wffn. \item If $\phi,\psi \in \wffn \cup \wfff$, then $\phi \Uop \psi, \Xop\phi \in \wfff$. \item @@ -71,8 +71,8 @@ They can be seen as counterparts of the derived LTL modalities $\square$ and $\l \begin{definition}[Derived PLTL operators] Given $\phi \in PLTL$, then: \begin{equation*} - \Fop^{-1} \phi \defeq \top \Sop \phi \qquad - \Gop^{-1} \phi \defeq \neg \Fop^{-1} \neg \phi + \Fop^{-1} \phi \enspace\defeq\enspace \top \Sop \phi \qquad + \Gop^{-1} \phi \enspace\defeq\enspace \neg \Fop^{-1} \neg \phi \qedhere \end{equation*} \end{definition} |