tl.tex 86.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
% rewriting rules that enlarge the formula
\newcommand{\equiV}{\stackrel{\star}{\equiv}}
111
112
113
% rewriting rules that favors event/univ
\newcommand{\equivEU}{\stackrel{\blacktriangleup}{\equiv}}
\newcommand{\equivNeu}{\stackrel{\smalltriangledown}{\equiv}}
114

115
116
117
% marked rewriting rules
\newcommand{\equivM}{\stackrel{\dag}{\equiv}}

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
145
146
147
\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}

148
149
150
151
% Tikz
\tikzstyle{annote}=[overlay,thick,<-,red,>=stealth']


152
153
154
155
156
% 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
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

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

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

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}

229
230
231
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
232
property to verify) holds on all possible behaviors of the system.
233

234
235
236
237
238
239
240
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.
241
242
243
244
245
246
247
248
249

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

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

254
255
When a formula $\varphi$ holds on an \emph{finite} sequence $\sigma$,
we write $\sigma \VDash \varphi$.
256

257
\chapter{Temporal Syntax \& Semantics}
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
305
306
307

\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
308
\samp{GFa} instead of the equivalent \samp{G(F(a))} or
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
\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
337
338
  therefore be used to embed constructs specific to the underlying formalism,
  and still regard the resulting construction as an atomic proposition.
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
\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}
366
367
368
369
370
371
\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}\\
372
  conjunction & $f\AND g$     & $f\ANDALT g$     & $f\ANDALTT g$     & $f\STARBIN g$\rlap{\footnotemark} & $\land$ \uni{2227} & $\cap$ \uni{2229}\\
373
374
375
  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}\\
376
377
\end{tabular}
\end{center}
378
379
380
381
382
\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.}
383
384
385
386
387
388

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.

389
390
391
392
393
394
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.

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

\subsection{Trivial Identities (Occur Automatically)}

419
420
421
422
423
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$}.

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
466
467
468
% 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}

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

478
\section{Temporal Operators}\label{sec:ltlops}
479
480
481
482
483

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

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

518
519
520
521
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$.
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
554
555
556
\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}

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

564
565
566
567
568
569
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*}
570
571
572
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}.
573

574
\section{SERE Operators}\label{sec:sere}
575
576
577
578
579
580
581
582
583
584

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

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

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

612
613
\footnotetext{\emph{Non-Length-Matching} interesction.}

614
615
616
617
618
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.
619

620
621
\subsection{Semantics}

622
The following semantics assume that $f$ and $g$ are two SEREs, while
623
$a$ is an atomic proposition.
624

625
{\allowdisplaybreaks
626
\begin{align*}
627
628
629
630
  \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\\
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
656
657
658
  \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}..}))\\
659
  \end{cases}
660
\end{align*}}
661

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

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

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

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

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

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

774
\section{SERE-LTL Binding Operators}
775

776
The following operators combine a SERE $r$ with a PSL
777
778
779
780
781
782
formula $f$ to form another PSL formula.

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

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

805
806
807
808
809
810
811
812
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}.

813
814
\subsection{Semantics}

815
The following semantics assume that $r$ is a SERE,
816
817
818
while $f$ is a PSL formula.

\begin{align*}
819
820
821
822
  \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))\\
823
824
825
\end{align*}

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

836
837
838
839
840
841
842
Note that the semantics of $\sere{r}$ comes from the
$\mathsf{cl}(\cdot)$ operator defined by~\citet{dax.09.atva}.  This
differs from the interpretation of a SERE in the context of a temporal
formula given by the PSL standard~\citep[Appendix~B.3.1.1.2,
item~7]{psl.04.lrm}: the $\mathit{cl}(\cdot)$ semantics accepts more
words.

843
\subsection{Syntactic Sugar}\label{sec:pslsugar}
844
845
846

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

\begin{align*}
851
852
853
  \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 &
854
  \sere{r}\AsuffixALTEQ f &\equivM \sere{r\CONCAT\1}\Asuffix f\\
855
856
857
858
859
\end{align*}

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

860
861
The $\seren{r}$ operator is a \emph{strong closure} operator.

862
863
\subsection{Trivial Identities (Occur Automatically)}

864
For any PSL formula $f$, any SERE $r$, and any Boolean
865
866
867
868
formula $b$, the following rewritings are systematically performed
(from left to right).

\begin{align*}
869
870
871
872
873
874
875
876
877
878
  \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
879
880
& \sere{\eword} & \equiv \0
& \nsere{\eword} & \equiv \1 \\
881
882
883
884
885
886
  \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  \\
887
888
889
890
891
892
893
894
895
\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*}
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
\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}}}  \\
920
921
922
923
\end{align*}

\section{Operator precedence}

924
925
926
927
928
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}.
929
930

\begin{center}
931
\begin{tabular}{clc}
932
 assoc. & operators                                                                                    & priority                                                  \\
