cb7bdf8c1f
This follows from a discussion with Ernesto Posse.
The semantics for the {...} operator we use in Spot comes from the
cl(...) operator defined by Dax et al. (ATVA'09). This is slightly
different from the the way the PSL spec interprets a SERE used in the
context of a temporal formula (appendix B.3.1.1.2, item 7).
cl({a;b}[*]) would match any infinite word that starts with a;b, while
in PSL {a;b}[*] would match any infinite word that alternates a and b.
Spot documents that {SERE} in a temporal formula is interpreted like
cl(SERE) however it failed to ignore the empty prefix of SERE. So
{{a;b}[*]} would match anything, because the empty word is a prefix of
any word, and is also accepted by {a;b}[*]. Some trivial identities
and basic rewritings were also wrongly considering these empty
prefixes as well.
This patch therefore fixes the translation and syntactic
simplification rules, to really ignore these empty prefixes.
In some future version it should probably be wise to rename this {...}
operator as cl(...), and use {...} for the semantics given in appendix
B.3.1.1.2 (item 7) of the PSL specs.
* src/ltlast/unop.cc: Fix trivial identities. We have
{[*0]} = 0 and !{[*0]} = 1.
* src/ltlvisit/simplify.cc: Fix basic rewriting rules.
{e[*]} = {e} and !{e[*]} = !{e}.
* doc/tl/tl.tex: Adjust documentation.
* doc/tl/tl.bib (dax.09.atva): New entry.
* src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any
infinite word for {e[*]} just because the empty
prefix is matched by e[*].
* src/tgbatest/ltl2tgba.test: Add a test case.
* NEWS: Mention it.
* THANKS: Add Ernesto.
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*}
|
||
|
||
Stared 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:
|