University of Technology and Design, Singapore University of Singapore, Singapore ‡ Nanyang Technological University, Singapore {shaojie_zhang, sunjun, junwei_ma}@sutd.edu.sg, {suncn, dongjs}@comp.nus.edu.sg, [email protected] † National

ignore other classes of symmetries which could reduce state space significantly. As a result, symmetries in the underlying state space are only partially discovered. In this work, we develop a novel approach for symmetry detection which addresses these two limitations. Not restricted to a particular modeling language, our approach works for general concurrent models (i.e., concurrent composition of finitestate machines which could communicate through channels, synchronous events or shared memories) in a fully automatic way. Further, it is able to detect many kinds of process symmetries and data symmetries together. The workflow of I. I NTRODUCTION our approach is shown in Figure 1. In practice, a certain (sometimes rich) degree of symmetries First, a concurrent model is translated into a semanticsis ubiquitous in concurrent and distributed systems [26], [36]. equivalent nondeterministic sequential model using existing A number of representative real-world complex networks, approaches [3], [25]. The motivation behind is two-fold. First, it including a broad selection of biological, technological and is nontrivial to analyze concurrent models whose behaviors are social networks, are found to have a nontrivial symmetric not obvious, such as subtle flexible communication patterns and structure [26]. In theory, given a model, a symmetry is an numerous possible interleavings between processes. Second, we automorphism of its underlying state space (which can be can take advantage of well-developed static analysis techniques viewed as a graph). A naive (and complete) symmetry detection for sequential models. The worst case complexity of the method thus needs to explore the complete space. In general, translation is linear in the total number of atomic statements if a symmetry detection method is performed on a state space, of all processes. then the complete state space is required to be constructed prior Second, we consider the problem of discovering symmetries to the exploration. It is not only computationally expensive from a new angle. Our key insight is recognizing the similarity or impossible, but also against the original goal of symmetry between the role of symmetries in constraint programming and reduction to reduce the explored state space. A practical and that in model checking. Our analysis transforms the sequential popular approach is to use static analysis to derive symmetries model into a constraint satisfaction problem, and extracts a at model level [22], [34]. graphical representation of the CSP called colored graph. Each Existing symmetry reduction approaches have two main automorphism of the colored graph is proved to correspond to limitations in the identification of symmetries in a model. one in the concurrent model, which is effectively discovered by First, the soundness and efficiency highly depend on human applying a graph automorphism generator named Saucy [12]. efforts. It is generally too difficult for machines to look through The detected symmetries can be used later to speed up the the behavior of concurrent models to pin down symmetries performance of a state space exploration tool, e.g., a model correctly. Most approaches require users to provide correct checker or a simulator. symmetries, which is tedious and error-prone. Some languages The above steps can be performed fully automatically. provide dedicated instructions for specifying symmetries [22], The effectiveness and efficiency of our approach have been [30], [31]. For instance, Murϕ provides a special data type with demonstrated via a variety of systems. a list of syntactic restrictions. All values that belongs to this The rest of this paper is organized as follows. Section II type are equivalent. Although there are automatic approaches presents a simple motivating example. Section III introduces which do not need expert insights, they are designed for specific relevant background information and terminology used throughlanguages [24], [23], or require models to be written in specific out this paper. Section IV describes our automatic symmetry patterns [13], [14]. Thus they trade off generality for efficiency, detection approach in details and proves the soundness of our and consequently a user has to transform his problem into a approach. Section V presents the results of our case studies. form amenable to the approach. Second, existing approaches Section VI surveys related work. Section VII concludes the can only handle a specific class of symmetries and largely paper and discusses possible future work. Abstract—We present an automatic approach to detecting symmetry relations for general concurrent models. Despite the success of symmetry reduction in mitigating state explosion problem, one essential step towards its soundness and effectiveness, i.e., how to discover sufficient symmetries with least human efforts, is often either overlooked or oversimplified. In this work, we show how a concurrent model can be viewed as a constraint satisfaction problem (CSP), and present an algorithm capable of detecting symmetries arising from the CSP which induce automorphisms of the model. To the best of our knowledge, our method is the first approach that can automatically detect both process and data symmetries as demonstrated via a number of systems.

c 2013 IEEE 978-1-4799-0215-6/13/$31.00

15

ASE 2013, Palo Alto, USA

Fig. 1: Automatic symmetry detection workflow

II. M OTIVATING E XAMPLE

Existing data symmetry detection approaches [10], [22] rely on scalarset annotations to discover fully symmetric components (i.e., components which are identical up to rearranging their identifiers). Although values of all label variables are fully symmetric in this case, that is, permuting the values 1 to 0 and 0 to 1 for all label variables together over all the states and transitions of the state space results in the same state space, the arithmetic operations on the variables prohibit the use of scalarsets. Further, the protocol does not take message-passing paradigm, so the approaches [13], [14], [24], [23] for detecting process symmetries are not applicable. Moreover, as far as we know, there is no approach that considers process and data symmetries which are not both full symmetries at the same time, i.e., no existing approaches can find all symmetries in this example.

