5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 103

Thebisimulation quotient of a given infinite state transition system might be infinite whereasits simulation quotient is finite.522Equivalences and AbstractionThe goal of this section is to present an algorithm which takes as input a finite transitionsystem TS = (S, Act, →, I, AP, L), possibly with terminal states, and computes the simulation order ,TS . Clearly, this algorithm yields at the same time an automatic approachto check whether one finite transition system simulates another one and a sound, butincomplete technique for proving finite trace inclusion.

The basic scheme for computingthe simulation order is sketched in Algorithm 33.Algorithm 33 Computation of the simulation order (basic idea)Input: finite transition system TS over AP with state space SOutput: simulation order ,TSR := { (s1 , s2 ) | L(s1 ) = L(s2 ) };while R is not a simulation dochoose (s1 , s2 ) ∈ R such that s1 → s1 , but there is no s2 such that s2 → s2 and(s1 , s2 ) ∈ R;R := R \ { (s1 , s2 ) }odreturn RThe number of iterations is bounded above by |S|2 , sinceS × S ⊇ R0 R1 R2 .

. . Rn = ,where Ri denotes the relation R at the start of the (i+1)st iteration.In the following, we discuss some details that permit an efficient implementation of thisalgorithm. Instead of explicitly representing R, we useSimR (s1 ) = { s2 ∈ S | (s1 , s2 ) ∈ R }.Note that SimR (s1 ) is a superset of SimTS (s1 ). This yields Algorithm 34.A straightforward implementation of Algorithm 34 yields a time complexity O(M · |S|3 ),where M , the number of edges in the state graph G(TS), is assumed to be at least |S|.

Letus briefly sketch how this time complexity is established. In every iteration, it is checkedfor each transition s1 → s1 , whether there exists a state s2 ∈ Sim(s1 ) that cannot simulatethis transition. Let counter δ(s1 , s2 ) denote the number of successors of s2 that belong tothe current simulator set of s1 , i.e.,δ(s1 , s2 ) = |Post(s2 ) ∩ Sim(s1 )|.The initialization of these counters can be done in O(M ·|S|) by setting δ(s1 , s2 ) = |Post(s2 )|for each s2 ∈ Sim(s1 ) and s1 ∈ Post(s1 ).

Checking Post(s2 ) ∩ Sim(s1 ) = ∅ reduces tocheck whether δ(s1 , s2 ) = 0. Given a matrix representation of δ, this takes O(1). Considernow the operations during an iteration. On removing state s2 from Sim(s1 ), we setSimulation-Quotienting Algorithms523Algorithm 34 Computation of the simulation order (first refinement)Input: finite transition system TS over AP with state space SOutput: simulation order ,TSfor all s1 ∈ S doSim(s1 ) := { s2 ∈ S | L(s1 ) = L(s2 ) };od(* initialization *)while ∃(s1 , s2 ) ∈ S × Sim(s1 ). ∃s1 ∈ Post(s1 ) with Post(s2 ) ∩ Sim(s1 ) = ∅ do(* s1 ,TS s2 *)choose such a pair of states (s1 , s2 );Sim(s1 ) := Sim(s1 ) \ { s2 };od(* Sim(s) = SimTS (s) for any s *)return { (s1 , s2 ) | s2 ∈ Sim(s1 ) }δ(s1 , v2 ) := δ(s1 , v2 ) − 1 for all v2 ∈ Pre(s2 ).(The number of direct successors of v2 that can simulate s1 is reduced by one, viz.

statess2 .) Assuming a list presentation of the sets Pre(·) and bit vector representations ofthe simulator sets Sim(·), the total time complexity of the body of the while-loop (whenranging over all iterations) is in O(M · |S|). Note that each state s2 is removed fromSim(s1 ) at most once. Hence, the total number of steps performed in the body of thewhile-loop is bounded by |Pre(s2 )| = O(M · |S|).Os1 ∈S s2 ∈S=MIn order to check whether R is a simulation, we may inspect all transitions s1 → s1 and allstates s2 and check whether the counter δ(s1 , s2 ) is 0. If so and (s1 , s2 ) ∈ R, then R is nota simulation. Otherwise we have found a pair (s1 , s2 ) to be removed from R in the bodyof the while-loop. As |S|2 is an upper bound for the number of iterations of the while-loopand the costs required to check the condition of the while-loop are in O(M ·|S|), the totaltime complexity of Algorithm 34 is O(M ·|S|3 ).With a simple trick, the time complexity can be reduced to O(M ·|S|2 ).

