f68f639e68
* src/ltlast/binop.cc, src/ltlast/binop.hh: Here. * doc/tl/tl.tex, src/ltltest/equals.test: Adjust.
1406 lines
59 KiB
TeX
1406 lines
59 KiB
TeX
\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}
|
|
|
|
|
|
% @SpotVersion@
|
|
\def\SpotVersion{0.7.1a}
|
|
|
|
%% ----------------------- %%
|
|
%% 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&\,\tsamp{(}\,\mathit{bformula}\,\tsamp{)} & \mid&\,\mathit{tformula}\,\msamp{\OR}\,\mathit{tformula} \\
|
|
\mid&\,\msamp{\NOT}\,\mathit{bformula} & \mid&\,\mathit{tformula}\,\msamp{\IMPLIES}\,\mathit{tformula} \\
|
|
\mid&\,\mathit{bformula}\,\msamp{\AND}\,\mathit{bformula} & \mid&\,\mathit{tformula}\,\msamp{\XOR}\,\mathit{tformula} \\
|
|
\mid&\,\mathit{bformula}\,\msamp{\OR}\,\mathit{bformula} & \mid&\,\mathit{tformula}\,\msamp{\EQUIV}\,\mathit{tformula} \\
|
|
\mid&\,\mathit{bformula}\,\msamp{\IMPLIES}\,\mathit{bformula} & \mid&\,\msamp{\X}\,\mathit{tformula}\\
|
|
\mid&\,\mathit{bformula}\,\msamp{\XOR}\,\mathit{bformula} & \mid&\,\msamp{\F}\,\mathit{tformula}\\
|
|
\mid&\,\mathit{bformula}\,\msamp{\EQUIV}\,\mathit{bformula} & \mid&\,\msamp{\G}\,\mathit{tformula}\\
|
|
\mathit{rformula} ::=&\, \mathit{bformula} & \mid&\,\mathit{tformula}\,\msamp{\U}\,\mathit{tformula} \\
|
|
\mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}} & \mid&\,\mathit{tformula}\,\msamp{\W}\,\mathit{tformula} \\
|
|
\mid&\,\mathit{rformula}\msamp{\OR}\mathit{rformula} & \mid&\,\mathit{tformula}\,\msamp{\R}\,\mathit{tformula} \\
|
|
\mid&\,\mathit{rformula}\msamp{\AND}\mathit{rformula} & \mid&\,\mathit{tformula}\,\msamp{\M}\,\mathit{tformula} \\
|
|
\mid&\,\mathit{rformula}\msamp{\ANDALT}\mathit{rformula} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\Asuffix}\,\mathit{tformula}\\
|
|
\mid&\,\mathit{rformula}\msamp{\CONCAT}\mathit{rformula} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\AsuffixEQ}\,\mathit{tformula}\\
|
|
\mid&\,\mathit{rformula}\msamp{\FUSION}\mathit{rformula} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\Esuffix}\,\mathit{tformula}\\
|
|
\mid&\,\mathit{rformula}\msamp{\STAR{\mvar{i}..\mvar{j}}} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\,\msamp{\EsuffixEQ}\,\mathit{tformula} \\
|
|
\mid&\,\mathit{rformula}\msamp{\PLUS} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}} \\
|
|
\mid&\,\mathit{rformula}\msamp{\EQUAL{\mvar{i}..\mvar{j}}} & \mid&\,\tsamp{\{}\mathit{rformula}\tsamp{\}}\msamp{\NOT} \\
|
|
\mid&\,\mathit{rformula}\msamp{\GOTO{\mvar{i}..\mvar{j}}} \\
|
|
\end{align*}
|
|
|
|
\section{Operator precedence}
|
|
|
|
\ltltodo[inline]{Document operator precedence.}
|
|
|
|
\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|'.
|
|
|
|
|
|
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*}
|
|
|
|
\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:
|