Transcript Algorithmic Software Verification

Algorithmic Software Verification
VII. Computation tree logic
and bisimulations
Motivation
See McMillan’s thesis where he models a synchronous
fair bus arbiter circuit.
See table: # of states, BDD size and time
Wants to check:
- No two acks are asserted simultaneously
- Every persistent request is eventually ack-ed
- Ack is not asserted without a request.
Not really safety/reachability properties:
so how do we state and check these specs?
Temporal logics!
References

Symbolic model checking
An approach to the state explosion problem
Ken McMillan 1992
Model: Kripke structures

Finite state machines with boolean variables
ignoring .
FSM = (X, {{true, false}} {x  X} , Q, Q_in, , δ )
X
finite set of variables/propositions
Q
finite set of states
Q_in  Q set of initial states
For each q  Q, (q) is a function that maps
each x in X to true or false
δ  Q x Q transition relation

CTL: Syntax
Fix X the set of atomic propositions.
CTL(X) f,g ::= p |  f | f  g | f  g |
EX f | EF f | E(f U g) | A(f U g)
Intuitively:
EX f --- some successor state satisfies f
AX f --- every successor state satisfies f
E(f U g) – along some path, f holds until g holds
A(f U g) – along every path, f holds until g holds
CTL: Syntax
Additional derived operators:
EF f --- there is some reachable state where f holds
(reachability)
E(true U f)
AG f --- in every reachable state, f holds
(safety)
 E (true U  f)
EG f --- there is some path along which f always holds.
 A(true U  f)
AF f --- along every path, f eventually holds
A(true U f)
Actually, EX, EG and EU are sufficient.
CTL: Examples
- ack1 and ack2 are never asserted simultaneously
-
Every request req is eventually acknowledged by
an ack.
-
ack is not asserted without a request
CTL: Examples
- ack1 and ack2 are never asserted simultaneously
AG(  (ack1  ack2) )
-
Every request req is eventually acknowledged by
an ack.
AG(req  (AF ack))
-
ack is not asserted without a request
 E( req U ack)
Semantics
FSM = (X, {{true, false}} {x  X} , Q, Q_in, , δ )
With every f associate the set of states of a
Kripke structure that satisfies f:
M, s |= p
M, s |= f  g
M, s |=  f
M, s |= EX f
M, s |= EF f
iff (s)(p) = true
iff M,s |= f or M,s |= g
iff M,s | f
iff there is an s’ with δ(s,s’) and
s’ |= f
iff there is an s’ reachable from s
such that s’ |= f
Semantics
M, s |= E (f U g) iff there is a path s=s1s2… from s
and a k such that s’ |= g and
for each i<k, si |= f
M, s’ |= A(f U g) iff for every path s=s1s2… from s
and a k such that sk |= g and
for every i<k, si |=f
Bisimulations
Let M =(X, Q, Q_in, , δ ) and M’ =(X’, Q’, Q_in’, ’, δ’ )
be two Kripke structures (can be same)
A bisimilation relation is a relation R  QxQ’ such that:
- For every (q, q’) in R, (q) = ’(q’)
- If (q,q’) is in R, and q  q1 then there is a q1’ in Q’
such that q1  q1’ in M’ and (q1,q1’) is in R.
- If (q,q’) is in R, and q’  q1’ then there is a q1 in Q
such that q  q1 in M and (q1,q1’) is in R.
Fact: If R and R’ are bisimulation relations, then so is
R  R’.
Bisimulations
Let R* be the largest bisimulation relation:
R* =  { R | R is a bisimulation relation}
If q is in Q and q’ is in Q’, then
q and q’ are bisimilar iff (q,q’) is in R*.
Denoted: q ~ q’
Two models are bisimilar if q_in ~ q_in’
Bisimulations
Let M =(X, Q, q_in, , δ ) be a model.
The unfolding of M, unf(M), is a tree model:
Nodes: xq where x is in Q*
Edges: xq  xqq’ iff q  q’
Initial node: q_in
’(xq) = (q)
Claim:
- M and unf(M) are bisimilar
- For each xq, q ~ xq.
CTL and bisimilarity
Lemma: Let f be a CTL formula.
Let q in Q and q’ in Q’ be two states such
that q ~ q’.
Then M,q |= f iff M,q’ |= f
Proof: By induction on structure of formulas.
CTL and bisimilarity
CTL can distinguish between models that exhibit
the same sequential behaviors.
Hence CTL is a branching-time logic and not a linear-time
logic.
What is the right notion of behavior of a model?
--- The set of strings exhibited by it
--- The tree unfolding of the model
Model-checking CTL
Given M and f.
Compute the set of all states of M that satisfy f,
by induction on structure of f.
║p║ = states where p holds
║f  g║ = ║f║  ║g ║
║  f ║ = complement of ║f ║
║EX f ║ = the set of states s that have a succ s’ in ║f ║
Model-checking CTL
║E f U g ║ :
Take the set X =║g ║.
Repeat{
Add the set of states that satisfy f and have
a successor in X.
} till X reaches a fixpoint.
Model-checking CTL
║EG f║ :
Let M’ be M restricted to states satisfying f.
A state s satisfies EG f iff
s is in M’ and there is a path from s to an
SCC of M’.
Model-checking CTL
Model-checking CTL can be done in time O(|f|. |M|).
Number of subformulas of f is O(|f|)
║p║, ║f  g║ , ║  f ║ and ║EX f ║ are easy.
║EX f U g║
-- Start with states T satisfying g; put them in
║EX f U g║
-- In each round, take a state in T, remove it from T,
and add predecessors of this state that satisfy f
and put them in T and ║EX f U g║.
-- Each state is processed only once – linear time.
Model-checking CTL
║EG f║
-- Construct M’.
-- Partition M’ into SCCs using Tarjan’s algorithm
-- Starting from states in nontrivial SCCs, work
backwards adding states that satisfy f.
-- Linear time.