In the following, we use a token circulation protocol [2] as a running example. All the agents, or nodes, are deployed in a directed ring. The protocol requires the existence of a leader. Each agent has two single-bit variables recording its token and label and one Boolean constant indicating whether it is a leader. Only agents that are adjacent can interact (the source node is the initiator and the target is the responder). During an interaction, two agents update both of their states according to two predefined transition rules . If two agents have the same label, the responder is a leader and the initiator is not, the responder sets its label to the complement of the initiator’s label; otherwise the responder copies the label from the initiator. If an interaction triggers a label change, a token is passed from the initiator to the responder. Starting from an arbitrary configuration, the protocol guarantees that eventually III. P RELIMINARIES there is always one and only one agent holding a token. This section is devoted to the background knowledge of The concurrent model of this protocol with N agents is symmetry reduction in one application area of state space described in Figure 2 using the syntax of Communicating exploration, i.e., model checking, and the relevant concepts of Sequential Programs [32]. Process Rule1 (or Rule2 ) defines constraint satisfaction problems. how an initiator u interacts with a responder v. Every time there is an interaction in the network, the initiator A. Model Checking with Symmetry Reduction and responder must update themselves according to the two We present our work in the setting of Labeled Transition transition rules. A rule is applicable only if the guard condition Systems (LTSs). An LTS is a tuple L = (S, init, Σ, →) where (e.g., !leader[v] ∧ label[u]! = label[v]) is satisfied. An event S is a finite set of states, init ∈ S is the initial state, Σ is a finite (e.g., rule2 ) may be attached with variables updating (e.g., set of events and →: S × Σ × S is a labeled transition relation. token[u] := 0; token[v] := 1; label[v] =: label[u]). The A permutation σ is said to be an automorphism of an LTS L whole token circulation protocol is described as process iff it preserves the transition relation and the initial state, i.e., T okenCirculation, which is the interleaving (modeled by e e (∀s1 , s2 ∈ S; e ∈ Σ. s1 → s2 ⇒ σ(s1 ) → σ(s2 )) ∧ σ(init) = the operator |||) of all possible interactions in the network. init. A group G is an automorphism group of L iff every Initially, the system can be in any possible configuration and σ ∈ G is an automorphism of L. A permutation σ is said to be the initial variable valuation is omitted here for simplicity. an invariance of L and property φ iff it is an automorphism of L and σ(φ) ≡ φ where ≡ denotes logical equivalence under all propositional interpretations [17]. G is an invariance group of L Rule1 (u, v) = [!leader[u] ∧ leader[v] ∧ label[u] = label[v]] rule1 and φ iff every σ ∈ G is an invariance of L and φ. Given a state {token[u] := 0; token[v] := 1; label[v] := 1 − label[u]; } s ∈ S, the orbit of s is the set θ(s) = {t| ∃σ ∈ G. σ(s) = t}, → Rule1 (u, v); i.e., the equivalence group which contains s. From the orbit Rule2 (u, v) = [!leader[v] ∧ label[u]! = label[v]] rule2 of state s, a unique representative state rep(s) can be picked {token[u] := 0; token[v] := 1; label[v] := label[u]; } such that for all s and s0 in the same orbit, rep(s) = rep(s0 ). → Rule2 (u, v}; Intuitively, if σ is an invariance of φ, states of the same orbit T okenCirculation() = (|||x : 0..N − [email protected] are behaviorally indistinguishable with respect to φ. Based on (Rule1 (x, (x + 1) mod N )|||(Rule2 (x, (x + 1) mod N )); this observation, an LTS L can be turned into a quotient LTS LG where states in the same orbit are grouped together. If G Fig. 2: Concurrent model of token circulation protocol is an invariance group of L and φ, then L satisfies φ iff LG satisfies φ [8]. Simple as the protocol is, the protocol exhibits non-trivial There are two common types of symmetries for improving symmetries: (a) process symmetries that rotate every process the performance of model checking. A process symmetry following the network direction; (b) data symmetries that swap is a permutation on identifiers of concurrent processes. A the label values; (c) the combinations of process and data data symmetry is a permutation on data values. For example, symmetries that permute processes and label values together. suppose a state st is (s1 , s2 , · · · , sn ) where si is the local

16

state valuation of process i. If σ is a process symmetry on the process ids {1, 2, · · · , n}, then σ acts on st in the form σ(st) = (sσ(1) , sσ(2) , · · · , sσ(n) ); if it is a data symmetry, then σ acts on st in the form σ(st) = (σ(s1 ), σ(s2 ), · · · , σ(sn )).

Algorithm 1: Overview of our approach 1 2 3 4

B. Constraint Satisfaction Problem

5 6

autos := ∅; V L := ∅; csps := ∅; SeqModel := Concurrent2Sequential(CurModel) identify the set of global variables V G in SeqModel; foreach summand sum in SeqModel do identify the set of local variables locals of sum; V L := V L ∪ locals; foreach function or enabling condition f in sum do csps := csps ∪ {Transform(f )};

A constraint satisfaction problem (CSP) is a triple (V, D, C) 7 where V is a finite set of variables, D is a set of finite domains 8 and C is a finite set of constraints. Each variable vi ∈ V has 9 csps := csps ∪ {Transform(init)}; an associated domain Di ∈ D of possible values. A literal is 10 autos := DetectSymmetries (Merge(csps), V G, V L); a statement of the form vi = d where vi ∈ V and d ∈ Di . For any literal l of the form vi = d, we use var(l) to denote its variable vi . The set of all literals is denoted by χ. An assignment is a set of literals, each of which is a variable LTS of the original concurrent model. Lastly, we present two valuation of the CSP. A solution of a CSP is a complete lightweight but effective optimization methods. assignment which satisfies each constraint in C. A constraint c is defined over a set of variables, and the set is denoted as A. Step 1: Conversion from Concurrent to Sequential Var (c). We briefly introduce the principle of modeling concurrent A solution symmetry is a permutation of literals that preserves the set of solutions [9]. A constraint symmetry is a solution models by means of nondeterministic sequential models. The symmetry that preserves the constraints of the CSP [9]. But corresponding sequential model can be built by simulating a solution symmetry may not be a constraint symmetry. For the behavior of the concurrent model and keeping track of example, a CSP is (V = {x, y, z}, D = {1, 2, 3}, C = {x < local states of each process and global states all the time. y, y < z}). It only has one solution {x = 1, y = 2, z = 3}. Basically, the preparatory step of the transformation is to One of its solutions symmetries is (x = 2, x = 3). But it introduce a new integer variable state for each process in is not a constraint symmetry, because it maps the literals the model to represent its control points, and then a syntactic {x = 2, y = 3} which satisfies x < y to {x = 3, y = 3} which transformation is performed to translate each statement into one does NOT satisfy it. For a CSP (V, D, C), a variable symmetry or more sequential statements recursively. Then a concurrent σ is a permutation on V such that for any constraint c ∈ C, model is reduced into a sequential one which captures all its {v1 =a1 , · · · , vn =an } satisfies c iff {σ(v1 )=a1 , · · · , σ(vn )=an } behaviors. Note that the idea of linking concurrent models to satisfies c; a value symmetry σ is a permutation on D such nondeterministic sequential models goes back to the work of that for any constraint c ∈ C, {v1 =a1 , · · · , vn =an } satisfies Ashcroft and Manna [3], [20] for proving the correctness of c iff {v1 =σ(a1 ), · · · , vn =σ(an )} satisfies c. A variable-value concurrent programs. The detailed transformation process is symmetry is a permutation of the literals (i.e., V × D) that is also explained in [37]. The transformation is general enough to a constraint symmetry. Note that a variable-value symmetry is handle three different types of systems with respect to execution not necessarily a composition of a variable symmetry and a patterns, i.e., sequential and parallel systems with synchronous and asynchronous communication. Therefore our approach is value symmetry. not specific to one particular specification language. Moveover, IV. AUTOMATIC S YMMETRY D ETECTION for a concurrent model, its corresponding sequential model can In the section, we describe an automatic approach to be extracted in linear time [37]. The resulting model has the detecting the symmetries of a concurrent model. It translates total number of atomic statements of all processes in the worst a concurrent model into a CSP whose symmetries can be case. exploited using the state-of-the-art detection approaches for Figure 3 shows the sequential model for the token circulation CSPs. protocol. The nondeterministic sequential model is written in Algorithm 1 gives an overview of the overall approach. There a single process with data variables that describes a system as are three main steps. The first step, as described in procedure a set of guarded and nondeterministic transitions. It contains Concurrent2Sequential, converts a concurrent model CurModel a single parameterized recursive process definition and the into its semantics-equivalent nondeterministic sequential model initial parameter valuations of this process. The left-hand side SeqModel. The second step, as described in lines 3-9, separately of the process definition is a process name with a vector of transforms each enabling condition and each next-state program data parameters. Here we refer to these parameters as global in SeqModel, and its init statement to a semantics-equivalent variables. An addition operator in the right-hand side ‘sums’ CSP as shown by Procedure Transform. These CSPs are then a list of nondeterministic transitions, to which we refer to as merged into one single CSP. The third step, detects variable, summands. A summand has a declaration of local variables value and variable-value symmetries in the merged CSP, as followed by an enabling condition, an event (if any) and a described in Procedure DetectSymmetries. Further, we prove next-state program from left to right. Each local variable can be that each detected symmetry is a real automorphism of the evaluated to any value of its type nondeterministically. It is read-

17

type AG : 0..N − 1 type BIT : 0..1 proc TokenCirculation(BIT[N ] token, BIT[N ] label, BOOL[N ] leader) = AG u1 .AG v1 .[v1 = (u1 + 1) mod N ∧!leader[u1 ] ∧ leader[v1 ] ∧ label[u1 ] = label[v1 ]] rule1 {token[u1 ] := 0; token[v1 ] := 1; label[v1 ] := 1 − label[u1 ]; } → TokenCirculation(token, label, leader) + AG u2 .AG v2 .[v2 = (u2 + 1) mod N ∧!leader[v2 ] ∧ label[u2 ]! = label[v2 ]] rule2 {token[u2 ] := 0; token[v2 ] := 1; label[v2 ] := label[u2 ]; } → TokenCirculation(token, label, leader); init TokenCirculation(∗);

Fig. 3: Sequential model of the token circulation protocol only and cannot be of array type1 . Executability of a summand is decided by its enabling condition that is a Boolean expression; the action of the summand is decided by the event name; the effect of the summand is decided by its next-state program which updates the global variables. A next-state program is composed of a sequence of statements. A statement can be an assignment, conditional, or while-loop statement. Besides, there is an initial valuation of global variables denoted by init, which is the entry where the process starts to execute. The symbol ∗ denotes the nondeterministic choice of all possible evaluations of global variables. For the running example, the transition in Process Rule1 (resp. Rule2 ) is transformed into the first (resp. second) summand in the sequential model. There are two process identifiers used in each transition from the domain {0 · · · N −1}. The initiator and responder ids u and v are transformed into u1 and v1 (resp. u2 and v2 ) in the first (resp. second) summand. B. Step 2: Transformation from the Sequential Model to a CSP We describe how to convert a function or the init statement into the static single assignment form (SSA) [11] below, from which an equivalent CSP is derived. SSA is a form of a semantics-preserving intermediate representation of a program, which requires that each variable be assigned exactly once. The key feature of SSA is that each variable with the same name always has the same value in everywhere in the program. The immutability of variables is the primary reason why we transform each function into a constraint system by the use of SSA. Converting ordinary source code into SSA is relatively straightforward. In essence, it replaces the target variable of each assignment with a fresh name. Every usage of this variable in the succeeding statements is replaced with the new name, until a new assignment to the same variable occurs. We call the existing variables original variables, and other new variables versioned variables. Further, SSA defines an artificial function φ to represent the choice between different branches of a conditional statement defined formally as follows. A new Boolean variable b, called 1 If a local variable is an array, the language can be extended to support it easily, as we have done in our tool.

decision variable, is introduced to store the value of the condition and the if and else branches are converted separately. For each variable x defined in the if or else branch, an additional assignment x000 := φ(x0 , x00 , b) is inserted at the end of the block to achieve branch selection, where x0 and x00 are the last definitions of x in the if and else branches respectively. φ(x0 , x00 , b) = if b then x0 else x00 Still, converting a program to SSA form becomes more complicated when while-loop statements are involved. A whileloop can be equivalently regarded as an infinite number of nested conditional statements. But it is impractical to transform it into such conditional statements. So the assumption here is that any loop can be finished in a finite number of iterations. In this way, we reduce the problem of converting a loop to converting a list of conditional statements. Note that this assumption puts little limitation on our approach. Because the loop considered here is the loop included in one next-state program that is atomically executed. It is rare for a practical system to put the whole loop in one atomic step. Another challenge is handling array manipulation. The reason is that a new assignment statement of an array does not necessarily kill all the old values in the array. For instance, the meaning of the assignment A[i] := A[i] + 5 is twofold. First, it increases the value of the ith element in the array A by 5. Second, all the values of other elements are unchanged. We cannot simply assign the left-hand side with a new name, which loses the second meaning. Thus we define a function ϕ as follows to handle array assignments. Suppose an array assignment is array[index] := value and array0 is the latest name of array before the assignment in the SSA form. We replace the original assignment with array1 := ϕ(array1 , array0 , index, value) where array1 is a fresh name. Note that ϕ can be a polymorphic function so as to handle multi-dimensional arrays. array1 := ϕ(array1 , array0 , index, value) = array1 [index] = value∧ ∀j 6= index. array1 [j] = array0 [j] Take the next-state program of the first summand in Figure 3 (i.e., token[u1 ] := 0; token[v1 ] := 1; label[v1 ] :=

18

1 − label[u1 ];) as an example. Its SSA form is

A variable node is created for each variable in c. An array represents a collection of scalar variables. So a distinct variable token1 := ϕ(token1 , token, u1 , 0) node is created for each element of the array. A constraint node token2 := ϕ(token2 , token1 , v1 , 1) label1 := ϕ(label1 , label, v1 , 1 − label[u1 ]) is created for c. A value node is created for each value of each variable in c. An assignment node is created for each allowed The SSA form we obtain can be more succinct by applying assignment of c. Edges connect each value node to its variable copy propagation technique, commonly used in compiler node, each assignment node to the value node representing optimization. It eliminates unnecessary temporary copies of a each variable-value literal occurring in the assignment, and value generated by our transformation, and further facilitates each assignment node to the constraint node. So the number our symmetry detection approach. An assignment is an identity of nodes in the colored graph is the sum of the number of assignment if it is in the form x := y which assigns the value of variables, literals, constraints and allowed assignments, and the y to x and y is either a variable or a constant. Copy propagation number of edges is the sum of the number of literals, allowed is the process of replacing the occurrences of targets of identity assignments and variables in allowed assignments. assignments with their values. The graphs for all constraints are combined into a single The SSA form of a program always has the same behaviors as the original program [11]. After the conversion of a graph, called colored graph. The coloring scheme for this graph function to SSA, the next conversion from SSA to a CSP is described in three rules: • all variable nodes with the same domain have the same is straightforward. Each assignment is directly mapped to unique color; a constraint by interpreting each assignment operator as an • for a variable, all of its value nodes have the same unique equivalence operator. Both representations are very similar. color. If two variables have the same color, their value It is easy to know the SSA and its CSP representation have nodes have the same color; equivalent behaviors as the following proposition states. • for a constraint, its assignment nodes all have the same Proposition 1. Given an SSA representation P, let CP be the unique color. If two constraints have the same color, their CSP converted from P. If for an input I the execution of P assignment nodes have the same color. produces valuations V for all variables, then I and V is a It addresses symmetries by computing the automorphisms of solution of CP and vice versa. the colored graph. It has been proved that each automorphism For an enabling condition, since it is already a constraint, it of this graph corresponds to a constraint symmetry as restated does not need any transformation. For the init statement, we in the following theorem. convert it into a constraint in a very similar way. Suppose the Theorem 2. [29] Let C = (V, D, C) be a CSP. Its colored process in the sequential model is P (Dom1 v1 , · · · , Domn vn ) graph G is constructed as illustrated above. Suppose σ is an and its init statement is P (a1 , · · · , an ). It is converted to automorphism of G and s is an assignment of C. For each v1 = a1 ∧ · · · ∧ vn = an . Then we simply combine all the constraint c ∈ C, s satisfies c iff σ(s) satisfies c. constraints derived from each next-state program, enabling Before applying this method to our problem, we have to condition and the init statement to build one large CSP for address the concern raised by the differences of ordinary CSPs this whole sequential model. For the running example, the conversion step builds the and the CSP we convert the sequential model into. Some corresponding CSP for its sequential model as shown in variables in a sequential model cannot be used at the same Figure 4. Since its init statement represents all possible time, local variables in different summands for example. So evaluations of global variables, it has no effect on symmetry for its corresponding CSP, it is unreasonable to detect variable symmetries between those variables. Therefore, the original breaking in the CSP and thus is skipped for simplicity. coloring scheme is refined such that variable nodes which have C. Step 3: Symmetry Detection on CSP the same domain are of the same unique color iff Next we explain the procedure to discover constraint • each of them is a local variable of the same domain in symmetries in the merged CSP which we denote as CF in the same summand, the following. First, we present the state-of-the-art symmetry • or each of them is an original global variable of the same detection method for CSP, on which our detection approach is domain, based. However, considering the role each constraint plays in • or each of them is the latest version of a global variable the sequential model, this method is not completely suitable of the same domain. in terms of correctness and performance. To cope with this It is not difficult to show that each automorphism found under problem, we describe our alternations as follows. the new coloring strategy is also an automorphism under Our approach is based on the automatic symmetry detection the original coloring strategy. So Theorem 2 still holds. The method for CSP proposed by Puget [29]. It allows us to detect soundness of our work is stated as follows. variable symmetries, value symmetries and non-trivial ones involving both variables and values. For each constraint, the Theorem 3. Let L = (S, init, Σ, →) be its labeled transition approach first calculates all the allowed assignments. Then the system of a concurrent model M. Each automorphism σ we graph of this constraint c is constructed in the following way. get in Algorithm 1 is an automorphism of L.

19

V D

C

= {u1 , v1 , u2 , v2 , leader[N ], token[N ], label[N ], token1 [N ], token2 [N ], token3 [N ], label1 [N ]} = {AG, AG, AG, AG, BOOL, BIT, BIT, BIT, BIT, BIT, BIT } v1 = (u1 + 1) mod N ∧!leader[u1 ] ∧ leader[v1 ] ∧ label[u1 ] = label[v1 ] token1 [u1 ] = 0 ∧ (∀t ∈ AG.t 6= u1 → token1 [t] = token[t]) token2 [v1 ] = 1 ∧ (∀t ∈ AG.t 6= v1 → token2 [t] = token1 [t]) label1 [v1 ] = 1 − label[u1 ] ∧ (∀t ∈ AG.t 6= v1 → label1 [t] = label[t]) = v2 = (u2 + 1) mod N ∧!leader[v2 ] ∧ label[u2 ]! = label[v2 ] token3 [u2 ] = 0 ∧ (∀t ∈ AG.t 6= u2 → token3 [t] = token[t]) token2 [v2 ] = 1 ∧ (∀t ∈ AG.t 6= v1 → token2 [t] = token3 [t]) label1 [v2 ] = label[u2 ] ∧ (∀t ∈ AG.t 6= v2 → label1 [t] = label[t])

Fig. 4: Constraint satisfaction problem of the token circulation protocol e

Proof sketch By definition, we must show that (i) if s1 → e s2 , then σ(s1 ) → σ(s2 ), and (ii) σ(init) = init. Suppose P is an equivalent sequential model of M, and e s1 → s2 corresponds to the execution of the summand sum of P. Without loss of generality, we assume there is only one e global variable vg in P and one local variable vl in sum. s1 → s2 is assumed to denote executing sum when vg := value1 and vl := value2 . That is, when vg := value1 and vl := value2 , its enabling condition fe is true, event e is executed and global variables are updated in its next-state function fn which leads to state s2 . Suppose C is the constraint satisfaction problem converted from P in Algorithm 1. By Theorem 1, all the constraints converted from fe and fn are satisfied when vg = value1 and vl = value2 . By Theorem 3, σ is a constraint symmetry of C. So all of the constraints from fe and fn are also satisfied when σ(vg = value1 ) and σ(vl = value2 ). Again by Theorem 1, we e get σ(s1 ) → σ(s2 ). Similarly, we can prove σ(init) = init.

three label variables clockwise still yields the same graph; swapping any literals of the form label[i] := 0 and label[i] := 1 for all 0 <= i < 3 in all the assignments yields the same graph.

Note that the inverse of the theorem may not hold. For example, if two processes of the same type identical up to swapping their process identifiers are intentionally modeled as processes of two different types, this process symmetry is not reflected in its corresponding colored graph. The number of nodes in the colored graph of a CSP is the sum of the number of literals, which is the product of the variable domain sizes, and the number of allowed assignments for constraints. For a constraint with n variables, it may have O(mn ) possible assignments in the worst case, where m is the size of the largest domain. The time complexity of computing allowed assignments of one constraint is O(mn ), and the time and space complexity of constructing the colored graph for a CSP accumulate to t × O(mn ) where t is in the number of constraints. Figure 5 shows a part of the colored graph obtained from the CSP of the running example with N = 3. Due to space restriction and graph complexity, we make the following alternations for simplicity in order to help users better understand its inherent symmetries while still preserving the essence of the graph. This graph fragment shown is built from part of the first constraint in the CSP, i.e., v1 = (u1 + 1) mod N ∧ label[u1 ] = label[v1 ]. We skip the representation of all nodes generated from v1 = (u1 +1) mod N and variable and value nodes for v1 and u1 . Note that rotating

Example For the running example, assume there are three processes with ids 0, 1 and 2, it has 3 process symmetries from rotating the processes following the direction of the network, i.e., (0)(1)(2), (0, 1)(1, 2), (0, 2)(1, 2)2 ; it has 2 data symmetries from swapping all the possible values of all label variables, i.e., (0)(1), (0, 1). Further, new symmetries are introduced by the product of these automorphisms. Therefore, we discover 6 symmetries in total.

Fig. 5: Part of the colored graph of the running example’s CSP

D. Optimization In the step of symmetry detection, we perform two lightweight but effective optimization techniques, the first one to speed up the construction of the colored graph and the second to remove symmetries which are useless for model checking. 1) Breaking Down Array Writing Constraints: Each array writing constraint is involved with at least all the variables of two arrays, which often becomes a performance bottleneck. In order to reduce the time consumption, one straightforward way is keeping the number of variables as small as possible. We transform it into K + 1 simple constraints each involving 2 Permutations are written in the cyclic notation. If a , a , · · · , a are n 1 2 distinct elements of Ω, then the cycle (a1 , a2 , · · · , an ) denotes the permutation σ on Ω, i.e., for 1 ≤ i < n, σ(ai ) = ai+1 , σ(an ) = a1 and for any b ∈ Ω \ {a1 , a2 , · · · , an }, σ(b) = b.

20

much fewer variables in the following way3 where K is the array size, and refine the coloring strategy such that elements of different arrays have different colors. array1 [index] = value∧ (∀j ∈ {0, · · · , N − 1}.j 6= index → array1 [j] = array0 [j]) ⇓ array1 [index] = value array1 [0] = array0 [0] array1 [1] = array0 [1] ··· array1 [N − 1] = array0 [N − 1]

The soundness of the transformation is stated by the following theorem. Theorem 4. Let C be a CSP. and C 0 its corresponding CSP of C after transforming all array writing constraints. Then any constraint symmetry of C 0 is also a constraint symmetry of C.

true. That is, evals (array1 [index] = value) = true and ∀j ∈ {0, · · · , N − 1} and j 6= evals (index) such that evals (array1 [j] = array0 [j]) = true. Considering σ is a constraint symmetry, evalσ (s)(σ(array1 [index] = value)) = evalσ (s)(array1 [σ(index)] = σ(value)) = true and ∀j ∈ {0, · · · , N − 1} and j 6= evals (index) such that evalσ(s) (σ(array1 [j] = array0 [j])) = evalσ(s) (array1 [σ(j)] = array0 [σ(j)]) = true. Because j 6= evals (index), evalσ(s) (σ(j)) 6= evalσ(s) (σ(index)). So evalσ(s) (σ(c)) = true. Therefore, σ is also a constraint symmetry of C. 2) Removing Redundant Value Symmetries: The colored graph may contain some values of a variable which do not satisfy any constraint transformed from an enabling condition or the init statement. It means that those values are impossible to appear at any time during the execution of the system. Take the CSP (V = {x, y}, D = {{0, 1, 2}, {2, 3, 4}}, C = {x > 1, y = x + 1}) as an example. A value symmetry σ = (x := 0, x := 1) exists in the CSP. Suppose the constraint x > 1 is originally derived from the enabling condition and y = x + 1 is the next-state program of the same summand in the sequential model. So neither x := 0 nor x := 1 is valid in any state, which makes σ useless for reducing the state space. Therefore, it is safe and appropriate to remove these values during the graph construction in order to avoid redundant symmetries later. For each variable’s value, we record whether it appears in at least one allowed assignment of a constraint representing an enabling condition or the init statement. If not, it will be removed.