The idea is toorganize all pairs (s1 , s2 ) where δ(s1 , s2 ) = 0 in a list and to pick one such pair (s1 , s2 )per iteration, rather than seeking for a pair (s1 , s2 ) that violates the simulation condition.In each iteration, we run through the predecessor list of s1 and check for each states1 ∈ Pre(s1 ) whether s2 ∈ Sim(s1 ). If so, then we remove s2 from Sim(s1 ) and decrementthe counters δ(s1 , v2 ) for all states v2 ∈ Pre(s2 ).

In case δ(s1 , v2 ) becomes 0, the pair(s1 , v2 ) is inserted in the list organizing all pairs where δ(·) is 0.524Equivalences and AbstractionAn Efficiency Improvement We now discuss a further refinement of Algorithm 34that leads to the worst-case time complexity O(M ·|S|). The crux of this more efficientrealization is the following observation. Suppose s1 → s1 and s2 → s2 , and we are aboutto remove s2 from Sim(s1 ).

If state s2 is the only direct successor of s2 that belongs tothe current simulator set of s1 , i.e,s1 ∈ Pre(s1 ), s2 ∈ Sim(s1 ) and Sim(s1 ) ∩ Post(s2 ) = { s2 },then there does not exist a transition s2 → s2 which can simulate s1 → s1 . Hence, s2 —infact, any direct predecessor of s2 for which this holds—can be safely removed from Sim(s1 ).This observation can be generalized to sets of states. Let Simold (s1 ) ⊇ Sim(s1 ) denote thesimulator set that preceded the last removal of states from Sim(s1 ); initially Simold (s1 ) =S.

On the removal of s2 from Sim(s1 ), we consider all direct predecessors of s1 , and removeall states inRemove(s1 ) = Pre Simold (s1 ) \ Pre Sim(s1 )from Sim(s1 ). This is justified as all the states in this set do not have a successor simulating s1 , and thus these states cannot simulate any of the predecessors of s1 . (Notethat Post(s2 ) ∩ Sim(s1 ) = ∅ if and only if s2 ∈ Pre(Sim(s1 )).) This yields Algorithm 35, which also takes into account that a terminal state cannot be in the simulator set of a nonterminal state.

Thus, when s1 is considered the first time, thenRemove(s1 ) consists of Pre (S) \ Pre (Sim(s1 )) and all terminal states (that is, we defineRemove(s1 ) = S \ Pre (Sim(s1 ))).The next observation is that there is no need to explicitly represent the sets Simold (·). Thesets Remove(·) are dynamically adapted on modifying Sim(s1 ).

The termination conditionof the iteration can be replaced by Remove(s1 ) = ∅ for all s1 ∈ S. Intuitively speaking,this means that there are no states that need to be removed from the sets of simulatorsSim(s1 ) for s1 ∈ Pre(s1 ). Let s1 be a state such that Remove(s1 ) = ∅. Now consider allpairs (s1 , s2 ) ∈ S × S such thats2 ∈ Remove(s1 ) = Pre Simold (s1 ) \ Pre Sim(s1 )and s1 ∈ Pre(s1 ). Then, s1 → s1 , but there is no transition in s2 → s2 ∈ Sim(s1 ).This yields s1 ,TS s2 . Therefore, s2 can be removed from Sim(s1 ). Accordingly, the setRemove(s1 ) is extended with any state s such thats ∈ Pre(s2 ) and Post(s) ∩ Sim(s1 ) = ∅.For these states s, we have: if u → s1 , then there is no matching transition s → t witht ∈ Sim(s1 ). Thus, u ,TS s.

Hence, if in a later iteration of the while-loop, state s1 isSimulation-Quotienting AlgorithmsAlgorithm 35 Computation of the simulation order (second refinement)Input: finite transition system TS over AP with state space SOutput: simulation order ,TSfor all s1 ∈ S doSimold (s1 ) := undefined;Sim(s1 ) := { s2 ∈ S | L(s1 ) = L(s2 ) }odwhile ∃s ∈ S with Simold (s) = Sim(s) dochoose s1 such that Simold (s1 ) = Sim(s1 )if Simold (s1 ) = undefined thenRemove(s1 ) := S \ Pre(Sim(s1 ))elseRemove(s1 ) := Pre(Simold (s1 )) \ Pre(Sim(s1 ))fifor all s1 ∈ Pre(s1 ) doSim(s1 ) := Sim(s1 ) \ Remove(s1 )odSimold (s1 ) := Sim(s1 )odreturn { (s1 , s2 ) | s2 ∈ Sim(s1 ) }525526Equivalences and Abstractionchosen, then the simulator sets of the predecessors u ∈ Pre(s1 ) are regarded and state sis to be removed from Sim(u).

