8 - LTL

Question 1

LTL syntax

Answer 1

Weaker than MSO (FO on infinite words)

Formulas in LTL over Σ := P(propositions)
-> Imitate second order variables Xi

a letter is a subset of the powerset of propositions P of the LTL formula

a letter can be represented as a tupple with values 1/0 for thruth values of each proposition where the proposition is in the set

p∈a is a proposition that is true for letter a

more precisely the satisfaction relation is:
w, i |= p if p ∈ ai

the proposition is true in position i if it is in the set of letter ai

φ ::= p | φ ∨ ψ |¬φ | ◯φ | φ U ψ
p in propositions, next, until

Abbreviations
◇φ := true U φ (eventually)
⬜φ := ¬◇¬φ (always)
φRψ := ¬(¬φ U ¬ψ)

Xa := (p∈a)⋀ p ∧(p∉a)⋀ ¬p

Question 2

write something as always the case see an a, in some step see b, write formula

Answer 2

⬜(Xa –> ◇Xb)

always when we see an a, there will eventually be a b

Question 3

LTL to NBA

Answer 3

(meyer will not talk about the proof that the automata construction is correct)

Vardi-Wolper Construction

Fisher-Ladner closure is a set of “expanded” formulas
hintika sets are subsets of FL-closures closed under satisfaction of subformulas
consisten HS are the ones that does not have contradiction

H(θ) := set of all consistent hintikka sets of θ

Aθ = (H(θ),QI, –> , (Qfi) 1 <= k )
QI = sets that contain θ
final states= unrolling U and R until accepting state
transition: Next of LTL, goes to set that contains this propositions