Chapter 2 - CTL Model Checking Flashcards
What does it mean TS ⊨ φ mean?
TS satisfies psi
Extended LTS with atomic propositions
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.
What are action labels of Transitions in a LTS used for?
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.
Kripke Structure KS(TS)
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.
Left-totality def…
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.
Left-totality means..
- there are no deadlock states
- all executions are infinite
CTL
Computation Tree Logic
is a logic for specifying properties of computation trees.
How is a computation tree formed?
it is formed from a KS by picking an initial state and unwinding the possible paths into a tree structure.
CTL Formulas
…consist of <b>path quantifiers</b> and <b>temporal operators</b>, combined with predicates over atomic propositions
Path quantifiers
<b>A</b> (for all paths)
<b>E</b> (for some path)
Temporal operators
<b>X</b> (next)
<b>F</b> (eventually, in the future)
<b>G</b> (always)
<b>U</b> (until)
CTL syntax definition
- <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 ψ]
Equivalences of CTL Formulas
AX φ
AX φ ≡ ¬EX(¬φ)
Equivalences of CTL Formulas
AF φ
AF φ ≡ ¬EG(¬φ)
Equivalences of CTL Formulas
AG φ
AG φ ≡ ¬EF(¬φ)
Equivalences of CTL Formulas
A[φ U ψ]
A[φ U ψ] ≡ ¬E [¬ψ U (¬φ ∧ ¬ψ)] ∧ ¬EG(¬ψ)
Equivalences of CTL Formulas
EF φ
EF φ ≡ E [true U φ ]
A path in a Kripke Structure is…
- 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
When does a KS M satisfy a formula?
a KS satisfies a CTL formula if and only if the formula holds in every start state of the KS.
Model checking with KS and CTL Formulas?
The defined model is represented by the Kripke Structure.
The specification is transformed into several CTL formulas.
When does a KS satisfy a formula in model checking?
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.
Complexity CheckEG, CheckEX and CheckEU
- 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|) )
Still difficult to prove the correctness of complex systems?
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.
What is a counter example?
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)
What is a witness?
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.
