A.1 LTL formulas
lbtt uses the traditional definition for propositional linear
temporal logic. Let AP be a finite set of atomic propositions.
The set of propositional linear temporal logic formulas is defined inductively
as follows:
- All atomic propositions in AP and the Boolean constant
`true'
are LTL formulas.
- If
`f1' and `f2'
are LTL formulas, then
`! f1', `X f1', `(f1 \/ f2)' and `(f1 U f2)'
are LTL formulas.
The semantics of linear temporal logic
(i.e., a satisfiability
relation)
is defined over infinite sequences
x = <y(0), y(1), y(2), ...>
over subsets of AP as follows:
- x satisfies `true' for all sequences x.
- x satisfies an atomic proposition `p'
if and only if
`p' belongs to y(0),
the first element of the sequence
x.
- x satisfies `! f'
if and only if it is not the case that
x satisfies `f'.
- x satisfies `f1 \/ f2'
if and only if
x satisfies `f1'
or
x satisfies `f2'.
- x satisfies `X f'
if and only if
<y(1), y(2), y(3), ...> satisfies `f'.
- x satisfies `f1 U f2'
if and only if there exists an
i >= 0
such that
<y(i), y(i+1), y(i+2), ...> satisfies `f2'
and for all
0 <= j < i, <y(j), y(j+1), y(j+2), ...> satisfies `f1'.
lbtt also supports the following operators and Boolean constants,
the definitions of which can be given in terms of the previously defined
operators:
- “false”:
`false' := `! true'
- logical conjunction:
`(f1 /\ f2)' := `! (! f1 \/ ! f2)'
- logical implication:
`(f1 -> f2)' := `(! f1 \/ f2)'
- logical equivalence:
`(f1 <-> f2)' := `((f1 -> f2) /\ (f2 -> f1))'
- logical “exclusive or”:
`(f1 xor f2)' := `! (f1 <-> f2)'
- temporal “finally”:
`<> f' := `(true U f)'
- temporal “globally”:
`[] f' := `! <> ! f'
- temporal “(weak) release”:
`(f1 V f2)' := `! (! f1 U ! f2)'
- temporal “weak until”:
`(f1 W f2)' := `((f1 U f2) \/ [] f1)'
- temporal “strong release”:
`(f1 M f2)' := `((f1 V f2) /\ <> f1)'
- temporal “before”:
`(f1 B f2)' := `! (! f1 U f2)'