Proof Assume σ is a constraint symmetry of C 0 . The constraints in C are separated into two sets: one containing all the array writing constraints S1 and the other containing all the rest constraints S2 ; similarly, the constraints in C 0 are separated into two sets: one containing all the constraints transformed from an array writing constraints S10 and the other containing all the rest constraints S20 . Since S2 and S20 are identical, σ is also a constraint symmetry for S2 . We define a function evals which takes an assignment s and a constraint c, and returns the satisfaction of c when evaluated as s. Without loss of generality, we assume there are no multi-dimensional arrays in C. Suppose an array writing constraint c in S1 is array1 [index] = value ∧ (∀j ∈ V. C ASE S TUDIES {0, · · · , N − 1}.j 6= index → array1 [j] = array0 [j]). We have implemented the colored graph construction deIt is transformed into the list L containing N + 1 scribed in Section IV. The resulting graph is input to Saucy [12] constraints {array1 [index] = value, array1 [0] = which produces the generating set of the automorphism group array0 [0], · · · , array1 [N − 1] = array0 [N − 1]} in S10 . Let of a graph. For a group, its generating set is a subset whose s be an assignment of C. Because all elements of an array elements are denoted by generators such that each element of have the same color which is different from that of any other the group can be obtained by the combination of generators variable. For any element array0 [k] where k ∈ {0, · · · , N −1}, of this subset. A generating set is often used as a compact σ(array0 [k]) = array0 [k 0 ] where k 0 ∈ {0, · · · , N − 1}. This representation of a group. Then the generating set is input to also applies to elements of array1 . There are three conditions GAP [19] system which produces all the elements in the group. to be considered: (1) if the first constraint in L is evaluated All experiment data is online [1], part of which is summarized to false at s, i.e., evals (array1 [index] = value) = f alse, in Table I. then evals (c) = f alse. Because σ is a constraint The experimental cases cover a variety of computing systems. symmetry, evalσ (s)(σ(array1 [index] = value)) = From the perspective of execution patterns, they include evalσ(s) (array1 [σ(index)] = value) = f alse. So sequential systems, concurrent systems with synchronous evalσ(s) (σ(c)) = f alse; (2) Otherwise if there exists communication using shared variables or shared actions, i ∈ {0, · · · , N − 1} such that evals (array1 [i] = array0 [i]) = and distributed systems with asynchronous message passing f alse where i 6= evals (index), then evals (c) = f alse. mechanism. From the perspective of communication topologies, Since evals (array1 [i] = array0 [i]) = f alse, they include networks of layers, rings, trees, stars, complete evals (c) = f alse and evalσ(s) (σ(array1 [i] = array0 [i])) = graphs and hypercubes. From the perspective of symmetry evalσ(s) (array1 [σ(i)] = array0 [σ(i)]) = f alse. Because types, there are systems with only process symmetries, with i 6= evals (index), evalσ(s) (σ(i)) 6= evalσ(s) (σ(index)). only data symmetries and with both of them. Therefore, evalσ(s) (σ(c)) = f alse; (3) Otherwise, evals (c) = In Table I, |Colored Graph| denotes the size of the colored graph generated for each configuration, Construction denotes 3 For ease of presentation, we only show how to transform a writing constraint the time (in seconds) taken to construct the colored graph; of a one-dimensional array. It can be easily extended to multi-dimensional arrays. |Generators| denotes the size of the generating set of the

