Notation: LTL and
Edges
LTL
LTL is a temporal logic comprised of propositional formulas and the following
temporal connectives:
In the above notations, all the operators are unary except U, W and P which
are binary. U is the strong until, that is, it requires that
B
actually happens sometime in the future. W is the weak version of
"until" and P is the "precedes" operator.
Also, the boolean operators are represented as follows:
-
&& -
"and"
-
|| -
"or"
-
! -
"not"
-
-> -
"implies"
-
<- -
"is implied by"
-
= -
"if and only if"
Some useful definitions
We define the weak version of "until" as: A W
B
= [] A || (A U
B)
And the other useful operator "precedes" is defined as follows:
A P B = ! ( !A U
B)
Edges and the Pattern-Based System
An edge signifies an event - a change of value of a variable. For example,
an event "item is dropped" can be represented as: hold &&
o ! hold, i.e, an item was held in the current
state and dropped in the next. Formally, the edges are defined as follows:
(1) Up or Rising edge:
/ A = !A &&
o
A
(2) Down or Falling edge:
\ A = A &&
o !A