tl.tex 82.5 KB
Newer Older
1
\RequirePackage[l2tabu, orthodox]{nag}
2
\documentclass[a4paper,twoside,10pt,DIV=12]{scrreprt}
3
4
5
6
7
8
9
10
11
12
\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}
13
\usepackage{mathabx}  % vDash
14
15
\usepackage{wasysym}
\usepackage{stmaryrd}
16
%\usepackage{showlabels}
17
18
19
\usepackage{tabulary}
\usepackage[numbers]{natbib}
\usepackage{rotating}
20
\usepackage{booktabs}
21
\usepackage{tikz}
22
\usepackage{calc}
23
24
25
26
27
28
\usetikzlibrary{backgrounds}
\usetikzlibrary{shadows}
\usetikzlibrary{arrows}
\pgfdeclarelayer{background}
\pgfdeclarelayer{foreground}
\pgfsetlayers{background,main,foreground}
29

30
31
32
\addtokomafont{caption}{\small}
\setkomafont{captionlabel}{\sffamily\bfseries}

33
34
35
36
37
38
39
40
% 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}}

41
42
\newcommand{\uni}[1]{\texttt{\small U+#1}}

43
44
45
46
% For tables.
\newcommand{\newfootnotemark}[1]{\addtocounter{footnote}{#1}\footnotemark[\value{footnote}]}
\newcommand{\newfootnotetext}[2]{\addtocounter{footnote}{#1}\footnotetext[\value{footnote}]{#2}}

47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

%% ---------------------- %%
%% 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`\\/}}}
80
\newcommand{\ORALTTT}{\mathbin{\texttt{+}}}
81
82
83
84
85
86
87
88
89
\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{*}}
90
\newcommand{\STARBIN}{\mathbin{\texttt{*}}}
91
92
93
94
95
96
97
98
99
100
101
102
103
\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{|=>}}

104
105
\newcommand{\sere}[1]{\texttt{\{}#1\texttt{\}}}
\newcommand{\nsere}[1]{\texttt{!\{}#1\texttt{\}}}
106
\newcommand{\nsereMarked}[1]{\texttt{!+\{}#1\texttt{\}}}
107
\newcommand{\seren}[1]{\texttt{\{}#1\texttt{\}!}}
108

109
110
111
% rewriting rules that enlarge the formula
\newcommand{\equiV}{\stackrel{\star}{\equiv}}

112
113
114
% marked rewriting rules
\newcommand{\equivM}{\stackrel{\dag}{\equiv}}

115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
\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}

145
146
147
148
% Tikz
\tikzstyle{annote}=[overlay,thick,<-,red,>=stealth']


149
150
151
152
153
% 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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201

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

202
Let $\N=\{0,1,2,\ldots\}$ denote the set of natural numbers and
203
204
205
206
207
208
209
210
211
212
213
214
$\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
215
$A^\star=\bigcup_{n\in\N}A^n$ denotes the set of all finite sequences.
216
217
The length of any sequence $\sigma$ is noted $|\sigma|$, with
$|\sigma|\in\N\cup\{\omega\}$.
218
219
220
221
222
223
224
225

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}

226
227
228
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
229
property to verify) holds on all possible behaviors of the system.
230

231
232
233
234
235
236
237
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.
238
239
240
241
242
243
244
245
246

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

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

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

254
\chapter{Temporal Syntax \& Semantics}
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304

\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
305
\samp{GFa} instead of the equivalent \samp{G(F(a))} or
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
\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
334
335
  therefore be used to embed constructs specific to the underlying formalism,
  and still regard the resulting construction as an atomic proposition.
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
\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}
363
364
365
366
367
368
\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}\\
369
  conjunction & $f\AND g$     & $f\ANDALT g$     & $f\ANDALTT g$     & $f\STARBIN g$\rlap{\footnotemark} & $\land$ \uni{2227} & $\cap$ \uni{2229}\\
370
371
372
  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}\\
373
374
\end{tabular}
\end{center}
375
376
377
378
379
\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.}
380
381
382
383
384
385

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.

386
387
388
389
390
391
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.

392
393
394
395
396
397
398
399
400
\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*}
401
402
403
404
405
406
407
408
409
410
411
\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))
412
413
414
415
\end{align*}

\subsection{Trivial Identities (Occur Automatically)}

416
417
418
419
420
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$}.

421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
% 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}

466
467
468
The `\verb=unabbreviate_logic()=' function rewrites all Boolean
operators using only the \samp{!}, \samp{\&}, and \samp{|} operators
using the following rewritings:
469
470
471
472
473
474
\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*}

475
\section{Temporal Operators}\label{sec:ltlops}
476
477
478
479
480

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

\begin{center}
481
482
483
484
485
486
487
\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}\\
488
489
490
491
492
493
494
495
496
497
  (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*}
498
  \sigma\vDash \X f &\iff \sigma^{1..}\vDash f\\
499
500
501
502
  \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}
503
    \forall i<j,\, \sigma^{i..}\vDash f\\
504
505
506
507
508
509
510
511
512
513
514
    \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*}

515
516
517
518
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$.
519

520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
\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}

554
The `\verb=unabbreviate_ltl()=' function applies all the rewritings from
555
556
557
558
559
560
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*}

561
562
563
564
565
566
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*}
567
568
569
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}.
570

571
\section{SERE Operators}\label{sec:sere}
572
573
574
575
576
577
578
579
580
581

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$'.
582

583
584
Any Boolean formula (section~\ref{def:boolform}) is a SERE.  SERE can
be further combined with the following operators, where $f$ and $g$
585
denote arbitrary SERE.
586
587

\begin{center}
588
589
590
591
\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}
592
  empty word   & $\eword$ \\
593
594
595
  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$ \\
596
597
598
599
600
601
  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}}$\\
602
  \llap{un}bounded repetition & $f\STAR{\mvar{i}..}$
603
604
605
606
607
608
                     & $f\STAR{\mvar{i}:}$
                     & $f\STAR{\mvar{i} to}$
                     & $f\STAR{\mvar{i},}$\\
\end{tabular}
\end{center}

609
610
\footnotetext{\emph{Non-Length-Matching} interesction.}

611
612
613
614
615
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.
616

617
618
\subsection{Semantics}

619
The following semantics assume that $f$ and $g$ are two SEREs, while
620
$a$ is an atomic proposition.
621

622
{\allowdisplaybreaks
623
\begin{align*}
624
625
626
627
  \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\\
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
  \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}..}))\\
656
  \end{cases}
657
\end{align*}}
658

659
660
661
Notes:
\begin{itemize}
\item The semantics of $\ANDALT$ and $\AND$ coincide if both
662
operands are Boolean formul\ae.
663
664
665
666
667
\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}
668
669
670
671
672

\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
673
674
formula, and \emph{some} are performed from right to left when writing
it for output.  $b$ must be a Boolean formula.
675

676
677
678
679
680
\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 \\
681
  && b\EQUAL{0..} &\equiv \1\STAR{0..}
682
\end{align*}
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
\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
709
710
they are then equal to $\infty$).  $f$ can be any SERE, while $b$,
$b_1$, $b_2$ are assumed to be Boolean formul\ae.
711
712
713

\begin{align*}
  \0\STAR{0..\mvar{j}} &\equiv \eword  &
714
  \0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 \\
715
  \eword\STAR{\var{i}..\mvar{j}} &\equiv \eword&
716
  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 \\
717
  f\STAR{0}&\equiv \eword &
718
  f\STAR{1}&\equiv f\\
719
720
721
\end{align*}

\noindent
722
The following rules are all valid with the two arguments swapped.
723
724
725
726
%(Even for the non-commutative operators \samp{$\CONCAT$} and
%\samp{$\FUSION$}.)

\begin{align*}
727
  \0\AND f &\equiv \0 &
728
729
730
731
  \0\ANDALT f   &\equiv \0 &
  \0\OR f &\equiv f &
  \0 \FUSION f &\equiv \0 &
  \0 \CONCAT f &\equiv \0 \\
732
733
  \1\AND f&\equiv
  \begin{cases}
734
735
    1\mathrlap{\text{~if~} \varepsilon\VDash f} \\
    f\mathrlap{\text{~if~} \varepsilon\nVDash f} \\
736
737
738
739
  \end{cases} &
  \1\ANDALT b   &\equiv b &
  \1\OR b &\equiv \1 &
  \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\
740
  &&
741
  \STAR{} \AND f &\equiv f &
742
  \STAR{} \OR f &\equiv \1\mathrlap{\STAR{}} &
743
  &&
744
  \STAR{} \CONCAT f &\equiv \STAR{}\mathrlap{\text{~if~}\varepsilon\VDash f}& \\
745
746
747
  \eword\AND f &\equiv f &
  \eword\ANDALT f &\equiv
  \begin{cases}
748
749
    \mathrlap{\eword\text{~if~} \varepsilon\VDash f} \\
    \0\mathrlap{\phantom{\STAR{}}\text{~if~} \varepsilon\nVDash f} \\
750
751
752
753
  \end{cases} &
  &&
  \eword \FUSION f &\equiv \0 &
  \eword \CONCAT f &\equiv f\\
754
755
756
757
758
  f\AND f &\equiv f&
  f\ANDALT f &\equiv f &
  f\OR f &\equiv f&
  &&
  f\CONCAT f&\equiv f\STAR{2}\\
759
  b_1 \AND b_2 &\equiv b_1\ANDALT b_2 &
760
  &&
761
  &&
762
763
764
765
766
767
768
  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}}\\
769
770
\end{align*}

771
\section{SERE-LTL Binding Operators}
772

773
The following operators combine a SERE $r$ with a PSL
774
775
776
777
778
779
formula $f$ to form another PSL formula.

\begin{center}
\begin{tabular}{ccccc}
              & preferred & \multicolumn{2}{c}{other supported} \\
   operation  & syntax    & \multicolumn{2}{c}{syntaxes}\\
780
  \midrule
781
  (universal) suffix implication
782
783
784
  & $\sere{r}\Asuffix{} f$
  & $\sere{r}\AsuffixALT{} f$
  & $\sere{r}\texttt{(}f\texttt{)}$
785
786
  \\
  existential suffix implication
787
  & $\sere{r}\Esuffix{} f$
788
  \\
789
  weak closure
790
  & $\sere{r}$
791
  \\
792
  negated weak closure
793
  & $\nsere{r}$
794
795
796
797
  \\
\end{tabular}
\end{center}

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

802
803
804
805
806
807
808
809
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}.

810
811
\subsection{Semantics}

812
The following semantics assume that $r$ is a SERE,
813
814
815
while $f$ is a PSL formula.

\begin{align*}
816
817
818
819
  \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))\\
820
821
822
\end{align*}

The $\prec$ symbol should be read as ``\emph{is a prefix of}''.  So
823
824
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
825
826
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$
827
828
829
830
831
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.
832

833
\subsection{Syntactic Sugar}\label{sec:pslsugar}
834
835
836

The syntax on the left is equivalent to the syntax on the right.
These rewritings are performed from left to right when parsing a
837
838
formula.  Except the one marked with $\equivM$, the opposite
rewritings are also preformed on output to ease reading.
839
840

\begin{align*}
841
842
843
  \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 &
844
  \sere{r}\AsuffixALTEQ f &\equivM \sere{r\CONCAT\1}\Asuffix f\\
845
846
847
848
849
\end{align*}

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

850
851
The $\seren{r}$ operator is a \emph{strong closure} operator.

852
853
\subsection{Trivial Identities (Occur Automatically)}

854
For any PSL formula $f$, any SERE $r$, and any Boolean
855
856
857
858
formula $b$, the following rewritings are systematically performed
(from left to right).

\begin{align*}
859
860
861
862
863
864
865
866
867
868
  \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
869
870
& \sere{\eword} & \equiv \1
& \nsere{\eword} & \equiv \0 \\
871
872
873
874
875
876
  \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  \\
877
878
879
880
881
882
883
884
885
\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*}
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
\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}}}  \\
910
911
912
913
\end{align*}

\section{Operator precedence}

914
915
916
917
918
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}.
919
920

\begin{center}
921
\begin{tabular}{clc}
922
 assoc. & operators                                                                                    & priority                                                  \\
923
\midrule
924
925
926
927
928
929
930
931
932
933
934
935
936
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}; \\
937
938
\end{tabular}
\end{center}
939
940
941
\begin{tikzpicture}[remember picture,overlay,>=stealth',semithick]
  \draw[->] (lowest) -- (highest);
\end{tikzpicture}
942

943
944
945
946
947
948
949
950
951
952
953
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 Bchi store), LTL2AUT, and LTL2Bchi (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.


954
955
956
957
958
959
960
961
\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
962
\label{property-methods}
963
\begin{tabulary}{.995\textwidth}{@{}lJ@{}}
964
\texttt{is\_boolean()}& Whether the formula uses only Boolean
965
  operators.
966
\\\texttt{is\_sugar\_free\_boolean()}& Whether the formula uses
967
968
969
970
971
972
973
974
975
976
977
978
979
  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
980
981
  SERE operators. (Boolean operators are also allowed, provided
  no SERE operator is negated.)
982
\\\texttt{is\_finite()}& Whether a SERE describes a finite
983
984
  language (no unbounded stars), or an LTL formula uses no
  temporal operator but $\X$.
985
986
987
988
\\\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.
989
990
\\\texttt{is\_syntactic\_guarantee()}& Whether the formula is a syntactic
  guarantee property.
991
992
993
994
995
996
997
\\\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
998
  ``marked'' version of the $\Esuffix$ or $\nsere{r}$ operators.\newfootnotemark{1}
999
1000
\\\texttt{accepts\_eword()}& Whether the formula accepts
  $\eword$. (This can only be true for a SERE formula.)
1001
1002
1003
1004
\\\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}
1005
\end{tabulary}
1006

1007
\newfootnotetext{-1}{These ``marked'' operators are used when
1008
  translating recurring $\Esuffix$ or $\nsere{r}$ operators.  They are
1009
1010
1011
1012
1013
  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/}}

1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035

\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$.


1036
1037
Let $\varphi$ denote any arbitrary formula and $\varphi_E$
(resp. $\varphi_U$) denote any instance of a pure eventuality
1038
1039
1040
1041
(resp. a purely universal) formula.  We have the following grammar
rules:

\begin{align*}
1042
  \varphi_E ::={}& \0
1043
1044
1045
1046
1047
1048
1049
           \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\\
1050
           \mid{}&\varphi  \U \varphi_E
1051
1052
1053
1054
1055
           \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\\
1056
  \varphi_U ::={}& \0
1057
1058
1059
1060
1061
1062
1063
           \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\\
1064
           \mid{}&\varphi_U\U \varphi_U
1065
1066
1067
1068
           \mid \varphi  \R \varphi_U
           \mid \0       \R \varphi
           \mid \varphi_U\W \varphi_U
           \mid \varphi  \W \0
1069
           \mid \varphi_U\M \varphi_U
1070
1071
1072
1073
\end{align*}

\section{Syntactic Hierarchy Classes}

1074
\begin{figure}[tbp]
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
  \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]
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
  \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$};

1102
1103
1104
1105
1106
    \node[align=right,below left] (det) at (-.2,6.7) {Deterministic\\Bchi\\Automata};
    \node[align=left,below right](weak) at (6.2,6.7) {Weak Bchi\\Automata};
    \node[align=left,right](wdba) at (6.2,4.3) {Weak\\Deterministic\\Bchi\\Automata};
    \node[align=left,above right](ter) at (6.2,1.7) {Terminal\\Bchi\\Automata};
    \node[align=right,above left](occ) at (-.2,2) {Terminal\\co-Bchi\\Automata};
1107
1108
1109
1110
1111

    \node[above right] (buc) at (3.35,7) {General Bchi Automata};

    \draw[annote] (rec) -- (det);
    \draw[annote] (per) -- (weak);
1112
1113
    \draw[annote] (obl.east) -- (wdba.west);
    \draw[annote] (gua.north) -- (ter.west);
1114
1115
1116
    \draw[annote] (saf) -- (occ);
    \draw[annote] (rea.north) .. controls +(north:5mm) and +(west:5mm) .. (buc.west);
  \end{tikzpicture}
1117
  \end{captionbeside}
1118
\end{figure}
1119

1120
1121
1122
1123
1124
1125
1126
1127
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}.

1128
1129
1130
1131
1132
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()},
1133
1134
1135
1136
1137
1138
\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$,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1139
$\varphi_R$ denote any formula belonging respectively to the
1140
Guarantee, Safety, Obligation, Persistence, or Recurrence classes.
1141
$\varphi_F$ denotes a finite LTL formula (the unnamed class at the
1142
1143
1144
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.
1145
1146

\begin{align*}
1147
1148
1149
1150
1151
1152
1153
  \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
1154
1155
                   \X\varphi_G \mid \F\varphi_G\mid
                   \varphi_G\U\varphi_G\mid \varphi_G\M\varphi_G\\
1156
           \mid{}& \sere{r_F}\mid
1157
1158
                   \sere{r}\Esuffix \varphi_G\mid
                   \sere{r_F}\Asuffix \varphi_G \\
1159
1160
1161
  \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
1162
1163
                   \X\varphi_S \mid \G\varphi_S\mid
                   \varphi_S\R\varphi_S\mid \varphi_S\W\varphi_S\\
1164
           \mid{}& \nsere{r_F}\mid
1165
                   \sere{r_F}\Esuffix \varphi_S\mid
1166
                   \sere{r}\Asuffix \varphi_S\\
1167
  \varphi_O ::={}& \varphi_G \mid \varphi_S\mid \NOT\varphi_O\mid
1168
                   \varphi_O\AND \varphi_O\mid (\varphi_O\OR \varphi_O)\mid
1169
1170
1171
                   \varphi_O\EQUIV \varphi_O\mid \varphi_O\XOR \varphi_O\mid
                   \varphi_O\IMPLIES \varphi_O\\
           \mid{}& \X\varphi_O \mid
1172
1173
                   \varphi_O\U\varphi_G\mid\varphi_O\R\varphi_S \mid
                   \varphi_S\W\varphi_O\mid \varphi_G\M\varphi_O\\
1174
           \mid{}& \sere{r} \mid \nsere{r}\mid
1175
1176
                   \sere{r_F}\Esuffix \varphi_O \mid \sere{r_I}\Esuffix \varphi_G\mid
                   \sere{r_F}\Asuffix \varphi_O\mid
1177
                   \sere{r_I}\Asuffix \varphi_S\\
1178
  \varphi_P ::={}& \varphi_O \mid \NOT\varphi_R\mid
1179
                   \varphi_P\AND \varphi_P\mid (\varphi_P\OR \varphi_P)\mid
1180
1181
1182
                   \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
1183
1184
                   \varphi_P\U\varphi_P\mid\varphi_P\R\varphi_S\mid
                   \varphi_S\W\varphi_P\mid\varphi_P\M\varphi_P\\
1185
           \mid{}& \sere{r}\Esuffix \varphi_P\mid
1186
1187
                   \sere{r_F}\Asuffix \varphi_P\mid
                   \sere{r_I}\Asuffix \varphi_S\\
1188
  \varphi_R ::={}& \varphi_O \mid \NOT\varphi_P\mid
1189
                   \varphi_R\AND \varphi_R\mid (\varphi_R\OR \varphi_R)\mid
1190
1191
1192
                   \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
1193
1194
                   \varphi_R\U\varphi_G\mid\varphi_R\R\varphi_R\mid
                   \varphi_R\W\varphi_R\mid\varphi_G\M\varphi_R\\
1195
           \mid{}& \sere{r}\Asuffix \varphi_R\mid \sere{r_F}\Esuffix \varphi_R \mid \sere{r_I}\Esuffix \varphi_G\\
1196
1197
\end{align*}

1198
1199
1200
1201
1202
1203
1204
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}.

1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
\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.

1228
A formula in negative normal form can only have negation
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
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) &
1244
  \NOT(\sere{r} \Asuffix f) &\equiv \sere{r} \Esuffix \NOT f
1245
  \\
1246
  \NOT(\sere{r})&\equiv \nsere{r}&
1247
  \NOT(f \M g) & \equiv (\NOT f) \W (\NOT g)&
1248
  \NOT(\sere{r} \Esuffix f) &\equiv \sere{r} \Asuffix \NOT f
1249
\end{align*}
1250
\noindent Recall the that negated weak closure $\nsere{r}$ is actually
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
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
1271
1272
1273
1274
1275
1276
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.
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292

\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
1293
  front therefore simplifies the translation.
1294
1295
1296
1297
1298
1299
1300
\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}

1301
\subsection{Basic Simplifications}\label{sec:basic-simp}
1302
1303

These simplifications are enabled with
1304
1305
1306
1307
1308
\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}.
1309

1310
\subsubsection{Basic Simplifications for Temporal Operators}
1311
\label{sec:basic-simp-ltl}
1312
1313
1314
1315

The following are simplification rules for unary operators (applied
from left to right, as usual):
\begin{align*}
1316
1317
1318
1319
1320
  \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) \\
1321
1322
\end{align*}
\begin{align*}
1323
  \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)
1324
\end{align*}
1325

1326
1327
1328
1329
1330
1331
% 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.
1332
1333
1334

Here are the basic rewriting rules for binary operators (excluding
$\OR$ and $\AND$ which are considered in Spot as $n$-ary operators).
1335
$b$ denotes any Boolean formula.
1336
1337

\begin{align*}
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
  \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           \\
1348
1349
  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
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
\end{align*}

Here are the basic rewriting rules for $n$-ary operators ($\AND$ and
$\OR$):
\begin{align*}
  (\F\G f) \AND(\F\G g) &\equiv \F\G(f\AND g)     &
  (\G\F f) \OR (\G\F g) &\equiv \G\F(f\OR g)      \\
  (\X f) \AND(\X g)     &\equiv \X(f\AND g)       &
  (\X f) \OR (\X g)     &\equiv \X(f\OR g)        \\
  (\X f) \AND(\F\G g)   &\equiv \X(f\AND \F\G g)  &
  (\X f) \OR (\G\F g)   &\equiv \X(f\OR \G\F g)   \\
1361
1362
  (\G f) \AND(\G g)     &\equiv \G(f\AND g)       &
  (\F f) \OR (\F g)     &\equiv \F(f\OR g)        \\
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
  (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 &
1382
1383
1384
1385
1386
  (\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 \\
1387
1388
1389
1390
  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 \\
1391
1392
1393
1394
1395
\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)$.

1396
The following more complicated rules are generalizations of $f\AND
1397
1398
1399
1400
1401
1402
1403
1404
1405
\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
1406
$