21

TABLE I: Symmetry detection results on a Linux laptop with Intel 2.8GHz and 3.8 GB memory System | Colored Graph | Construction(s) Saucy(s) |Generators| Reader-writer problem [33] 3 120 0.127 0.004 1 Peterson’s mutual exclusion protocol [28] 9 2311 0.695 0.018 8 12 4207 1.037 0.030 11 A prioritized resource allocator1[14] 2-2-3 393 0.553 0.004 4 3-3-4 534 0.902 0.005 7 Three-tiered architecture2[14] 3-3-2 419 0.480 0.005 5 3-3-3 452 0.515 0.006 6 4-4-3 518 0.508 0.006 8 Message passing in a hypercube network3[14] 5 3586 1.447 0.026 4 6 11555 3.317 0.066 5 Dining philosophers 10 556 0.492 0.005 1 20 1086 1.033 0.007 1 Miler’s scheduler [27] 10 487 2.665 0.001 0 Non-deterministic two-hop coloring protocol in undirected rings [2] 9 2013 0.788 0.012 5 12 3105 1.282 0.013 5 Self-stabilizing leader election protocol in complete graphs [18] 12 21155 2.684 0.394 11 15 164809 15.783 8.326 14 Self-stabilizing leader election protocol in directed rooted trees [6] 15 466 3.954 0.275 4 19 580 7.404 0.005 6 Self-stabilizing leader election protocol in rings [18] 9 21378 4.781 0.093 1 12 214169 51.265 1.266 1 Hanoi puzzle 3 891 0.523 0.003 1 6 6520 1.636 0.023 1 Scheduling the social golfer problem4[16] 3-3-4 1542 1.374 0.009 9 1 2 3 4

