diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 9f5b676e9..3c89131a6 100644 --- a/doc/tl/tl.tex +++ b/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