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)
Explain Atomic formula:
atomic formulas, f, g, h, … (can be true or false).
CTL:
Computation tree logic.
propositional operators:
¬ (not) ∧ (and) ∨ (or)
Fair CTL:
Fairness constraints rule out unrealistic executions
by putting constraints on the actions that occur along infinite executions
Difference between FSM and Kripke model.
Difference is that Kripke model abstracts the inputs and focus only on state transitions. The output function is the Kripke labeling function l: A->2^s .
