\RequirePackage[l2tabu, orthodox]{nag}
\documentclass[a4paper,twoside,10pt,DIV=12,draft]{scrreprt}
\usepackage[stretch=10]{microtype}
\usepackage[american]{babel}
\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage[sc]{mathpazo}
\usepackage{hyperref}
\usepackage{url}
\usepackage{xspace}
\usepackage{dsfont}
\usepackage{mathabx}
\usepackage{showlabels}
\usepackage{chngpage}
\usepackage{tabulary}
\usepackage[numbers]{natbib}
\usepackage{rotating}

% TODO
\usepackage{todonotes}
\newcommand{\stodo}[2][]
    {\todo[caption={#2},#1]
    {\footnotesize #2}}
\newcommand{\spottodo}[2][]{\stodo[color=green!40,caption={#2},#1]{#2}}
\newcommand{\ltltodo}[2][]{\stodo[color=red!40,caption={#2},#1]{#2}}


%% ---------------------- %%
%% Mathematical symbols.  %%
%% ---------------------- %%
\newcommand{\Z}{\texorpdfstring{\ensuremath{\mathds{Z}}}{Z}}
\newcommand{\B}{\texorpdfstring{\ensuremath{\mathds{B}}}{B}}
\newcommand{\N}{\texorpdfstring{\ensuremath{\mathds{N}}}{N}}
\newcommand{\AP}{\ensuremath{\mathrm{AP}}}

\DeclareMathOperator{\F}{\texttt{F}}
\DeclareMathOperator{\FALT}{\texttt{<>}}
\DeclareMathOperator{\G}{\texttt{G}}
\DeclareMathOperator{\GALT}{\texttt{[]}}
\newcommand{\U}{\mathbin{\texttt{U}}}
\newcommand{\R}{\mathbin{\texttt{R}}}
\newcommand{\RALT}{\mathbin{\texttt{V}}}
\DeclareMathOperator{\X}{\texttt{X}}
\DeclareMathOperator{\XALT}{\texttt{()}}
\newcommand{\M}{\mathbin{\texttt{M}}}
\newcommand{\W}{\mathbin{\texttt{W}}}
\DeclareMathOperator{\NOT}{\texttt{!}}
\DeclareMathOperator{\NOTALT}{\texttt{\char`~}}
\newcommand{\XOR}{\mathbin{\texttt{xor}}}
\newcommand{\XORALT}{\mathbin{\texttt{\char`^}}}
\newcommand{\IMPLIES}{\mathbin{\texttt{->}}}
\newcommand{\IMPLIESALT}{\mathbin{\texttt{=>}}}
\newcommand{\IMPLIESALTT}{\mathbin{\texttt{-->}}}
\newcommand{\EQUIV}{\mathbin{\texttt{<->}}}
\newcommand{\EQUIVALT}{\mathbin{\texttt{<=>}}}
\newcommand{\EQUIVALTT}{\mathbin{\texttt{<-->}}}
\newcommand{\OR}{\mathbin{\texttt{|}}}
\newcommand{\ORALT}{\mathbin{\texttt{||}}}
\newcommand{\ORALTT}{\mathbin{\texttt{\char`\\/}}}
\newcommand{\AND}{\mathbin{\texttt{\&}}}
\newcommand{\ANDALT}{\mathbin{\texttt{\&\&}}}
\newcommand{\ANDALTT}{\mathbin{\texttt{/\char`\\}}}
\newcommand{\FUSION}{\mathbin{\texttt{:}}}
\newcommand{\CONCAT}{\mathbin{\texttt{;}}}
\newcommand{\0}{\texttt{0}}
\newcommand{\1}{\texttt{1}}
\newcommand{\STAR}[1]{\texttt{[*#1]}}
\newcommand{\STARALT}{\texttt{*}}
\newcommand{\EQUAL}[1]{\texttt{[=#1]}}
\newcommand{\GOTO}[1]{\texttt{[->#1]}}
\newcommand{\PLUS}{\texttt{[+]}}
\newcommand{\eword}{\texttt{[*0]}}

\newcommand{\Esuffix}{\texttt{<>->}}
\newcommand{\EsuffixMarked}{\texttt{<>+>}}
\newcommand{\Asuffix}{\texttt{[]->}}
\newcommand{\AsuffixALT}{\texttt{|->}}
\newcommand{\EsuffixEQ}{\texttt{<>=>}}
\newcommand{\AsuffixEQ}{\texttt{[]=>}}
\newcommand{\AsuffixALTEQ}{\texttt{|=>}}

\newcommand{\ratgroup}[1]{\texttt{\{}#1\texttt{\}}}
\newcommand{\nratgroup}[1]{\texttt{!\{}#1\texttt{\}}}
\newcommand{\ratgroupn}[1]{\texttt{\{}#1\texttt{\}!}}

\def\limplies{\rightarrow}
\def\simp{\rightrightharpoons}
\def\Simp{\stackrel{+}{\simp}}
\def\liff{\leftrightarrow}

\makeatletter
\newcommand{\Cxx}{%
  \valign{\vfil\hbox{##}\vfil\cr
    {C\kern-.1em}\cr
    $\hbox{\fontsize\sf@size\z@\textbf{+\kern-0.05em+}}$\cr}%
    \xspace
}
\makeatother

\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{%
           \llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{%
           \rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{%
           \clap{$\mathsurround=0pt#1{#2}$}}

% The same argument is output and put in the index.
\usepackage{makeidx}
\makeindex
\newcommand{\Index}[1]{\index{#1}#1}

% Make sure we can compile this file even without use the version
% supplied by the Makefile.
\ifdefined\SpotVersion\else
 \def\SpotVersion{\textbf{UNKNOWN VERSION}}
\fi

%% ----------------------- %%
%% Texinfo like commands.  %%
%% ----------------------- %%

\newcommand\file[1]{`\texttt{#1}'}
\newcommand\command[1]{\texttt{#1}}
\newcommand\var[1]{{\ttfamily\itshape #1}}
\newcommand\mvar[1]{\ensuremath{\mathit{#1}}}
\newcommand\code[1]{\texttt{#1}}
\newcommand\samp[1]{`\texttt{#1}'}
\newcommand\tsamp[1]{\text{\texttt{#1}}}
\newcommand\msamp[1]{#1}


\def\manualtitle{Spot's Temporal Logic Formul\ae}

%% ---------- %%
%% Document.  %%
%% ---------- %%
\begin{document}

\vspace*{50pt}
\vskip4pt \hrule height 4pt width \hsize \vskip4pt
\begin{center}
  \huge \manualtitle
\end{center}
\vspace*{-1.5ex}
\vskip4pt \hrule height 4pt width \hsize \vskip4pt

\hfill Alexandre Duret-Lutz
\href{mailto:adl@lrde.epita.fr}{\nolinkurl{<adl@lrde.epita.fr>}}

\hfill compiled on \today, for Spot \SpotVersion

\vfill

\setcounter{tocdepth}{2}
\makeatletter
\@starttoc{toc}
\makeatother

\vfill

\chapter{Reasoning with Infinite Sequences}

\section{Finite and Infinite Sequences}

Let $\N=\{0,1,2,\ldots\}$ designate the set of natural numbers and
$\omega\not\in\N$ the first transfinite ordinal.  We extend the $<$
relation from $\N$ to $\N\cup\{\omega\}$ with $\forall n\in N,\,
n<\omega$.  Similarly let us extend the addition and subtraction with
$\forall n\in\N,\,\omega+n = \omega-n = \omega+\omega = \omega$.

For any set $A$, and any number $n\in\N\cup\{\omega\}$, a
\textit{sequence} of length $n$ is a function $\sigma:
\{0,1,\ldots,n-1\}\to A$ that associates each index $i<n$ to an
element $\sigma(i)\in A$.  The sequence of length $0$ is a particular
sequence called the \textit{empty word} and denoted $\varepsilon$.  We
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
$A^\star=\cup_{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
$|\sigma|=n$.

For any set $A$, we note $E^\star$ the set of finite sequence
built by concatenating elements of $E$, and $E^\omega$ is set of
infinite sequence over $E$.

For any sequence $\sigma$, we denote $\sigma^{i..j}$ the finite
subsequence built using letters from $\sigma(i)$ to $\sigma(j)$.  If
$\sigma$ is infinite, we denote $\sigma^{i..}$ the suffix of $\sigma$
starting at letter $\sigma(i)$.

\section{Usage in Model Checking}

The temporal formul\ae{} described in this document, and used by Spot,
should be interpreted on a behavior (or an execution) of the system to
verify.  The idea of model checking is that we want to ensure that a
formula (the property to verify) holds on all possibles behaviors of
the system.

In this document we will describe the syntax of the temporal
formul\ae{} used in Spot, and give their interpretation on an infinite
sequence.

If we model the system as some sort of giant automaton, where each
state represent a configuration of the system, a behavior of the
system can be represented by an infinite sequence of configurations.
Each configuration can be described as an affectation of some
proposition variables that we will call atomic propositions.  For
instance $r=1,y=0,g=0$ describes the configuration of a traffic light
with only the red light turned on.

Let $\AP$ be a set of atomic propositions, for instance
$\AP=\{r,y,g\}$.  A configuration of the model is a function
$\rho:\AP\to\B$ (or $\rho\in\B^\AP$) that associates a truth value
($\B=\{0,1\}$) to each atomic proposition.

A behavior of the model is an infinite sequence $\sigma$ of such
configurations.  In other words: $\sigma\in(\B^\AP)^\omega$.

When a formula $\varphi$ holds on an \emph{infinite} sequence $\sigma$, we
will write $\sigma \vDash \varphi$ (read as $\sigma$ is a model of
$\varphi$).

When a formula $\varphi$ holds on an \emph{finite} sequence $\sigma$, we
will write $\sigma \VDash \varphi$.

\chapter{Temporal Syntax}

\section{Boolean Constants}\label{sec:bool}

The two Boolean constants are \samp{1} and \samp{0}.  They can also be
input as \samp{true} or \samp{false} (case insensitive) for
compatibility with the output of other tools, but Spot will always use
\samp{1} and \samp{0} in its output.

\subsection{Semantics}

\begin{align*}
  \sigma &\nvDash \0 \\
  \sigma &\vDash \1 \\
\end{align*}

\section{Atomic Propositions}\label{sec:ap}

Atomic propositions in Spot are strings of characters.  There are no
restrictions on the characters that appear in the strings, however
because some of the characters may also be used to denote operators
you may have to represent the strings differently if they include
these characters.

\begin{enumerate}
\item Any string of characters represented between double quotes is an
  atomic proposition.
\item Any sequence of alphanumeric characters \label{rule:ap2}
  (including \samp{\_}) that is not a reserved keyword and that starts
  with a characters that is not an uppercase \samp{F}, \samp{G}, or
  \samp{X}, is also an atomic proposition.  In this case the double
  quotes are not necessary.
\item \label{rule:ap3} Any sequence of alphanumeric character that
  starts with \samp{F}, \samp{G}, or \samp{X}, has a digit in second
  position, and anything afterwards, is also an atomic propositions,
  and the double quotes are not necessary.
\end{enumerate}

Here is the list of reserved keywords:
\begin{itemize}
\item \samp{true}, \samp{false}  (both are case insensitive)
\item \samp{F}, \samp{G}, \samp{M}, \samp{R}, \samp{U}, \samp{V},
  \samp{W}, \samp{X}, \samp{xor}
\end{itemize}

The only way to use an atomic proposition that has the name of a
reserved keyword, or one that starts with a digit, is to use double quotes.

The reason we deal with leading \samp{F}, \samp{G}, and \samp{X}
specifically in rule~\ref{rule:ap2} is that these are unary LTL
operators and we want to be able to write compact formul\ae{} like
$\samp{GFa}$ instead of the equivalent \samp{G(F(a))} or
\samp{G~F~a}.  If you want to name an atomic proposition \samp{GFa},
you will have to quote it as \samp{"GFa"}.

The exception done by rule~\ref{rule:ap3} when these letters are
followed by a digit is meant to allow \samp{X0}, \samp{X1}, \samp{X2},
\dots to be used as atomic propositions.  With only
rule~\ref{rule:ap2}, \samp{X0} would be interpreted as \samp{X(0)},
that is, the LTL operator $\X$ applied to the constant \textit{false},
but there is really little reason to use such a construction in a
formula (the same is true for \samp{F} and \samp{G}, and also when
applied to \samp{1}).  On the other hand, having numbered versions of
a variable is pretty common, so it makes sense to favor this
interpretation.

If you are typing in formul\ae{} by hand, we suggest you name all your
atomic propositions in lower case, to avoid clashes with the uppercase
operators.

If you are writing a tool that produces formula that will be feed to
Spot and if you cannot control the atomic propositions that will be
used, we suggest that you always output atomic propositions between
double quotes to avoid any unintended misinterpretation.


\subsection{Examples}

\begin{itemize}
\item \samp{"a<=b+c"} is an atomic proposition.  Double quotes can
  therefore be used to embed language-specific constructs into an
  atomic proposition.
\item \samp{light\_on} is an atomic proposition.
\item \samp{Fab} is not an atomic proposition, this is actually
  equivalent to the formula \samp{F(ab)} where the temporal operator
  $\F$ is applied to the atomic proposition \samp{ab}.
\item \samp{FINISHED} is not an atomic proposition for the same
  reason; it actually stands for \samp{F(INISHED)}
\item \samp{F100ZX} is an atomic proposition by rule~\ref{rule:ap3}.
\item \samp{FX100} is not an atomic proposition, it is equivalent to the
  formula \samp{F(X100)}, where \samp{X100} is an atomic proposition
  by rule~\ref{rule:ap3}.
\end{itemize}

\subsection{Semantics}

For any atomic proposition $a$, we have
\begin{align*}
  \sigma \vDash a \iff \sigma(0)(a) = 1
\end{align*}
In other words $a$ holds if and only if it is true in the first
configuration of $\sigma$.

\section{Boolean Operators (for Temporal Formul\ae{})}\label{sec:boolops}

Two temporal formul\ae{} $f$ and $g$ can be combined using the
following Boolean operators:

\begin{center}
\begin{tabular}{cccc}
              & preferred & \multicolumn{2}{c}{other supported} \\
   operation  & syntax    & \multicolumn{2}{c}{syntaxes}\\
  \hline
  negation    & $\NOT f$      & $\NOTALT f$  \\
  disjunction & $f\OR g$      & $f\ORALT g$      & $f\ORALTT g$ \\
  conjunction & $f\AND g$     & $f\ANDALT g$     & $f\ANDALTT g$ \\
  implication & $f\IMPLIES g$ & $f\IMPLIESALT g$ & $f\IMPLIESALTT g$\\
  exclusion   & $f\XOR g$     & $f\XORALT g$ \\
  equivalence & $f\EQUIV g$   & $f\EQUIVALT g$   & $f\EQUIVALTT g$ \\
\end{tabular}
\end{center}

Additionally, an atomic proposition $a$ can be negated using the
syntax \samp{$a$=0}, which is equivalent to \samp{$\NOT a$}.  Also
\samp{$a$=1} is equivalent to just \samp{a}.  These two syntaxes help
us read formul\ae{} written using Wring's syntax.

\label{def:boolform}
When a formula is built using only Boolean constants
(section~\ref{sec:bool}), atomic proposition (section~\ref{sec:ap}),
and the above operators, we say that the formula is a \emph{Boolean
  formula}.

\subsection{Semantics}

\begin{align*}
\NOT f\vDash \sigma &\iff (f\nvDash\sigma) \\
f\AND g\vDash \sigma &\iff (f\vDash\sigma)\land(g\vDash\sigma) \\
f\OR g\vDash \sigma &\iff (f\vDash\sigma)\lor(g\vDash\sigma) \\
f\IMPLIES g\vDash \sigma &\iff
           (f\nvDash\sigma)\lor(g\vDash\sigma)\\
f\XOR g\vDash \sigma &\iff
           ((f\vDash\sigma)\land(g\nvDash\sigma))\lor
           ((f\nvDash\sigma)\land(g\vDash\sigma))\\
f\EQUIV g\vDash \sigma &\iff
           ((f\vDash\sigma)\land(g\vDash\sigma))\lor
           ((f\nvDash\sigma)\land(g\nvDash\sigma))
\end{align*}

\subsection{Trivial Identities (Occur Automatically)}

% These first rules are for the \samp{!} and \samp{->} operators.

\begin{align*}
  \NOT \0 &\equiv \1 &
  \1\IMPLIES f &\equiv f &
  f\IMPLIES\1 &\equiv \1 \\
  \NOT\1 &\equiv \0 &
  \0\IMPLIES f &\equiv \1&
  f \IMPLIES 0 &\equiv \NOT f \\
  \NOT\NOT f &\equiv f &
  && f\IMPLIES f &\equiv \1
\end{align*}

The next set of rules apply to operators that are commutative, so
these identities are also valid with the two arguments swapped.

\begin{align*}
  \0\AND f   &\equiv \0 &
  \0\OR f &\equiv f&
  \0\XOR f &\equiv f &
  \0\EQUIV f &\equiv \NOT f \\
  \1\AND f   &\equiv f &
  \1\OR f &\equiv \1 &
  \1\XOR f &\equiv \NOT f&
  \1\EQUIV f &\equiv f \\
  f\AND f &\equiv f &
  f\OR f &\equiv f &
  f\XOR f &\equiv \0&
  f\EQUIV f &\equiv \1
\end{align*}

The \samp{\&} and \samp{|} operators are associative, so they are
actually implemented as $n$-ary operators (i.e., not binary): this
allows us to reorder all arguments in a unique way
(e.g. alphabetically).  For instance the two expressions
\samp{a\&c\&b\&!d} and \samp{c\&!d\&b\&a} are actually represented as
the operator \samp{\&} applied to the arguments
$\{\code{a},\code{b},\code{c},\code{!d}\}$.  Because these two
expressions have the same internal representation, they are actually
considered equal for the purpose of the above identities.  For
instance \samp{(a\&c\&b\&!d)->(c\&!d\&b\&a)} will be rewritten to
\samp{1} automatically.

\subsection{Unabbreviations}\label{sec:unabbbool}

The `\verb=unabbreviate_logic_visitor=' rewrites all Boolean operators
using only the \samp{!}, \samp{\&}, and \samp{|} operators using the
following rewritings:
\begin{align*}
  f\IMPLIES g &\equiv  (\NOT f)\OR g\\
  f\EQUIV g &\equiv  (f\AND g)\OR ((\NOT g)\AND(\NOT f))\\
  f\XOR g &\equiv  (f\AND\NOT g)\OR (g\AND\NOT f)\\
\end{align*}

\section{Temporal Operators}

Given two temporal formul\ae{} $f$, and $g$, the following
temporal operators can be used to construct another temporal formula.

\begin{center}
\begin{tabular}{ccc}
                 & preferred & \multicolumn{1}{c}{other supported} \\
   operator      & syntax    & \multicolumn{1}{c}{syntaxes}\\
  \hline
  Next           & $\X f$    & $\XALT f$ \\
  Eventually     & $\F f$    & $\FALT f$ \\
  Always         & $\G f$    & $\GALT f$ \\
  (Strong) Until & $f \U g$ \\
  Weak Until     & $f \W g$ \\
  (Weak) Release & $f \R g$  & $f \RALT g$ \\
  Strong Release & $f \M g$ \\
\end{tabular}
\end{center}

\subsection{Semantics}\label{sec:opltl:sem}

\begin{align*}
  \sigma\vDash \X f &\iff f\vDash \sigma^{1..}\\
  \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 f\U g &\iff \exists j\in\N,\,
  \begin{cases}
    \forall i<j,\, f\vDash \sigma^{i..}\\
    \sigma^{j..} \vDash g\\
  \end{cases}\\
  \sigma \vDash f\W g &\iff (\sigma\vDash f\U g)\lor(\sigma\vDash\G f)\\
  \sigma \vDash f\M g &\iff \exists j\in\N,\,
  \begin{cases}
    \forall i\le j,\, \sigma^{i..}\vDash g\\
    \sigma^{j..}\vDash f\\
  \end{cases}\\
  \sigma \vDash f\R g &\iff (\sigma \vDash f\M g)\lor(\sigma\vDash \G g)
\end{align*}

\subsection{Trivial Identities (Occur Automatically)}

  \begin{align*}
    \X\0 &\equiv \0 &
    \F\0 &\equiv \0 &
    \G\0 &\equiv \0 \\
    \X\1 &\equiv \1 &
    \F\1 &\equiv \1 &
    \G\1 &\equiv \1 \\
               &                &
    \F\F f&\equiv \F f &
    \G\G f&\equiv \G f
  \end{align*}
  \begin{align*}
    f\U\1&\equiv \1 &
    f\W\1&\equiv \1 &
    f\M\0&\equiv \0 &
    f\R\1&\equiv \1 \\
    \0\U f&\equiv f &
    \0\W f&\equiv f &
    \0\M f&\equiv \0 &
    f\R\0&\equiv \0 \\
    f\U\0&\equiv \0 &
    \1\W f&\equiv \1 &
    \1\M f&\equiv f &
    \1\R f&\equiv f \\
    f\U f&\equiv f &
    f\W f&\equiv f &
    f\M f&\equiv f &
    f\R f&\equiv f
  \end{align*}

\subsection{Other Equivalences}

The following equivalences are listed here only to give a different
view of the semantics of section~\ref{sec:opltl:sem}.

The operator \samp{F}, \samp{G}, \samp{U}, \samp{R}, \samp{M}, and
\samp{W} can all be defined using only Boolean operators, \samp{X},
and one of \samp{U}, \samp{W}, \samp{R}, or \samp{M}.  This property
is usually used to simplify proofs.

\begin{align*}
\intertext{Equivalences using $\U$:}
  \F f &\equiv \1\U f\\
  \G f &\equiv \NOT\F\NOT f\equiv \NOT(\1\U\NOT f)\\
  f\W g &\equiv (f\U g)\OR(\G f)\equiv (f\U g)\OR\NOT(\1\U\NOT f)\\
        &\equiv f\U (g\OR \G f)\equiv f\U (g\OR\NOT(\1\U\NOT f))\\
  f\M g &\equiv g \U (f\AND g)\\
  f\R g &\equiv g \W (f\AND g) \equiv (g \U (f\AND g))\OR\NOT(\1\U\NOT g)\\
        &\phantom{\equiv g \W (f\AND g)} \equiv g \U ((f\AND g)\OR\NOT(\1\U\NOT g))\\
\intertext{Equivalences using $\W$:}
  \F f &\equiv \NOT\G\NOT f\equiv \NOT((\NOT f)\W\0)\\
  \G f &\equiv \0\R f \equiv f\W \0\\
  f\U g &\equiv (f \W g)\AND(\F g)\equiv (f \W g)\AND\NOT((\NOT g)\W\0)\\
  f\M g &\equiv (g \W (f\AND g))\AND\F(f\AND g)\equiv(g \W (f\AND g))\AND\NOT((\NOT (f\AND g))\W\0)\\
  f\R g &\equiv g \W (f\AND g)\\
\intertext{Equivalences using $\R$:}
  \F f &\equiv \NOT\G\NOT f\equiv \NOT (\0\R\NOT f)\\
  \G f &\equiv \0 \R f \\
  f\U g&\equiv (((\X g) \R f)\AND\F g)\OR g \equiv (((\X g) \R f)\AND(\NOT (\0\R\NOT g)))\OR g \\
  f \W g&\equiv ((\X g)\R f)\OR g\\
  f \M g&\equiv (f \R g)\AND\F f\equiv (f \R g)\AND\NOT (\0\R\NOT f)\\
        &\equiv f \R (g\AND\F g)\equiv f \R (g\AND\NOT (\0\R\NOT f))\\
\intertext{Equivalences using $\M$:}
  \F f &\equiv f\M\1\\
  \G f &\equiv \NOT\F\NOT f \equiv \NOT((\NOT f)\M\1)\\
  f\U g&\equiv ((\X g)\M f)\OR g \\
  f \W g&\equiv (f\U g)\OR \G f \equiv ((\X g)\M f)\OR g\OR \NOT((\NOT f)\M\1)\\
  f \R g&\equiv (f \M g)\OR\G f \equiv (f \M g)\OR \NOT((\NOT f)\M\1)
\end{align*}
\ltltodo[noline]{Why do we have two ways to rewrite $f\W g$ with $\U$,
  and two ways to rewrite $f\M g$ with $\R$, but no similar rules for other operators? What are we missing?}

Note: these equivalences make it possible to build artificially
complex formul\ae{}.\spottodo{Make sure Spot is able to simplify all these
  equivalences.}  For instance by applying the above rules to
successively rewrite $\U\to\M\to\R\to\U$ we get
\begin{align*}
f\U g &\equiv ((\X g)\M f)\OR g \\
      &\equiv (((\X g) \R f)\AND\NOT (\0\R\NOT \X g))\OR g \\
      &\equiv (((f \U (\X g\AND f))\OR\NOT(\1\U\NOT f)) \AND\NOT (\underbrace{((\X g) \U
\0)}_{\text{trivially false}}\OR\NOT(\1\U\NOT\X g)))\OR g\\
      &\equiv (((f \U (\X g\AND f))\OR\NOT(\1\U\NOT f))
               \AND(\1\U\NOT\X g))\OR g\\
\end{align*}


\subsection{Unabbreviations}

The `\verb=unabbreviate_ltl_visitor=' applies all the rewritings from
section~\ref{sec:unabbbool} as well as the following two rewritings:
\begin{align*}
  \F f&\equiv \1\U f\\
  \G f&\equiv \0\R f
\end{align*}

\spottodo[inline]{Spot should offer some way to rewrite a formula to
  selectively remove $\U$, $\R$, $\M$, or $\W$, using the equivalences
  from the previous section.}

\section{Rational Operators}

Any Boolean formula (section~\ref{def:boolform}) is a rational
expression.  Rational expression can be further combined with the
following operators, where $f$ and $g$ denote arbitrary rational
expressions and $b$ denotes a Boolean expression.

\begin{center}
\begin{tabular}{ccccc}
              & preferred & \multicolumn{2}{c}{other supported} \\
   operation  & syntax    & \multicolumn{2}{c}{syntaxes}\\
  \hline
  empty word   & $\eword$ \\
  union        & $f\OR g$  & $f\ORALT g$ & $f\ORALTT g$ \\
  (synchronized) intersection & $f\ANDALT g$ & $f\ANDALTT g$ \\
  unsynchronized intersection & $f\AND g$ \\
  concatenation & $f\CONCAT g$ \\
  fusion & $f\FUSION g$ \\
  bounded repetition & $f\STAR{\mvar{i}..\mvar{j}}$
                     & $f\STAR{\mvar{i}:\mvar{j}}$
                     & $f\STAR{\mvar{i} to \mvar{j}}$
                     & $f\STAR{\mvar{i},\mvar{j}}$\\
  unbounded repetition & $f\STAR{\mvar{i}..}$
                     & $f\STAR{\mvar{i}:}$
                     & $f\STAR{\mvar{i} to}$
                     & $f\STAR{\mvar{i},}$\\
  bounded occurrence & $b\EQUAL{\mvar{i}..\mvar{j}}$
                     & $b\EQUAL{\mvar{i}:\mvar{j}}$
                     & $b\EQUAL{\mvar{i} to \mvar{j}}$
                     & $b\EQUAL{\mvar{i},\mvar{j}}$\\
  unbounded occurrence & $b\EQUAL{\mvar{i}..}$
                     & $b\EQUAL{\mvar{i}:}$
                     & $b\EQUAL{\mvar{i} to}$
                     & $b\EQUAL{\mvar{i},}$\\
  bounded goto       & $b\GOTO{\mvar{i}..\mvar{j}}$
                     & $b\GOTO{\mvar{i}:\mvar{j}}$
                     & $b\GOTO{\mvar{i} to \mvar{j}}$
                     & $b\GOTO{\mvar{i},\mvar{j}}$\\
  unbounded goto     & $b\GOTO{\mvar{i}..}$
                     & $b\GOTO{\mvar{i}:}$
                     & $b\GOTO{\mvar{i} to}$
                     & $b\GOTO{\mvar{i},}$\\
\end{tabular}
\end{center}

\subsection{Semantics}

The following semantics assume that $f$ and $g$ are two rational
expressions, while $b$ is a Boolean formula.

\begin{align*}
  \sigma\VDash \eword & \iff |\sigma| = 0 \\
  \sigma\VDash a      & \iff \sigma(0)(a) = 1 \\
  \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\AND g &\iff \exists k\in\N,\,
  \begin{cases}
    \text{either} &(\sigma \VDash f) \land (\sigma^{0..k-1} \VDash g)\\
    \text{or} &(\sigma^{0..k-1} \VDash f) \land (\sigma \VDash g)
  \end{cases} \\
  \sigma\VDash f\CONCAT g&\iff \exists k\in\N,\,(\sigma^{0..k-1} \VDash f)\land(\sigma^{k..} \VDash g)\\
  \sigma\VDash f\FUSION g&\iff \exists k\in\N,\,(\sigma^{0..k} \VDash f)\land(\sigma^{k..} \VDash g)\\
  \sigma\VDash f\STAR{\mvar{i}..\mvar{j}}& \iff
  \begin{cases}
    \text{either} & \mvar{i}=0 \land \sigma=\varepsilon \\
    \text{or} & \mvar{i}=0 \land \mvar{j}>0 \land (\exists k\in\N,\,
      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
      \VDash f\STAR{\mvar{0}..\mvar{j-1}}))\\
    \text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\,
      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
      \VDash f\STAR{\mvar{i-1}..\mvar{j-1}}))\\
  \end{cases}\\
  \sigma\VDash f\STAR{\mvar{i}..} & \iff
  \begin{cases}
    \text{either} & \mvar{i}=0 \land \sigma=\varepsilon \\
    \text{or} & \mvar{i}=0 \land (\exists k\in\N,\,
      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
      \VDash f\STAR{\mvar{0}..}))\\
    \text{or} & \mvar{i}>0 \land (\exists k\in\N,\,
      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
      \VDash f\STAR{\mvar{i-1}..}))\\
  \end{cases}\\
  \sigma\VDash b\EQUAL{\mvar{i}..\mvar{j}} & \iff
  \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..\mvar{j}}\CONCAT\mathtt\{\NOT b\,\mathtt\}\STAR{0..}\\
  \sigma\VDash b\EQUAL{\mvar{i}..} & \iff
  \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..}\CONCAT\mathtt\{\NOT b\,\mathtt\}\STAR{0..}\\
  \sigma\VDash b\GOTO{\mvar{i}..\mvar{j}} & \iff
  \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..\mvar{j}}\\
  \sigma\VDash b\GOTO{\mvar{i}..} & \iff
  \sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..}\\
\end{align*}

Note that the semantics of $\ANDALT$ and $\AND$ coincide if both
operands are Boolean formul\ae.

\subsection{Syntactic Sugar}

The syntax on the left is equivalent to the syntax on the right.
These rewritings are performed from left to right when parsing a
formula, and some are performed from right to left when writing it for
output.

\begin{align*}
  f\STARALT &\equiv f\STAR{0..}\\
  f\STAR{}    &\equiv f\STAR{0..}  &
  f\PLUS{}    &\equiv f\STAR{1..}  &
  f\EQUAL{}   &\equiv f\EQUAL{0..} &
  f\GOTO{}   &\equiv f\GOTO{1..1} \\
  f\STAR{..}  &\equiv f\STAR{0..}  &
  &&
  f\EQUAL{..}  &\equiv f\EQUAL{0..} &
  f\GOTO{..}  &\equiv f\GOTO{1..} \\
  f\STAR{..\mvar{j}} &\equiv f\STAR{0..\mvar{j}} &
  &&
  f\EQUAL{..\mvar{j}} &\equiv f\EQUAL{0..\mvar{j}} &
  f\GOTO{..\mvar{j}} &\equiv f\GOTO{1..\mvar{j}} \\
  f\STAR{\mvar{k}}  &\equiv f\STAR{\mvar{k}..\mvar{k}}  &
  &&
  f\EQUAL{\mvar{k}}   &\equiv f\EQUAL{\mvar{k}..\mvar{k}} &
  f\GOTO{\mvar{k}}   &\equiv f\GOTO{\mvar{k}..\mvar{k}} \\
  \STAR{}    &\equiv \1\STAR{0..}  &
  \PLUS{}    &\equiv \1\STAR{1..}  \\
  \STAR{\mvar{k}}    &\equiv \1\STAR{\mvar{k}..\mvar{k}}  &
\end{align*}

\subsection{Trivial Identities (Occur Automatically)}

The following identities also hold if $j$ or $l$ are missing (assuming
they are then equal to $\infty$).  $f$ can be any regular expression,
while $b$, $b_1$, $b_2$ are assumed to be Boolean formul\ae.

\begin{align*}
  \0\STAR{0..\mvar{j}} &\equiv \eword  &
  \0\EQUAL{0..\mvar{j}} &\equiv \1\STAR{} &
  \0\GOTO{0..\mvar{j}} &\equiv \eword \\
  \0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 &
  \0\EQUAL{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0&
  \0\GOTO{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0\\
  \eword\STAR{\var{i}..\mvar{j}} &\equiv \eword&
  \1\EQUAL{0} &\equiv\eword&
  \1\GOTO{0} &\equiv\eword\\
  f\STAR{0}&\equiv \eword &
  \1\EQUAL{\mvar{i}..\mvar{j}}&\equiv \1\STAR{\mvar{i}..\mvar{j}}&
  \1\GOTO{\mvar{i}..\mvar{j}}&\equiv \1\STAR{\mvar{i}..\mvar{j}}\\
  f\STAR{\mvar{i}..\mvar{j}}\STAR{\mvar{k}..\mvar{l}} &\equiv f\STAR{\mvar{ik}..\mvar{jl}}&
  b\EQUAL{0..}&\equiv 1\STAR{} &
  b\GOTO{0}&\equiv \eword \\
  &\drsh\text{~if~}i(k+1)\le jk+1 &
  b\EQUAL{0}&\equiv (\NOT b)\STAR{} \\
\end{align*}

\noindent
The following rules are all valid with the two arguments swapped, except the one marked with $\stackrel{\dag}{\equiv}$.
%(Even for the non-commutative operators \samp{$\CONCAT$} and
%\samp{$\FUSION$}.)

\begin{align*}
  f\AND f &\equiv \0&
  f\ANDALT f &\equiv f &
  f\OR f &\equiv f \\
  \0\AND f &\equiv f &
  \0\ANDALT f   &\equiv \0 &
  \0\OR f &\equiv f &
  \0 \FUSION f &\equiv \0 &
  \0 \CONCAT f &\equiv \0 \\
  \1\AND f &\equiv \NOT f&
  \1\ANDALT f   &\equiv f &
  \1\OR f &\equiv \1 &
  \1 \FUSION f & \equiv f\\
  \eword\AND f &\equiv f &
  \eword\ANDALT f &\equiv
  \begin{cases}
    \eword \mathrlap{\text{~if~} \varepsilon\VDash f} \\
    \0 \mathrlap{\text{~if~} \varepsilon\nVDash f} \\
  \end{cases} &
  &&
  \eword \FUSION f &\equiv \0 &
  \eword \CONCAT f &\equiv f\\
  &&
  b_1 \ANDALT b_2 &\equiv b_1\AND b_2 &
  &&
  b:f &\stackrel{\dag}{\equiv} b\AND f\\
\end{align*}

\section{Rational-LTL Binding Operators}

The following operators combine a rational expression $r$ with a PSL
formula $f$ to form another PSL formula.

\begin{center}
\begin{tabular}{ccccc}
              & preferred & \multicolumn{2}{c}{other supported} \\
   operation  & syntax    & \multicolumn{2}{c}{syntaxes}\\
  \hline
  (universal) suffix implication
  & $\ratgroup{r}\Asuffix{} f$
  & $\ratgroup{r}\AsuffixALT{} f$
  & $\ratgroup{r}\texttt{(}f\texttt{)}$
  \\
  existential suffix implication
  & $\ratgroup{r}\Esuffix{} f$
  \\
  closure
  & $\ratgroup{r}$
  \\
  negated closure
  & $\nratgroup{r}$
  \\
\end{tabular}
\end{center}

For technical reasons, the negated closure is actually implemented as
an operator, even if it is syntactically and semantically equal to the
combination of $\NOT$ and $\ratgroup{r}$.

\subsection{Semantics}

The following semantics assume that $r$ is a rational expression,
while $f$ is a PSL formula.

\begin{align*}
  \sigma\vDash \ratgroup{r}\Esuffix f &\iff \exists k\ge 0, (\sigma^{0..k}\VDash r)\land(\sigma^{k..}\vDash f)\\
  \sigma\vDash \ratgroup{r}\Asuffix f &\iff \forall k\ge 0, (\sigma^{0..k}\VDash r)\limplies (\sigma^{k..}\vDash f)\\
  \sigma\vDash \ratgroup{r} & \iff (\exists k\ge 0, \sigma^{0..k}\VDash r)\lor(\forall k\ge 0,\,\exists\pi\in(\B^\AP)^\star,\, (\sigma^{0..k}\prec \pi)\land(\pi\VDash r))\\
  \sigma\vDash \nratgroup{r} & \iff (\forall k\ge 0, \sigma^{0..k}\nVDash r)\land(\exists k\ge 0,\,\forall\pi\in(\B^\AP)^\star,\, (\sigma^{0..k}\prec \pi)\limplies(\pi\nVDash r))\\
\end{align*}

The $\prec$ symbol should be read as ``\emph{is a prefix of}''.  So
the semantic for `$\sigma\vDash \ratgroup{r}$' is that either there is
a (non-empty) finite prefix of $\sigma$ that is a model of $r$, or any
prefix of $\sigma$ can be extended into a finite sequence $\pi$ that
is a model of $r$.  An infinite sequence $\texttt{a;a;a;a;a;}\ldots$
is therefore a model of the formula \samp{$\ratgroup{a\PLUS{};\NOT
    a}$} even though it never sees \samp{$\NOT a$}.

\subsection{Syntactic Sugar}

The syntax on the left is equivalent to the syntax on the right.
These rewritings are performed from left to right when parsing a
formula.\spottodo{It would be nice to have the opposite rewritings on
  output.}

\begin{align*}
  \ratgroup{r}\EsuffixEQ f &\equiv \ratgroup{r\CONCAT\1}\Esuffix f &
  \ratgroup{r}\AsuffixEQ f &\equiv \ratgroup{r\CONCAT\1}\Asuffix f\\
  \ratgroupn{r} &\equiv \ratgroup{r}\Esuffix \1 &
  \ratgroup{r}\AsuffixALTEQ f &\equiv \ratgroup{r\CONCAT\1}\Asuffix f\\
\end{align*}

$\AsuffixEQ$ and $\AsuffixALTEQ$ are synonyms in the same way as
$\Asuffix$ and $\AsuffixALT$ are.

\subsection{Trivial Identities (Occur Automatically)}

For any PSL formula $f$, any rational expression $r$, and any Boolean
formula $b$, the following rewritings are systematically performed
(from left to right).

\begin{align*}
  \ratgroup{\0}\Asuffix f &\equiv \1
& \ratgroup{\0}\Esuffix f &\equiv \0
& \ratgroup{\0} & \equiv \0
& \nratgroup{\0} & \equiv \1 \\
  \ratgroup{\1}\Asuffix f &\equiv f
& \ratgroup{\1}\Esuffix f &\equiv f
& \ratgroup{\1} & \equiv \1
& \nratgroup{\1} & \equiv \0 \\
  \ratgroup{\eword}\Asuffix f&\equiv \1
& \ratgroup{\eword}\Esuffix f&\equiv \0
& \ratgroup{\eword} & \equiv \0
& \nratgroup{\eword} & \equiv \1 \\
  \ratgroup{b}\Asuffix f&\equiv (\NOT{b})\OR f
& \ratgroup{b}\Esuffix f&\equiv b\AND f
& \ratgroup{b} &\equiv b
& \nratgroup{b} &\equiv \NOT b\\
  \ratgroup{r}\Asuffix \1&\equiv \1
& \ratgroup{r}\Esuffix \0&\equiv \0  \\
\end{align*}

\chapter{Grammar}

For simplicity, this grammar gives only one rule for each
operator, even if the operator has multiple synonyms (like \samp{|},
\samp{||}, and {`\verb=\/='}).

\begin{align*}
  \mathit{constant} ::=&\, \0 \mid \1                             &  \mathit{tformula} ::=&\,\mathit{bformula}\\
  \mathit{atomic\_prop} ::=&\, \text{see section~\ref{sec:ap}}    &    \mid&\,\tsamp{(}\,\mathit{tformula}\,\tsamp{)} \\
  \mathit{bformula} ::=&\, \mathit{constant}                      &    \mid&\,\msamp{\NOT}\,\mathit{tformula}\,\\
    \mid&\,\mathit{atomic\_prop}                                  &    \mid&\,\mathit{tformula}\,\msamp{\AND}\,\mathit{tformula} \\
    \mid&\,\mathit{atomic\_prop}\code{=0}                         &    \mid&\,\mathit{tformula}\,\msamp{\OR}\,\mathit{tformula} \\
    \mid&\,\mathit{atomic\_prop}\code{=1}                         &    \mid&\,\mathit{tformula}\,\msamp{\IMPLIES}\,\mathit{tformula} \\
    \mid&\,\tsamp{(}\,\mathit{bformula}\,\tsamp{)}                &    \mid&\,\mathit{tformula}\,\msamp{\XOR}\,\mathit{tformula} \\
    \mid&\,\msamp{\NOT}\,\mathit{bformula}                        &    \mid&\,\mathit{tformula}\,\msamp{\EQUIV}\,\mathit{tformula} \\
    \mid&\,\mathit{bformula}\,\msamp{\AND}\,\mathit{bformula}     &    \mid&\,\msamp{\X}\,\mathit{tformula}\\
    \mid&\,\mathit{bformula}\,\msamp{\OR}\,\mathit{bformula}      &    \mid&\,\msamp{\F}\,\mathit{tformula}\\
    \mid&\,\mathit{bformula}\,\msamp{\IMPLIES}\,\mathit{bformula} &    \mid&\,\msamp{\G}\,\mathit{tformula}\\
    \mid&\,\mathit{bformula}\,\msamp{\XOR}\,\mathit{bformula}     &    \mid&\,\mathit{tformula}\,\msamp{\U}\,\mathit{tformula} \\
    \mid&\,\mathit{bformula}\,\msamp{\EQUIV}\,\mathit{bformula}   &    \mid&\,\mathit{tformula}\,\msamp{\W}\,\mathit{tformula} \\
  \mathit{rformula} ::=&\, \mathit{bformula}                      &    \mid&\,\mathit{tformula}\,\msamp{\R}\,\mathit{tformula} \\
    \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}                  &    \mid&\,\mathit{tformula}\,\msamp{\M}\,\mathit{tformula} \\
    \mid&\,\mathit{rformula}\msamp{\OR}\mathit{rformula}          &    \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\Asuffix}\,\mathit{tformula}\\
    \mid&\,\mathit{rformula}\msamp{\AND}\mathit{rformula}         &    \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\AsuffixEQ}\,\mathit{tformula}\\
    \mid&\,\mathit{rformula}\msamp{\ANDALT}\mathit{rformula}      &    \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\Esuffix}\,\mathit{tformula}\\
    \mid&\,\mathit{rformula}\msamp{\CONCAT}\mathit{rformula}      &    \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\EsuffixEQ}\,\mathit{tformula} \\
    \mid&\,\mathit{rformula}\msamp{\FUSION}\mathit{rformula}      &    \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}} \\
    \mid&\,\mathit{rformula}\msamp{\STAR{\mvar{i}..\mvar{j}}}     &    \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\msamp{\NOT} \\
    \mid&\,\mathit{rformula}\msamp{\PLUS}                         \\
    \mid&\,\mathit{rformula}\msamp{\EQUAL{\mvar{i}..\mvar{j}}}    \\
    \mid&\,\mathit{rformula}\msamp{\GOTO{\mvar{i}..\mvar{j}}}     \\
\end{align*}

\section{Operator precedence}

\spottodo[inline]{The following operator precedence describe the
  current parser of Spot, but this is not what we want eventually.
  For instance $\IMPLIES$ should be right associative.  $\U$ and $\W$
  would probably make more sense as right associative operators too.\\
  %
  Tools that have $\U$, $\R$, $\W$, and $\M$ operators as left
  associative: Spin, ltl2ba (same parser as spin), Wring, psl2ba,
  Spot, Modella, NuSMV.\\
  %
  Tools (and doc) that have these operators as right associative: Goal
  (hence Büchi Store), PSL reference manual, LTL2AUT, LTL2Büchi (from
  JavaPathFinder).\\
  %
  Tools that have these operators as non-associative (parentheses are
  required): Vis, LBTT.\\
  %
  While compiling these lists I have also discovered that not all
  people aggreed on the associativity of $\IMPLIES$ and $\EQUIV$.
  Some have both left-assoc, or both right-assoc, other have only
  $\IMPLIES$ as right-assoc.\\
  %
  We want to get closer to the PSL standard eventually.}

\begin{center}
\begin{tabular}{cll}
 assoc. & operators                                                                                    & priority \\
\hline
left    & $\Asuffix,\,\AsuffixEQ,\,\Esuffix,\,\EsuffixEQ$                                              & lowest   \\
left    & $\CONCAT,\,\FUSION$                                                                          &          \\
left    & $\IMPLIES,\,\EQUIV$                                                                          &          \\
left    & $\XOR$                                                                                       &          \\
left    & $\OR$                                                                                        &          \\
left    & $\AND,\,\ANDALT$                                                                             &          \\
left    & $\U,\,\W,\,\M,\,\R$                                                                          &          \\
        & $\F,\,\G$                                                                                    &          \\
        & $\X$                                                                                         &          \\
        & $\STAR{\mvar{i}..\mvar{j}},\,\PLUS,\,\EQUAL{\mvar{i}..\mvar{j}},\,\GOTO{\mvar{i}..\mvar{j}}$ &          \\
        & $\NOT$                                                                                       &          \\
        & $\code{=0},\,\code{=1}$                                                                      & highest  \\
\end{tabular}
\end{center}

\chapter{Properties}

When Spot builds a formula (represented by an AST with shared
subtrees) it computes a set of properties for each node.  These
properties can be queried from any \texttt{spot::ltl::formula}
instance using the following methods:

\noindent
\begin{tabulary}{\textwidth}{lL}
\texttt{is\_boolean()}& Whether the formula use only Boolean
  operators.
\\\texttt{is\_sugar\_free\_boolean()}& Whether the formula use
  only $\AND$, $\OR$, and $\NOT$ operators.  (Especially, no
  $\IMPLIES$ or $\EQUIV$ are allowed.)
\\\texttt{is\_in\_nenoform()}& Whether the formula is in negative
  normal form. See section~\ref{sec:nnf}.
\\\texttt{is\_X\_free()}&
  Whether the formula avoids the $\X$ operator.
\\\texttt{is\_ltl\_formula()}& Whether the formula uses only LTL
  operators. (Boolean operators are also allowed.)
\\\texttt{is\_eltl\_formula()}& Whether the formula uses only ELTL
  operators. (Boolean and LTL operators are also allowed.)
\\\texttt{is\_psl\_formula()}& Whether the formula uses only PSL
  operators. (Boolean and LTL operators are also allowed.)
\\\texttt{is\_sere\_formula()}& Whether the formula uses only
  rational operators. (Boolean operators are also allowed, provided
  no rational operator is negated.)
\\\texttt{is\_finite()}& Whether a SERE describes a finite
  language, or an LTL formula uses no temporal operator but $\X$.
\\\texttt{is\_eventual()}& Whether the formula is a pure eventuality.
\\\texttt{is\_universal()}& Whether the formula is purely universal.
\\\texttt{is\_syntactic\_safety()}& Whether the formula is a syntactic
  safety property.
\\\texttt{is\_syntactic\_guaranty()}& Whether the formula is a syntactic
  guaranty property.
\\\texttt{is\_syntactic\_obligation()}& Whether the formula is a syntactic
  obligation property.
\\\texttt{is\_syntactic\_recurrence()}& Whether the formula is a syntactic
  recurrence property.
\\\texttt{is\_syntactic\_persistence()}& Whether the formula is a syntactic
  persistence property.
\\\texttt{is\_marked()}& Whether the formula contains a special
  ``marked'' version of the $\Esuffix$ operator.\footnote{This special
    operator is used when translating recurring $\Esuffix$, it is
    rendered as $\EsuffixMarked$ and it obeys the same simplification
    rules and properties as $\Esuffix$ (except for the
    \texttt{is\_marked()} property).}
\\\texttt{accepts\_eword()}& Whether the formula accept
  $\eword$. (This can only be true for a rational formula.)
\end{tabulary}

\section{Pure Eventualities and Purely Universal Formul\ae{}}
\label{sec:eventuniv}

These two syntactic classes of formul\ae{} were introduced
by~\citet{etessami.00.concur} to simplify LTL formul\ae{}.  We shall
present the associated simplification rules in
Section~\ref{sec:eventunivrew}, for now we only define these two
classes.

Pure eventual formul\ae{} describe properties that are left-append
closed, i.e., any accepted (infinite) sequence can be prefixed by a
finite sequence and remain accepted.  From an LTL standpoint, if
$\varphi$ is a left-append closed formula, then $\F\varphi \equiv
\varphi$.

Purely universal formul\ae{} describe properties that are
suffix-closed, i.e., if you remove any finite prefix of an accepted
(infinite) sequence, it remains accepted.  From an LTL standpoint if
$\varphi$ is a suffix-closed formula, then $\G\varphi \equiv \varphi$.


Let $\varphi$ designate any arbitrary formula and $\varphi_E$
(resp. $\varphi_U$) designate any instance of a pure eventuality
(resp. a purely universal) formula.  We have the following grammar
rules:

\begin{align*}
  \varphi_E ::=&\, \0
           \mid \1
           \mid \X \varphi_E
           \mid \F \varphi
           \mid \G \varphi_E
           \mid \varphi_E\AND \varphi_E
           \mid (\varphi_E\OR \varphi_E)
           \mid \NOT\varphi_U\\
           \mid&\,\varphi  \U \varphi_E
           \mid 1        \U \varphi
           \mid \varphi_E\R \varphi_E
           \mid \varphi_E\W \varphi_E
           \mid \varphi_E\M \varphi_E
           \mid \varphi  \M \1\\
  \varphi_U ::=&\, \0
           \mid \1
           \mid \X \varphi_U
           \mid \F \varphi_U
           \mid \G \varphi
           \mid \varphi_U\AND \varphi_U
           \mid (\varphi_U\OR \varphi_U)
           \mid \NOT\varphi_E\\
           \mid&\,\varphi_U\U \varphi_U
           \mid \varphi  \R \varphi_U
           \mid \0       \R \varphi
           \mid \varphi_U\W \varphi_U
           \mid \varphi  \W \0
           \mid \varphi_U\M \varphi_U\\
\end{align*}

\section{Syntactic Hierarchy Classes}

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}.

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 rational
property, $r_F$ a finite rational property (no loops), and $r_I$ an
infinite rational property.


\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&\, \ratgroup{r}\Esuffix \varphi_G\mid
                   \ratgroup{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&\, \ratgroup{r_F}\Esuffix \varphi_S\mid
                   \ratgroup{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&\, \ratgroup{r_F}\Esuffix \varphi_O \mid \ratgroup{r_I}\Esuffix \varphi_G\mid
                  \ratgroup{r_F}\Asuffix \varphi_O\mid
                   \ratgroup{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
                   \X\varphi_P \mid \F\varphi_P \mid
                   \varphi_P\U\varphi_P\mid\varphi_P\R\varphi_S\mid
                   \varphi_S\W\varphi_P\mid\varphi_P\M\varphi_P\\
           \mid&\, \ratgroup{r}\Esuffix \varphi_P\mid
                   \ratgroup{r_F}\Asuffix \varphi_P\mid
                   \ratgroup{r_I}\Asuffix \varphi_S\\
  \varphi_R ::=&\, \varphi_O \mid \NOT\varphi_P\mid
                   \varphi_R\AND \varphi_R\mid (\varphi_R\OR \varphi_R)\mid
                   \X\varphi_R \mid \G\varphi_R \mid
                   \varphi_R\U\varphi_G\mid\varphi_R\R\varphi_R\mid
                   \varphi_R\W\varphi_R\mid\varphi_G\M\varphi_R\\
           \mid&\, \ratgroup{r_F}\Esuffix \varphi_R \mid \ratgroup{r_I}\Esuffix \varphi_G\mid \ratgroup{r}\Asuffix \varphi_P\\
\end{align*}

\chapter{Rewritings}

The LTL rewritings described in this section are all implemented in
the `\verb|ltl_simplifier|' class defined in
\texttt{spot/ltlvisit/simplify.hh}.  This class implements several
caches in order to quickly rewrite formul\ae{} that have already been
rewritten previously.  For this reason, it is suggested that you reuse
your instance of `\verb|ltl_simplifier|' as much as possible.  If you
write an algorithm that will simplify LTL formul\ae{}, we suggest you
accept an optional `\verb|ltl_simplifier|' argument, so that you can
benefit from an existing instance.

The `\verb|ltl_simplifier|' takes an optional
`\verb|ltl_simplifier_options|' argument, making it possible to tune
the various rewritings that can be performed by this class.  These
options cannot be changed afterwards (because changing these options
would invalidate the results stored in the caches).

\section{Negative normal form}\label{sec:nnf}

This is implemented by the `\verb|ltl_simplifier::negative_normal_form|`
method.

A formula in negative normal form can only have only have negation
operators ($\NOT$) in front of atomic properties, and does not use any
of the $\XOR$, $\IMPLIES$ and $\EQUIV$ operators.  The following
rewriting arrange any PSL formula into negative normal form.

\begin{align*}
  \NOT\X f & \equiv \X\NOT f &
  \NOT(f \U g) & \equiv (\NOT f) \R (\NOT g) &
  \NOT(f \AND g)&\equiv (\NOT f) \OR (\NOT g)
  \\
  \NOT\F f & \equiv \G\NOT f &
  \NOT(f \R g) & \equiv (\NOT f) \U (\NOT g) &
  \NOT(f \OR g)&\equiv (\NOT f)\AND (\NOT g)
  \\
  \NOT\G f & \equiv \F\NOT f &
  \NOT(f \W g) & \equiv (\NOT f) \M (\NOT g) &
  \NOT(\ratgroup{r} \Asuffix f) &\equiv \ratgroup{r} \Esuffix \NOT f
  \\
  \NOT(\ratgroup{r})&\nratgroup{r}&
  \NOT(f \M g) & \equiv (\NOT f) \W (\NOT g)&
  \NOT(\ratgroup{r} \Esuffix f) &\equiv \ratgroup{r} \Asuffix \NOT f
\end{align*}
\noindent Recall the that negated closure $\nratgroup{r}$ is actually
implemented as a specific operator, so it not actually prefixed by the
$\NOT$ operator.
\begin{align*}
  f \XOR g & \equiv ((\NOT f)\AND g)\OR(f\AND\NOT g) &
  \NOT(f \XOR g) & \equiv ((\NOT f)\AND(\NOT g))\OR(f\AND g) &
  \NOT(f \AND g) & \equiv (\NOT f)\OR(\NOT g) \\
  f \EQUIV g & \equiv ((\NOT f)\AND(\NOT g))\OR(f\AND g) &
  \NOT(f \EQUIV g) & \equiv ((\NOT f)\AND g)\OR(f\AND\NOT g) &
  \NOT(f \OR g) & \equiv (\NOT f)\AND(\NOT g) \\
  f \IMPLIES g & \equiv (\NOT f) \AND g &
  \NOT(f \IMPLIES g) & \equiv f \AND \NOT g
\end{align*}

Note that the above rules include those from
`\verb=unabbreviate_logic_visitor=` described in
Section~\ref{sec:unabbbool}.  Therefore it is never necessary to apply
`\verb=unabbreviate_logic_visitor=` before or after
`\verb|ltl_simplifier::negative_normal_form|`.

If the option `\verb|nenoform_stop_on_boolean|' is set, the above
recursive rewriting will not be applied to subformul\ae{} that are
Boolean formul\ae.  For instance calling
`\verb|ltl_simplifier::negative_normal_form|` on $\NOT\F\G(a \XOR b)$
will produce $\G\F(((\NOT a)\AND(\NOT b))\OR(a\AND b))$ if
`\verb|nenoform_stop_on_boolean|' is unset, while it will produce
$\G\F(\NOT(a \XOR b))$ if `\verb|nenoform_stop_on_boolean|' is set.

\section{Simplifications}

The `\verb|ltl_simplifier::simplify|' method performs several kinds of
simplifications, depending on which `\verb|ltl_simplifier_options|'
was set.

The goals in most of these simplification are to:
\begin{itemize}
\item remove useless terms and operator.
\item move the $\X$ operators to the front of the formula (e.g., $\X\G
  f$ is better than the equivalent $\G\X f$).  This is because LTL
  translators will usually want to rewrite LTL formul\ae{} in
  a kind of disjunctive form: $\displaystyle\bigvee_i
  \left(\beta_i\land\X\psi_i\right)$ where $\beta_i$s are Boolean
  formul\ae{} and $\psi_i$s are LTL formul\ae{}.  Moving $\X$ to the
  front therefore simplify the translation.
\item move the $\F$ operators to the front of the formula (e.g., $\F(f
  \OR g)$ is better than the equivalent $(\F f)\OR (\F g)$), but not
  before $\X$ ($\X\F f$ is better than $\F\X f$).  Because $\F f$
  incurs some indeterminism, it is best to factorize these terms to
  limit the sources of indeterminism.
\end{itemize}

\subsection{Basic Simplifications}

These simplifications are enabled with
\verb|ltl_simplifier_options::reduce_basics|'.

\subsubsection{Basic Simplifications for Temporal Operators}

The following are simplification rules for unary operators (applied
from left to right, as usual):
\begin{align*}
  \X\F\G f &\equiv \F\G f   & \X\G\F f &\equiv \G\F f \\
  \F(f\U g) &\equiv \F g     & \F\X f &\equiv \X\F f \\
  \G(f \R g) &\equiv \G g    & \G\X f &\equiv \X\G f
\end{align*}
\begin{align*}
  \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m))&\equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)
\end{align*}
Note that the latter three rewriting rules for $\G$ have no dual:
rewriting $\F(f \AND \G\F g)$ to $\F(f) \AND \G\F(g)$ (instance as
suggested by~\citet{somenzi.00.cav}) goes against our goal of moving
the $\F$ operator in front of the formula.  Conceptually, it is also
easier to understand $\F(f \AND \G\F g)$: has long as $f$ has not been
verified, there is no need to worry about the $\G\F g$ term.

Here are the basic rewriting rules for binary operators (excluding $\OR$ and
$\AND$ which are considered in Spot as $n$-ary operators):
\begin{align*}
  \1 \U f &\equiv \F f             & f \W \0 &\equiv \G f \\
  f \M \1 &\equiv \F f             & \0 \R f &\equiv \G f \\
  (\X f)\U (\X g) &\equiv \X(f\U g) & (\X f)\W(\X g) &\equiv \X(f\W g) \\
  (\X f)\M (\X g) &\equiv \X(f\M g) & (\X f)\R(\X g) &\equiv \X(f\R g) \\
  f \U(\G f) &\equiv \G f          & f \W(\G f) &\equiv \G f \\
  f \M(\F f) &\equiv \F f          & f \R(\F f) &\equiv \F f \\
  f \U (g \OR \G(f)) &\equiv f\W g & f \W (g \OR \G(f)) &\equiv f\W g\\
  f \M (g \AND \F(f)) &\equiv f\M g & f \R (g \AND \F(f)) &\equiv f\M g
\end{align*}

Here are the basic rewriting rules for $n$-ary operators ($\AND$ and
$\OR$):
\begin{align*}
  (\F\G f) \AND(\F\G g) &\equiv \F\G(f\AND g)     &
  (\G\F f) \OR (\G\F g) &\equiv \G\F(f\OR g)      \\
  (\X f) \AND(\X g)     &\equiv \X(f\AND g)       &
  (\X f) \OR (\X g)     &\equiv \X(f\OR g)        \\
  (\X f) \AND(\F\G g)   &\equiv \X(f\AND \F\G g)  &
  (\X f) \OR (\G\F g)   &\equiv \X(f\OR \G\F g)   \\
  (f_1 \U f_2)\AND (f_3 \U f_2)&\equiv (f_1\AND f_3)\U f_2&
  (f_1 \U f_2)\OR  (f_1 \U f_3)&\equiv f_1\U (f_2\OR f_3) \\
  (f_1 \U f_2)\AND (f_3 \W f_2)&\equiv (f_1\AND f_3)\U f_2&
  (f_1 \U f_2)\OR  (f_1 \W f_3)&\equiv f_1\W (f_2\OR f_3) \\
  (f_1 \W f_2)\AND (f_3 \W f_2)&\equiv (f_1\AND f_3)\W f_2&
  (f_1 \W f_2)\OR  (f_1 \W f_3)&\equiv f_1\W (f_2\OR f_3) \\
  (f_1 \R f_2)\AND (f_1 \R f_3)&\equiv f_1\R (f_2\AND f_3)&
  (f_1 \R f_2)\OR  (f_3 \R f_2)&\equiv (f_1\OR f_3) \R f_2\\
  (f_1 \R f_2)\AND (f_1 \M f_3)&\equiv f_1\M (f_2\AND f_3)&
  (f_1 \R f_2)\OR  (f_3 \M f_2)&\equiv (f_1\OR f_3) \R f_3\\
  (f_1 \M f_2)\AND (f_1 \M f_3)&\equiv f_1\M (f_2\AND f_3)&
  (f_1 \M f_2)\OR  (f_3 \M f_2)&\equiv (f_1\OR f_3) \M f_3\\
  (\F g)\AND (f \U g)&\equiv f\U g &
  (\G f)\OR  (f \U g)&\equiv f\W g \\
  (\F g)\AND (f \W g)&\equiv f\U g &
  (\G f)\OR  (f \W g)&\equiv f\W g \\
  (\F f)\AND (f \R g)&\equiv f\M g &
  (\G g)\OR  (f \R g)&\equiv f\R g \\
  (\F f)\AND (f \M g)&\equiv f\M g &
  (\G g)\OR  (f \M g)&\equiv f\R g
\end{align*}
The above rules are applied even if more terms are presents in the
operator's arguments.  For instance $\F\G(a)\AND \G(b) \AND \F\G(c) \AND
\X(d)$ will be rewritten as $\X(d \AND \F\G(a\AND c))\AND \G(b)$.

Finally the following rule is applied only when no other terms are present
in the OR arguments:
\begin{align*}
  \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g_1) \OR \ldots \OR \G\F(g_m)
   &\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots \OR g_m)) \\
\end{align*}

\subsubsection{Basic Simplifications for SERE Operators}

\spottodo[inline]{These rules, mostly taken from ``Symbolic
  computation of PSL'' (Cimatti, Roveri, and Tonetta) are not complete
  yet.}

The following simplification rules are used for the $n$-ary operators
$\ANDALT$, $\AND$, and $\OR$, and are of course commutative.

\begin{align*}
  b \ANDALT r\STAR{\mvar{i}..\mvar{j}} &\equiv
  \begin{cases}
    b \ANDALT r &\text{if~} i\le 1\le j\\
    \0 &\text{else}\\
  \end{cases}\\
  b \ANDALT r\EQUAL{\mvar{i}..\mvar{j}} &\equiv
  \begin{cases}
    b \ANDALT r &\text{if~} i\le 1\le j\\
    \0 &\text{else}\\
  \end{cases}\\
  b \ANDALT r\GOTO{\mvar{i}..\mvar{j}} &\equiv
  \begin{cases}
    b \ANDALT r &\text{if~} i\le 1\le j\\
    \0 &\text{else}\\
  \end{cases}\\
  b \ANDALT \ratgroup{r_1 \FUSION \ldots \FUSION r_n}& \equiv b \ANDALT r_1 \ANDALT \ldots \ANDALT r_n \\
\end{align*}

\subsection{Simplifications for Eventual and Universal Formul\ae}
\label{sec:eventunivrew}

The class of \textit{pure eventuality} and \textit{purely universal}
formul\ae{} are described in section~\ref{sec:eventuniv}.

In the following rewritings, we use the following
notation to distinguish the class of subformul\ae:

\begin{center}
\begin{tabular}{rl}
\hline
$f,\,f_i,\,g,\,g_i$ & any PSL formula \\
$e,\,e_i$           & a pure eventuality \\
$u,\,u_i$           & a purely universal formula \\
$q,\,q_i$           & a pure eventuality that is also purely universal \\
\hline
\end{tabular}
\end{center}

\begin{align*}
  \F e &\equiv e & f \U e &\equiv e & e \M f &\equiv e\AND f \\
  \G u &\equiv u & f \R u &\equiv u &  u \W f &\equiv u\OR f \\
  \X q &\equiv q & q \AND \X f &\equiv \X(q \AND f) & q\OR \X f &\equiv \X(q \OR f)
\end{align*}
\begin{align*}
  \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)\OR q_1 \OR \ldots \OR q_p)&\equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)\OR q_1 \OR \ldots q_p \\
\intertext{Finally the following rule is applied only when no other
    terms are present in the OR arguments:}
  \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g_1) \OR \ldots \OR \G\F(g_m)
  \OR q_1 \OR \ldots \OR q_p
   &\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots\OR g_m) \OR q_1\OR \ldots q_p)
\end{align*}

\subsection{Simplifications Based on Implications}
\label{sec:syntimpl}

The following rewriting rules are performed only when we can prove
that some subformula $f$ implies another subformula $g$.  Showing such
implication can be done in two ways:
\begin{description}
\item[Syntactic Implication Checks] were initially proposed
  by~\citet{somenzi.00.cav}.  This detection is enabled by the
  ``\verb|ltl_simplifier_options::synt_impl|'' option.  This is a
  cheap way to detect implications, but it may miss some.  The rules
  we implement are described in Annex~\ref{ann:syntimpl}.

\item[Language Containment Checks] were initially proposed
  by~\citet{tauriainen.03.a83}.  This detection is enabled by the
  ``\verb|ltl_simplifier_options::containment_checks|'' option.
\end{description}

In the following rewritings rules, $f\simp g$ means that $g$ was
proved to be implied by $f$ using either of the above two methods.
Additionally, implications denoted by $f\Simp g$ are only checked
if the ``\verb|ltl_simplifier_options::containment_checks_stronger|''
option is set (otherwise the rewriting rule is not applied).

\begin{equation*}
\begin{array}{cccr@{\,}l}
\text{if}& f\simp g        &\text{then}& f\OR g &\equiv g \\
\text{if}& f\simp g        &\text{then}& f\AND g &\equiv f \\
\text{if}& f\simp \NOT g   &\text{then}& f\OR g &\equiv \1 \\
\text{if}& f\simp \NOT g   &\text{then}& f\AND g &\equiv \0 \\
\text{if}& f\simp g        &\text{then}& f\U g &\equiv g \\
\text{if}& (f\U g)\Simp g  &\text{then}& f\U g &\equiv g \\
\text{if}& (\NOT f)\simp g &\text{then}& f\U g &\equiv \F g \\
\text{if}& f\simp g        &\text{then}& f\U (g \U h) &\equiv g \U h \\
\text{if}& f\simp g        &\text{then}& f\U (g \W h) &\equiv g \W h \\
\text{if}& f\simp g        &\text{then}& f\W g &\equiv g \\
\text{if}& (f\W g)\Simp g  &\text{then}& f\W g &\equiv g \\
\text{if}& (\NOT f)\simp g &\text{then}& f\W g &\equiv \1 \\
\text{if}& f\simp g        &\text{then}& f\W (g \W h) &\equiv g \W h \\
\text{if}& g\simp f        &\text{then}& f\R g &\equiv g \\
\text{if}& g\simp \NOT f   &\text{then}& f\R g &\equiv \G g \\
\text{if}& g\simp f        &\text{then}& f\R (g \R h) &\equiv g \R h \\
\text{if}& g\simp f        &\text{then}& f\R (g \M h) &\equiv g \M h \\
\text{if}& f\simp g        &\text{then}& f\R (g \R h) &\equiv f \R h \\
\text{if}& g\simp f        &\text{then}& f\M g &\equiv g \\
\text{if}& g\simp \NOT f   &\text{then}& f\M g &\equiv \0 \\
\text{if}& g\simp f        &\text{then}& f\M (g \M h) &\equiv g \M h \\
\text{if}& f\simp g        &\text{then}& f\M (g \M h) &\equiv f \M h \\
\text{if}& f\simp g        &\text{then}& f\M (g \R h) &\equiv f \M h \\
\end{array}
\end{equation*}


\appendix
\chapter{Syntactic Implications}\label{ann:syntimpl}

Syntactic implications are used for the rewriting of
Section~\ref{sec:syntimpl}.  The rules presented bellow extend those
first presented by~\citet{somenzi.00.cav}.

A few words about implication first.  For two PSL formul\ae{} $f$ and
$g$, we say that $f\implies g$ if $\forall\sigma,\,(\sigma\vDash
f)\implies(\sigma\vDash g)$.  For two rational formul\ae{} $f$ and
$g$, we say that $f\implies g$ if $\forall\pi,\,(\pi\VDash
f)\implies(\pi\VDash g)$.

The recursive rules for syntactic implication are rules are described
in table~\ref{tab:syntimpl}, in which $\simp$ denotes the syntactic
implication, $f$, $f_1$, $f_2$, $g$, $g_1$ and $g_2$ designate any PSL
formula in negative normal form, and $f_U$ and $g_E$ designate a
purely universal formula and a pure eventuality.

The form on the left of the table syntactically implies the form on
the top of the table if the condition in the corresponding cell holds.

Note that a given formula may match several forms, and require
multiple recursive tests.  To limit the number of recursive calls,
some rules have been removed when they are already implied by other
rules.

For instance it one would legitimately expect the rule ``$\F f \simp
\F g$ \textit{if} $f\simp g$'' to appear in the table.  However in
that case $\F g$ is pure eventuality, so we can reach the same
conclusion by chaining two rules: ``$\F f \simp \underbrace{\F
  g}_{g_E}$ \textit{if} $f\simp \underbrace{\F g}_{g_E}$'' and then
``$f \simp \F g$ \textit{if} $f\simp g$''.

The rules from table~\ref{tab:syntimpl} should be completed by the
following cases, where $f_b$ and $g_b$ designate Boolean formul\ae{}:
\begin{center}
\begin{tabular}{rl}
we have                       & if                                    \\
\hline
$f\simp \1$                   & always                                \\
$\0\simp g$                   & always                                \\
$f_b \simp g_b$               & $\mathrm{BDD}(f_b)\land \mathrm{BDD}(g_b) =
                                \mathrm{BDD}(f_b)$                    \\
\end{tabular}
\end{center}

\begin{sidewaystable}
\footnotesize
\def\bone#1#2{$\phantom{{}\land{}} #1\simp #2$}
\def\bor#1#2#3#4{$\begin{aligned}#1 &\simp #2 \\{}\lor #3 &\simp #4\end{aligned}$}
\def\band#1#2#3#4{$\begin{aligned}#1 &\simp #2 \\{}\land #3 &\simp #4\end{aligned}$}
\def\banD#1#2#3#4#5#6{$\begin{aligned}#1 &\simp #2 \\{}\land #3 &\simp #4\\{}\land #5 &\simp #6\end{aligned}$}

\begin{center}
\begin{tabular}{|c||c|c|c|c|c|c|c|c|c|c|c|}
\hline
$\simp$       & $g$                   & $g_E$        & $\X g$       & $g_1\U g_2$               & $g_1\W g_2$               & $g_1 \R g_2$                        & $g_1\M g_2$                         & $\F g$                & $\G g$        & $g_1\OR g_2$         & $g_1 \AND g_2$        \\
\hline
\hline
$f$           & $f=g$                 &              &              & \bone{f}{g_2}             & \bone{f}{g_2}             & \band{f}{g_1}{f}{g_2}               & \band{f}{g_1}{f}{g_2}               & \bone{f}{g}           &               & \bor{f}{g_1}{f}{g_2} & \band{f}{g_1}{f}{g_2} \\
\hline
$f_U$         &                       &              & $f_U\simp g$ &                           &                           &                                     &                                     &                       & $f_U \simp g$ &                      &                       \\
\hline
$\X f$        &                       & $f\simp g_E$ & $f\simp g$   &                           &                           &                                     &                                     &                       &               &                      &                       \\
\hline
$f_1\U f_2$   & \band{f_1}{g}{f_2}{g} &              &              & \band{f_1}{g_1}{f_2}{g_2} & \band{f_1}{g_1}{f_2}{g_2} & \banD{f_1}{g_1}{f_2}{g_1}{f_2}{g_2} & \banD{f_1}{g_1}{f_2}{g_1}{f_2}{g_2} & \bone{f_2}{g}         &               &                      &                       \\
\hline
$f_1\W f_2$   & \band{f_1}{g}{f_2}{g} &              &              & \band{f_1}{g_2}{f_2}{g_2} & \band{f_1}{g_1}{f_2}{g_2} & \banD{f_1}{g_1}{f_2}{g_1}{f_2}{g_2} &                                     & \band{f_1}{g}{f_2}{g} &               &                      &                       \\
\hline
$f_1\R f_2$   & \bone{f_2}{g}         &              &              &                           & \band{f_1}{g_2}{f_2}{g_1} & \band{f_1}{g_1}{f_2}{g_2}           & \band{f_2}{g_1}{f_2}{g_2}           & \bone{f_2}{g}         &               &                      &                       \\
\hline
$f_1\M f_2$   & \bone{f_2}{g}         &              &              & \band{f_1}{g_2}{f_2}{g_1} & \band{f_1}{g_2}{f_2}{g_1} & \band{f_1}{g_1}{f_2}{g_2}           & \band{f_1}{g_1}{f_2}{g_2}           & \bor{f_1}{g}{f_2}{g}  &               &                      &                       \\
\hline
$\F f$        &                       & $f\simp g_E$ &              &                           &                           &                                     &                                     &                       &               &                      &                       \\
\hline
$\G f$        & \bone{f}{g}           &              &              & \bone{f}{g_2}             & \bor{f}{g_1}{f}{g_2}      & \bone{f}{g_2}                       & \band{f}{g_1}{f}{g_2}               &                       &               &                      &                       \\
\hline
$f_1\OR f_2$  & \band{f_1}{g}{f_2}{g} &              &              &                           &                           &                                     &                                     &                       &               &                      &                       \\
\hline
$f_1\AND f_2$ & \bor{f_1}{g}{f_2}{g}  &              &              &                           &                           &                                     &                                     &                       &               &                      &                       \\
\hline
\end{tabular}
\end{center}
\caption{Recursive rules for syntactic implication.\label{tab:syntimpl}}
\end{sidewaystable}


\phantomsection % fix hyperlinks
\addcontentsline{toc}{chapter}{\bibname}
\bibliographystyle{plainnat}
\bibliography{tl}

\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
