alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* doc/tl/tl.tex: Refine note about {r} vs. r in PSL.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2015-08-19 14:20:17 +02:00
parent c5541a2189
commit 8a3a07d8a4
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
doc/tl/tl.tex
View file

@ -869,10 +869,10 @@ is not a model of \samp{$\sere{a\PLUS{}\CONCAT\NOT
Note that the semantics of $\sere{r}$ comes from the
$\mathsf{cl}(\cdot)$ operator defined by~\citet{dax.09.atva}. This
differs from the interpretation of a SERE in the context of a temporal
formula given by the PSL standard~\citep[Appendix~B.3.1.1.2,
item~7]{psl.04.lrm}: the $\mathit{cl}(\cdot)$ semantics accepts more
words.
differs from the interpretation of a SERE $r$ in the context of a
temporal formula given by the PSL standard~\citep[Appendix~B.3.1.1.2,
item~7]{psl.04.lrm}: the $\sere{r}$ semantics used here corresponds to
$r!\lor r$ in the PSL standard.
\subsection{Syntactic Sugar}\label{sec:pslsugar}