|Aut(G)|

Scalar

SCD

2

N

N

362880 479001600

N

Y

24 864

N

Y

N

Y

3840 46080

N

N

10 20

N

N

0

N

N

216 288

N

N

479001600 1307674368000

N

N

16 128

N

N

9 12

N

N

2 2

N

N

725760

N

N

144 1296 6912

A configuration is written in the form a0 − a1 − · · · − ak−1 , where client processes 0, 1, · · · , a0 have priority level 0, a0 + 1, a0 + 2, · · · , a1 have priority level 1, etc. A configuration is written in the form a1 − a2 − · · · − ak , which denotes that the system consists of k server processes and ai clients connected to server i. A configuration is denoted by the number of dimensions of the hypercube. Note that the configuration d is composed of 2d processes. A configuration is written in the form G-S -W where G is the number of groups, S is the number of golfers in one group and W is the number of weeks.

automorphism group G of the colored graph computed by As Table I shows, the overhead of our approach is quite low Saucy; Saucy denotes the time taken by Saucy to compute even for the systems with large automorphism groups. We study generators; |Aut(G)| denotes the size of G computed by GAP. the same cases as the static channel diagram approach [13], For systems whose configurations are not explained here, [14] (i.e., Peterson’s protocol, resource allocator, three-tiered a configuration of each one is identified by the number of architecture and message passing in a hypercube network) and processes/components. The last two columns denote whether our approach is able to find all symmetries reported in their these symmetries can also be detectable by two popular work efficiently. However, the effectiveness of our approach is existing approaches scalarset (Scalar) and static channel not limited to message passing systems or process symmetries. diagrams (SCD) (which are introduced in Section VI) without major changes on the original model, e.g., rewriting each A. Performance Improvement arithmetic or relational operation on variables related to process The performance bottleneck of our approach lies in the size identifiers into the logical disjunction of all explicit variable of the colored graph. First, allowed assignments for constraints values allowed by this operation, or remodeling the process often contribute the largest portion of the graph size. For a communication mechanism into channels only. For a system constraint with n variables, as discussed in Section IV-D1, with data symmetries, such as two-hop coloring protocol, in order to reduce its time consumption, one straightforward existing approaches are still unable to discover them even way is keeping n as small as possible. So we break down if the system is changed into the form the approaches require. a constraint into a set of sub-constraints and guarantee that

