* doc/tl/tl.tex: More text for the temporal hierarchy.
This commit is contained in:
Alexandre Duret-Lutz
parent
dc5a0620b7
commit
2c37367075
1 changed files with 91 additions and 15 deletions
106
doc/tl/tl.tex
106
doc/tl/tl.tex
|
|
@ -16,6 +16,13 @@
|
|||
\usepackage{tabulary}
|
||||
\usepackage[numbers]{natbib}
|
||||
\usepackage{rotating}
|
||||
\usepackage{tikz}
|
||||
\usetikzlibrary{backgrounds}
|
||||
\usetikzlibrary{shadows}
|
||||
\usetikzlibrary{arrows}
|
||||
\pgfdeclarelayer{background}
|
||||
\pgfdeclarelayer{foreground}
|
||||
\pgfsetlayers{background,main,foreground}
|
||||
|
||||
% TODO
|
||||
\usepackage{todonotes}
|
||||
|
|
@ -115,6 +122,10 @@
|
|||
\makeindex
|
||||
\newcommand{\Index}[1]{\index{#1}#1}
|
||||
|
||||
% Tikz
|
||||
\tikzstyle{annote}=[overlay,thick,<-,red,>=stealth']
|
||||
|
||||
|
||||
% Make sure we can compile this file even without use the version
|
||||
% supplied by the Makefile.
|
||||
\ifdefined\SpotVersion\else
|
||||
|
|
@ -959,6 +970,7 @@ properties can be queried from any \texttt{spot::ltl::formula}
|
|||
instance using the following methods:
|
||||
|
||||
\noindent
|
||||
\label{property-methods}
|
||||
\begin{tabulary}{\textwidth}{lL}
|
||||
\texttt{is\_boolean()}& Whether the formula uses only Boolean
|
||||
operators.
|
||||
|
|
@ -1057,44 +1069,101 @@ rules:
|
|||
\mid \0 \R \varphi
|
||||
\mid \varphi_U\W \varphi_U
|
||||
\mid \varphi \W \0
|
||||
\mid \varphi_U\M \varphi_U\\
|
||||
\mid \varphi_U\M \varphi_U
|
||||
\end{align*}
|
||||
|
||||
\section{Syntactic Hierarchy Classes}
|
||||
|
||||
\begin{figure}[tbp]
|
||||
\centering
|
||||
\begin{tikzpicture}
|
||||
\draw[drop shadow,fill=white] (0,0) rectangle (6,7);
|
||||
\path[fill=yellow!20] (0,6) -- (3,4.5) -- (0,3);
|
||||
\path[fill=red!20] (6,6) -- (3,4.5) -- (6,3);
|
||||
\path[fill=orange!20] (0,3) -- (3,4.5) -- (6,3) -- (3,1);
|
||||
\path[fill=blue!40,fill opacity=.5] (0,0) -- (0,3) -- (4.5,0);
|
||||
\path[fill=green!40,fill opacity=.5] (6,0) -- (1.5,0) -- (6,3);
|
||||
\draw (0,0) rectangle (6,7);
|
||||
|
||||
\node[align=center] (rea) at (3,6) {Reactivity\\ $\bigwedge\G\F p_i\lor \F\G q_i$};
|
||||
\node[align=center] (rec) at (1,4.5) {Recurrence\\ $\G\F p$};
|
||||
\node[align=center] (per) at (5,4.5) {Persistence\\ $\F\G p$};
|
||||
\node[align=center] (obl) at (3,2.85) {Obligation\\ $\bigwedge\G p_i\lor \F q_i$};
|
||||
\node[align=center] (saf) at (1,1) {Safety\\ $\G p$};
|
||||
\node[align=center] (gua) at (5,1) {Guarantee\\ $\F p$};
|
||||
|
||||
\node[align=center,below left] (det) at (-.2,6.7) {Deterministic\\Büchi Automata};
|
||||
\node[align=center,below right](weak) at (6.2,6.7) {Weak Büchi\\Automata};
|
||||
\node[align=center,right](wdba) at (6.2,4.3) {Weak Deteterministic\\Büchi Automata};
|
||||
\node[align=center,above right](ter) at (6.2,2) {Terminal\\Büchi Automata};
|
||||
\node[align=center,above left](occ) at (-.2,2) {Terminal\\co-Büchi Automata};
|
||||
|
||||
\node[above right] (buc) at (3.35,7) {General Büchi Automata};
|
||||
|
||||
\draw[annote] (rec) -- (det);
|
||||
\draw[annote] (per) -- (weak);
|
||||
\draw[annote] (obl.east) -- (wdba);
|
||||
\draw[annote] (gua) -- (ter);
|
||||
\draw[annote] (saf) -- (occ);
|
||||
\draw[annote] (rea.north) .. controls +(north:5mm) and +(west:5mm) .. (buc.west);
|
||||
\end{tikzpicture}
|
||||
\caption{The temporal hierarchy of \citet{manna.87.podc} with their
|
||||
associated classes of automata~\citep{cerna.03.mfcs}. The
|
||||
formul\ae{} associated to each class are more than canonical
|
||||
examples: they show the normal forms under which any LTL formula of
|
||||
the class can be rewritten, assuming that $p,p_i,q,q_i$ denote
|
||||
subformul\ae{} involving only Boolean operators, $\X$, and past
|
||||
temporal operators (Spot does not support the
|
||||
latter). \label{fig:hierarchy}}
|
||||
\end{figure}
|
||||
|
||||
The hierarchy of linear temporal properties was introduced
|
||||
by~\citet{manna.87.podc}. A first syntactic characterization of the
|
||||
classes was presented by~\citet{chang.92.icalp}, but other
|
||||
presentations have been done including negation~\citep{cerna.03.mfcs}
|
||||
and weak until~\citep{schneider.01.lpar}.
|
||||
by~\citet{manna.87.podc} and is illustrated on
|
||||
Fig.~\ref{fig:hierarchy}. In the case of the LTL subset of the
|
||||
hierarchy, a first syntactic characterization of the classes was
|
||||
presented by~\citet{chang.92.icalp}, but other presentations have been
|
||||
done including negation~\citep{cerna.03.mfcs} and weak
|
||||
until~\citep{schneider.01.lpar}.
|
||||
|
||||
In the following grammar rules, the symbols $\varphi_G$, $\varphi_S$,
|
||||
$\varphi_O$, $\varphi_P$, $\varphi_R$ designate any formula belonging
|
||||
respectively to the Guarantee, Safety, Obligation, Persistence, or
|
||||
Recurrence classes. $v$ designates any variable, $r$ any SERE, $r_F$
|
||||
a bounded SERE (no loops), and $r_I$ an unbounded SERE.
|
||||
The following grammar rules describes extend the aforementioned
|
||||
work slightly by dealing with PSL operators. These are the
|
||||
rules used by Spot to decide upon
|
||||
construction to which class a formula belongs (see the methods
|
||||
\texttt{is\_syntactic\_safety()}, \texttt{is\_syntactic\_guaranty()},
|
||||
\texttt{is\_syntactic\_obligation()},
|
||||
\texttt{is\_syntactic\_recurrence()}, and
|
||||
\texttt{is\_syntactic\_persistence()} listed on
|
||||
page~\pageref{property-methods}).
|
||||
|
||||
The symbols $\varphi_G$, $\varphi_S$, $\varphi_O$, $\varphi_P$,
|
||||
$\varphi_R$ designate any formula belonging respectively to the
|
||||
Guarantee, Safety, Obligation, Persistence, or Recurrence classes.
|
||||
$v$ denotes any variable, $r$ any SERE, $r_F$ any bounded SERE (no
|
||||
loops), and $r_I$ any unbounded SERE.
|
||||
|
||||
\begin{align*}
|
||||
\varphi_G ::=&\, \0\mid\1\mid v\mid \NOT\varphi_S\mid
|
||||
\varphi_G\AND \varphi_G\mid (\varphi_G\OR \varphi_G)\mid
|
||||
\X\varphi_G \mid \F\varphi_G\mid
|
||||
\varphi_G\U\varphi_G\mid \varphi_G\M\varphi_G\\
|
||||
\mid&\, \sere{r}\Esuffix \varphi_G\mid
|
||||
\sere{r_F}\Asuffix \varphi_G\\
|
||||
\mid&\, \sere{r_F}\mid
|
||||
\sere{r}\Esuffix \varphi_G\mid
|
||||
\sere{r_F}\Asuffix \varphi_G \\
|
||||
\varphi_S ::=&\, \0\mid\1\mid v\mid \NOT\varphi_G\mid
|
||||
\varphi_S\AND \varphi_S\mid (\varphi_S\OR \varphi_S)\mid
|
||||
\X\varphi_S \mid \G\varphi_S\mid
|
||||
\varphi_S\R\varphi_S\mid \varphi_S\W\varphi_S\\
|
||||
\mid&\, \sere{r_F}\Esuffix \varphi_S\mid
|
||||
\mid&\, \nsere{r_F}\mid
|
||||
\sere{r_F}\Esuffix \varphi_S\mid
|
||||
\sere{r}\Asuffix \varphi_S\\
|
||||
\varphi_O ::=&\, \varphi_G \mid \varphi_S\mid \NOT\varphi_O\mid
|
||||
\varphi_O\AND \varphi_O\mid (\varphi_O\OR \varphi_O)\mid
|
||||
\X\varphi_O \mid
|
||||
\varphi_O\U\varphi_G\mid\varphi_O\R\varphi_S \mid
|
||||
\varphi_S\W\varphi_O\mid \varphi_G\M\varphi_O\\
|
||||
\mid&\, \sere{r_F}\Esuffix \varphi_O \mid \sere{r_I}\Esuffix \varphi_G\mid
|
||||
\sere{r_F}\Asuffix \varphi_O\mid
|
||||
\mid&\, \sere{r} \mid \nsere{r}\mid
|
||||
\sere{r_F}\Esuffix \varphi_O \mid \sere{r_I}\Esuffix \varphi_G\mid
|
||||
\sere{r_F}\Asuffix \varphi_O\mid
|
||||
\sere{r_I}\Asuffix \varphi_S\\
|
||||
\varphi_P ::=&\, \varphi_O \mid \NOT\varphi_R\mid
|
||||
\varphi_P\AND \varphi_P\mid (\varphi_P\OR \varphi_P)\mid
|
||||
|
|
@ -1112,6 +1181,13 @@ a bounded SERE (no loops), and $r_I$ an unbounded SERE.
|
|||
\mid&\, \sere{r_F}\Esuffix \varphi_R \mid \sere{r_I}\Esuffix \varphi_G\mid \sere{r}\Asuffix \varphi_P\\
|
||||
\end{align*}
|
||||
|
||||
It should be noted that a formula can belong to a class of the
|
||||
temporal hierarchy even if it does not syntactically appears so. For
|
||||
instance the formula $(\G(q\OR \F\G p)\AND \G(r\OR \F\G\NOT p))\OR\G
|
||||
q\OR \G r$ is not syntactically safe, yet it is a safety formula
|
||||
equivalent to $\G q\OR \G r$. Such a formula is usually said
|
||||
\emph{pathologically safe}.
|
||||
|
||||
\chapter{Rewritings}
|
||||
|
||||
The LTL rewritings described in this section are all implemented in
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue