Model Checking with Temporal Logic Flashcards
What is a Kripke Model?
Is a quintuple:
{S - Set of states
So - Initial States
R - transition relation describing all possible transitions in the model.
A - set of atomic formulas that can be either true or false}
l - valuation function A -> 2^s: specify all formulas in A a set of all states in S for which the formula is valid.
}
Which are the Modal Operators used in modal propositional logic and their meaning.
E -> it is possible
A -> it is necessary.
Which are the temporal operators used in extension of modal propositional logic and their meaning:
F -> Future (Fp: at least once in the future p will be valid)
G -> Globally (Gp: every point in the future p will be valid)
X -> Next (Xp: at next point p is valid)
U -> until (pUq: at some time in the future, q will be valid and until this time, p will be valid).
Role of modal operators
Check validity of propositions under temporal circumstances.
What is the definition of CTL syntax?
Every atomic formula is a CTL formula, if p and q are atomic formulas, then:
!p (p v q) EXp EGp E(pUq) (p^q) EFp AXp AFp AGp and A(pUq) are atomic formulas.
Every modal operator(E A) MUST be followed by a temporal operator(F X U G) and every temporal op. MUST be preceded by a modal op.
Obs: First four formulas can be used to represent all formulas.
Notation: K, s |= f means that formula f is valid in state s of the Kripke model K. -Let f and g be arbitrary CTL formulas. How is the semantics of CTL formulas with respect to a Kripke model K = (S, S0, R, A, l) defined for the following formulas: 1) S |= p 2) S |= !f 3) S |= f^g 4) So |= AXf 5) So |= EXf 6) So |= A(fUg) 7) So |= E(fUg) 8) So |= AGf 9) So |= EGf 10) So |= AFf 11) So |= EFf
1) s ∈ l(p), for p ∈ A
2) f not valid in S
3) S |= g and S |= f (same for or op.)
4) for all paths from So, in the next state Sx, Sx |= f.
5) there exists a path from So, such that the next state Sx, Sx |= f.
6) for all paths from So: (So, S1,S2,…,Si,…) there exists an i >= 0 such that Si |= g and Sj |= f for all 0= 0 such that Si |= g and Sj |= f for all 0
Meaning of the CTL formula AG!p
It is necessary that p never happens (safety property).
Meaning of the CTL formula AFp
At some time in the future, p will happen
Meaning of the CTL formula EFp
It is possible that p is valid some time in the future.
AGAFp
p occurs infinitely often: it is always necessary that at some time in the future p will occur.
AFAGp
At some time in the future, p will always hold
AG(p -> AFq)
No matter what states are reached in the future, whenever p occurs, at some latter point q will occur. (freedom of starvation)
AGEFp
p will always be possible at some later point.
How to compute the states R that can be reached in K from S0?
The set of reachable states van be iteratively (fixed point iteration) computed with operator xreach(A) -> compute all immediate successors from set of states A:
reach (S0){
Rit = null;
do{
R = Rit;
Rit = S0 U xreach (R)
}while (R != Rit);
return R;
}
Given a model K and a state set S, how can the CTL formulas EFp EGp E(pUq) be computed?
By a fixed point iteration on XREACH (Yi)
The CTL operators and their fixed point iterations are:
EFp: Yi+1 = p v XREACH(Yi), Y0 = {} = false
EGp: Yi+1 = p ^ XREACH(Yi), Y0 = S = true
E(pUq): Yi+1 = (q v (p ^ XREACH(Yi))), Y0 = {}
Hint: p is the set of states at which p is valid.
All other operations are then reduced to fixed point operations on XREACH(Yi)