22

TABLE II: Symmetry reduction results I on a Windows laptop with Intel 3.4GHz and 8 GB memory with PAT 3.5 [32]

is shown that multi-representatives symmetry reduction stores more states than single-representative as expected. Here we consider the algorithm of calculating multiple representatives called local search in [15], which is only dependent on the generators of an automorphism group. A group with a large number of elements has a much smaller number of generators. So the multi-representatives approach is much faster than the single-representative one in most cases. It remains our future work to solve the COP problem efficiently for certain classes of automorphism groups in practice.

Model

States (Without Reduction) States With Reduction Gain Dining philosophers 10 154450 15489 90.0% 12 1684801 140536 91.7% 14 OM 1313052 Three-tiered architecture 3-3-2 7840 462 94.1% 3-3-3 21952 286 98.7% 4-4-3 188272 OT Non-deterministic two-hop coloring protocol in undirected rings 3 13824 442 96.8% 4 331776 8058 97.6% 5 OM OT -

VI. R ELATED W ORK The importance of detecting symmetries for state space exploration has garnered much interest in recent years and several methods have emerged. The discussion on each method will largely be focused on the answers to two questions: (1) How much effort is required from model designers? (2) How many kinds of symmetries can be detected?

the logical conjunction of sub-constraints is equivalent to the original constraint. This method has a side effect: it increases the number of constraints. Fortunately, this effect is negligible because the time consumption for computing allowed assignments is much more sensitive to the number of variables in a constraint than to the number of constraints, and the performance bottleneck is its time consumption instead of its memory. Second, we have observed that users may sometimes define larger variable domains than necessary. Our approach does not rely on the exact domain of variables, but can take advantage of it to construct a smaller colored graph.

