Week 5

Question 1

Operators of Linear Temporal Logic

Answer 1

1. X (next)
2. U (until)
3. G (always)
4. F (eventually)

Question 2

Next Operator

Answer 2

unary operator that expresses what happens at the next point in time

Question 3

Until Operator

Answer 3

binary operator that indicates one thing (first argument) will not become false until the second becomes true

Question 4

Globally Operator

Answer 4

unary operator that expresses that something is always true from this point on

Question 5

Eventually Operator

Answer 5

unary operator that expresses something will definitely happen at some point in time but does not specify when

Question 6

What does pi |= y mean when pi is a path and y is a formula

Answer 6

That the path satisfies the formula.

Question 7

pi |= a if and only if

Answer 7

a is in L(pi[0])

where L is the function that maps states to atomic propositions

Question 8

pi |= not y if and only if

Answer 8

pi |= y does not hold

Question 9

pi |= y1 and y2 if and only if

Answer 9

pi |= y1 and pi |= y2

Question 10

pi |= y1 or y2 if and only if

Answer 10

pi |= y1 or pi |= y2

Question 11

pi |= X(y) if and only if

Answer 11

pi[1…] =| y

Question 12

pi |= (y1 U y2) if and only if

Answer 12

there exists some j > 0 such that pi[j…] |= y2 and for all 0 <= i < j pi[i…]|=y1

Question 13

pi |= F(y) if and only if

Answer 13

there exists some i>=0 such that pi[i…] |= y

Question 14

pi |= G(y) if and only if

Answer 14

for all i>= 0, pi[i….] |= y

Question 15

When is a formula true in a state? Explanation in natural language and formal

Answer 15

A formula is true in a state if it is true for all paths that start in that state.

That is, s |= y if and only if for all pi in Paths(s), pi |= y

Question 16

When is a formula true in a Kripke structure?

Answer 16

A formula is true in a Kripe structure if it holds in its initial state

That is, K |= y if and only if s0 |= y

Question 17

Which two LTL operators are derived?

Answer 17

F and G

Question 18

F(y) is equivalent to - Hint: Includes U

Answer 18

true U y

Question 19

G(y) is equivalent to - Hint: Includes F

Answer 19

not F not y

Question 20

Duality: not X(y) is equivalent to

Answer 20

X(not y)

Question 21

Duality of F and G: not F(y), not G(y)

Answer 21

not F(y) is equivalent to G(not y)
not G(y) is equivalent to F(not y)

Question 22

Idempotency: GGy, FFy, yU(yUx), (yUx)Ux

Answer 22

G(G(y)) is equivalent to G(y)
F(F(y)) is equivalent to F(y)
yU(yUx) is equivalent to yUx
(yUx)Ux is equivalent to yUx

Question 23

Absorption: FGFy, GFGy

Answer 23

FGFy is equivalent to GFy
GFGy is equivalent to FGy

Question 24

Distributivity: X(y and x), X(y or x), F(y or x), G(y and x), X(F(y)), X(G(y)), X(y U x)

Answer 24

X(y and x) equivalent to X(y) and X(x)
X(y or x) equivalent to X(y) or X(x)
F(x or y) equivalent to F(x) or F(y)
G(y and x) equivalent to G(y) and G(x)
X(F(y)) equivalent to F(X(y))
X(G(y)) equivalent to G(X(y))
X(y U x) equivalent to X(y) U X(x)

Question 25

LTL Operators in PROMELA

Answer 25

Xy - Xy
Gy - []y
Fy - <>y
p U q - p U q

Question 26

Weak Until ( p W q)

Answer 26

(p U q) or (G p)

Question 27

Release p V q

Answer 27

not (not p U not q)

Question 28

Adding LTL formulas to SPIN

Answer 28

Add LTL formula to model in format:

ltl name { formula }

Question 29

Weak Fairness

Answer 29

each continuously executable statement is eventually executed

avoids unrealistic counter-examples to LTL formulas