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

* doc/tl/tl.tex: Remarks from Denis Poitrenaud.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-06-04 15:43:03 +02:00
parent f620d9a231
commit 87765ca8e8
1 changed files with 34 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

61
doc/tl/tl.tex
View file

@ -208,8 +208,8 @@ sequence called the \textit{empty word} and denoted $\varepsilon$. We
denote $A^n$ the set of all sequences of length $n$ on $A$ (in denote $A^n$ the set of all sequences of length $n$ on $A$ (in
particular $A^\omega$ is the set of infinite sequences on $A$), and particular $A^\omega$ is the set of infinite sequences on $A$), and
$A^\star=\bigcup_{n\in\N}A^n$ denotes the set of all finite sequences. $A^\star=\bigcup_{n\in\N}A^n$ denotes the set of all finite sequences.
The length of $n\in\N\cup\{\omega\}$ any sequence $\sigma$ is noted The length of any sequence $\sigma$ is noted $|\sigma|$, with
$|\sigma|=n$. $|\sigma|\in\N\cup\{\omega\}$.
For any sequence $\sigma$, we denote $\sigma^{i..j}$ the finite For any sequence $\sigma$, we denote $\sigma^{i..j}$ the finite
subsequence built using letters from $\sigma(i)$ to $\sigma(j)$. If subsequence built using letters from $\sigma(i)$ to $\sigma(j)$. If
@ -221,7 +221,7 @@ starting at letter $\sigma(i)$.
The temporal formul\ae{} described in this document, should be The temporal formul\ae{} described in this document, should be
interpreted on behaviors (or executions, or scenarios) of the system interpreted on behaviors (or executions, or scenarios) of the system
to verify. In model checking we want to ensure that a formula (the to verify. In model checking we want to ensure that a formula (the
property to verify) holds on all possibles behaviors of the system. property to verify) holds on all possible behaviors of the system.
If we model the system as some sort of giant automaton (e.g., a Kripke If we model the system as some sort of giant automaton (e.g., a Kripke
structure) where each state represent a configuration of the system, a structure) where each state represent a configuration of the system, a
@ -246,7 +246,7 @@ model of $\varphi$).
When a formula $\varphi$ holds on an \emph{finite} sequence $\sigma$, When a formula $\varphi$ holds on an \emph{finite} sequence $\sigma$,
we write $\sigma \VDash \varphi$. we write $\sigma \VDash \varphi$.
\chapter{Temporal Syntax} \chapter{Temporal Syntax \& Semantics}
\section{Boolean Constants}\label{sec:bool} \section{Boolean Constants}\label{sec:bool}
@ -326,8 +326,8 @@ double quotes to avoid any unintended misinterpretation.
\begin{itemize} \begin{itemize}
\item \samp{"a<=b+c"} is an atomic proposition. Double quotes can \item \samp{"a<=b+c"} is an atomic proposition. Double quotes can
therefore be used to embed language-specific constructs into an therefore be used to embed constructs specific to the underlying formalism,
atomic proposition. and still regard the resulting construction as an atomic proposition.
\item \samp{light\_on} is an atomic proposition. \item \samp{light\_on} is an atomic proposition.
\item \samp{Fab} is not an atomic proposition, this is actually \item \samp{Fab} is not an atomic proposition, this is actually
equivalent to the formula \samp{F(ab)} where the temporal operator equivalent to the formula \samp{F(ab)} where the temporal operator
@ -388,21 +388,26 @@ and the above operators, we say that the formula is a \emph{Boolean
\subsection{Semantics} \subsection{Semantics}
\begin{align*} \begin{align*}
\NOT f\vDash \sigma &\iff (f\nvDash\sigma) \\ \sigma\vDash \NOT f &\iff (\sigma\nvDash f) \\
f\AND g\vDash \sigma &\iff (f\vDash\sigma)\land(g\vDash\sigma) \\ \sigma\vDash f\AND g &\iff (\sigma\vDash f)\land(\sigma\vDash g) \\
f\OR g\vDash \sigma &\iff (f\vDash\sigma)\lor(g\vDash\sigma) \\ \sigma\vDash f\OR g &\iff (\sigma\vDash f)\lor(\sigma\vDash g) \\
f\IMPLIES g\vDash \sigma &\iff \sigma\vDash f\IMPLIES g &\iff
(f\nvDash\sigma)\lor(g\vDash\sigma)\\ (\sigma\nvDash f)\lor(\sigma\vDash g)\\
f\XOR g\vDash \sigma &\iff \sigma\vDash f\XOR g &\iff
((f\vDash\sigma)\land(g\nvDash\sigma))\lor ((\sigma\vDash f)\land(\sigma\nvDash g))\lor
((f\nvDash\sigma)\land(g\vDash\sigma))\\ ((\sigma\nvDash f)\land(\sigma\vDash g))\\
f\EQUIV g\vDash \sigma &\iff \sigma\vDash f\EQUIV g &\iff
((f\vDash\sigma)\land(g\vDash\sigma))\lor ((\sigma\vDash f)\land(\sigma\vDash g))\lor
((f\nvDash\sigma)\land(g\nvDash\sigma)) ((\sigma\nvDash f)\land(\sigma\nvDash g))
\end{align*} \end{align*}
\subsection{Trivial Identities (Occur Automatically)} \subsection{Trivial Identities (Occur Automatically)}
Trivial identities are applied every time an expression is
constructed. This means for instance that there is not way to
construct the expression \samp{$\NOT\NOT a$} in Spot, such an attempt
will always yield the expression \samp{$a$}.
% These first rules are for the \samp{!} and \samp{->} operators. % These first rules are for the \samp{!} and \samp{->} operators.
\begin{align*} \begin{align*}
@ -480,12 +485,12 @@ temporal operators can be used to construct another temporal formula.
\subsection{Semantics}\label{sec:opltl:sem} \subsection{Semantics}\label{sec:opltl:sem}
\begin{align*} \begin{align*}
\sigma\vDash \X f &\iff f\vDash \sigma^{1..}\\ \sigma\vDash \X f &\iff \sigma^{1..}\vDash f\\
\sigma\vDash \F f &\iff \exists i\in \N,\, \sigma^{i..}\vDash f\\ \sigma\vDash \F f &\iff \exists i\in \N,\, \sigma^{i..}\vDash f\\
\sigma\vDash \G f &\iff \forall i\in \N,\, \sigma^{i..}\vDash f\\ \sigma\vDash \G f &\iff \forall i\in \N,\, \sigma^{i..}\vDash f\\
\sigma\vDash f\U g &\iff \exists j\in\N,\, \sigma\vDash f\U g &\iff \exists j\in\N,\,
\begin{cases} \begin{cases}
\forall i<j,\, f\vDash \sigma^{i..}\\ \forall i<j,\, \sigma^{i..}\vDash f\\
\sigma^{j..} \vDash g\\ \sigma^{j..} \vDash g\\
\end{cases}\\ \end{cases}\\
\sigma \vDash f\W g &\iff (\sigma\vDash f\U g)\lor(\sigma\vDash\G f)\\ \sigma \vDash f\W g &\iff (\sigma\vDash f\U g)\lor(\sigma\vDash\G f)\\
@ -497,10 +502,10 @@ temporal operators can be used to construct another temporal formula.
\sigma \vDash f\R g &\iff (\sigma \vDash f\M g)\lor(\sigma\vDash \G g) \sigma \vDash f\R g &\iff (\sigma \vDash f\M g)\lor(\sigma\vDash \G g)
\end{align*} \end{align*}
Appendix~\ref{sec:ltl-equiv} explains how to rewrite all LTL operators Appendix~\ref{sec:ltl-equiv} explains how to rewrite the above LTL
using only $\X$ and one operated chosen among $\U$, $\W$, $\M$,and operators using only $\X$ and one operator chosen among $\U$, $\W$,
$\R$. This could be useful to understand the operators $\R$, $\M$, $\M$,and $\R$. This could be useful to understand the operators $\R$,
and $\W$ if you are only familiar with $\X$ and $\U$. $\M$, and $\W$ if you are only familiar with $\X$ and $\U$.
\subsection{Trivial Identities (Occur Automatically)} \subsection{Trivial Identities (Occur Automatically)}
@ -567,7 +572,7 @@ intersection `$\ANDALT$', and fusion `$\FUSION$'.
Any Boolean formula (section~\ref{def:boolform}) is a SERE. SERE can Any Boolean formula (section~\ref{def:boolform}) is a SERE. SERE can
be further combined with the following operators, where $f$ and $g$ be further combined with the following operators, where $f$ and $g$
denote arbitrary SERE and $b$ denotes a Boolean formula. denote arbitrary SERE.
\begin{center} \begin{center}
\begin{tabular}{cccccrl} \begin{tabular}{cccccrl}
@ -602,12 +607,14 @@ instance `$a\STAR{i,\texttt{\$}}$', `$a\STAR{i\texttt{:inf}}$' and
\subsection{Semantics} \subsection{Semantics}
The following semantics assume that $f$ and $g$ are two SEREs, while The following semantics assume that $f$ and $g$ are two SEREs, while
$b$ is a Boolean formula. $a$ is an atomic proposition.
{\allowdisplaybreaks {\allowdisplaybreaks
\begin{align*} \begin{align*}
\sigma\VDash \eword & \iff |\sigma| = 0 \\ \sigma\nVDash \0 &\\
\sigma\VDash a & \iff \sigma(0)(a) = 1 \\ \sigma\VDash \1 & \iff |\sigma|=1\\
\sigma\VDash \eword & \iff |\sigma|=0 \\
\sigma\VDash a & \iff \sigma(0)(a)=1 \land |\sigma|=1\\
\sigma\VDash f\OR g &\iff (\sigma\VDash f) \lor (\sigma\VDash g) \\ \sigma\VDash f\OR g &\iff (\sigma\VDash f) \lor (\sigma\VDash g) \\
\sigma\VDash f\ANDALT g &\iff (\sigma \VDash f) \land (\sigma\VDash g) \\ \sigma\VDash f\ANDALT g &\iff (\sigma \VDash f) \land (\sigma\VDash g) \\
\sigma\VDash f\AND g &\iff \exists k\in\N,\, \sigma\VDash f\AND g &\iff \exists k\in\N,\,