Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Spot
Spot
Commits
eebbcac2
Commit
eebbcac2
authored
Jan 15, 2015
by
Alexandre DuretLutz
Browse files
tl: formul\ae > formulas
* doc/tl/tl.tex: Use "formulas" everywhere in this file.
parent
731561cd
Changes
1
Hide whitespace changes
Inline
Sidebyside
doc/tl/tl.tex
View file @
eebbcac2
...
...
@@ 86,6 +86,7 @@
\newcommand
{
\0
}{
\texttt
{
0
}}
\newcommand
{
\1
}{
\texttt
{
1
}}
\newcommand
{
\STAR
}
[1]
{
\texttt
{
[*#1]
}}
\newcommand
{
\FSTAR
}
[1]
{
\texttt
{
[:*#1]
}}
\newcommand
{
\STARALT
}{
\texttt
{
*
}}
\newcommand
{
\STARBIN
}{
\mathbin
{
\texttt
{
*
}}}
\newcommand
{
\EQUAL
}
[1]
{
\texttt
{
[=#1]
}}
...
...
@@ 169,7 +170,7 @@
\newcommand\msamp
[1]
{
#1
}
\def\manualtitle
{
Spot's Temporal Logic Formul
\ae
}
\def\manualtitle
{
Spot's Temporal Logic Formul
as
}
%%  %%
%% Document. %%
...
...
@@ 226,7 +227,7 @@ starting at letter $\sigma(i)$.
\section
{
Usage in Model Checking
}
The temporal formul
\ae
{}
described in this document, should be
The temporal formul
as
described in this document, should be
interpreted on behaviors (or executions, or scenarios) of the system
to verify. In model checking we want to ensure that a formula (the
property to verify) holds on all possible behaviors of the system.
...
...
@@ 304,7 +305,7 @@ 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
operators and we want to be able to write compact formul
as
like
\samp
{
GFa
}
instead of the equivalent
\samp
{
G(F(a))
}
or
\samp
{
G~F~a
}
. If you want to name an atomic proposition
\samp
{
GFa
}
,
you will have to quote it as
\samp
{
"GFa"
}
.
...
...
@@ 320,7 +321,7 @@ 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
If you are typing in formul
as
by hand, we suggest you name all your
atomic propositions in lower case, to avoid clashes with the uppercase
operators.
...
...
@@ 357,9 +358,9 @@ For any atomic proposition $a$, we have
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
}
\section
{
Boolean Operators (for Temporal Formul
as
)
}
\label
{
sec:boolops
}
Two temporal formul
\ae
{}
$
f
$
and
$
g
$
can be combined using the
Two temporal formul
as
$
f
$
and
$
g
$
can be combined using the
following Boolean operators:
\begin{center}
...
...
@@ 377,14 +378,14 @@ following Boolean operators:
\end{center}
\footnotetext
{
The
$
\STARALT
$
form of the conjunction operator
(allowing better compatibility with Wring and VIS) may only used in
temporal formul
\ae
. Boolean expressions that occur inside SERE (see
temporal formul
as
. Boolean expressions that occur inside SERE (see
Section~
\ref
{
sec:sere
}
) may not use this form because the
$
\STARALT
$
symbol is used as the Kleen star.
}
Additionally, an atomic proposition
$
a
$
can be negated using the
syntax
\samp
{$
a
$
=0
}
, which is equivalent to
\samp
{$
\NOT
a
$}
. Also
\samp
{$
a
$
=1
}
is equivalent to just
\samp
{
a
}
. These two syntaxes help
us read formul
\ae
{}
written using Wring's syntax.
us read formul
as
written using Wring's syntax.
When using UTF8 input, a
\samp
{
=0
}
that follow a singleletter atomic
proposition may be replaced by a combining overline
\uni
{
0305
}
or a
...
...
@@ 477,7 +478,7 @@ using the following rewritings:
\section
{
Temporal Operators
}
\label
{
sec:ltlops
}
Given two temporal formul
\ae
{}
$
f
$
, and
$
g
$
, the following
Given two temporal formul
as
$
f
$
, and
$
g
$
, the following
temporal operators can be used to construct another temporal formula.
\begin{center}
...
...
@@ 662,7 +663,7 @@ $a$ is an atomic proposition.
Notes:
\begin{itemize}
\item
The semantics of
$
\ANDALT
$
and
$
\AND
$
coincide if both
operands are Boolean formul
\ae
.
operands are Boolean formul
as
.
\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
...
...
@@ 710,7 +711,7 @@ it for output. $b$ must be a Boolean formula.
The following identities also hold if
$
j
$
or
$
l
$
are missing (assuming
they are then equal to
$
\infty
$
).
$
f
$
can be any SERE, while
$
b
$
,
$
b
_
1
$
,
$
b
_
2
$
are assumed to be Boolean formul
\ae
.
$
b
_
1
$
,
$
b
_
2
$
are assumed to be Boolean formul
as
.
\begin{align*}
\0\STAR
{
0..
\mvar
{
j
}}
&
\equiv
\eword
&
...
...
@@ 1022,22 +1023,22 @@ instance using the following methods:
\newfootnotetext
{
1
}{
\url
{
http://www.tcs.hut.fi/Software/maria/tools/lbt/
}}
\section
{
Pure Eventualities and Purely Universal Formul
\ae
{}
}
\section
{
Pure Eventualities and Purely Universal Formul
as
}
\label
{
sec:eventuniv
}
These two syntactic classes of formul
\ae
{}
were introduced
by~
\citet
{
etessami.00.concur
}
to simplify LTL formul
\ae
{}
. We shall
These two syntactic classes of formul
as
were introduced
by~
\citet
{
etessami.00.concur
}
to simplify LTL formul
as
. 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 leftappend
Pure eventual formul
as
describe properties that are leftappend
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 leftappend closed formula, then
$
\F\varphi
\equiv
\varphi
$
.
Purely universal formul
\ae
{}
describe properties that are
Purely universal formul
as
describe properties that are
suffixclosed, i.e., if you remove any finite prefix of an accepted
(infinite) sequence, it remains accepted. From an LTL standpoint if
$
\varphi
$
is a suffixclosed formula, then
$
\G\varphi
\equiv
\varphi
$
.
...
...
@@ 1086,10 +1087,10 @@ rules:
\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
formul
as
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
subformul
as
involving only Boolean operators,
$
\X
$
, and past
temporal operators (Spot does not support the
latter).
\label
{
fig:hierarchy
}}
[o]
\centering
...
...
@@ 1149,7 +1150,7 @@ The symbols $\varphi_G$, $\varphi_S$, $\varphi_O$, $\varphi_P$,
$
\varphi
_
R
$
denote any formula belonging respectively to the
Guarantee, Safety, Obligation, Persistence, or Recurrence classes.
$
\varphi
_
F
$
denotes a finite LTL formula (the unnamed class at the
intersection of Safety and Guarantee formul
\ae
{}
on
intersection of Safety and Guarantee formul
as
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.
...
...
@@ 1217,10 +1218,10 @@ equivalent to $\G q\OR \G r$. Such a formula is usually said
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
caches in order to quickly rewrite formul
as
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
write an algorithm that will simplify LTL formul
as
, we suggest you
accept an optional `
\verb

ltl_simplifier

' argument, so that you can
benefit from an existing instance.
...
...
@@ 1278,7 +1279,7 @@ Section~\ref{sec:unabbbool}. Therefore it is never necessary to apply
`
\verb

ltl_simplifier::negative_normal_form

`.
If the option `
\verb

nenoform_stop_on_boolean

' is set, the above
recursive rewritings are not applied to Boolean subformul
\ae
{}
. For
recursive rewritings are not applied to Boolean subformul
as
. 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
...
...
@@ 1296,10 +1297,10 @@ The goals in most of these simplification are to:
\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
translators will usually want to rewrite LTL formul
as
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
formul
as
and
$
\psi
_
i
$
s are LTL formul
as
. Moving
$
\X
$
to the
front therefore simplifies the translation.
\item
move the
$
\F
$
operators to the front of the formula (e.g.,
$
\F
(
f
\OR
g
)
$
is better than the equivalent
$
(
\F
f
)
\OR
(
\F
g
)
$
), but not
...
...
@@ 1417,7 +1418,7 @@ The following more complicated rules are generalizations of $f\AND
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
$
\F
$
formul
as
can be removed from the argument of
$
\X
$
with the
rewriting. For instance
$
a
\OR
b
\OR
c
\OR
\X
(
\F
(
a
\OR
b
)
\OR
\F
(
c
)
\OR
\G
d
)
$
will be rewritten to
$
\F
(
a
\OR
b
\OR
c
)
\OR
\X\G
d
$
but
$
b
\OR
c
\OR
\X
(
\F
(
a
\OR
b
)
\OR
\F
(
c
)
\OR
\G
d
)
$
will only become
...
...
@@ 1467,7 +1468,7 @@ SERE.
\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
}
\mathrlap
{
\quad\text
{
if~
}
\varepsilon\nVDash
r
_
1
\land\varepsilon\nVDash
r
_
2
}
\\
\end{align*}
Starred subformul
\ae
{}
are rewritten in Star Normal
Starred subformul
as
are rewritten in Star Normal
Form~
\cite
{
bruggeman.96.tcs
}
with:
\[
r
\STAR
{}
\equiv
r
^
\circ\STAR
{}
\]
where
$
r
^
\circ
$
is recursively defined as follows:
...
...
@@ 1581,14 +1582,14 @@ Here are basic the rewritings for the weak closure and its negation:
\nsere
{
r
_
1
\OR
r
_
2
}&
\equiV\nsere
{
r
_
1
}
\AND\nsere
{
r
_
2
}
\end{align*}
\subsection
{
Simplifications for Eventual and Universal Formul
\ae
}
\subsection
{
Simplifications for Eventual and Universal Formul
as
}
\label
{
sec:eventunivrew
}
The class of
\textit
{
pure eventuality
}
and
\textit
{
purely universal
}
formul
\ae
{}
are described in section~
\ref
{
sec:eventuniv
}
.
formul
as
are described in section~
\ref
{
sec:eventuniv
}
.
In the following rewritings, we use the following
notation to distinguish the class of subformul
\ae
:
notation to distinguish the class of subformul
as
:
\begin{center}
\begin{tabular}
{
rl
}
...
...
@@ 1747,7 +1748,7 @@ only familiar with some of the operators.
\end{align*}
}
These equivalences make it possible to build artificially complex
formul
\ae
{}
. For instance by applying the above rules to successively
formul
as
. For instance by applying the above rules to successively
rewrite
$
\U\to\M\to\R\to\U
$
we get
\begin{align*}
f
\U
g
&
\equiv
((
\X
g)
\M
f)
\OR
g
\\
...
...
@@ 1772,7 +1773,7 @@ Syntactic implications are used for the rewriting of
Section~
\ref
{
sec:syntimpl
}
. The rules presented bellow extend those
first presented by~
\citet
{
somenzi.00.cav
}
.
A few words about implication first. For two PSL formul
\ae
{}
$
f
$
and
A few words about implication first. For two PSL formul
as
$
f
$
and
$
g
$
, we say that
$
f
\implies
g
$
if
$
\forall\sigma
,
\,
(
\sigma\vDash
f
)
\implies
(
\sigma\vDash
g
)
$
. For two SERE
$
f
$
and
$
g
$
, we say that
$
f
\implies
g
$
if
$
\forall\pi
,
\,
(
\pi\VDash
...
...
@@ 1800,7 +1801,7 @@ conclusion by chaining two rules: ``$\F f \simp \underbrace{\F
``
$
f
\simp
\F
g
$
\textit
{
if
}
$
f
\simp
g
$
''.
The rules from table~
\ref
{
tab:syntimpl
}
should be completed by the
following cases, where
$
f
_
b
$
and
$
g
_
b
$
denote Boolean formul
\ae
{}
:
following cases, where
$
f
_
b
$
and
$
g
_
b
$
denote Boolean formul
as
:
\begin{center}
\begin{tabular}
{
rl
}
we have
&
if
\\
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment