Chapter 3 - LTL Model Checking

Question 1

LTL

Answer 1

Linear Temporal Logic

also <i>Linear-time Temporal Logic</i>

Question 2

LTL Syntax

Answer 2

Be AP a set of atomic propositions.
The set of valid LTL formulas over AP is inductively defined as follow
- p aus AP is an LTL formula
- if psi is an LTL formula, so is not psi
- if psi and fi are LTL formulas, so is psi || fi
- if psi is an LTL formula so is X psi, G psi and F psi
- if psi and fi are LTL formulas, so is psi U fi

A formula without X, G, F or U is a state formula.

Question 3

Trace of a path π = s0 s1 s2 … of M…

Answer 3

.. is an infinite sequence of labels of the states of π:

• trace(π) = L(s0)L(s1)…
• trace(π) ∈ (2^AP)^ω, since L(si) ∈ 2^AP where L(s) = (s, {set of APs true in the state s})

Question 4

Trace language of M…

Answer 4

L(M) = { trace(π) | trace(π), π is a path of M}

Question 5

Language accepted by φ…

Answer 5

…the set of all traces satisfying φ.

L(φ) = { trace(π) | π is a path of some Kripke structure and π ⊨ φ }

Question 6

When does a KS M satisfy an LTL formula φ?

Answer 6

… iff for all paths π of M, π ⊨ φ holds.

Question 7

Characterizing properties

Answer 7

A LTL formula can describe a SAFETY or LIVENESS property.
> safety: nothing bad ever happens
> liveness: eventually sth good will happen

Question 8

when is φ a safety formula?

Answer 8

φ is a safety formula iff every path π such that π ⊭ φ has a prefixπ[0..k] such that for all infinite extensions π′ of π[0..k], π′ ⊭ φ holds

Question 9

when is φ a liveness formula?

Answer 9

φ is a liveness formula iff every finite sequence of states s0, …, sk can be extended to an infinite path π such that π φ⊨ φ holds (or such that it does not hold)

Question 10

Expressiveness: LTL vsCTL

Answer 10

• Two temporal logics L and L′ are equally expressive iff the following holds:

1. ∀φ ∈ L ∃ψ ∈ L’: ∀M : M ⊨φ ⇔ M ⊨ψ
2. ∀ψ ∈ L’ ∃φ ∈ L : ∀M : M ⊨φ ⇔ M ⊨ψ

• If just 1. holds then L is less expressive than L’

Question 11

Büchi Automata…

Answer 11

Automata that accepts infinite words.

Question 12

What does a LTL formula φ describe in a KS?

Answer 12

…describes a set of valid (infinite) traces.

Question 13

Language of φ L(φ)?

Answer 13

…is the set of infinite traces in a KS described by a LTL formula φ.

Question 14

Language of M, L(M)?

Answer 14

is defined by all the infinite traces of a KS M.

Question 15

M ⊨ φ ⇔ L(M) ⊆ L(φ) ??

Answer 15

If M ⊨ φ holds for a KS M, then all traces of M must be in the set of valid traces described by φ.