This yields Algorithm 36.Algorithm 36 Computation of the simulation orderInput: finite transition system TS with state space SOutput: simulation order ,TSfor all s1 ∈ S doSim(s1 ) := { s2 ∈ S | L(s1 ) = L(s2 ) };Remove(s1 ) := S \ Pre(Sim(s1 ))od(* loop invariant: Remove(s1 ) ⊆ S \ Pre (Sim(s1 ))while (∃s1 ∈ S with Remove(s1 ) = ∅) dochoose s1 such that Remove(s1 ) = ∅;for all s2 ∈ Remove(s1 ) dofor all s1 ∈ Pre(s1 ) doif s2 ∈ Sim(s1 ) then(* s2 ∈ Simold (s1 ) \ Sim(s1 )Sim(s1 ) := Sim(s1 ) \ { s2 };for all s ∈ Pre(s2 ) with Post(s) ∩ Sim(s1 ) = ∅ do(* s ∈ Pre (Simold (s1 )) \ Pre(Sim(s1 ))Remove(s1 ) := Remove(s1 ) ∪ { s }odfiodod(* Simold (s1 ) := Sim(s1 )Remove(s1 ) := ∅;odreturn { (s1 , s2 ) | s2 ∈ Sim(s1 ) }Theorem 7.81.*)*)*)*)Partial Correctness of Algorithm 36On termination, Algorithm 36 returns ,TS .Proof: First, observe that the outermost loop (i.e., the while-loop) maintains the followingloop invariant.

For all states s1 ∈ S:(a) Remove(s1 ) ⊆ S \ Pre(Sim(s1 )).(b) { s2 ∈ S | s1 ,TS s2 } ⊆ Sim(s1 ) ⊆ { s2 ∈ S | L(s1 ) = L(s2 ) }.(c) For all s2 ∈ Sim(s1 ), one of the following two statements holds:Simulation-Quotienting Algorithms527• ∃s1 ∈ Post(s1 ) with Post(s2 ) ∩ Sim(s1 ) = ∅ and s2 ∈ Remove(s1 ),• Post(s2 ) ∩ Sim(s1 ) = ∅ for all s1 ∈ Post(s1 ).From (c), it follows that whenever Remove(s1 ) = ∅ for all s1 ∈ S, then:∀s1 ∈ S. ∀s2 ∈ Sim(s1 ). ∀s1 ∈ Post(s1 ). Post(s2 ) ∩ Sim(s1 ) = ∅.Therefore, on termination, the relation R = { (s1 , s2 ) | s2 ∈ Sim(s1 ) } is a simulation forTS. Assertion (b) implies that R agrees with ,TS , as ,TS is the coarsest simulation forTS.Lemma 7.82.Termination of Algorithm 36For each pair (s2 , s1 ) ∈ S×S, state s2 is inserted in (and removed from) the set Remove(s1 )at most once.In particular, Algorithm 36 requires at most O(|S|2 ) iterations.Proof: Assume s2 ∈ Remove(s1 ) and let s1 be the state that is selected in the outermost/ Pre(Sim(s1 )) (by part (a) of the loop invariant established in the proofiteration.

Then s2 ∈/ Pre(Sim(s1 )) in all furtherof Theorem 7.81). Since the simulator sets are decreasing, s2 ∈iterations: the only possibility to insert s = s2 in Remove(s1 ) is when s ∈ Pre(s̄2 ) forsome state s̄2 ∈ Sim(s1 ) with Post(s) ∩ Sim(s1 ) = { s̄2 }. But then s2 = s ∈ Pre(Sim(s1 )).Thus, s2 will never be added to Remove(s1 ) once it has been deleted from Remove(s1 ).This lemma is the starting point for deriving the time complexity of Algorithm 36. Let Mbe the number of edges in the state graph of TS and assume M |S|. Assume that listrepresentations for the sets of predecessors Pre(·) are available.