Model Checking Algorithms - probabilistic (week 8)

Question 1

What does DTMC stand for

Answer 1

Discrete Time Markov Chain

Question 2

What does PCTL stand for

Answer 2

Probabilistic Computation Tree Logic

Question 3

What is the definition for when a TS (transition system) T satisfies a property

Answer 3

T ⊨ iff ∀s ∈ I.s ⊨ φ

or equivalently

T ⊨ φ ∀s ∈ I ⊆ sat(φ)

Question 4

What is the definition of a satisfaction set

Answer 4

sat(ϕ) = {s ∣ s ⊧ ϕ}

“The satisfaction is the set of all states that satisfy the property ϕ)

Question 5

What is the Global Algorithm

Answer 5

modelCheck(TS, phi) = {
return I ⊆ sat(phi)
}

Question 6

What is the recursive bottom-up computation?

Answer 6

A method to find a solution to a PCTL formula by start from the bottom of a parse tree on the formula and working upwards. The solution, which is a satisfaction set, can be used to find a solution to the global algorithm!

Question 7

The semantic definition for the probabilities for next, eventually/finally, and until, both bounded and unbounded

Answer 7

Check slides