1840 lines
86 KiB
TeX
1840 lines
86 KiB
TeX
\RequirePackage[l2tabu, orthodox]{nag}
|
||
\documentclass[a4paper,twoside,10pt,DIV=12]{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} % vDash
|
||
\usepackage{wasysym}
|
||
\usepackage{stmaryrd}
|
||
%\usepackage{showlabels}
|
||
\usepackage{tabulary}
|
||
\usepackage[numbers]{natbib}
|
||
\usepackage{rotating}
|
||
\usepackage{booktabs}
|
||
\usepackage{tikz}
|
||
\usepackage{calc}
|
||
\usetikzlibrary{backgrounds}
|
||
\usetikzlibrary{shadows}
|
||
\usetikzlibrary{arrows}
|
||
\pgfdeclarelayer{background}
|
||
\pgfdeclarelayer{foreground}
|
||
\pgfsetlayers{background,main,foreground}
|
||
|
||
\addtokomafont{caption}{\small}
|
||
\setkomafont{captionlabel}{\sffamily\bfseries}
|
||
|
||
% 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}}
|
||
|
||
\newcommand{\uni}[1]{\texttt{\small U+#1}}
|
||
|
||
% For tables.
|
||
\newcommand{\newfootnotemark}[1]{\addtocounter{footnote}{#1}\footnotemark[\value{footnote}]}
|
||
\newcommand{\newfootnotetext}[2]{\addtocounter{footnote}{#1}\footnotetext[\value{footnote}]{#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{\ORALTTT}{\mathbin{\texttt{+}}}
|
||
\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{\STARBIN}{\mathbin{\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{\sere}[1]{\texttt{\{}#1\texttt{\}}}
|
||
\newcommand{\nsere}[1]{\texttt{!\{}#1\texttt{\}}}
|
||
\newcommand{\nsereMarked}[1]{\texttt{!+\{}#1\texttt{\}}}
|
||
\newcommand{\seren}[1]{\texttt{\{}#1\texttt{\}!}}
|
||
|
||
% rewriting rules that enlarge the formula
|
||
\newcommand{\equiV}{\stackrel{\star}{\equiv}}
|
||
% rewriting rules that favors event/univ
|
||
\newcommand{\equivEU}{\stackrel{\blacktriangleup}{\equiv}}
|
||
\newcommand{\equivNeu}{\stackrel{\smalltriangledown}{\equiv}}
|
||
|
||
% marked rewriting rules
|
||
\newcommand{\equivM}{\stackrel{\dag}{\equiv}}
|
||
|
||
\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}
|
||
|
||
% Tikz
|
||
\tikzstyle{annote}=[overlay,thick,<-,red,>=stealth']
|
||
|
||
|
||
% Make sure we can compile this file even without use the version
|
||
% supplied by the Makefile.
|
||
\ifdefined\SpotVersion\else
|
||
\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\}$ denote 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=\bigcup_{n\in\N}A^n$ denotes the set of all finite sequences.
|
||
The length of any sequence $\sigma$ is noted $|\sigma|$, with
|
||
$|\sigma|\in\N\cup\{\omega\}$.
|
||
|
||
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, should be
|
||
interpreted on behaviors (or executions, or scenarios) of the system
|
||
to verify. In model checking we want to ensure that a formula (the
|
||
property to verify) holds on all possible behaviors of the system.
|
||
|
||
If we model the system as some sort of giant automaton (e.g., a Kripke
|
||
structure) 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 by an affectation
|
||
of some proposition variables that we will call \emph{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 write $\sigma \vDash \varphi$ (read as $\sigma$ is a
|
||
model of $\varphi$).
|
||
|
||
When a formula $\varphi$ holds on an \emph{finite} sequence $\sigma$,
|
||
we write $\sigma \VDash \varphi$.
|
||
|
||
\chapter{Temporal Syntax \& Semantics}
|
||
|
||
\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 constructs specific to the underlying formalism,
|
||
and still regard the resulting construction as 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}{cccccrl}
|
||
& preferred & \multicolumn{2}{c}{other supported}&& \multicolumn{2}{l}{UTF8 characters supported}\\
|
||
operation & syntax & \multicolumn{2}{c}{syntaxes} && preferred & others\\
|
||
\cmidrule(r){1-5} \cmidrule(l){6-7}
|
||
negation & $\NOT f$ & $\NOTALT f$ & & & $\lnot$ \uni{00AC} \\
|
||
disjunction & $f\OR g$ & $f\ORALT g$ & $f\ORALTT g$ & $f\ORALTTT g$ & $\lor$ \uni{2228} & $\cup$ \uni{222A}\\
|
||
conjunction & $f\AND g$ & $f\ANDALT g$ & $f\ANDALTT g$ & $f\STARBIN g$\rlap{\footnotemark} & $\land$ \uni{2227} & $\cap$ \uni{2229}\\
|
||
implication & $f\IMPLIES g$ & $f\IMPLIESALT g$ & $f\IMPLIESALTT g$ & & $\limplies$ \uni{2192} & $\rightarrow$ \uni{27F6}, $\Rightarrow$ \uni{21D2} \uni{27F9} \\
|
||
exclusion & $f\XOR g$ & $f\XORALT g$ & & & $\oplus$ \uni{2295} \\
|
||
equivalence & $f\EQUIV g$ & $f\EQUIVALT g$ & $f\EQUIVALTT g$ & & $\liff$ \uni{2194} & $\Leftrightarrow$ \uni{21D4}\\
|
||
\end{tabular}
|
||
\end{center}
|
||
\footnotetext{The $\STARALT$-form of the conjunction operator
|
||
(allowing better compatibility with Wring and VIS) may only used in
|
||
temporal formul\ae. Boolean expressions that occur inside SERE (see
|
||
Section~\ref{sec:sere}) may not use this form because the $\STARALT$
|
||
symbol is used as the Kleen star.}
|
||
|
||
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.
|
||
|
||
When using UTF-8 input, a \samp{=0} that follow a single-letter atomic
|
||
proposition may be replaced by a combining overline \uni{0305} or a
|
||
combining overbar \uni{0304}. When instructed to emit UTF-8, Spot
|
||
will output \samp{$\bar{\mathtt{a}}$} using a combining overline
|
||
instead of \samp{$\lnot$a} for any single-letter atomic proposition.
|
||
|
||
\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*}
|
||
\sigma\vDash \NOT f &\iff (\sigma\nvDash f) \\
|
||
\sigma\vDash f\AND g &\iff (\sigma\vDash f)\land(\sigma\vDash g) \\
|
||
\sigma\vDash f\OR g &\iff (\sigma\vDash f)\lor(\sigma\vDash g) \\
|
||
\sigma\vDash f\IMPLIES g &\iff
|
||
(\sigma\nvDash f)\lor(\sigma\vDash g)\\
|
||
\sigma\vDash f\XOR g &\iff
|
||
((\sigma\vDash f)\land(\sigma\nvDash g))\lor
|
||
((\sigma\nvDash f)\land(\sigma\vDash g))\\
|
||
\sigma\vDash f\EQUIV g &\iff
|
||
((\sigma\vDash f)\land(\sigma\vDash g))\lor
|
||
((\sigma\nvDash f)\land(\sigma\nvDash g))
|
||
\end{align*}
|
||
|
||
\subsection{Trivial Identities (Occur Automatically)}
|
||
|
||
Trivial identities are applied every time an expression is
|
||
constructed. This means for instance that there is not way to
|
||
construct the expression \samp{$\NOT\NOT a$} in Spot, such an attempt
|
||
will always yield the expression \samp{$a$}.
|
||
|
||
% These first rules are for the \samp{!} and \samp{->} operators.
|
||
|
||
\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()=' function 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}\label{sec:ltlops}
|
||
|
||
Given two temporal formul\ae{} $f$, and $g$, the following
|
||
temporal operators can be used to construct another temporal formula.
|
||
|
||
\begin{center}
|
||
\begin{tabular}{cccrl}
|
||
& preferred & \multicolumn{1}{c}{other supported} & \multicolumn{2}{l}{UTF8 characters supported} \\
|
||
operator & syntax & \multicolumn{1}{c}{syntaxes} & preferred & others \\
|
||
\cmidrule(r){1-3} \cmidrule(l){4-5}
|
||
Next & $\X f$ & $\XALT f$ & $\Circle$ \uni{25CB} & $\Circle$ \uni{25EF}\\
|
||
Eventually & $\F f$ & $\FALT f$ & $\Diamond$ \uni{25C7} & $\Diamond$ \uni{22C4} \uni{2662}\\
|
||
Always & $\G f$ & $\GALT f$ & $\Square$ \uni{25A1} & $\Square$ \uni{2B1C} \uni{25FB}\\
|
||
(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 \sigma^{1..}\vDash f\\
|
||
\sigma\vDash \F f &\iff \exists i\in \N,\, \sigma^{i..}\vDash f\\
|
||
\sigma\vDash \G f &\iff \forall i\in \N,\, \sigma^{i..}\vDash f\\
|
||
\sigma\vDash f\U g &\iff \exists j\in\N,\,
|
||
\begin{cases}
|
||
\forall i<j,\, \sigma^{i..}\vDash f\\
|
||
\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*}
|
||
|
||
Appendix~\ref{sec:ltl-equiv} explains how to rewrite the above LTL
|
||
operators using only $\X$ and one operator chosen among $\U$, $\W$,
|
||
$\M$,and $\R$. This could be useful to understand the operators $\R$,
|
||
$\M$, and $\W$ if you are only familiar with $\X$ and $\U$.
|
||
|
||
\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{Unabbreviations}
|
||
|
||
The `\verb=unabbreviate_ltl()=' function 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*}
|
||
|
||
The `\verb=unabbreviate_wm()=` function removes only the $\W$ and $\M$
|
||
operators using the following two rewritings:
|
||
\begin{align*}
|
||
f \W g&\equiv g \R (g \OR f)\\
|
||
f \M g&\equiv g \U (g \AND f)
|
||
\end{align*}
|
||
Among all the possible rewritings (see Appendix~\ref{sec:ltl-equiv})
|
||
those two were chosen because they are easier to translate in a
|
||
tableau construction~\cite[Fig.~11]{duret.11.vecos}.
|
||
|
||
\section{SERE Operators}\label{sec:sere}
|
||
|
||
The ``SERE'' acronym will be translated to different word depending on
|
||
the source. It can mean either ``\textit{Sequential Extended Regular
|
||
Expression}''~\citep{eisner.06.psl,psl.04.lrm}, ``\textit{Sugar
|
||
Extended Regular Expression}''~\citep{beer.01.cav}, or
|
||
``\textit{Semi-Extended Regular Expression}''~\citep{eisner.08.hvc}.
|
||
In any case, the intent is the same: regular expressions with
|
||
traditional operations (union `$\OR$', concatenation `$\CONCAT$',
|
||
Kleen star `$\STAR{}$') are extended with operators such as
|
||
intersection `$\ANDALT$', and fusion `$\FUSION$'.
|
||
|
||
Any Boolean formula (section~\ref{def:boolform}) is a SERE. SERE can
|
||
be further combined with the following operators, where $f$ and $g$
|
||
denote arbitrary SERE.
|
||
|
||
\begin{center}
|
||
\begin{tabular}{cccccrl}
|
||
& preferred & \multicolumn{2}{c}{other supported} && \multicolumn{2}{l}{UTF8 characters supported}\\
|
||
operation & syntax & \multicolumn{2}{c}{syntaxes} && preferred & others \\
|
||
\cmidrule(r){1-5}\cmidrule(l){6-7}
|
||
empty word & $\eword$ \\
|
||
union & $f\OR g$ & $f\ORALT g$ & $f\ORALTT g$ & $f\ORALTTT g$ && $\lor$ \uni{2228} $\cup$ \uni{222A}\\
|
||
intersection & $f\ANDALT g$ & $f\ANDALTT g$ &&& $\cap$ \uni{2229} & $\land$ \uni{2227}\\
|
||
NLM intersection\footnotemark & $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}}$\\
|
||
\llap{un}bounded repetition & $f\STAR{\mvar{i}..}$
|
||
& $f\STAR{\mvar{i}:}$
|
||
& $f\STAR{\mvar{i} to}$
|
||
& $f\STAR{\mvar{i},}$\\
|
||
\end{tabular}
|
||
\end{center}
|
||
|
||
\footnotetext{\emph{Non-Length-Matching} interesction.}
|
||
|
||
The character \samp{\$} or the string \samp{inf} can also be used as
|
||
value for $\mvar{j}$ in the above operators to denote an unbounded
|
||
range.\footnote{SVA uses \samp{\$} while PSL uses \samp{inf}.} For
|
||
instance `$a\STAR{i,\texttt{\$}}$', `$a\STAR{i\texttt{:inf}}$' and
|
||
`$a\STAR{i..}$' all represent the same SERE.
|
||
|
||
\subsection{Semantics}
|
||
|
||
The following semantics assume that $f$ and $g$ are two SEREs, while
|
||
$a$ is an atomic proposition.
|
||
|
||
{\allowdisplaybreaks
|
||
\begin{align*}
|
||
\sigma\nVDash \0 &\\
|
||
\sigma\VDash \1 & \iff |\sigma|=1\\
|
||
\sigma\VDash \eword & \iff |\sigma|=0 \\
|
||
\sigma\VDash a & \iff \sigma(0)(a)=1 \land |\sigma|=1\\
|
||
\sigma\VDash f\OR g &\iff (\sigma\VDash f) \lor (\sigma\VDash g) \\
|
||
\sigma\VDash f\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}
|
||
\end{align*}}
|
||
|
||
Notes:
|
||
\begin{itemize}
|
||
\item The semantics of $\ANDALT$ and $\AND$ coincide if both
|
||
operands are Boolean formul\ae.
|
||
\item The SERE $f\FUSION g$ will never hold on $\eword$,
|
||
regardless of the value of $f$ and $g$. For instance
|
||
$a\STAR{}\FUSION b\STAR{}$ is actually equivalent to
|
||
$a\STAR{}\CONCAT\sere{a\ANDALT b}\CONCAT b\STAR{}$.
|
||
\end{itemize}
|
||
|
||
\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 \emph{some} are performed from right to left when writing
|
||
it for output. $b$ must be a Boolean formula.
|
||
|
||
\begin{align*}
|
||
b\GOTO{\mvar{i}..\mvar{j}} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..\mvar{j}} &
|
||
b\EQUAL{\mvar{i}..\mvar{j}} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..\mvar{j}}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..} \\
|
||
b\GOTO{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..} &
|
||
b\EQUAL{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..}\text{~if~}i>0 \\
|
||
&& b\EQUAL{0..} &\equiv \1\STAR{0..}
|
||
\end{align*}
|
||
\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 SERE, while $b$,
|
||
$b_1$, $b_2$ are assumed to be Boolean formul\ae.
|
||
|
||
\begin{align*}
|
||
\0\STAR{0..\mvar{j}} &\equiv \eword &
|
||
\0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 \\
|
||
\eword\STAR{\var{i}..\mvar{j}} &\equiv \eword&
|
||
f\STAR{\mvar{i}..\mvar{j}}\STAR{\mvar{k}..\mvar{l}} &\equiv f\STAR{\mvar{ik}..\mvar{jl}}\text{~if~}i(k+1)\le jk+1 \\
|
||
f\STAR{0}&\equiv \eword &
|
||
f\STAR{1}&\equiv f\\
|
||
\end{align*}
|
||
|
||
\noindent
|
||
The following rules are all valid with the two arguments swapped.
|
||
%(Even for the non-commutative operators \samp{$\CONCAT$} and
|
||
%\samp{$\FUSION$}.)
|
||
|
||
\begin{align*}
|
||
\0\AND f &\equiv \0 &
|
||
\0\ANDALT f &\equiv \0 &
|
||
\0\OR f &\equiv f &
|
||
\0 \FUSION f &\equiv \0 &
|
||
\0 \CONCAT f &\equiv \0 \\
|
||
\1\AND f&\equiv
|
||
\begin{cases}
|
||
1\mathrlap{\text{~if~} \varepsilon\VDash f} \\
|
||
f\mathrlap{\text{~if~} \varepsilon\nVDash f} \\
|
||
\end{cases} &
|
||
\1\ANDALT b &\equiv b &
|
||
\1\OR b &\equiv \1 &
|
||
\1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\
|
||
&&
|
||
\STAR{} \AND f &\equiv f &
|
||
\STAR{} \OR f &\equiv \1\mathrlap{\STAR{}} &
|
||
&&
|
||
\STAR{} \CONCAT f &\equiv \STAR{}\mathrlap{\text{~if~}\varepsilon\VDash f}& \\
|
||
\eword\AND f &\equiv f &
|
||
\eword\ANDALT f &\equiv
|
||
\begin{cases}
|
||
\mathrlap{\eword\text{~if~} \varepsilon\VDash f} \\
|
||
\0\mathrlap{\phantom{\STAR{}}\text{~if~} \varepsilon\nVDash f} \\
|
||
\end{cases} &
|
||
&&
|
||
\eword \FUSION f &\equiv \0 &
|
||
\eword \CONCAT f &\equiv f\\
|
||
f\AND f &\equiv f&
|
||
f\ANDALT f &\equiv f &
|
||
f\OR f &\equiv f&
|
||
&&
|
||
f\CONCAT f&\equiv f\STAR{2}\\
|
||
b_1 \AND b_2 &\equiv b_1\ANDALT b_2 &
|
||
&&
|
||
&&
|
||
b_1:b_2 &\equiv b_1\ANDALT b_2 &
|
||
f\STAR{\mvar{i}..\mvar{j}}\CONCAT f&\equiv f\STAR{\mvar{i+1}..\mvar{j+1}}\\
|
||
&&
|
||
&&
|
||
&&
|
||
&&
|
||
\mathllap{f\STAR{\mvar{i}..\mvar{j}}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar{i+k}..\mvar{j+l}}\\
|
||
\end{align*}
|
||
|
||
\section{SERE-LTL Binding Operators}
|
||
|
||
The following operators combine a SERE $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}\\
|
||
\midrule
|
||
(universal) suffix implication
|
||
& $\sere{r}\Asuffix{} f$
|
||
& $\sere{r}\AsuffixALT{} f$
|
||
& $\sere{r}\texttt{(}f\texttt{)}$
|
||
\\
|
||
existential suffix implication
|
||
& $\sere{r}\Esuffix{} f$
|
||
\\
|
||
weak closure
|
||
& $\sere{r}$
|
||
\\
|
||
negated weak closure
|
||
& $\nsere{r}$
|
||
\\
|
||
\end{tabular}
|
||
\end{center}
|
||
|
||
For technical reasons, the negated weak closure is actually implemented as
|
||
an operator, even if it is syntactically and semantically equal to the
|
||
combination of $\NOT$ and $\sere{r}$.
|
||
|
||
UTF-8 input may combine one box or diamond character from
|
||
section~\ref{sec:ltlops} with one arrow character from
|
||
section~\ref{sec:boolops} to replace the operators $\Asuffix$,
|
||
$\Esuffix$, as well as the operators $\AsuffixEQ$ and $\EsuffixEQ$
|
||
that will be defined in \ref{sec:pslsugar}. Additionally,
|
||
$\AsuffixALT$ may be replaced by $\mapsto$ \uni{21A6}, and
|
||
$\AsuffixALTEQ$ by $\Mapsto$ \uni{2907}.
|
||
|
||
\subsection{Semantics}
|
||
|
||
The following semantics assume that $r$ is a SERE,
|
||
while $f$ is a PSL formula.
|
||
|
||
\begin{align*}
|
||
\sigma\vDash \sere{r}\Esuffix f &\iff \exists k\ge 0, (\sigma^{0..k}\VDash r)\land(\sigma^{k..}\vDash f)\\
|
||
\sigma\vDash \sere{r}\Asuffix f &\iff \forall k\ge 0, (\sigma^{0..k}\VDash r)\limplies (\sigma^{k..}\vDash f)\\
|
||
\sigma\vDash \sere{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 \nsere{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 \sere{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{$\sere{a\PLUS{}\CONCAT\NOT
|
||
a}$} even though it never sees \samp{$\NOT a$}. The same sequence
|
||
is not a model of \samp{$\sere{a\PLUS{}\CONCAT\NOT
|
||
a\CONCAT(a\STAR{}\ANDALT(a\STAR{}\CONCAT\NOT a\CONCAT
|
||
a\STAR{}))}$} because this SERE does accept any word.
|
||
|
||
Note that the semantics of $\sere{r}$ comes from the
|
||
$\mathsf{cl}(\cdot)$ operator defined by~\citet{dax.09.atva}. This
|
||
differs from the interpretation of a SERE in the context of a temporal
|
||
formula given by the PSL standard~\citep[Appendix~B.3.1.1.2,
|
||
item~7]{psl.04.lrm}: the $\mathit{cl}(\cdot)$ semantics accepts more
|
||
words.
|
||
|
||
\subsection{Syntactic Sugar}\label{sec:pslsugar}
|
||
|
||
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. Except the one marked with $\equivM$, the opposite
|
||
rewritings are also preformed on output to ease reading.
|
||
|
||
\begin{align*}
|
||
\sere{r}\EsuffixEQ f &\equiv \sere{r\CONCAT\1}\Esuffix f &
|
||
\sere{r}\AsuffixEQ f &\equiv \sere{r\CONCAT\1}\Asuffix f\\
|
||
\seren{r} &\equiv \sere{r}\Esuffix \1 &
|
||
\sere{r}\AsuffixALTEQ f &\equivM \sere{r\CONCAT\1}\Asuffix f\\
|
||
\end{align*}
|
||
|
||
$\AsuffixEQ$ and $\AsuffixALTEQ$ are synonyms in the same way as
|
||
$\Asuffix$ and $\AsuffixALT$ are.
|
||
|
||
The $\seren{r}$ operator is a \emph{strong closure} operator.
|
||
|
||
\subsection{Trivial Identities (Occur Automatically)}
|
||
|
||
For any PSL formula $f$, any SERE $r$, and any Boolean
|
||
formula $b$, the following rewritings are systematically performed
|
||
(from left to right).
|
||
|
||
\begin{align*}
|
||
\sere{\0}\Asuffix f &\equiv \1
|
||
& \sere{\0}\Esuffix f &\equiv \0
|
||
& \sere{\0} & \equiv \0
|
||
& \nsere{\0} & \equiv \1 \\
|
||
\sere{\1}\Asuffix f &\equiv f
|
||
& \sere{\1}\Esuffix f &\equiv f
|
||
& \sere{\1} & \equiv \1
|
||
& \nsere{\1} & \equiv \0 \\
|
||
\sere{\eword}\Asuffix f&\equiv \1
|
||
& \sere{\eword}\Esuffix f&\equiv \0
|
||
& \sere{\eword} & \equiv \0
|
||
& \nsere{\eword} & \equiv \1 \\
|
||
\sere{b}\Asuffix f&\equiv (\NOT{b})\OR f
|
||
& \sere{b}\Esuffix f&\equiv b\AND f
|
||
& \sere{b} &\equiv b
|
||
& \nsere{b} &\equiv \NOT b\\
|
||
\sere{r}\Asuffix \1&\equiv \1
|
||
& \sere{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{sere} ::={}&\mathit{bformula} & \mid{}&\mathit{tformula}\,\msamp{\R}\,\mathit{tformula} \\
|
||
\mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}} & \mid{}&\mathit{tformula}\,\msamp{\M}\,\mathit{tformula} \\
|
||
\mid{}&\mathit{sere}\msamp{\OR}\mathit{sere} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\Asuffix}\,\mathit{tformula}\\
|
||
\mid{}&\mathit{sere}\msamp{\AND}\mathit{sere} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\AsuffixEQ}\,\mathit{tformula}\\
|
||
\mid{}&\mathit{sere}\msamp{\ANDALT}\mathit{sere} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\Esuffix}\,\mathit{tformula}\\
|
||
\mid{}&\mathit{sere}\msamp{\CONCAT}\mathit{sere} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\EsuffixEQ}\,\mathit{tformula} \\
|
||
\mid{}&\mathit{sere}\msamp{\FUSION}\mathit{sere} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}} \\
|
||
\mid{}&\mathit{sere}\msamp{\STAR{\mvar{i}..\mvar{j}}} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\msamp{\NOT} \\
|
||
\mid{}&\mathit{sere}\msamp{\PLUS} \\
|
||
\mid{}&\mathit{sere}\msamp{\EQUAL{\mvar{i}..\mvar{j}}} \\
|
||
\mid{}&\mathit{sere}\msamp{\GOTO{\mvar{i}..\mvar{j}}} \\
|
||
\end{align*}
|
||
|
||
\section{Operator precedence}
|
||
|
||
The following operator precedence describes the current parser of
|
||
Spot. It has not always been this way. Especially, all operators
|
||
were left associative until version 0.9, when we changed the
|
||
associativity of $\IMPLIES$, $\EQUIV$, $\U$, $\R$, $\W$, and $\M$ to get closer
|
||
to the PSL standard~\cite{psl.04.lrm,eisner.06.psl}.
|
||
|
||
\begin{center}
|
||
\begin{tabular}{clc}
|
||
assoc. & operators & priority \\
|
||
\midrule
|
||
right & $\Asuffix,\,\AsuffixEQ,\,\Esuffix,\,\EsuffixEQ$ & \tikz[remember picture,baseline]\node (lowest){lowest}; \\
|
||
left & $\CONCAT$ & \\
|
||
left & $\FUSION$ & \\
|
||
right & $\IMPLIES,\,\EQUIV$ & \\
|
||
left & $\XOR$ & \\
|
||
left & $\OR$ & \\
|
||
left & $\AND,\,\ANDALT$ & \\
|
||
right & $\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}$ & \tikz[remember picture,baseline]\node (highest){highest}; \\
|
||
\end{tabular}
|
||
\end{center}
|
||
\begin{tikzpicture}[remember picture,overlay,>=stealth',semithick]
|
||
\draw[->] (lowest) -- (highest);
|
||
\end{tikzpicture}
|
||
|
||
Beware that not all tools agree on the associativity of these
|
||
operators. For instance Spin, ltl2ba (same parser as spin), Wring,
|
||
psl2ba, Modella, and NuSMV all have $\U$ and $\R$ as left-associative,
|
||
while Goal (hence B<>chi store), LTL2AUT, and LTL2B<32>chi (from
|
||
JavaPathFinder) have $\U$ and $\R$ as right-associative. Vis and LBTT
|
||
have these two operators as non-associative (parentheses required).
|
||
Similarly the tools do not aggree on the associativity of $\IMPLIES$
|
||
and $\EQUIV$: some tools handle both operators as left-associative, or
|
||
both right-associative, other have only $\IMPLIES$ as right-associative.
|
||
|
||
|
||
\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
|
||
\label{property-methods}
|
||
\begin{tabulary}{.995\textwidth}{@{}lJ@{}}
|
||
\texttt{is\_boolean()}& Whether the formula uses only Boolean
|
||
operators.
|
||
\\\texttt{is\_sugar\_free\_boolean()}& Whether the formula uses
|
||
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
|
||
SERE operators. (Boolean operators are also allowed, provided
|
||
no SERE operator is negated.)
|
||
\\\texttt{is\_finite()}& Whether a SERE describes a finite
|
||
language (no unbounded stars), 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\_guarantee()}& Whether the formula is a syntactic
|
||
guarantee 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$ or $\nsere{r}$ operators.\newfootnotemark{1}
|
||
\\\texttt{accepts\_eword()}& Whether the formula accepts
|
||
$\eword$. (This can only be true for a SERE formula.)
|
||
\\\texttt{has\_lbt\_atomic\_props()}& Whether the atomic
|
||
propositions of the formula are all of the form ``\texttt{p}$nn$''
|
||
where $nn$ is a string of digits. This is required when converting
|
||
formula into LBT's format.\newfootnotemark{1}
|
||
\end{tabulary}
|
||
|
||
\newfootnotetext{-1}{These ``marked'' operators are used when
|
||
translating recurring $\Esuffix$ or $\nsere{r}$ operators. They are
|
||
rendered as $\EsuffixMarked$ and $\nsereMarked{r}$ and obey the same
|
||
simplification rules and properties as their unmarked counterpart
|
||
(except for the \texttt{is\_marked()} property).}
|
||
\newfootnotetext{1}{\url{http://www.tcs.hut.fi/Software/maria/tools/lbt/}}
|
||
|
||
|
||
\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$ denote any arbitrary formula and $\varphi_E$
|
||
(resp. $\varphi_U$) denote 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}
|
||
|
||
\begin{figure}[tbp]
|
||
\setcapindent{1em}
|
||
\begin{captionbeside}{
|
||
The temporal hierarchy of \citet{manna.87.podc} with their
|
||
associated classes of automata~\citep{cerna.03.mfcs}. The
|
||
formul\ae{} associated to each class are more than canonical
|
||
examples: they show the normal forms under which any LTL formula
|
||
of the class can be rewritten, assuming that $p,p_i,q,q_i$ denote
|
||
subformul\ae{} involving only Boolean operators, $\X$, and past
|
||
temporal operators (Spot does not support the
|
||
latter). \label{fig:hierarchy}}[o]
|
||
\centering
|
||
\begin{tikzpicture}
|
||
\draw[drop shadow,fill=white] (0,0) rectangle (6,7);
|
||
\path[fill=yellow!20] (0,6) -- (3,4.5) -- (0,3);
|
||
\path[fill=red!20] (6,6) -- (3,4.5) -- (6,3);
|
||
\path[fill=orange!20] (0,3) -- (3,4.5) -- (6,3) -- (3,1);
|
||
\path[fill=blue!40,fill opacity=.5] (0,0) -- (0,3) -- (4.5,0);
|
||
\path[fill=green!40,fill opacity=.5] (6,0) -- (1.5,0) -- (6,3);
|
||
\draw (0,0) rectangle (6,7);
|
||
|
||
\node[align=center] (rea) at (3,6) {Reactivity\\ $\bigwedge\G\F p_i\lor \F\G q_i$};
|
||
\node[align=center] (rec) at (1,4.5) {Recurrence\\ $\G\F p$};
|
||
\node[align=center] (per) at (5,4.5) {Persistence\\ $\F\G p$};
|
||
\node[align=center] (obl) at (3,2.85) {Obligation\\ $\bigwedge\G p_i\lor \F q_i$};
|
||
\node[align=center] (saf) at (1,1) {Safety\\ $\G p$};
|
||
\node[align=center] (gua) at (5,1) {Guarantee\\ $\F p$};
|
||
|
||
\node[align=right,below left] (det) at (-.2,6.7) {Deterministic\\B<EFBFBD>chi\\Automata};
|
||
\node[align=left,below right](weak) at (6.2,6.7) {Weak B<>chi\\Automata};
|
||
\node[align=left,right](wdba) at (6.2,4.3) {Weak\\Deterministic\\B<EFBFBD>chi\\Automata};
|
||
\node[align=left,above right](ter) at (6.2,1.7) {Terminal\\B<EFBFBD>chi\\Automata};
|
||
\node[align=right,above left](occ) at (-.2,2) {Terminal\\co-B<>chi\\Automata};
|
||
|
||
\node[above right] (buc) at (3.35,7) {General B<>chi Automata};
|
||
|
||
\draw[annote] (rec) -- (det);
|
||
\draw[annote] (per) -- (weak);
|
||
\draw[annote] (obl.east) -- (wdba.west);
|
||
\draw[annote] (gua.north) -- (ter.west);
|
||
\draw[annote] (saf) -- (occ);
|
||
\draw[annote] (rea.north) .. controls +(north:5mm) and +(west:5mm) .. (buc.west);
|
||
\end{tikzpicture}
|
||
\end{captionbeside}
|
||
\end{figure}
|
||
|
||
The hierarchy of linear temporal properties was introduced
|
||
by~\citet{manna.87.podc} and is illustrated on
|
||
Fig.~\ref{fig:hierarchy}. In the case of the LTL subset of the
|
||
hierarchy, a first syntactic characterization of the classes was
|
||
presented by~\citet{chang.92.icalp}, but other presentations have been
|
||
done including negation~\citep{cerna.03.mfcs} and weak
|
||
until~\citep{schneider.01.lpar}.
|
||
|
||
The following grammar rules extend the aforementioned work slightly by
|
||
dealing with PSL operators. These are the rules used by Spot to
|
||
decide upon construction to which class a formula belongs (see the
|
||
methods \texttt{is\_syntactic\_safety()},
|
||
\texttt{is\_syntactic\_guarantee()},
|
||
\texttt{is\_syntactic\_obligation()},
|
||
\texttt{is\_syntactic\_recurrence()}, and
|
||
\texttt{is\_syntactic\_persistence()} listed on
|
||
page~\pageref{property-methods}).
|
||
|
||
The symbols $\varphi_G$, $\varphi_S$, $\varphi_O$, $\varphi_P$,
|
||
$\varphi_R$ denote any formula belonging respectively to the
|
||
Guarantee, Safety, Obligation, Persistence, or Recurrence classes.
|
||
$\varphi_F$ denotes a finite LTL formula (the unnamed class at the
|
||
intersection of Safety and Guarantee formul\ae{} on
|
||
Fig.~\ref{fig:hierarchy}). $v$ denotes any variable, $r$ any SERE,
|
||
$r_F$ any bounded SERE (no loops), and $r_I$ any unbounded SERE.
|
||
|
||
\begin{align*}
|
||
\varphi_F ::={}& \0\mid\1\mid v\mid\NOT\varphi_F\mid\varphi_F\AND\varphi_F
|
||
\mid(\varphi_F\OR\varphi_F)\mid\varphi_F\EQUIV\varphi_F
|
||
\mid\varphi_F\XOR\varphi_F\mid\varphi_F\IMPLIES\varphi_F
|
||
\mid\X\varphi_F\\
|
||
\varphi_G ::={}& \varphi_F\mid \NOT\varphi_S\mid
|
||
\varphi_G\AND \varphi_G\mid (\varphi_G\OR \varphi_G)
|
||
\mid\varphi_S\IMPLIES\varphi_G\mid
|
||
\X\varphi_G \mid \F\varphi_G\mid
|
||
\varphi_G\U\varphi_G\mid \varphi_G\M\varphi_G\\
|
||
\mid{}& \sere{r_F}\mid
|
||
\sere{r}\Esuffix \varphi_G\mid
|
||
\sere{r_F}\Asuffix \varphi_G \\
|
||
\varphi_S ::={}& \varphi_F\mid \NOT\varphi_G\mid
|
||
\varphi_S\AND \varphi_S\mid (\varphi_S\OR \varphi_S)
|
||
\mid\varphi_G\IMPLIES\varphi_S\mid
|
||
\X\varphi_S \mid \G\varphi_S\mid
|
||
\varphi_S\R\varphi_S\mid \varphi_S\W\varphi_S\\
|
||
\mid{}& \nsere{r_F}\mid
|
||
\sere{r_F}\Esuffix \varphi_S\mid
|
||
\sere{r}\Asuffix \varphi_S\\
|
||
\varphi_O ::={}& \varphi_G \mid \varphi_S\mid \NOT\varphi_O\mid
|
||
\varphi_O\AND \varphi_O\mid (\varphi_O\OR \varphi_O)\mid
|
||
\varphi_O\EQUIV \varphi_O\mid \varphi_O\XOR \varphi_O\mid
|
||
\varphi_O\IMPLIES \varphi_O\\
|
||
\mid{}& \X\varphi_O \mid
|
||
\varphi_O\U\varphi_G\mid\varphi_O\R\varphi_S \mid
|
||
\varphi_S\W\varphi_O\mid \varphi_G\M\varphi_O\\
|
||
\mid{}& \sere{r} \mid \nsere{r}\mid
|
||
\sere{r_F}\Esuffix \varphi_O \mid \sere{r_I}\Esuffix \varphi_G\mid
|
||
\sere{r_F}\Asuffix \varphi_O\mid
|
||
\sere{r_I}\Asuffix \varphi_S\\
|
||
\varphi_P ::={}& \varphi_O \mid \NOT\varphi_R\mid
|
||
\varphi_P\AND \varphi_P\mid (\varphi_P\OR \varphi_P)\mid
|
||
\varphi_P\EQUIV \varphi_P\mid \varphi_P\XOR \varphi_P\mid
|
||
\varphi_P\IMPLIES \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{}& \sere{r}\Esuffix \varphi_P\mid
|
||
\sere{r_F}\Asuffix \varphi_P\mid
|
||
\sere{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
|
||
\varphi_R\EQUIV \varphi_R\mid \varphi_R\XOR \varphi_R\mid
|
||
\varphi_R\IMPLIES \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{}& \sere{r}\Asuffix \varphi_R\mid \sere{r_F}\Esuffix \varphi_R \mid \sere{r_I}\Esuffix \varphi_G\\
|
||
\end{align*}
|
||
|
||
It should be noted that a formula can belong to a class of the
|
||
temporal hierarchy even if it does not syntactically appears so. For
|
||
instance the formula $(\G(q\OR \F\G p)\AND \G(r\OR \F\G\NOT p))\OR\G
|
||
q\OR \G r$ is not syntactically safe, yet it is a safety formula
|
||
equivalent to $\G q\OR \G r$. Such a formula is usually said
|
||
\emph{pathologically safe}.
|
||
|
||
\chapter{Rewritings}
|
||
|
||
The LTL rewritings described in this section are all implemented in
|
||
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 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(\sere{r} \Asuffix f) &\equiv \sere{r} \Esuffix \NOT f
|
||
\\
|
||
\NOT(\sere{r})&\equiv \nsere{r}&
|
||
\NOT(f \M g) & \equiv (\NOT f) \W (\NOT g)&
|
||
\NOT(\sere{r} \Esuffix f) &\equiv \sere{r} \Asuffix \NOT f
|
||
\end{align*}
|
||
\noindent Recall the that negated weak closure $\nsere{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 rewritings are not applied to Boolean subformul\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 simplifies 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}
|
||
|
||
Rewritings defined with $\equivEU$ are applied only when
|
||
\verb|ltl_simplifier_options::favor_event_univ|' is \texttt{true}:
|
||
they try to lift subformulas that are both eventual and universal
|
||
\emph{higher} in the syntax tree. Conversely, rules defined with $\equivNeu$
|
||
are applied only when \verb|favor_event_univ|' is \texttt{false}: they
|
||
try to \textit{lower} subformulas that are both eventual and universal.
|
||
|
||
\subsection{Basic Simplifications}\label{sec:basic-simp}
|
||
|
||
These simplifications are enabled with
|
||
\verb|ltl_simplifier_options::reduce_basics|'. A couple of them may
|
||
enlarge the size of the formula: they are denoted using $\equiV$
|
||
instead of $\equiv$, and they can be disabled by setting the
|
||
\verb|ltl_simplifier_options::reduce_size_strictly|' option to
|
||
\texttt{true}.
|
||
|
||
\subsubsection{Basic Simplifications for Temporal Operators}
|
||
\label{sec:basic-simp-ltl}
|
||
|
||
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 & \F\X f & \equiv \X\F f & \G\X f & \equiv \X\G f \\
|
||
\X\G\F f & \equiv \G\F f & \F(f\U g) & \equiv \F g & \G(f \R g) & \equiv \G g \\
|
||
& & \F(f\M g) & \equiv \F (f\AND g) & \G(f \W g) & \equiv \G(f\OR g) \\
|
||
& & \F\G(f\AND \X g) & \equiv \F\G(f\AND g) & \G\F(f\OR \X g) & \equiv \G\F(f\OR g) \\
|
||
& & \F\G(f\AND \G g) & \equiv \F\G(f\AND g) & \G\F(f\OR \F g) & \equiv \G\F(f\OR g) \\
|
||
\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)$ (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).
|
||
$b$ denotes any Boolean formula.
|
||
|
||
\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) \\
|
||
(\X f)\U b & \equiV b\OR \X(b\M f) & (\X f)\W b & \equiV b\OR \X(f\R b) \\
|
||
(\X f)\M b & \equiV b\AND \X(b\U f) & (\X f)\R b & \equiV b\AND \X(f\W b) \\
|
||
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 \\
|
||
f \U (g \AND f) & \equiv g\M f & f \W (g \AND f) & \equiv g\R f \\
|
||
f \M (g \OR f) & \equiv g\U f & f \R (g \OR f) & \equiv g\W f
|
||
\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) &\equivNeu \X(f\AND \F\G g) &
|
||
(\X f) \OR (\G\F g) &\equivNeu \X(f\OR \G\F g) \\
|
||
(\G f) \AND(\G g) &\equivNeu \G(f\AND g) &
|
||
(\F f) \OR (\F g) &\equivNeu \F(f\OR 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 \\
|
||
f \AND ((\X f) \W g) &\equiv g \R f &
|
||
f \OR ((\X f) \R g) &\equiv g \W f \\
|
||
f \AND ((\X f) \U g) &\equiv g \M f &
|
||
f \OR ((\X f) \M g) &\equiv g \U f \\
|
||
f \AND (g \OR \X(g \R f)) &\equiv g \R f &
|
||
f \OR (g \AND \X(g \W f)) &\equiv g \W f \\
|
||
f \AND (g \OR \X(g \M f)) &\equiv g \M f &
|
||
f \OR (g \AND \X(g \U f)) &\equiv g \U f \\
|
||
\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)$.
|
||
|
||
The following more complicated rules are generalizations of $f\AND
|
||
\X\G f\equiv \G f$ and $f\OR \X\F f\equiv \F f$:
|
||
\begin{align*}
|
||
f\AND \X(\G(f\AND g\ldots)\AND h\ldots) &\equiv \G(f) \AND \X(\G(g\ldots)\AND h\ldots) \\
|
||
f\OR \X(\F(f)\OR h\ldots) &\equiv \F(f) \OR \X(h\ldots)
|
||
\end{align*}
|
||
The latter rule for $f\OR \X(\F(f)\OR h\ldots)$ is only applied if all
|
||
$\F$-formul\ae{} can be removed from the argument of $\X$ with the
|
||
rewriting. For instance $a \OR b \OR c\OR \X(\F(a\OR b)\OR \F(c)\OR \G d)$
|
||
will be rewritten to $\F(a \OR b \OR c) \OR \X\G d$ but
|
||
$b \OR c\OR \X(\F(a\OR b)\OR \F(c)\OR \G d)$ will only become
|
||
$b \OR c\OR \X(\F(a\OR b\OR c)\OR \G d)$.
|
||
|
||
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)
|
||
&\equivNeu \F(f_1\OR \ldots \OR f_n \OR \G\F(g)) \\
|
||
\end{align*}
|
||
|
||
\subsubsection{Basic Simplifications for SERE Operators}
|
||
|
||
\spottodo[inline]{The following rules, mostly taken
|
||
from~\citet{cimatti.08.tcad} are not complete yet. We only show
|
||
those that are implemented.}
|
||
|
||
The following simplification rules are used for the $n$-ary operators
|
||
$\ANDALT$, $\AND$, and $\OR$. The patterns are of course commutative.
|
||
$b$ or $b_i$ denote any Boolean formula while $r$ or $r_i$ denote any
|
||
SERE.
|
||
|
||
\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 \AND r &\equiV
|
||
\begin{cases}
|
||
b \OR \mathtt{\{}b\FUSION r\mathtt{\}}&\text{if~} \varepsilon\VDash r_i\\
|
||
b\FUSION r&\text{if~} \varepsilon\not\VDash r_i\\
|
||
\end{cases} \\
|
||
b \ANDALT \sere{r_1 \FUSION \ldots \FUSION r_n} &\equiv b \ANDALT r_1 \ANDALT \ldots \ANDALT r_n \\
|
||
b \ANDALT \sere{r_1 \CONCAT \ldots \CONCAT r_n} &\equiv
|
||
\begin{cases}
|
||
b \ANDALT r_i & \text{if~}\exists!i,\,\varepsilon\not\VDash r_i\\
|
||
b \ANDALT (r_1 \OR \ldots \OR r_n) & \text{if~}\forall i,\, \varepsilon\VDash r_i\\
|
||
\0 &\text{else}\\
|
||
\end{cases}\\
|
||
\sere{b_1\CONCAT r_1}\ANDALT\sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\ANDALT r_2} &
|
||
\sere{b_1\CONCAT r_1}\AND \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND r_2} \\
|
||
\sere{b_1\FUSION r_1}\ANDALT\sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\ANDALT r_2} &
|
||
\sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \\
|
||
\sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} &
|
||
\sere{r_1\CONCAT b_1}\AND \sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\AND b_2} \\
|
||
\sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} &
|
||
\sere{r_1\FUSION b_1}\AND \sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\AND b_2} \\
|
||
\end{align*}
|
||
|
||
Starred subformul\ae{} are rewritten in Star Normal
|
||
Form~\cite{bruggeman.96.tcs} with:
|
||
\[r\STAR{\mvar{0}..\mvar{j}} \equiv r^\circ\STAR{\mvar{0}..\mvar{j}} \]
|
||
where $r^\circ$ is recursively defined as follows:
|
||
\begin{align*}
|
||
r^\circ &= r\text{~if~} \varepsilon\not\VDash r \\
|
||
\eword^\circ &= \0 &
|
||
(r_1\CONCAT r_2)^\circ &= r_1^\circ\OR r_2^\circ \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\
|
||
r\STAR{\mvar{0}..\mvar{j}}^\circ &= r^\circ &
|
||
(r_1\AND r_2)^\circ &= r_1^\circ\OR r_2^\circ \text{~if~} \varepsilon\VDash r_1\text{~and~}\varepsilon\VDash r_2\\
|
||
(r_1\OR r_2)^\circ &= r_1^\circ \OR r_2^\circ &
|
||
(r_1\ANDALT r_2)^\circ &= r_1 \ANDALT r_2
|
||
\end{align*}
|
||
|
||
Note: the original SNF definition~\cite{bruggeman.96.tcs} does not
|
||
include \samp{$\FUSION$}, \samp{$\AND$}, and \samp{$\ANDALT$}
|
||
operators, and it guarantees that $\forall r,\,\varepsilon\not\VDash
|
||
r^\circ$ because $r^\circ$ is stripping all the stars and empty words
|
||
that occur in $r$. For instance $\sere{a\STAR{}\CONCAT
|
||
b\STAR{}\CONCAT\sere{\1\OR c}}^\circ\STAR{} = \sere{a\OR b\OR
|
||
c}\STAR{}$. Our extended definition still respects this property in
|
||
presence of \samp{$\FUSION$} and \samp{$\AND$} operators, but
|
||
unfortunately not when the \samp{$\ANDALT$} operator is used.
|
||
|
||
\subsubsection{Basic Simplifications SERE-LTL Binding Operators}
|
||
|
||
The following rewritings are applied to the operators $\Asuffix$ and
|
||
$\Esuffix$. They assume that $b$, denote a Boolean formula.
|
||
|
||
As noted at the beginning for section~\ref{sec:basic-simp}, rewritings
|
||
denoted with $\equiV$ can be disabled by setting the
|
||
\verb|ltl_simplifier_options::reduce_size_strictly|' option to
|
||
\texttt{true}.
|
||
|
||
\begin{align*}
|
||
\sere{\STAR{}}\Asuffix f &\equiv \G f\\
|
||
\sere{b\STAR{}}\Asuffix f &\equiv f \W \NOT b\\
|
||
\sere{b\PLUS{}}\Asuffix f &\equiv f \W \NOT b\\
|
||
\sere{r\STAR{\mvar{i}..\mvar{j}}}\Asuffix f &\equiV
|
||
\sere{r}\Asuffix \X(
|
||
\sere{r}\Asuffix \X(\ldots
|
||
\Asuffix\X(r\STAR{\mvar{1}..\mvar{j-i+1}})))
|
||
\text{~if~}i\ge 1\text{~and~}\varepsilon\not\VDash r\\
|
||
\sere{r\CONCAT \STAR{}}\Asuffix f &\equiv \sere{r}\Asuffix \G f\\
|
||
\sere{r\CONCAT b\STAR{}}\Asuffix f &\equiV \sere{r}\Asuffix (f\AND \X(f \W \NOT b)) \text{~if~}\varepsilon\not\VDash r\\
|
||
\sere{\STAR{}\CONCAT r}\Asuffix f &\equiV \G(\sere{r}\Asuffix f)\\
|
||
\sere{b\STAR{}\CONCAT r}\Asuffix f &\equiV (\NOT b)\R(\sere{r}\Asuffix f) \text{~if~}\varepsilon\not\VDash r\\
|
||
\sere{r_1\CONCAT r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix\X(\sere{r_2}\Asuffix f)\text{~if~}\varepsilon\not\VDash r_1\text{~and~}\varepsilon\not\VDash r_2\\
|
||
\sere{r_1\FUSION r_2}\Asuffix f &\equiV \sere{r_1}\Asuffix(\sere{r_2}\Asuffix f)\\
|
||
\sere{r_1\OR r_2}\Asuffix f &\equiV (\sere{r_1}\Asuffix f)\AND(\sere{r_2}\Asuffix f)\\
|
||
\sere{\STAR{}}\Esuffix f &\equiv \F f\\
|
||
\sere{b\STAR{}}\Esuffix f &\equiv f \M b\\
|
||
\sere{b\PLUS{}}\Esuffix f &\equiv f \M b\\
|
||
\sere{r\STAR{\mvar{i}..\mvar{j}}}\Esuffix f &\equiV
|
||
\sere{r}\Esuffix \X(
|
||
\sere{r}\Esuffix \X(\ldots
|
||
\Esuffix\X(r\STAR{\mvar{1}..\mvar{j-i+1}})))
|
||
\text{~if~}i\ge 1\text{~and~}\varepsilon\not\VDash r\\
|
||
\sere{r\CONCAT \STAR{}}\Esuffix f &\equiv \sere{r}\Esuffix \F f\\
|
||
\sere{r\CONCAT b\STAR{}}\Esuffix f &\equiV \sere{r}\Esuffix (f\OR \X(f \M b)) \text{~if~}\varepsilon\not\VDash r\\
|
||
\sere{\STAR{}\CONCAT r}\Esuffix f &\equiV \F(\sere{r}\Esuffix f)\\
|
||
\sere{b\STAR{}\CONCAT r}\Esuffix f &\equiV b\U(\sere{r}\Esuffix f) \text{~if~}\varepsilon\not\VDash r\\
|
||
\sere{r_1\CONCAT r_2}\Esuffix f &\equiV \sere{r_1}\Esuffix\X(\sere{r_2}\Esuffix f)\text{~if~}\varepsilon\not\VDash r_1\text{~and~}\varepsilon\not\VDash r_2\\
|
||
\sere{r_1\FUSION r_2}\Esuffix f &\equiV \sere{r_1}\Esuffix(\sere{r_2}\Esuffix f)\\
|
||
\sere{r_1\OR r_2}\Esuffix f &\equiV (\sere{r_1}\Esuffix f)\OR(\sere{r_2}\Esuffix f)
|
||
\end{align*}
|
||
|
||
Here are basic the rewritings for the weak closure and its negation:
|
||
\begin{align*}
|
||
\sere{r\STAR{}}&\equiv \sere{r}&
|
||
\nsere{r\STAR{}}&\equiv \nsere{r}\\
|
||
\sere{r_1;r_2}&\equiv \sere{r_1}\phantom{{}\OR\sere{r_2}}\quad\text{if~}\varepsilon\not\VDash r_1\land\varepsilon\VDash r_2&
|
||
\nsere{r_1;r_2}&\equiv \nsere{r_1}\phantom{{}\AND\nsere{r_2}}\quad\text{if~}\varepsilon\not\VDash r_1\land\varepsilon\VDash r_2\\
|
||
\sere{r_1;r_2}&\equiv \sere{r_1}\OR\sere{r_2}\quad\text{if~}\varepsilon\VDash r_1\land\varepsilon\VDash r_2&
|
||
\nsere{r_1;r_2}&\equiv \nsere{r_1}\AND\nsere{r_2}\quad\text{if~}\varepsilon\VDash r_1\land\varepsilon\VDash r_2\\
|
||
\sere{b;r}&\equiV b\AND\X\sere{r}&
|
||
\nsere{b;r}&\equiV (\NOT b)\OR\X\nsere{r}\\
|
||
\sere{b\STAR{};r}&\equiv b\W\sere{r}&
|
||
\nsere{b\STAR{};r}&\equiv (\NOT b)\M\nsere{r}\\
|
||
\sere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{b\AND \X(b\ldots}_{\mathclap{i\text{~occurences of~}b}}\AND\X\sere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r})&
|
||
\nsere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{(\NOT b)\OR \X((\NOT b)\ldots}_{\mathclap{i\text{~occurences of~}\NOT b}}\OR\X\nsere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r}) \\
|
||
\sere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{b\AND \X(b\AND \X(\ldots b))}_{i\text{~occurences of~}b}&
|
||
\nsere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{(\NOT b)\OR \X((\NOT b)\OR \X(\ldots(\NOT b)))}_{i\text{~occurences of~}\NOT b}\\
|
||
\sere{r_1\OR r_2}&\equiV\sere{r_1}\OR\sere{r_2} &
|
||
\nsere{r_1\OR r_2}&\equiV\nsere{r_1}\AND\nsere{r_2}
|
||
\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}
|
||
\toprule
|
||
$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 \\
|
||
\bottomrule
|
||
\end{tabular}
|
||
\end{center}
|
||
|
||
\begin{align*}
|
||
\F e & \equiv e & f \U e & \equiv e & e \M g & \equiv e\AND g & u_1 \M u_2 & \equiV (\F u_1) \AND u_2 \\
|
||
\F(u)\OR q & \equivEU \F(u\OR q) & f \U (g\OR e) & \equivEU (f \U g)\OR e & f\M (g\AND u) & \equivEU (f \M g)\AND u \\
|
||
& & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q \\
|
||
\G u & \equiv u & u \W g & \equiv u\OR g & f \R u & \equiv u & e_1 \W e_2 & \equiV (\G e_1) \OR e_2 \\
|
||
\G(e)\AND q & \equiv \G(e\AND q) & f \W (g\OR e) & \equivEU (f \W g)\OR e & f\R (g\AND u) & \equivEU (f \R g)\AND u \\
|
||
& & (f\OR u) \W g & \equivEU (f \W g)\OR u \\
|
||
\X q & \equiv q & q \AND \X f & \equivNeu \X(q \AND f) & q\OR \X f & \equivNeu \X(q \OR f) \\
|
||
& & \X(q \AND f) & \equivEU q \AND \X f & \X(q \OR f) & \equivEU q\OR \X f \\
|
||
\end{align*}
|
||
|
||
\begin{align*}
|
||
\G(f_1\OR\ldots\OR f_n \OR q_1 \OR \ldots \OR q_p)&\equiv \G(f_1\OR\ldots\OR f_n)\OR q_1 \OR \ldots \OR q_p \\
|
||
\F(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \F(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\
|
||
\G(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\
|
||
\G(f_1\AND\ldots\AND f_n \AND e_1 \AND \ldots \AND e_m \AND \G(e_{m+1}) \AND \ldots\AND \G(e_p))&\equivEU \G(f_1\AND\ldots\AND f_n)\AND \G(e_1 \AND \ldots \AND e_p) \\
|
||
\G(f_1\AND\ldots\AND f_n \AND \G(g_1) \AND \ldots \AND \G(g_m) &\equiv \G(f_1\AND\ldots\AND f_n\AND g_1 \AND \ldots \AND g_m) \\
|
||
\F(f_1 \OR \ldots \OR f_n \OR u_1 \OR \ldots \OR u_m \OR \F(u_{m+1})\OR\ldots\OR \F(u_p)) &\equivEU \F(f_1\OR \ldots\OR f_n) \OR \F(u_1 \OR \ldots \OR u_p)\\
|
||
\F(f_1 \OR \ldots \OR f_n \OR \F(g_1) \OR \ldots \OR \G(g_m)) &\equiv \F(f_1\OR \ldots\OR f_n \OR g_1 \OR \ldots \OR g_m)\\
|
||
\G(f_1)\AND\ldots\AND \G(f_n) \AND \G(e_1) \AND \ldots\AND \G(e_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND \G(e_1 \AND \ldots \AND e_p) \\
|
||
\F(f_1) \OR\ldots\OR \F(f_n) \OR \F(u_1)\OR\ldots\OR \F(u_p) &\equivEU \F(f_1\OR \ldots\OR f_n) \OR \F(u_1 \OR \ldots \OR u_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 q_1 \OR \ldots \OR q_p &\equivNeu \F(f_1\OR \ldots \OR f_n \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 Appendix~\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}& g\simp f &\text{then}& f\U (g \U h) &\equiv f \U h \\
|
||
\text{if}& f\simp h &\text{then}& f\U (g \R (h \U k)) &\equiv g \R (h \U k) \\
|
||
\text{if}& f\simp h &\text{then}& f\U (g \R (h \W k)) &\equiv g \R (h \W k) \\
|
||
\text{if}& f\simp h &\text{then}& f\U (g \M (h \U k)) &\equiv g \M (h \U k) \\
|
||
\text{if}& f\simp h &\text{then}& f\U (g \M (h \W k)) &\equiv g \M (h \W k) \\
|
||
\text{if}& f\simp h &\text{then}& (f\U g) \U h &\equiv g \U h \\
|
||
\text{if}& f\simp h &\text{then}& (f\W g) \U h &\equiv g \U h \\
|
||
\text{if}& g\simp h &\text{then}& (f\U g) \U h &\equiv (f \U g) \OR 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\W (g \U h) &\equiv f \W h \\
|
||
\text{if}& g\simp f &\text{then}& f\W (g \W h) &\equiv f \W h \\
|
||
\text{if}& f\simp h &\text{then}& (f\U g) \W h &\equiv g \W h \\
|
||
\text{if}& f\simp h &\text{then}& (f\W g) \W h &\equiv g \W h \\
|
||
\text{if}& g\simp h &\text{then}& (f\W g) \W h &\equiv (f \W g) \OR h \\
|
||
\text{if}& g\simp h &\text{then}& (f\U g) \W h &\equiv (f \U g) \OR 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}& h\simp f &\text{then}& (f\R g) \R h &\equiv g \R h \\
|
||
\text{if}& h\simp f &\text{then}& (f\M g) \R h &\equiv g \R h \\
|
||
\text{if}& g\simp h &\text{then}& (f\R g) \R h &\equiv (f \AND g) \R h \\
|
||
\text{if}& g\simp h &\text{then}& (f\M g) \R h &\equiv (f \AND g) \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 \\
|
||
\text{if}& h\simp f &\text{then}& (f\M g) \M h &\equiv g \M h \\
|
||
\text{if}& h\simp f &\text{then}& (f\R g) \M h &\equiv g \M h \\
|
||
\text{if}& g\simp h &\text{then}& (f\M g) \M h &\equiv (f \AND g) \M h \\
|
||
\end{array}
|
||
\end{equation*}
|
||
|
||
The above rules were collected from various
|
||
sources~\cite{somenzi.00.cav,tauriainen.03.a83,babiak.12.tacas} and
|
||
sometimes generalized to support operators such as $\M$ and $\W$.
|
||
|
||
\appendix
|
||
\chapter{Defining LTL with only one of $\U$, $\W$, $\R$, or $\M$}
|
||
\label{sec:ltl-equiv}
|
||
|
||
The operators \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. These equivalences can also help
|
||
to understand the semantics of section~\ref{sec:opltl:sem} if you are
|
||
only familiar with some of the operators.
|
||
{\allowdisplaybreaks
|
||
\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 g\R(f\OR 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 g\M (f\OR 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 g \equiv (f \M g)\OR \NOT((\NOT g)\M\1)
|
||
\end{align*}}
|
||
|
||
These equivalences make it possible to build artificially complex
|
||
formul\ae{}. 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{((\NOT\X g) \U
|
||
(\0\AND \NOT\X g))}_{\text{trivially false}}\OR\NOT(\1\U\NOT\NOT\X g)))\OR g\\
|
||
&\equiv (((f \U (\X g\AND f))\OR\NOT(\1\U\NOT f)) \AND(\1\U\X g))\OR g\\
|
||
\end{align*}
|
||
|
||
Spot is able to simplify most of the above equivalences, but it starts
|
||
to have trouble when the $\X$ operator is involved. For instance $(f
|
||
\W g) \AND \F g \equiv f \U g$ is one of the rewriting rules from
|
||
\ref{sec:basic-simp-ltl}. But the formula $(f \W \X g) \AND \F\X g$,
|
||
which looks like it should be reduced similarly to $f \U \X g$, will
|
||
be rewritten instead to $(f \W \X g) \AND \X\F g$, because $\X\F g
|
||
\equiv \F\X g$ is another rule that gets applied first during the
|
||
bottom-up rewriting.
|
||
|
||
\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 SERE $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$ denote any PSL
|
||
formula in negative normal form, and $f_U$ and $g_E$ denote 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$ denote Boolean formul\ae{}:
|
||
\begin{center}
|
||
\begin{tabular}{rl}
|
||
we have & if \\
|
||
\midrule
|
||
$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}$}
|
||
|
||
\centering
|
||
\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_2}{f_2}{g_1}{f_2}{g_2} & \banD{f_1}{g_2}{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_2}{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}
|
||
\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:
|