A. Scalarset Method

B. Symmetry Reduction We apply detected symmetries to the depth-first exploration of the whole state spaces of system configurations. A classic canonicalization function [22] is used to calculate a unique representative for each equivalence class of states, i.e., applying all the automorphisms to a visited state to find the lexicographically smallest image. Table II contains the experimental results before and after symmetry reduction for part of systems configurations in Table I. In the table, States means the number of states stored, OM means exploring the configuration ran out of memory, OT means more than 2 hours, and Gain means the relative improvement on stored states brought by symmetry reduction. For the conducted experiments, the saving in terms of memory is 95.9% in average. The computational overhead of symmetry reduction stems from checking whether the unique representative state of a visited state has been explored. Thus calculating representative states would be costly in time if there are a large number of automorphisms. It is known as constructive orbit problem (COP), which is NP-hard in general [7]. In practice, only systems with full symmetries are supported by existing symmetry reduction approaches, because representatives can be efficiently calculated in polynomial time. One way of relaxing the prohibitive time requirement of COP is to allow multiple representatives for each equivalence class of states. Table III contains the experimental results for state space exploration without symmetry reduction, with symmetry reduction using unique representative, and with symmetry reduction using multiple representatives. From the table, it

One of the oldest and most widespread symmetry detection approaches is using scalarset. It is first introduced by Ip and Dill in the explicit model checker Murϕ [22]. Scalarset is a data type which determines an unordered finite set of consecutive integer values. It is a fully symmetric type, i.e., permuting any values of a scalarset type throughout the state space must result in an automorphism. So this method is only capable of handling fully symmetric components. For usage, a user may define a new scalarset type for a class of fully symmetric components and assign each component’s identifier to a unique value of this type. Then the verifier automatically extracts the automorphisms from scalarset types. In this way, scalarsets provide a convenient and efficient way for users to define symmetries, considering the number of automorphisms generated by a scalarset is the factorial of its size. This method is applied to several other model checkers like Spin [4], [5], Uppaal [21]. However, it has two disadvantages that impose a heightened burden on designers. First, the applicability of this method relies on designers to have expert insights to precisely identify identical components in a system. Second, in order to make sure the symmetry extraction method is sound, a much rigorous syntactic requirement is placed on operations of scalarsets to rule out all possible symmetry breaking constructs. Last but not least, it is applicable only for fully symmetric systems. It is worth to mention that the local variables in our work act as a much more generalized version of the popular scalarset. They both represent a subrange of values. A local variable may be the source of symmetries in a model, whereas a scalarset variable must be the source of symmetries in a model. Since scalarset variables have to be specified by designers, the lack of a computer-assisted approach results in correctly expressing symmetries as wholly the designers’ responsibility. But our approach automatically identifies which local variables are real symmetry makers and which operations are symmetry breaking constructs so as to remove all the burden from designers.

23

TABLE III: Symmetry reduction results II on a Windows laptop with Intel 3.4GHz and 8 GB memory with PAT 3.5 [32] Model

10 12 14 3-3-2 3-3-3 4-4-3 3 4 5

Without Reduction States Time (Sec) 154450 1684801 OM

15.3 212 -

7840 1.1 21952 3.6 188272 42.3 Non-deterministic 13824 10.3 331776 511 OM -

With Reduction (Unique) With Reduction (Multi) States Time (Sec) States Time (Sec) Dining philosophers 15489 14.2 106819 23.2 140536 242 1149178 341 1313052 3563 OM Three-tiered architecture 462 8.4 966 1.0 286 60.4 2290 5.1 OT 35524 103 two-hop coloring protocol in undirected rings 442 15.4 1567 4.6 8058 668 33415 160 OT 661454 5718

B. Static Channel Diagrams Donaldson and Miler design a fully automatic approach to detecting process symmetries for channel-based communication systems [13], [14]. Their approach also involves constructing a graph called static channel diagram from a Promela model, whose automorphisms possibly correspond to the automorphism of the Kripke structure along with the model. Each node is created for each process or channel. If a process possibly sends a message to a channel, then a directional edge is created from the process node to the channel node. Similarly, if a process possibly receives a message from a channel, then a directional edge is created from the channel node to the process node. All process (resp. channel) nodes representing the same type of processes (resp. channel) have the same unique color. The generators for the automorphism group in the static channel diagram are computed using a graph automorphism algorithm. But a computed generator may not be a real automorphism in the state space. In order to preserve the soundness of the detection approach, each generator obtained from the diagram has to be validated that it transforms the original program P into an equivalent program with the complexity O(|P| log |P|). Similar to scalarset approaches, there is a series of limitations on input Promela programs to rule out symmetry breaking constructs. One of them is disallowing the use of process identifiers in relational and arithmetic operations, which is commonly thought to be the source of breaking symmetries. However, it is not necessary the case in many systems such as the motivating example. They propose a straightforward strategy to relax this restriction, i.e., rewriting a relational or arithmetic operation into a disjunction of all possible combinations of variable valuations. But the validity checking for each generator would suffer a significant loss in performance because the size of the program becomes at most O(nk ) of the original one, where n is the largest size of domains of variables representing process identifiers and k is the highest arity of any relational or arithmetic operations involving these variables. Lastly, our method is remotely related to an on-the-fly symmetry detection and reduction approach proposed by Wahl and D’Silva [35]. It starts a reachability checking with the assumption that all processes are fully symmetric. As

