tl.tex 79.8 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
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

%% ---------------------- %%
%% 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`\\/}}}
76
\newcommand{\ORALTTT}{\mathbin{\texttt{+}}}
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
\newcommand{\AND}{\mathbin{\texttt{\&}}}
\newcommand{\ANDALT}{\mathbin{\texttt{\&\&}}}
\newcommand{\ANDALTT}{\mathbin{\texttt{/\char`\\}}}
\newcommand{\FUSION}{\mathbin{\texttt{:}}}
\newcommand{\CONCAT}{\mathbin{\texttt{;}}}
\newcommand{\0}{\texttt{0}}
\newcommand{\1}{\texttt{1}}
\newcommand{\STAR}[1]{\texttt{[*#1]}}
\newcommand{\STARALT}{\texttt{*}}
\newcommand{\EQUAL}[1]{\texttt{[=#1]}}
\newcommand{\GOTO}[1]{\texttt{[->#1]}}
\newcommand{\PLUS}{\texttt{[+]}}
\newcommand{\eword}{\texttt{[*0]}}

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

99
100
101
\newcommand{\sere}[1]{\texttt{\{}#1\texttt{\}}}
\newcommand{\nsere}[1]{\texttt{!\{}#1\texttt{\}}}
\newcommand{\seren}[1]{\texttt{\{}#1\texttt{\}!}}
102

103
104
105
% rewriting rules that enlarge the formula
\newcommand{\equiV}{\stackrel{\star}{\equiv}}

106
107
108
% marked rewriting rules
\newcommand{\equivM}{\stackrel{\dag}{\equiv}}

109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
\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}

139
140
141
142
% Tikz
\tikzstyle{annote}=[overlay,thick,<-,red,>=stealth']


143
144
145
146
147
% 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
148
149
150
151
152
153
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
202
203
204
205
206
207
208

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

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


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

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

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

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

\hfill compiled on \today, for Spot \SpotVersion

\vfill

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

\vfill

\chapter{Reasoning with Infinite Sequences}

\section{Finite and Infinite Sequences}

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

For any set $A$, and any number $n\in\N\cup\{\omega\}$, a
\textit{sequence} of length $n$ is a function $\sigma:
\{0,1,\ldots,n-1\}\to A$ that associates each index $i<n$ to an
element $\sigma(i)\in A$.  The sequence of length $0$ is a particular
sequence called the \textit{empty word} and denoted $\varepsilon$.  We
denote $A^n$ the set of all sequences of length $n$ on $A$ (in
particular $A^\omega$ is the set of infinite sequences on $A$), and
209
$A^\star=\bigcup_{n\in\N}A^n$ denotes the set of all finite sequences.
210
211
212
213
214
215
216
217
218
219
The length of $n\in\N\cup\{\omega\}$ any sequence $\sigma$ is noted
$|\sigma|=n$.

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}

220
221
222
223
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 possibles behaviors of the system.
224

225
226
227
228
229
230
231
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.
232
233
234
235
236
237
238
239
240

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

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

245
246
When a formula $\varphi$ holds on an \emph{finite} sequence $\sigma$,
we write $\sigma \VDash \varphi$.
247
248
249
250
251
252
253
254
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

\chapter{Temporal Syntax}

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

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

\subsection{Semantics}

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

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

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

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

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

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

The reason we deal with leading \samp{F}, \samp{G}, and \samp{X}
specifically in rule~\ref{rule:ap2} is that these are unary LTL
operators and we want to be able to write compact formul\ae{} like
299
\samp{GFa} instead of the equivalent \samp{G(F(a))} or
300
301
302
303
304
305
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
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
\samp{G~F~a}.  If you want to name an atomic proposition \samp{GFa},
you will have to quote it as \samp{"GFa"}.

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

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

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


\subsection{Examples}

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

\subsection{Semantics}

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

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

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

\begin{center}
357
358
359
360
361
362
363
364
365
366
\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$     &               & $\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}\\
367
368
369
370
371
372
373
374
\end{tabular}
\end{center}

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

375
376
377
378
379
380
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.

381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
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
\label{def:boolform}
When a formula is built using only Boolean constants
(section~\ref{sec:bool}), atomic proposition (section~\ref{sec:ap}),
and the above operators, we say that the formula is a \emph{Boolean
  formula}.

\subsection{Semantics}

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

\subsection{Trivial Identities (Occur Automatically)}

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

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

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

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

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

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

450
451
452
The `\verb=unabbreviate_logic()=' function rewrites all Boolean
operators using only the \samp{!}, \samp{\&}, and \samp{|} operators
using the following rewritings:
453
454
455
456
457
458
\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*}

459
\section{Temporal Operators}\label{sec:ltlops}
460
461
462
463
464

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

\begin{center}
465
466
467
468
469
470
471
\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}\\
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
  (Strong) Until & $f \U g$ \\
  Weak Until     & $f \W g$ \\
  (Weak) Release & $f \R g$  & $f \RALT g$ \\
  Strong Release & $f \M g$ \\
\end{tabular}
\end{center}

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

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

499
500
501
502
503
Appendix~\ref{sec:ltl-equiv} explains how to rewrite all LTL operators
using only $\X$ and one operated 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$.

504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
\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}

538
The `\verb=unabbreviate_ltl()=' function applies all the rewritings from
539
540
541
542
543
544
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*}

545
546
547
548
549
550
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*}
551
552
553
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}.
554

555
556
557
558
559
560
561
562
563
564
565
\section{SERE Operators}

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

567
568
569
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 and $b$ denotes a Boolean formula.
570
571

\begin{center}
572
573
574
575
\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}
576
  empty word   & $\eword$ \\
577
578
579
  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$ \\
580
581
582
583
584
585
  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}}$\\
586
  \llap{un}bounded repetition & $f\STAR{\mvar{i}..}$
587
588
589
590
591
592
                     & $f\STAR{\mvar{i}:}$
                     & $f\STAR{\mvar{i} to}$
                     & $f\STAR{\mvar{i},}$\\
\end{tabular}
\end{center}

593
594
\footnotetext{\emph{Non-Length-Matching} interesction.}

595
596
597
598
599
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.
600

601
602
\subsection{Semantics}

603
604
The following semantics assume that $f$ and $g$ are two SEREs, while
$b$ is a Boolean formula.
605

606
{\allowdisplaybreaks
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
\begin{align*}
  \sigma\VDash \eword & \iff |\sigma| = 0 \\
  \sigma\VDash a      & \iff \sigma(0)(a) = 1 \\
  \sigma\VDash f\OR g &\iff (\sigma\VDash f) \lor (\sigma\VDash g) \\
  \sigma\VDash f\ANDALT g &\iff (\sigma \VDash f) \land (\sigma\VDash g) \\
  \sigma\VDash f\AND g &\iff \exists k\in\N,\,
  \begin{cases}
    \text{either} &(\sigma \VDash f) \land (\sigma^{0..k-1} \VDash g)\\
    \text{or} &(\sigma^{0..k-1} \VDash f) \land (\sigma \VDash g)
  \end{cases} \\
  \sigma\VDash f\CONCAT g&\iff \exists k\in\N,\,(\sigma^{0..k-1} \VDash f)\land(\sigma^{k..} \VDash g)\\
  \sigma\VDash f\FUSION g&\iff \exists k\in\N,\,(\sigma^{0..k} \VDash f)\land(\sigma^{k..} \VDash g)\\
  \sigma\VDash f\STAR{\mvar{i}..\mvar{j}}& \iff
  \begin{cases}
    \text{either} & \mvar{i}=0 \land \sigma=\varepsilon \\
    \text{or} & \mvar{i}=0 \land \mvar{j}>0 \land (\exists k\in\N,\,
      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
      \VDash f\STAR{\mvar{0}..\mvar{j-1}}))\\
    \text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\,
      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
      \VDash f\STAR{\mvar{i-1}..\mvar{j-1}}))\\
  \end{cases}\\
  \sigma\VDash f\STAR{\mvar{i}..} & \iff
  \begin{cases}
    \text{either} & \mvar{i}=0 \land \sigma=\varepsilon \\
    \text{or} & \mvar{i}=0 \land (\exists k\in\N,\,
      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
      \VDash f\STAR{\mvar{0}..}))\\
    \text{or} & \mvar{i}>0 \land (\exists k\in\N,\,
      (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
      \VDash f\STAR{\mvar{i-1}..}))\\
638
  \end{cases}
639
\end{align*}}
640

641
642
643
Notes:
\begin{itemize}
\item The semantics of $\ANDALT$ and $\AND$ coincide if both
644
operands are Boolean formul\ae.
645
646
647
648
649
\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}
650
651
652
653
654

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

658
659
660
661
662
\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 \\
663
  && b\EQUAL{0..} &\equiv \1\STAR{0..}
664
\end{align*}
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
\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
691
692
they are then equal to $\infty$).  $f$ can be any SERE, while $b$,
$b_1$, $b_2$ are assumed to be Boolean formul\ae.
693
694
695

\begin{align*}
  \0\STAR{0..\mvar{j}} &\equiv \eword  &
696
  \0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 \\
697
  \eword\STAR{\var{i}..\mvar{j}} &\equiv \eword&
698
  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 \\
699
  f\STAR{0}&\equiv \eword &
700
  f\STAR{1}&\equiv f\\
701
702
703
\end{align*}

\noindent
704
The following rules are all valid with the two arguments swapped.
705
706
707
708
%(Even for the non-commutative operators \samp{$\CONCAT$} and
%\samp{$\FUSION$}.)

\begin{align*}
709
  \0\AND f &\equiv \0 &
710
711
712
713
  \0\ANDALT f   &\equiv \0 &
  \0\OR f &\equiv f &
  \0 \FUSION f &\equiv \0 &
  \0 \CONCAT f &\equiv \0 \\
714
715
  \1\AND f&\equiv
  \begin{cases}
716
717
    1\mathrlap{\text{~if~} \varepsilon\VDash f} \\
    f\mathrlap{\text{~if~} \varepsilon\nVDash f} \\
718
719
720
721
  \end{cases} &
  \1\ANDALT b   &\equiv b &
  \1\OR b &\equiv \1 &
  \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\
722
  &&
723
  \STAR{} \AND f &\equiv f &
724
  \STAR{} \OR f &\equiv \1\mathrlap{\STAR{}} &
725
  &&
726
  \STAR{} \CONCAT f &\equiv \STAR{}\mathrlap{\text{~if~}\varepsilon\VDash f}& \\
727
728
729
  \eword\AND f &\equiv f &
  \eword\ANDALT f &\equiv
  \begin{cases}
730
731
    \mathrlap{\eword\text{~if~} \varepsilon\VDash f} \\
    \0\mathrlap{\phantom{\STAR{}}\text{~if~} \varepsilon\nVDash f} \\
732
733
734
735
  \end{cases} &
  &&
  \eword \FUSION f &\equiv \0 &
  \eword \CONCAT f &\equiv f\\
736
737
738
739
740
  f\AND f &\equiv f&
  f\ANDALT f &\equiv f &
  f\OR f &\equiv f&
  &&
  f\CONCAT f&\equiv f\STAR{2}\\
741
  b_1 \AND b_2 &\equiv b_1\ANDALT b_2 &
742
  &&
743
  &&
744
745
746
747
748
749
750
  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}}\\