933
\midrule
934
935
936
937
938
939
940
941
942
943
944
945
946
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}; \\
947
948
\end{tabular}
\end{center}
949
950
951
\begin{tikzpicture}[remember picture,overlay,>=stealth',semithick]
  \draw[->] (lowest) -- (highest);
\end{tikzpicture}
952

953
954
955
956
957
958
959
960
961
962
963
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.


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

1017
\newfootnotetext{-1}{These ``marked'' operators are used when
1018
  translating recurring $\Esuffix$ or $\nsere{r}$ operators.  They are
1019
1020
1021
1022
1023
  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/}}

1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045

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


1046
1047
Let $\varphi$ denote any arbitrary formula and $\varphi_E$
(resp. $\varphi_U$) denote any instance of a pure eventuality
1048
1049
1050
1051
(resp. a purely universal) formula.  We have the following grammar
rules:

\begin{align*}
1052
  \varphi_E ::={}& \0
1053
1054
1055
1056
1057
1058
1059
           \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\\
1060
           \mid{}&\varphi  \U \varphi_E
1061
1062
1063
1064
1065
           \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\\
1066
  \varphi_U ::={}& \0
1067
1068
1069
1070
1071
1072
1073
           \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\\
1074
           \mid{}&\varphi_U\U \varphi_U
1075
1076
1077
1078
           \mid \varphi  \R \varphi_U
           \mid \0       \R \varphi
           \mid \varphi_U\W \varphi_U
           \mid \varphi  \W \0
1079
           \mid \varphi_U\M \varphi_U
1080
1081
1082
1083
\end{align*}

\section{Syntactic Hierarchy Classes}

1084
\begin{figure}[tbp]
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
  \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]
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
  \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$};

1112
1113
1114
1115
1116
    \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};
1117
1118
1119
1120
1121

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

    \draw[annote] (rec) -- (det);
    \draw[annote] (per) -- (weak);
1122
1123
    \draw[annote] (obl.east) -- (wdba.west);
    \draw[annote] (gua.north) -- (ter.west);
1124
1125
1126
    \draw[annote] (saf) -- (occ);
    \draw[annote] (rea.north) .. controls +(north:5mm) and +(west:5mm) .. (buc.west);
  \end{tikzpicture}
1127
  \end{captionbeside}
1128
\end{figure}
1129

1130
1131
1132
1133
1134
1135
1136
1137
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}.

1138
1139
1140
1141
1142
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()},
1143
1144
1145
1146
1147
1148
\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
1149
$\varphi_R$ denote any formula belonging respectively to the
1150
Guarantee, Safety, Obligation, Persistence, or Recurrence classes.
1151
$\varphi_F$ denotes a finite LTL formula (the unnamed class at the
1152
1153
1154
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.
1155
1156

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

1208
1209
1210
1211
1212
1213
1214
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}.

1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
\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.

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

\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
1303
  front therefore simplifies the translation.
1304
1305
1306
1307
1308
1309
1310
\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}

1311
1312
1313
1314
1315
1316
1317
Rewritings defined with $\equivEU$ are applied only when
\verb|ltl_simplifier_options::favor_event_univ|' is \texttt{true}:
they try to lift subformulas that are both eventual and universal
\emph{higher} in the syntax tree.  Conversely, rules defined with $\equivNeu$
are applied only when \verb|favor_event_univ|' is \texttt{false}: they
try to \textit{lower} subformulas that are both eventual and universal.

1318
\subsection{Basic Simplifications}\label{sec:basic-simp}
1319
1320

These simplifications are enabled with
1321
1322
1323
1324
1325
\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}.
1326

1327
\subsubsection{Basic Simplifications for Temporal Operators}
1328
\label{sec:basic-simp-ltl}
1329
1330
1331
1332

The following are simplification rules for unary operators (applied
from left to right, as usual):
\begin{align*}
1333
1334
1335
1336
1337
  \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) \\
1338
1339
\end{align*}
\begin{align*}
1340
  \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)
1341
\end{align*}
1342

1343
1344
1345
1346
1347
1348
% 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.
1349
1350
1351

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

\begin{align*}
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
  \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           \\
1365
1366
  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
1367
1368
1369
1370
1371
1372
1373
1374
1375
\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)        \\
1376
1377
1378
1379
  (\X f) \AND(\F\G g)   &\equivNeu \X(f\AND \F\G g)  &
  (\X f) \OR (\G\F g)   &\equivNeu \X(f\OR \G\F g)  \\
  (\G f) \AND(\G g)     &\equivNeu \G(f\AND g)       &
  (\F f) \OR (\F g)     &\equivNeu \F(f\OR g)        \\
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
  (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 &
1399
1400
1401
1402
1403
  (\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 \\
1404
1405
1406
1407
  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 \\
1408
1409