each transition is analyzed, the asymmetries it induces are used to partition the processes. Our approach can deduce how an arbitrary transition breaks symmetries not limited to process symmetries prior to model checking. So combining two approaches can potentially improve the performance of symmetry reduction. VII. C ONCLUSION AND F UTURE W ORK The main contribution of our work is a new automatic symmetry detection approach. To the best of our knowledge, our study is the first work to relax all the syntactic restrictions on the model form, and also the first work to consider various process symmetries, data symmetries and their combinations. A variety of case studies showed that the overhead of symmetry detection is negligible and detected symmetries save the majority of a state space to be explored. A line of our future work is to design efficient algorithms for calculating representative states for automorphism groups that satisfy certain structural properties and are often used in practice. All existing symmetry detection approaches only work on one instance of a parameterized system at a time. We observe that, for a parameterized system, the distinctive features of symmetries are often determined by the essence of the system structure rather than concrete valuations of the parameters. So the other interesting line of future work is to provide a once-for-all solution of obtaining universal symmetries for the entire instances in a parameterized system. ACKNOWLEDGEMENTS We thank the anonymous reviewers for their invaluable comments. This work is supported by project “IDD11100102A/IDG31100105A” from Singapore University of Technology and Design and in part by NTU-NAP project: “Formal Verification on Cloud” from Nanyang Technological University.

24

R EFERENCES [1] http://www.comp.nus.edu.sg/~pat/detection/. [2] D. Angluin, J. Aspnes, M. J. Fischer, and H. Jiang. Self-stabilizing population protocols. ACM Transactions on Autonomous and Adaptive Systems, pages 643–644, 2008.

[3] E. Ashcroft and Z. Manna. Formalization of Properties of Parallel Programs. In Machine Intelligence, 1970. [4] D. Bosnacki, D. Dams, and L. Holenderski. Symmetric Spin. In SPIN, pages 1–19, 2000. [5] D. Bosnacki, L. Holenderski, and D. Dams. A Heuristic for Symmetry Reductions with Scalarsets. In FME, pages 518–533. 2001. [6] Canepa, Davide and Potop-Butucaru, Maria Gradinariu. Stabilizing token schemes for population protocols. CoRR, 2008. [7] E. Clarke, E. Emerson, S. Jha, and A. Sistla. Symmetry Reductions in Model Checking. In CAV, pages 147–158, 1998. [8] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 2000. [9] D. Cohen, P. Jeavons, C. Jefferson, K. E. Petrie, and B. M. Smith. Symmetry definitions for constraint satisfaction problems. Constraints, 11(2-3):115–137, 2006. [10] M. Cohen, M. Dam, A. Lomuscio, and H. Qu. A Data Symmetry Reduction Technique for Temporal-epistemic Logic. In ATVA, pages 69–83, 2009. [11] R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Transactions on Programming Languages and Systems, pages 451–490, 1991. [12] P. T. Darga, K. A. Sakallah, and I. L. Markov. Faster Symmetry Discovery using Sparsity of Symmetries. In DAC, pages 149–154, 2008. [13] A. F. Donaldson and A. Miller. Automatic Symmetry Detection for Model Checking Using Computational Group Theory. In FM, pages 631–631, 2005. [14] A. F. Donaldson and A. Miller. Automatic Symmetry Detection for Promela. Journal of Automated Reasoning, pages 251–293, 2008. [15] A. F. Donaldson and A. Miller. On the Constructive Orbit Problem. Annals of Mathematics and Artificial Intelligence, 57(1):1–35, 2009. [16] I. Dotú and P. Van Hentenryck. Scheduling Social Golfers Locally. In CPAIOR’05, 2005. [17] E. A. Emerson and A. P. Sistla. Symmetry and Model Checking. Formal Methods in System Design, pages 105–131, 1996. [18] M. J. Fischer and H. Jiang. Self-stabilizing Leader Election in Networks of Finite-state Anonymous Agents. In OPODIS’06, 2006. [19] The GAP Group. GAP – Groups, Algorithms, and Programming, 2012. [20] J. F. Groote, A. Ponse, and Y. S. Usenko. Linearization in Parallel pCRL. Journal of Logic and Algebraic Programming, 2001.

[21] M. Hendriks, G. Behrmann, K. Larsen, P. Niebert, and F. Vaandrager. Adding Symmetry Reduction to UPPAAL. In FORMATS, pages 46–59. 2004. [22] C. N. Ip and D. L. Dill. Better Verification through Symmetry. Formal Methods in System Design, pages 41–75, 1996. [23] M. M. Jaghoori, M. Sirjani, M. R. Mousavi, E. Khamespanah, and A. Movaghar. Symmetry and Partial Order Reduction Techniques in Model Checking Rebeca. Acta Inf., pages 33–66, 2010. [24] M. M. Jaghoori, M. Sirjani, M. R. Mousavi, and A. Movaghar. Efficient Symmetry Reduction for an Actor-based model. In ICDCIT’05, pages 494–507, 2005. [25] R. A. Krzysztof and E.-R. Olderog. Verification of Sequential and Concurrent Programs. 1991. [26] B. D. MacArthur, R. J. Sa ´nchez-Garc´ia, and J. W. Anderson. Symmetry in Complex Networks. Discrete Applied Mathematics, pages 3525 – 3531, 2008. [27] R. Milner. Communication and Concurrency. 1989. [28] G. L. Peterson. Myths About the Mutual Exclusion Problem. Information Processing Letters, 1981. [29] J.-F. Puget. Automatic Detection of Variable and Value Symmetries. In CP, pages 475–489, 2005. [30] A. P. Sistla, V. Gyuris, and E. A. Emerson. SMC: a Symmetry-Based Model Checker for Verification of Safety and Liveness Properties. ACM Transactions on Software Engineering and Methodology, pages 133–166, 2000. [31] C. Spermann and M. Leuschel. ProB Gets Nauty: Effective Symmetry Reduction for B and Z Models. In TASE, pages 15–22, 2008. [32] J. Sun, Y. Liu, J. S. Dong, and J. Pang. PAT: Towards Flexible Verification under Fairness. In CAV, pages 709–714, 2009. [33] T. Wahl. Adaptive Symmetry Reduction. In CAV, pages 393–405. Springer-Verlag, 2007. [34] T. Wahl and A. Donaldson. Replication and Abstraction: Symmetry in Automated Formal Verification. Symmetry, pages 799–847, 2010. [35] T. Wahl and V. D’Silva. A Lazy Approach to Symmetry Reduction. Form. Asp. Comput., pages 713–733, 2010. [36] Y. Xiao, M. Xiong, W. Wang, and H. Wang. Emergence of Symmetry in Complex Networks. Phys. Rev. E, page 066108, 2008. [37] S. J. Zhang, J. Sun, C. Sun, Y. Liu, J. Ma, and J. S. Dong. Symmetry Detection for Model Checking. http://www.comp.nus.edu.sg/~pat/detection/report, 2013.

25