1EECS 219C: Computer-Aided VerificationSymmetry Reduction, Simulation/BisimulationSanjit A. SeshiaEECS, UC BerkeleyS. A. Seshia 2Today’s Lecture• Optimizations in Model checking– Symmetry Reduction• Simulation/Bisimulation2S. A. Seshia 3Simulation and BisimulationS. A. Seshia 4Simulation --- Intuition • Two finite state machines (Kripkestructures) M and M’• M’ simulates M if – M’ can start in a similarly labeled state as M– For every step that M takes from s to t, M’ can mimic it by stepping to a state with similar label as t3S. A. Seshia 5Simulation• M = (S, S0, R, L) and M’ = (S’, S0’, R’, L’)• A relation H ⊆ S x S’ is a simulation relation between M and M’ means that: For all (s, s’), if H(s, s’) then:– L’(s’) = L(s) ∩ AP’– For every state t s.t. R(s, t) there is a state t’ such that R’(s’, t’) and H(t, t’)• M’ simulates M if – there exists a simulation relation H between them, and – For each s0∈ S0, there exists s0’ ∈ S0’ s.t. H(s0, s0’)S. A. Seshia 6ExampleAtomic propositions: go and stopWhich machine simulates which?4S. A. Seshia 7Bisimulation• M and M’ are bisimulation equivalent (bisimilar) if– M can match each step of M’ and vice-versa– Note: this is NOT the same as “M simulates M’ and M’simulates M”• A relation H ⊆ S x S’ is a bisimulation relation between M and M’ means that: For all (s, s’), if H(s, s’) then:– L’(s’) = L(s) ∩ AP’– For every state t s.t. R(s, t) there is a state t’ such that R’(s’, t’) and H(t, t’)– For every state t’ s.t. R’(s’, t’) there is a state t such that R(s, t) and H(t, t’)S. A. Seshia 8(Bi)Simulation and (A)CTL*• If M’ simulates M, then any ACTL* property satisfied by M’ is satisfied by M• If M’ and M are bisimilar, any CTL* property satisfied by one is also satisfied by the other5S. A. Seshia 9Symmetry ReductionS. A. Seshia 10Symmetry• Many systems have inherent symmetry– Overall system might be composed of k identical modules– E.g., a multi-processor system with k processors– E.g., a multi-threaded program with k threads executing the same code with same inputs– Anything with replicated structure• Question: How can we detect and exploit the symmetry in the underlying state space for model checking?6S. A. Seshia 11Symmetry in Behavior• Given a system with two identical modules– Run: s0, s1, s2, …– Trace: L(s0), L(s1), L(s2), …– Each si= (si1, si2, rest) comprises values to variables of both modules 1 and 2– If we can interchange these without changing the set of traces of the overall system, then there is symmetry in the system behaviorS. A. Seshia 12Exploiting Symmetry• If a state space is symmetric, we can group states into equivalence classes – Just as in abstraction• Resulting state graph/space is called “quotient” graph/space– Model check this quotient graph7S. A. Seshia 13Quotient (first attempt)M = (S, S0, R, L)Let be an equivalence relation on SAssume: s t iff L(s) = L(t)& s S0iff t S0Quotient: M’ = ( S’, S0’, R’, L’ )–S’= S/ , S0’= S0/ (states are equivalence classes with respect to )– R’([s], [t]) whenever R(s,t)– L’([s]) = L(s)S. A. Seshia 14Is that definition enough?Suppose we want to check an invariant:Does M satisfy ?Instead if we check:Does quotient M’ satisfy ?If M’ is constructed using the definition of on the previous slide, will the above check generate spurious counterexamples?8S. A. Seshia 15Stable EquivalencesEquivalence is called stable if:R (x, y) for every s in [x]there exists some t in [y] such that R (s,t)Claim: Suppose is stable, then:M satisfies iff M’ satisfies (Proof idea: show M and M’ are bisimilar)S. A. Seshia 16Detecting Symmetry• Given symmetry expressed as an equivalence relation between states, we know how to exploit it• How do we detect/compute this equivalence relation?– Need to characterize it more formally9S. A. Seshia 17Symmetry as Permutation• Symmetry in the state space can be viewed as “equivalence under permutation”• Permute the set of states so that the set of traces remains the same– A subset of states that remains the same under permutation forms the needed equivalence class• A representation of all possible such permutations represents symmetry in the system S. A. Seshia 18Automorphisms0,01,10,1 1,0A permutation function f : S S is an automorphism if:R(s, t) R(f(s), f(t))What is an example automorphism for this state space?10S. A. Seshia 19Automorphisms0,01,10,1 1,0f: f(0,0) = 1,1 f(1,1) = 0,0f(0,1) = 0,1 f(1,0) = 1,0g: g(0,0) = 0,0 g(1,1) = 1,1g(0,1) = 1,0 g(1,0) = 0,1A = { f, g, f g, id}The set of all automorphisms forms a group!S. A. Seshia 20Equivalence using AutomorphismsLet s t if there is some automorphism f such that f(s) = t (and L(s) = L(t) ∧ s ∈ S0iff t ∈ S0)The equivalence classes of an automorphism(sets mapped to themselves) are called orbitsClaim 1: is an equivalenceClaim 2: is stable (why? - HW)11S. A. Seshia 21Orbits0,01,10,1 1,0[ (0,0), (1,1) ][ (0,1), (1,0) ]S. A. Seshia 22Symmetry reduction[ (0,0),(1,1) ][ (0,1), (1,0) ]Map each state to its representative in the orbit12S. A. Seshia 23How Symmetry Reduction works in practice• A permutation (automorphism) group is manuallyconstructed– Syntactically specify which modules are identical • Orbit relation (equivalence relation) automatically generated from this– Using fixpoint computation (MC, Sec. 14.3)• An (lexicographically smallest) element of each equivalence class is picked as its representative•S0’ and R’ generated from orbit relation• Model checking explores only representative statesS. A. Seshia 24Symmetry reduction• Implemented in many model checkers• E.g., SMV, Mur (finite-state systems), Brutus (security
View Full Document
Unlocking...