Chapter 2 - CTL Model Checking

Question 1

What does it mean TS ⊨ φ mean?

Answer 1

TS satisfies psi

Question 2

Extended LTS with atomic propositions

Answer 2

is an LTS = (S, Σ, T, I, AP, L)

• AP is the set of atomic propositions
• L: S -> 2^AP is a labeling function that labels each state with a set of atomic propositions that are true in this state.

Question 3

What are action labels of Transitions in a LTS used for?

Answer 3

are mainly used to model the possibility of interactions of parts of a system.
They are needed to build the parallel composition(handshaking), where it needs to be defined which actions of concurrent processes must be carried out synchronously.

Question 4

Kripke Structure KS(TS)

Answer 4

is the Kripke Structure of a LTS TS.

A KS over a set of atomic propositions AP is a tuple M=(S, S0, R, L)

• S finite, non empty set of States
• S0 ⊆ S is a set of initial states
• R ⊆ SxS a transition relation that must be left-total
• L: S -> 2^AP a labeling function that labels each state with a set of atomic propositions that are true in this state.

Question 5

Left-totality def…

Answer 5

For all states s in S, there exists a state s’ in S such that there exists a transition from s to s’.

R is left-total iff ∀s ∈ S ∃s′∈S such that (s, s′)∈R.

Question 6

Left-totality means..

Answer 6

• there are no deadlock states

- all executions are infinite

Question 7

CTL

Answer 7

Computation Tree Logic

is a logic for specifying properties of computation trees.

Question 8

How is a computation tree formed?

Answer 8

it is formed from a KS by picking an initial state and unwinding the possible paths into a tree structure.

Question 9

CTL Formulas

Answer 9

…consist of <b>path quantifiers</b> and <b>temporal operators</b>, combined with predicates over atomic propositions

Question 10

Path quantifiers

Answer 10

<b>A</b> (for all paths)

<b>E</b> (for some path)

Question 11

Temporal operators

Answer 11

<b>X</b> (next)
<b>F</b> (eventually, in the future)
<b>G</b> (always)
<b>U</b> (until)

Question 12

CTL syntax definition

Answer 12

• <i>true</i> and <i>false</i> are CTL formulas
• if a ∈ AP an atomic proposition, then a is a CTL formula
• if φ and ψ are CTL formulas, so are
  ¬φ, φ ∧ ψ, φ ∨ ψ
  AX φ, EXφ
  AGφ, EGφ
  AFφ, EFφ
  A[φ U ψ], E[ φ U ψ]

Question 13

Equivalences of CTL Formulas

AX φ

Answer 13

AX φ ≡ ¬EX(¬φ)

Question 14

Equivalences of CTL Formulas

AF φ

Answer 14

AF φ ≡ ¬EG(¬φ)

Question 15

Equivalences of CTL Formulas

AG φ

Answer 15

AG φ ≡ ¬EF(¬φ)

Question 16

Equivalences of CTL Formulas

A[φ U ψ]

Answer 16

A[φ U ψ] ≡ ¬E [¬ψ U (¬φ ∧ ¬ψ)] ∧ ¬EG(¬ψ)

Question 17

Equivalences of CTL Formulas

EF φ

Answer 17

EF φ ≡ E [true U φ ]

Question 18

A path in a Kripke Structure is…

Answer 18

• an infinite sequence of states π = s0, s1, s2,…
  -that follow each other

<pre> </pre>

∀ i ∈ N: s’i = si+1 ∃ (si, si+1) ∈ R
- and where s0 is an initial state, s0 ∈ S0

Question 19

When does a KS M satisfy a formula?

Answer 19

a KS satisfies a CTL formula if and only if the formula holds in every start state of the KS.

Question 20

Model checking with KS and CTL Formulas?

Answer 20

The defined model is represented by the Kripke Structure.

The specification is transformed into several CTL formulas.

Question 21

When does a KS satisfy a formula in model checking?

Answer 21

Given a CTL formula without nested temporal operators, the KS satisfies the formula iff after applying the checking function all start states are marked to satisfy the formula.

Question 22

Complexity CheckEG, CheckEX and CheckEU

Answer 22

• has linear runtime with respect to (wrt) the number of nodes and transitions
  »> Complexity O(|S| + |R|)
  > called for each subformula of φ, where |φ| = nr of subformulas
  »»»» O( |φ| x (|S| + |R|) )

Question 23

Still difficult to prove the correctness of complex systems?

Answer 23

because of the <b><i>state-space explosion problem</i></b>.

> the size of the Kripke Structure grows <b>exponentially</b> with the number of variables or threads in the system.

Question 24

What is a counter example?

Answer 24

Is an example provided to prove that the model does not satisfy the specification. It is used to show how the specification can be violated.

> it is a path for which a given CTL formula (extracted from the specifications) does not hold. (mostly for an unsatisfied universally quantified formula, eg AG)

Question 25

What is a witness?

Answer 25

For an unsatisfied existentially quantified formula, eg EF
>there is no single execution to show that it does not hold
>but if the formula is satisfied, we can generate a witness: a path that shows that the formula is satisfied.