blob: 0f84a4e138bb0eedaa00ef5d25d00439084a11cb (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
\subsubsection{Specifying Properties}
% TODO Once operator
\camil
\begin{remark}[Other Notations]
% TODO: I don't find this place logical for this remark, but it is the same place as Remark 5.16 in the book.
Like for LTL, many different notations are used in literature for PLTL.
These include
$\mathbf X^{-1}, \mathbf G^{-1}, \mathbf F^{-1}$~\citep[e.g.]{Markey2003},
but also \raisebox{-1pt}{\tikz\draw[black,fill=black](0,0)circle(.4em);}$,\blacksquare,\blacklozenge$~\citep[e.g.]{Gabbay1989}
or $\stackinset{c}{}{c}{}{$\cdot$}{$\bigcirc$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep[e.g.]{Havelund2002}.
% It is always fun to come up with new versions and watch people struggling to reproduce them in \LaTeX.
\end{remark}
|