751
752
\end{align*}

753
\section{SERE-LTL Binding Operators}
754

755
The following operators combine a SERE $r$ with a PSL
756
757
758
759
760
761
formula $f$ to form another PSL formula.

\begin{center}
\begin{tabular}{ccccc}
              & preferred & \multicolumn{2}{c}{other supported} \\
   operation  & syntax    & \multicolumn{2}{c}{syntaxes}\\
762
  \midrule
763
  (universal) suffix implication
764
765
766
  & $\sere{r}\Asuffix{} f$
  & $\sere{r}\AsuffixALT{} f$
  & $\sere{r}\texttt{(}f\texttt{)}$
767
768
  \\
  existential suffix implication
769
  & $\sere{r}\Esuffix{} f$
770
  \\
771
  weak closure
772
  & $\sere{r}$
773
  \\
774
  negated weak closure
775
  & $\nsere{r}$
776
777
778
779
  \\
\end{tabular}
\end{center}

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

784
785
786
787
788
789
790
791
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}.

792
793
\subsection{Semantics}

794
The following semantics assume that $r$ is a SERE,
795
796
797
while $f$ is a PSL formula.

\begin{align*}
798
799
800
801
  \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))\\
802
803
804
\end{align*}

The $\prec$ symbol should be read as ``\emph{is a prefix of}''.  So
805
the semantic for `$\sigma\vDash \sere{r}$' is that either there is
806
807
808
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$
809
is therefore a model of the formula \samp{$\sere{a\PLUS{};\NOT
810
    a}$} even though it never sees \samp{$\NOT a$}.
811

812
\subsection{Syntactic Sugar}\label{sec:pslsugar}
813
814
815

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

\begin{align*}
820
821
822
  \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 &
823
  \sere{r}\AsuffixALTEQ f &\equivM \sere{r\CONCAT\1}\Asuffix f\\
824
825
826
827
828
\end{align*}

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

829
830
The $\seren{r}$ operator is a \emph{strong closure} operator.

831
832
\subsection{Trivial Identities (Occur Automatically)}

833
For any PSL formula $f$, any SERE $r$, and any Boolean
834
835
836
837
formula $b$, the following rewritings are systematically performed
(from left to right).

\begin{align*}
838
839
840
841
842
843
844
845
846
847
  \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
848
849
& \sere{\eword} & \equiv \1
& \nsere{\eword} & \equiv \0 \\
850
851
852
853
854
855
  \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  \\
856
857
858
859
860
861
862
863
864
\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*}
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
\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}}}  \\
889
890
891
892
\end{align*}

\section{Operator precedence}

893
894
895
896
897
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}.
898
899

\begin{center}
900
\begin{tabular}{clc}
901
 assoc. & operators                                                                                    & priority                                                  \\
902
\midrule
903
904
905
906
907
908
909
910
911
912
913
914
915
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}; \\
916
917
\end{tabular}
\end{center}
918
919
920
\begin{tikzpicture}[remember picture,overlay,>=stealth',semithick]
  \draw[->] (lowest) -- (highest);
\end{tikzpicture}
921

922
923
924
925
926
927
928
929
930
931
932
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.


933
934
935
936
937
938
939
940
\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
941
\label{property-methods}
942
\begin{tabulary}{.995\textwidth}{@{}lJ@{}}
943
\texttt{is\_boolean()}& Whether the formula uses only Boolean
944
  operators.
945
\\\texttt{is\_sugar\_free\_boolean()}& Whether the formula uses
946
947
948
949
950
951
952
953
954
955
956
957
958
  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
959
960
  SERE operators. (Boolean operators are also allowed, provided
  no SERE operator is negated.)
961
\\\texttt{is\_finite()}& Whether a SERE describes a finite
962
963
  language (no unbounded stars), or an LTL formula uses no
  temporal operator but $\X$.
964
965
966
967
\\\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.
968
969
\\\texttt{is\_syntactic\_guarantee()}& Whether the formula is a syntactic
  guarantee property.
970
971
972
973
974
975
976
\\\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
977
  ``marked'' version of the $\Esuffix$ operator.\footnotemark
978
979
\\\texttt{accepts\_eword()}& Whether the formula accepts
  $\eword$. (This can only be true for a SERE formula.)
980
\end{tabulary}
981

982
983
984
985
\footnotetext{This special operator is used when translating recurring
  $\Esuffix$, it is rendered as $\EsuffixMarked$ and it obeys the same
  simplification rules and properties as $\Esuffix$ (except for the
  \texttt{is\_marked()} property).}
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013

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

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

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

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


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

\begin{align*}
1014
  \varphi_E ::={}& \0
1015
1016
1017
1018
1019
1020
1021
           \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\\
1022
           \mid{}&\varphi  \U \varphi_E
1023
1024
1025
1026
1027
           \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\\
1028
  \varphi_U ::={}& \0
1029
1030
1031
1032
1033
1034
1035
           \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\\
1036
           \mid{}&\varphi_U\U \varphi_U
1037
1038
1039
1040
           \mid \varphi  \R \varphi_U
           \mid \0       \R \varphi
           \mid \varphi_U\W \varphi_U
           \mid \varphi  \W \0
1041
           \mid \varphi_U\M \varphi_U
1042
1043
1044
1045
\end{align*}

\section{Syntactic Hierarchy Classes}

1046
\begin{figure}[tbp]
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
  \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]
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
  \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$};

1074
1075
1076
1077
1078
    \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};
1079
1080
1081
1082
1083

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

    \draw[annote] (rec) -- (det);
    \draw[annote] (per) -- (weak);
1084
1085
    \draw[annote] (obl.east) -- (wdba.west);
    \draw[annote] (gua.north) -- (ter.west);
1086
1087
1088
    \draw[annote] (saf) -- (occ);
    \draw[annote] (rea.north) .. controls +(north:5mm) and +(west:5mm) .. (buc.west);
  \end{tikzpicture}
1089
  \end{captionbeside}
1090
\end{figure}
1091

1092
1093
1094
1095
1096
1097
1098
1099
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}.

1100
1101
1102
1103
1104
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()},
1105
1106
1107
1108
1109
1110
1111
1112
\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$ designate any formula belonging respectively to the
Guarantee, Safety, Obligation, Persistence, or Recurrence classes.
1113
1114
1115
1116
$\varphi_F$ designates 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.
1117
1118

\begin{align*}
1119
1120
1121
1122
1123
1124
1125
  \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
1126
1127
                   \X\varphi_G \mid \F\varphi_G\mid
                   \varphi_G\U\varphi_G\mid \varphi_G\M\varphi_G\\
1128
           \mid{}& \sere{r_F}\mid
1129
1130
                   \sere{r}\Esuffix \varphi_G\mid
                   \sere{r_F}\Asuffix \varphi_G \\
1131
1132
1133
  \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
1134
1135
                   \X\varphi_S \mid \G\varphi_S\mid
                   \varphi_S\R\varphi_S\mid \varphi_S\W\varphi_S\\
1136
           \mid{}& \nsere{r_F}\mid
1137
                   \sere{r_F}\Esuffix \varphi_S\mid
1138
                   \sere{r}\Asuffix \varphi_S\\
1139
  \varphi_O ::={}& \varphi_G \mid \varphi_S\mid \NOT\varphi_O\mid
1140
                   \varphi_O\AND \varphi_O\mid (\varphi_O\OR \varphi_O)\mid
1141
1142
1143
                   \varphi_O\EQUIV \varphi_O\mid \varphi_O\XOR \varphi_O\mid
                   \varphi_O\IMPLIES \varphi_O\\
           \mid{}& \X\varphi_O \mid
1144
1145
                   \varphi_O\U\varphi_G\mid\varphi_O\R\varphi_S \mid
                   \varphi_S\W\varphi_O\mid \varphi_G\M\varphi_O\\
1146
           \mid{}& \sere{r} \mid \nsere{r}\mid
1147
1148
                   \sere{r_F}\Esuffix \varphi_O \mid \sere{r_I}\Esuffix \varphi_G\mid
                   \sere{r_F}\Asuffix \varphi_O\mid
1149
                   \sere{r_I}\Asuffix \varphi_S\\
1150
  \varphi_P ::={}& \varphi_O \mid \NOT\varphi_R\mid
1151
                   \varphi_P\AND \varphi_P\mid (\varphi_P\OR \varphi_P)\mid
1152
1153
1154
                   \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
1155
1156
                   \varphi_P\U\varphi_P\mid\varphi_P\R\varphi_S\mid
                   \varphi_S\W\varphi_P\mid\varphi_P\M\varphi_P\\
1157
           \mid{}& \sere{r}\Esuffix \varphi_P\mid
1158
1159
                   \sere{r_F}\Asuffix \varphi_P\mid
                   \sere{r_I}\Asuffix \varphi_S\\
1160
  \varphi_R ::={}& \varphi_O \mid \NOT\varphi_P\mid
1161
                   \varphi_R\AND \varphi_R\mid (\varphi_R\OR \varphi_R)\mid
1162
1163
1164
                   \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
1165
1166
                   \varphi_R\U\varphi_G\mid\varphi_R\R\varphi_R\mid
                   \varphi_R\W\varphi_R\mid\varphi_G\M\varphi_R\\
1167
           \mid{}& \sere{r_F}\Esuffix \varphi_R \mid \sere{r_I}\Esuffix \varphi_G\mid \sere{r}\Asuffix \varphi_P\\
1168
1169
\end{align*}

1170
1171
1172
1173
1174
1175
1176
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}.

1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
\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.

1200
A formula in negative normal form can only have negation
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
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) &
1216
  \NOT(\sere{r} \Asuffix f) &\equiv \sere{r} \Esuffix \NOT f
1217
  \\
1218
  \NOT(\sere{r})&\equiv \nsere{r}&
1219
  \NOT(f \M g) & \equiv (\NOT f) \W (\NOT g)&
1220
  \NOT(\sere{r} \Esuffix f) &\equiv \sere{r} \Asuffix \NOT f
1221
\end{align*}
1222
\noindent Recall the that negated weak closure $\nsere{r}$ is actually
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
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
1243
1244
1245
1246
1247
1248
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.
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264

\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
1265
  front therefore simplifies the translation.
1266
1267
1268
1269
1270
1271
1272
\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}

1273
\subsection{Basic Simplifications}\label{sec:basic-simp}
1274
1275

These simplifications are enabled with
1276
1277
1278
1279
1280
\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}.
1281

1282
\subsubsection{Basic Simplifications for Temporal Operators}
1283
\label{sec:basic-simp-ltl}
1284
1285
1286
1287

The following are simplification rules for unary operators (applied
from left to right, as usual):
\begin{align*}
1288
1289
1290
  \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)
1291
1292
\end{align*}
\begin{align*}
1293
  \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)
1294
\end{align*}
1295

1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
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 a Boolean formula.
1306
1307

\begin{align*}
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
  \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           \\
1318
1319
  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
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
\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)   \\
1331
1332
  (\G f) \AND(\G g)     &\equiv \G(f\AND g)       &
  (\F f) \OR (\F g)     &\equiv \F(f\OR g)        \\
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
  (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 &
1352
1353
1354
1355
1356
  (\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 \\
1357
1358
1359
1360
  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 \\
1361
1362
1363
1364
1365
\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)$.

1366
The following more complicated rules are generalizations of $f\AND
1367
1368
1369
1370
1371
1372
1373
1374
1375
\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
1376
$b \OR c\OR \X(\F(a\OR b)\OR \F(c)\OR \G d)$ will only become
1377
1378
$b \OR c\OR \X(\F(a\OR b\OR c)\OR \G d)$.

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

1386
1387
\subsubsection{Basic Simplifications for SERE Operators}

1388
1389
1390
\spottodo[inline]{The following rules, mostly taken
  from~\citet{cimatti.08.tcad} are not complete yet.  We only show
  those that are implemented.}
1391
1392

The following simplification rules are used for the $n$-ary operators
1393
1394
1395
$\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.
1396
1397
1398
1399
1400
1401

\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}\\
1402
1403
1404
1405
1406
1407
  \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} \\
1408
1409
  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
1410
1411
1412
1413
1414
  \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}\\
1415
1416
1417
1418
1419
1420
1421
1422
  \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} \\
1423
1424
\end{align*}

1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
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.

1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
\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)\\