Regular Symmetry Patterns (Technical Report)
Anthony W. Lin1 , Truong Khanh Nguyen2 , Philipp Rümmer3 , and Jun Sun4
Yale-NUS College, Singapore
2
Autodesk, Singapore
3
Uppsala University, Sweden
4
Singapore University of Design and Technology
1

Abstract. Symmetry reduction is a well-known approach for alleviating the state
explosion problem in model checking. Automatically identifying symmetries in
concurrent systems, however, is computationally expensive. We propose a symbolic framework for capturing symmetry patterns in parameterised systems (i.e.
an infinite family of finite-state systems): two regular word transducers to represent, respectively, parameterised systems and symmetry patterns. The framework
subsumes various types of “symmetry relations” ranging from weaker notions(e.g. simulation preorders) to the strongest notion (i.e. isomorphisms). Our framework enjoys two algorithmic properties: (1) symmetry verification: given a transducer, we can automatically check whether it is a symmetry pattern of a given
system, and (2) symmetry synthesis: we can automatically generate a symmetry
pattern for a given system in the form of a transducer. Furthermore, our symbolic language allows additional constraints that the symmetry patterns need tosatisfy to be easily incorporated in the verification/synthesis. We show how theseproperties can help identify symmetry patterns in examples like dining philosopher protocols, self-stabilising protocols, and prioritised resource-allocator protocol. In some cases (e.g. Gries’s coffee can problem), our technique automaticallysynthesises a safety-preserving finite approximant, which can then be verified forsafety solely using a finite-state model checker.

1

Introduction

Symmetry reduction [12, 19, 22] is a well-known approach for alleviating the state explosion problem in automatic verification of concurrent systems. The essence of symmetry reduction is to identify symmetries in the system and avoid exploring states thatare “similar” (under these symmetries) to previously explored states.
One main challenge with symmetry reduction methods is the difficulty in identifying symmetries in a given system in general. One approach is to provide dedicatedlanguage instructions for specifying symmetries (e.g. see [22, 28, 29]) or specific languages (e.g. see [13, 24, 25]) so that users can provide insight on what symmetries are
there in the system. For instance, Murϕ provides a special data type with a list of syntactic restrictions and all values that belong to this type are symmetric. Another approachis to detect symmetry automatically without requiring expert insights. Automatic detection of symmetries is an extremely difficult computational problem. A number ofapproaches have been proposed in this direction (e.g. [15, 16, 32]). For example, Donaldson and Miller [15, 16] designed an automatic approach to detecting process symmetries for channel-based communication systems, based on constructing a graph calledstatic channel diagram from a Promela model whose automorphisms correspond tosymmetries in the model. Nonetheless, it is clear from their experiments that existing
approaches work only for small numbers of processes.
In practice, concurrent systems are often obtained by replicating a generic behavioral description [31]. For example, a prioritised resource-allocator protocol [14, Section 4.4] provides a description of an allocator program and a client program in a network with a star topology (allocator in the center), from which a concurrent systemwith 1 allocator and m clients (for any given m ∈ Z>0 ) can be generated. This is infact the standard setting of parameterised systems (e.g. see [4, 30]), which are symbolic
descriptions of infinite families {Si }∞i=1 of transition systems Si that can be generated
by instantiating some parameters (e.g. the number of processes).
Adopting this setting of parameterised systems, we consider the problem of formulating and generating symbolic symmetry patterns, abstract descriptions of symmetries
that can be instantiated to obtain concrete symmetries for every instance of a parameterised system. A formal language to specify symmetry patterns should be able tocapture interesting symmetry patterns, e.g., that each instance Si of the parameterised
system S = {Si }∞i=1 exhibits the full symmetry Sn (i.e. invariant under permuting thelocations of the processes). Ideally, such a language L should also enjoy the following
algorithmic properties: (1) symmetry verification, i.e., given a symmetry pattern P ∈ L,
we can automatically check whether P is a symmetry pattern of a given parameterised
system, and (2) symmetry synthesis: given a parameterised system, we can automatically generate symmetry patterns P ∈ L that the system exhibits. In particular, if L issufficiently expressive to specify commonly occuring symmetry patterns, Property (1)would allow us to automatically compute which common symmetry patterns hold for agiven parameterised system. In the case when symmetry patterns might be less obvious,
Property (2) would allow us to identify further symmetries that are satisfied by the given
parameterised systems. To the best of our knowledge, to date no such languages havebeen proposed.
Contribution: We propose a general symbolic framework for capturing symmetry patterns for parameterised systems. The framework uses finite-state letter-to-letter wordtransducers to represent both parameterised systems and symmetry patterns. In the sequel, symmetry patterns that are recognised by transducers are called regular symmetry
patterns. Based on extensive studies in regular model checking (e.g. see [1, 4, 27, 30]),
finite-state word transducers are now well-known to be good symbolic representations of parameterised systems. Moreover, equivalent logic-based (instead of automatabased) formalisms are also available, e.g., LTL(MSO) [3] which can be used to specify
parameterised systems and properties (e.g. safety and liveness) in a convenient way. In
this paper, we show that transducers are not only also sufficiently expressive for representing many common symmetry patterns, but they enjoy the two aforementioned
desirable algorithmic properties: automatic symmetry verification and synthesis.
There is a broad spectrum of notions of “symmetries” for transition systems thatare of interest to model checking. These include simulation preorders (a weak variant)and isomorphisms (the strongest), e.g., see [6]. We suggest that transducers are not only
sufficiently powerful in expressing many such notions of symmetries, but they are also a
flexible symbolic language in that constraints (e.g. the symmetry pattern is a bijection)
can be easily added to or relaxed from the specification. In this paper, we shall illustrate2

this point by handling simulation preorders and isomorphisms (i.e. bijective simulation
preorders) within the same framework. Another notable point of our symbolic language
is its ability to specify that the simulation preorder gives rise to an abstracted systemthat is finite-state and preserves non-safety (i.e. if the original system is not safe, thenso is the abstracted system). In other words, we can specify that the symmetry pattern
reduces the infinite-state parameterised system to a finite-state system. Safety of finitestate systems can then be checked using standard finite-state model checkers.
We next show how to specialise our framework to process symmetries [12, 19, 22].
Roughly speaking, a process symmetry for a concurrent system S with n processes is apermutation π : [n] → [n] (where [n] := {1, . . . , n}) such that the behavior of S is invariant under permuting the process indices by π (i.e. the resulting system is isomorphic
to the original one under the natural bijection induced by π). For example, if the process
indices of clients in the aforementioned resource-allocator protocol with 1 allocator andm clients are 1, . . . , m + 1, then any permutation π : [m + 1] → [m + 1] that fixes 1 is aprocess symmetry for the protocol. The set of such process symmetries is a permutationgroup on [m+1] (under functional composition) generated by the following two permutations specified in standard cyclic notations: (2, 3) and (2, 3, . . . , m + 1). This is truefor every value of m ≥ 2. In addition, finite-state model checkers represent symmetry
permutation groups by their (often exponentially more succinct) finite set of generators. Thus, if S = {Sn }∞n=1 is a parameterised system where Sn is the instance withn processes, we represent the parameterised symmetry groups G = {Gn }∞n=1 (where
Gn is the process symmetry group for Sn ) by a finite list of regular symmetry patterns
that generate G. We postulate that commonly occuring parameterised process symmetrygroups (e.g. full symmetry groups and rotations groups) can be captured in this framework, e.g., parameterised symmetry groups for the aforementioned resource-allocator
protocol can be generated by the symmetry patterns {(2, 3)(4) · · · (m + 1)}m≥3 and{(2, 3, . . . , m + 1)}m≥3 , which can be easily expressed using transducers. Thus, using our symmetry verification algorithm, commonly occuring process symmetries for agiven parameterised system could be automatically identified.
The aforementioned approach of checking a given parameterised system against a“library” of common regular symmetry patterns has two problems. Firstly, some common symmetry patterns are not regular, e.g., reflections. To address this, we equip ourtransducers with an unbounded pushdown stack. Since pushdown transducers in general cannot be synchronised [5] (a crucial property to obtain our symmetry verification
algorithm), we propose a restriction of pushdown transducers for which we can recoverautomatic symmetry verification. Secondly, there are many useful but subtle symmetry
patterns in practice. To address this, we propose the use of our symmetry synthesis algorithm. Since a naive enumeration of all transducers with k = 1, . . . , n states does notscale, we devise a CEGAR loop for our algorithm in which a SAT-solver provides a candidate symmetry pattern (perhaps satisfying some extra constraints) and an automatabased algorithm either verifies the correctness of the guess, or returns a counterexample
that can be further incorporated into the guess of the SAT-solver.
We have implemented our symmetry verification/synthesis algorithms and demonstrated its usefulness in identifying regular symmetry patterns for examples like dining philosopher protocols, self-stabilising protocols, resource-allocator protocol, and3

Gries’s coffee can problem. In the case of the coffee can problem, we managed to obtain a reduction from the infinite system to a finite-state system.
Related Work: Our work is inspired by regular model checking (e.g. [1, 3, 4, 30]),
which focuses on symbolically computing the sets of reachable configurations of parameterised systems as regular languages. Such methods are generic, but are not guaranteed to terminate in general. As in regular model checking, our framework uses transducers to represent parameterised systems. However, instead of computing their sets ofreachable configurations, our work finds symmetry patterns of the parameterised systems, which can be exploited by an explicit-state finite-state model checker to verify thedesired property over finite instances of the system (see [31] for more details). Although
our verification algorithm is guaranteed to terminate in general (in fact, in polynomialtime assuming the parameterised system is given as a DFA), our synthesis algorithm
only terminates when we fix the number of states for the transducers. Finding process
symmetry patterns is often easier since there are available tools for finding symmetries
for finite (albeit small) instances of the systems (e.g. [15, 16, 32]).
Another related line of works is “cutoff techniques” (e.g. see [17, 18] and the survey[30]), which allows one to reduce verification of parameterised systems into verificationof finitely many instances (in some cases, ≤ 10 processes). These works usually assume
verification of LTL\X properties. Although such techniques are extremely powerful, thesystems that can be handled using the techniques are often quite specific (e.g. see [30]).
Organisation: Section 2 contains preliminaries. In Section 3, we present our framework of regular symmetry patterns. In Section 4 (resp. Section 5), we present our symmetry verification algorithm (resp. synthesis) algorithms. Section 6 discusses our implementation and experiment results. Section 7 concludes with future work. Due to spaceconstraints, some details are relegated into the appendix.

2

Preliminaries

General notations. For two given natural numbers i ≤ j, we define [i, j] = {i, i +1, . . . , j}. Define [k] = [1, k]. Given a set S, we use S ∗ to denote the set of all finite
sequences of elements from S. The set S ∗ always includes the empty sequence which
we denote by . Given two sets of words S1 , S2 , we use S1 · S2 to denote the set{v · w | v ∈ S1 , w ∈ S2 } of words formed by concatenating words from S1 withwords from S2 . Given two relations R1 , R2 ⊆ S × S, we define their composition as
R1 ◦ R2 = {(s1 , s3 ) | ∃s2 . (s1 , s2 ) ∈ R1 ∧ (s2 , s3 ) ∈ R2 }. Given a subset X ⊆ S,
we define the image R(X) (resp. preimage R−1 (X)) of X under R as the set {s ∈S | ∃s0 . (s0 , s) ∈ R} (resp. {s0 ∈ S | ∃s. (s0 , s) ∈ R}). Given a finite set S ={s1 , . . . , sn }, the Parikh vector P(v) of a word v ∈ S ∗ is the vector (|v|s1 , . . . , |v|sn )of the number of occurrences of the elements s1 , . . . , sn , respectively, in v.
Transition systems Let ACT be a finite set of action symbols. A transition systemover ACT is a tuple S = hS; {→}a∈ACT i, where S is a set of configurations,andS→a ⊆ S ×S is a binary relation over S. We use → to denote the relation a∈ACT →a .
In the sequel, we will often only consider the case when |ACT| = 1 for simplicity.
The notation →+ (resp. →∗ ) is used to denote the transitive (resp. transitive-reflexive)4

closure of →. We say that a sequence s1 → · · · → sn is a path (or run) in S (or in→). Given two paths π1 : s1 →∗ s2 and π2 : s2 →∗ s3 in →, we may concatenate
them to obtain π1 π2 (by gluing together s2 ). In the sequel, for each S 0 ⊆ S we use
the notation post∗→ (S 0 ) to denote the set of configurations s ∈ S reachable in S fromsome s ∈ S.
Words, automata, and transducers. We assume basic familiarity with word automata.
Fix a finite alphabet Σ. For each finite word w = w1 . . . wn ∈ Σ ∗ , we write w[i, j],where 1 ≤ i ≤ j ≤ n, to denote the segment wi . . . wj . Given a (nondeterministic
finite) automaton A = (Σ, Q, δ, q0 , F ), a run of A on w is a function ρ : {0, . . . , n} →Q with ρ(0) = q0 that obeys the transition relation δ. We may also denote the runρ by the word ρ(0) · · · ρ(n) over the alphabet Q. The run ρ is said to be accepting if
ρ(n) ∈ F , in which case we say that the word w is accepted by A. The language L(A)of A is the set of words in Σ ∗ accepted by A. In the sequel, we will use the standard
abbreviations DFA/NFA (Deterministic/Nondeterministic Finite Automaton).
Transducers are automata that accept binary relations over words [8, 9] (a.k.a.
“letter-to-letter” automata, or synchronised transducers). Given two words w =0over the alphabet Σ, let k = max{n, m} andw1 . . . wn and w0 = w10 . . . wm
Σ# := Σ ∪ {#}, where # is a special padding symbol not in Σ. We define a wordw ⊗ w0 of length k over alphabet Σ# × Σ# as follows:
(
(
w
i
≤
n
wi0 i ≤ miw ⊗ w0 = (a1 , b1 ) . . . (ak , bk ), where ai =and bi =# i > n,# i > m.
In other words, the shorter word is padded with #’s, and the ith letter of w ⊗ w0 isthen the pair of the ith letters of padded w and w0 . A transducer (a.k.a. letter-to-letter
automaton) is simply a finite-state automaton over Σ# × Σ# , and a binary relationR ⊆ Σ ∗ ×Σ ∗ is regular if the set {w⊗w0 : (w, w0 ) ∈ R} is accepted by a letter-to-letter
automaton. The relation R is said to be length-preserving if R only relates words of thesame length [4], i.e., that any automaton recognising R consumes no padded lettersof the form (a, #) or (#, a). In the sequel, for notation simplicity, we will confuse atransducer and the binary relation that it recognises (i.e. R is used to mean both).
Finally, notice that the notion of regular relations can be easily extended to r-ary
relations R for each positive integer r (e.g. see [8, 9]). To this end, the input alphabetrof the transducer will be Σ#. Similarly, for R to be regular, the set {w1 ⊗ · · · ⊗ wr :
(w1 , . . . , wr ) ∈ R} of words over the alphabet Σ r must be regular.
Permutation groups. We assume familiarity with basic group theory (e.g. see [11]). A
permutation on [n] is any bijection π : [n] → [n]. The set of all permutations on [n]forms the (nth) full symmetry group Sn under functional composition. A permutationgroup on [n] is any set of permutations on [n] that is a subgroup of Sn (i.e. closed undercomposition). A generating set for a permutation group G on [n] is a finite set X of
permutations (called generators) such that each permutation in G can be expressed bytaking compositions of elements in X. In this case, we say that G can be generated by
X. A word w = a0 . . . ak−1 ∈ [n]∗ containing distinct elements of [n] (i.e. ai 6= aj
if i 6= j) can be used to denote the permutation that maps ai 7→ ai+1 mod k for eachi ∈ [0, k) and fixes other elements of [n]. In this case, w is called a cycle (more precisely,5

k-cycle or transposition in the case when k = 2), which we will often write in thestandard notation (a0 , . . . , ak−1 ) so as to avoid confusion. Any permutation can be
written as a composition of disjoint cycles [11]. In addition, it is known that Sn can begenerated by the set {(1, 2), (1, 2, . . . , n)}. Each subgroup G of Sn acts on the set Σ n(over any finite alphabet Σ) under the group action of permuting indices, i.e., for eachπ ∈ G and v = (a1 , . . . , an ) ∈ Σ n , we define πv := (aπ−1 (1) , . . . , aπ−1 (n) ). That way,each π induces the bijection fπ : Σ n → Σ n such that fπ (v) = πv.
Given a permutation group G on [n] and a transition system S = hS; →i withstate space S = Σ n , we say that S is G-invariant if the bijection fπ : Σ n → Σ ninduced by each π ∈ Gn is an automorphism on S, i.e., ∀v, w ∈ S: v → w impliesfπ (v) → fπ (w).

3

The formal framework

This section describes our symbolic framework regular symmetry patterns.
3.1

Representing parameterised systems

As is standard in regular model checking [1, 4, 30], we use length-preserving transducers to represent parameterised systems. As we shall see below, we will use non-lengthpreserving transducers to represent symmetry patterns.
Definition 1 (Automatic transition systems5 ). A transition system S=
hS; {→}a∈ACT i is said to be (length-preserving) automatic if S is a regular set
over a finite alphabet Σ and each relation →a is given by a transducer over Σ.
More precisely, the parameterised system defined by S is the family {Sn }n≥0 with
Sn = hSn ; →a,n i, where Sn := S ∩ Σ n is the set of all words in S of length n and→a,n is the transition relation →a restricted to Sn . In the sequel, for simplicity wewill mostly consider examples when |ACT| = 1. When the meaning is understood, weshall confuse the notation →a for the transition relation of S and the transducer thatrecognises it. To illustrate our framework and methods, we shall give three examples ofautomatic transition systems (see [3, 30] for numerous other examples).
Example 1. We describe a prioritised resource-allocator protocol [14, Section 4.4],
which is a simple mutual exclusion protocol in network with a star topology. The protocol has one allocator and m clients. Initially, each process is in an idle state. However,clients might from time to time request for an access to a resource (critical section),
which can only be used by one process at a time. For simplicity, we will assume that
there is only one resource shared by all the clients. The allocator manages the use of theresource. When a request is lodged by a client, the allocator can allow the client to use
the resource. When the client has finished using the resource, it will send a message tothe allocator, which can then allow other clients to use the resource.
To model the protocol as a transducer, we let Σ = {i, r, c}, where i stands for“idle”, r for “request”, and c for “critical”. Allocator can be in either the state i or
5

Length-preserving automatic transition systems are instances of automatic structures [8, 9]

6

the state c, while a client can be in one of the three states in Σ. A valid configuration
is a word aw, where a ∈ {i, c} represents the state of the allocator and w ∈ Σ ∗represents the states of the |w| clients (i.e. each position in w represents a state of aclient). Letting I = {(a, a) : a ∈ Σ} (representing idle local transitions), the transducer
can be described by a union of the following regular expressions:– I + (i, r)I ∗ — a client requesting for a resource.
– (i, c)I ∗ (r, c)I ∗ — a client request granted by the allocator.
– (c, i)I ∗ (c, i)I ∗ — the client has finished using the resource.

tuExample 2. We describe Israeli-Jalfon self-stabilising protocol [23]. The original protocol is probabilistic, but since we are only interested in reachability, we may use nondeterminism to model randomness. The protocol has a ring topology, and each process
either holds a token (denoted by >) or does not hold a token (denoted by ⊥). Dynamics
is given by the following rules:– A process P holding a token can pass the token to either the left or the right neighbouring process P 0 , provided that P 0 does not hold a token.
– If two neighbouring processes P1 and P2 hold tokens, the tokens can be merged
and kept at process P1 .
We now provide a transducer that formalises this parameterised system. Our relation is
on words over the alphabet Σ = {⊥, >}, and thus a transducer is an automaton thatruns over Σ × Σ. In the following, we use I := {(>, >), (⊥, ⊥)}. The automaton is
given by a union of the following regular expressions:– I ∗ (>, ⊥)(⊥, >)I ∗– I ∗ (⊥, >)(>, ⊥)I ∗– I ∗ (>, >)(>, ⊥)I ∗– (⊥, >)I ∗ (>, ⊥)– (>, ⊥)I ∗ (⊥, >)– (>, ⊥)I ∗ (>, >)tuExample 3. Our next example is the classical David Gries’s coffee can problem, whichuses two (nonnegative) integer variables x and y to store the number of black and white
coffee beans, respectively. At any given step, if x + y ≥ 2 (i.e. there are at least two
coffee beans), then two coffee beans are nondeterministically chosen. First, if both areof the same colour, then they are both discarded and a new black bean is put in thecan. Second, if they are of a different colour, the white bean is kept and the black one
is discarded. We are usually interested in the colour of the last bean in the can. We
formally model Gries’s coffee can problem as a transition system with domain N × N
and transitions:(a) if x ≥ 2, then x := x − 1 and y := y.
(b) if y ≥ 2, then x := x + 1 and y := y − 2.
(c) if x ≥ 1 and y ≥ 1, then x := x − 1 and y := y.
To distinguish the colour of the last bean, we shall add self-loops to all configurations
in N × N, except for the configuration (1, 0). We can model the system as a lengthpreserving transducer as follows. The alphabet is Σ := Ωx ∪Ωy , where Ωx := {1x , ⊥x }and Ωy := {1y , ⊥y }. A configuration is a word in the regular language 1∗x ⊥∗x 1∗y ⊥∗y . For
example, the configuration with x = 5 and y = 3, where the maximum size of theinteger buffers x and y is 10, is represented as the word (1x )5 (⊥x )5 (1y )3 (⊥y )7 . The
transducer for the coffee can problem can be easily constructed.
t
u
7

3.2

Representing symmetry patterns

Definition 2. Let S = hS; →i be a transition system with S ⊆ Σ ∗ . A symmetry pattern
for S = hS; →i is a simulation preorder R ⊆ S × S for S, i.e., satisfying:(S1) R respects each →a , i.e., for all v1 , v2 , w1 ∈ S, if v1 →a w1 , and (v1 , v2 ) ∈ R,
then there exists w2 ∈ S such that (w1 , w2 ) ∈ R and v2 →a w2 ;(S2) R is length-decreasing, i.e., for all v1 , v2 ∈ S, if (v1 , v2 ) ∈ R, then |v1 | ≥ |v2 |.
The symmetry pattern is said to be complete if additionally the relation is lengthpreserving and a bijective function.
Complete symmetry patterns will also be denoted by functional notation f . In the caseof complete symmetry pattern f , it can be observed that Condition (S1) also entails thatf (v) →a f (w) implies v →a w. This condition does not hold in general for simulation
preorders. We shall also remark that, owing to the well-known property of simulation
preorders, symmetry patterns preserve non-safety. To make this notion more precise,
we define the image of a transition system S = hS; →i (with S ⊆ Σ ∗ ) under thesymmetry pattern R as the transition system S1 = hS1 ; →1 i such that S1 = R(S) andthat →1 is the restriction of → to S1 .
Proposition 1. Given two sets I, F ⊆ Σ ∗ , if post∗→1 (R(I)) ∩ R(F ) = ∅, thenpost∗→ (I) ∩ F = ∅.
In other words, if S1 is safe, then so is S. In the case when S1 is finite-state, this checkcan be performed using a standard finite-state model checker. We shall define now aclass of symmetry patterns under which the image S1 of the input transition system
can be automatically computed.
Definition 3 (Regular symmetry pattern). A symmetry pattern R ⊆ S × S for an
automatic transition system S = hS; →i is said to be regular if the relation R is regular.
Proposition 2. Given an automatic transition system S = hS; →i (with S ⊆ Σ ∗ )and a regular symmetry pattern R ⊆ S × S, the image of S under R is an automatictransition system and can be constructed in polynomial-time.
In particular, whether the image of S under R is a finite system can be automatically checked since checking whether the language of an NFA is finite can be done inpolynomial-time. The proof of this proposition (in the appendix) is a simple automata
construction that relies on the fact that regular relations are closed under projections.
We shall next illustrate the concept of regular symmetry patterns in action, especiallyfor Israeli-Jalfon self-stabilising protocol and Gries’s coffee can problem.
We start with Gries’s coffee can problem (cf. Example 3). Consider the functionf : (N × N) → (N × N) where f (x, y) is defined to be (i) (0, 1) if y is odd, (ii) (2, 0)
if y is even and (x, y) 6= (1, 0), and (iii) (1, 0) if (x, y) = (1, 0). This is a symmetry
pattern since the last bean for the coffee can problem is white iff y is odd. Also, thata configuration (x, y) with y ≡ 0 (mod 2) and x > 1 is mapped to (2, 0) is because(2, 0) has a self-loop, while (1, 0) is a dead end. It is easy to show that f is a regularsymmetry pattern. To this end, we construct a transducer for each of the cases (i)–(iii).
For example, the transducer handling the case (x, y) when y ≡ 1 (mod 2) works asfollows: simultaneously read the pair (v, w) of words and ensure that w = ⊥x ⊥x 1y andv ∈ 1∗x ⊥∗x 1y (1y 1y )∗ ⊥∗y . As an NFA, the final transducer has ∼ 10 states.
8

Process symmetry patterns. We now apply the idea of regular symmetry patterns tocapture process symmetries in parameterised systems. We shall show how this applies to Israeli-Jalfon self-stabilising protocol. A parameterised permutation is a familyπ̄ = {πn }n≥1 of permutations πn on [n]. We say that π̄ is regular if, for each alphabet Σ, the bijection fπ̄ : Σ ∗ → Σ ∗ defined by fπ̄ (v) := πn v, where v ∈ Σ n , is aregular relation. We say that π̄ is effectively regular if π̄ is regular and if there is analgorithm which, on input Σ, constructs a transducer for the bijection fπ̄ . As we shall
only deal with effectively regular permutations, when understood we will omit mentionof the word “effectively”. As we shall see below, examples of effectively regular parameterised permutations include transpositions (e.g. {(1, 2)(3) · · · (n)}n≥2 ) and rotations{(1, 2, . . . , n)}n≥1 .
We now extend the notion of parameterised permutations to parameterised symmetry groups G := {Gn }n≥1 for parameterised systems, i.e., each Gn is a permutation group on [n]. A finite set F = {π̄ 1 , . . . , π̄ r } of parameterised permutations (withπ̄ j = {πnj }n≥1 ) generates the parameterised symmetry groups G if each group Gn ∈ G
can be generated by the set {πnj : j ∈ [r]}, i.e., the nth instances of parameterised
permutations in F . We say that G is regular if each π̄ j in F is regular.
We will single out three commonly occuring process symmetry groups for concurrent systems with n processes: full symmetry group Sn (i.e. generated by (1, 2)
and (1, 2, . . . , n)), rotation group Rn (i.e. generated by (1, 2, . . . , n)), and the dihedralgroup Dn (i.e. generated by (1, 2, . . . , n) and the “reflection” permutation (1, n)(2, n −1) · · · (bn/2c, dn/2e)). The parameterised versions of them are: (1) S := {Sn }n≥1 , (2)R := {Rn }n≥1 , and (3) D := {Dn }n≥1 .
Theorem 1. Parameterised full symmetry groups S and parameterised rotation symmetry groups R are effectively regular.
As we will see in Proposition 3 below, parameterised dihedral groups are not regular.
We will say how to deal with this in the next section. As we will see in Theorem 4,
Theorem 1 can be used to construct a fully-automatic method for checking whether
each instance Sn of a parameterised system S = {Sn }n≥0 represented by a given
transducer A has a full/rotation process symmetry group.
Proof (sketch of Theorem 1). To show this, it suffices to show that F ={(1, 2)(3) · · · (n)}n≥2 and F 0 = {(1, 2, . . . , n)}n≥2 are effectively regular. [The degenerate case when n = 1 can be handled easily if necessary.] For, if this is thecase, then the parameterised full symmetry S and the parameterised rotation symmetrygroups can be generated by (respectively) {F, F 0 } and F 0 . Given an input Σ, the transducers for both F and F 0 are easy. For example, the transducer for F simply swaps thefirst two letters in the input, i.e., accepts pairs of words of the form (abw, baw) wherea, b ∈ Σ and w ∈ Σ ∗ . These transducers can be constructed in polynomial time (details
in the appendix).
tu
The above proof shows that {(1, 2)(3) · · · (n)}n≥0 and {(1, 2, . . . , n)}n≥0 are regularparameterised permutations. Using the same proof techniques, we can also show that thefollowing simple variants of these parameterised permutations are also regular for eachi ∈ Z>0 : (a) {(i, i + 1)(i + 2) · · · (n)}n≥1 , and (b) {(i, i + 1, . . . , n)}n≥1 . As we sawfrom Introduction, the prioritised resource-allocator protocol has a star topology and so
9both {(2, 3)(4) · · · }n≥1 and {(2, 3, . . . , n)}n≥1 generate complete symmetry patterns
for the protocol (i.e. invariant under permuting the clients). Therefore, our library L of
regular symmetry patterns could store all of these regular parameterised permutations(up to some fixed i).
Parameterised dihedral groups D are generated by rotations π̄ = {(1, 2, . . . , n)}n≥2
and reflections σ̄ = {(1, n)(2, n − 1) · · · (bn/2c, dn/2e)}n≥2 . Reflections σ̄ are, however, not regular for the same reason that the language of palindromes (i.e. words thatare the same read backward as forward). In fact, it is not possible to find a different listof generating parameterised permutations that are regular (proof in the appendix):
Proposition 3. Parameterised dihedral groups D are not regular.

4

Symmetry verification

In this section, we will present our symmetry verification algorithm for regular symmetry patterns. We then show how to extend the algorithm to a more general framework ofsymmetry patterns that subsumes parameterised dihedral groups.
4.1

The algorithm

Theorem 2. Given an automatic transition system S = hS; →i and a regular relation
R ⊆ S × S, we can automatically check if R is a symmetry pattern of S.
Proof. Let D be the set of words over the alphabet Σ 3 of the form v1 ⊗ v2 ⊗ w1 , forsome words v1 , v2 , w2 ∈ Σ ∗ satisfying: (1) v1 → w1 , (2) (v1 , v2 ) ∈ R, and (3) there
does not exist w2 ∈ Σ ∗ such that v2 → w2 and (w1 , w2 ) ∈ R. Observe that R is asymmetry pattern for S iff D is empty. An automaton A = (Σ 3 , Q, ∆, q0 , F ) for D
can be constructed via a classical automata construction.
As before, for simplicity of presentation, we will assume that S = Σ ∗ ; for, otherwise, we can perform a simple product automata construction with the automaton for S. Let A1 = (Σ 2 , Q1 , ∆1 , q01 , F1 ) be an automaton for →, and A2 =2
(Σ#
, Q2 , ∆2 , q02 , F2 ) an automaton for R.
2
We first construct an NFA A3 = (Σ#, Q3 , ∆3 , q03 , F3 ) for the set Y ⊆ S × S consisting of pairs (v2 , w1 ) such that the condition (3) above is false. This can be done bya simple product/projection automata construction that takes into account the fact thatR might not be length-preserving: That is, define Q3 := Q1 × Q2 , q03 := (q01 , q02 ), andF3 := F1 ×F2 . The transition relation ∆ consists of transitions ((q1 , q2 ), (a, b), (q10 , q20 ))such that, for some c ∈ Σ# , it is the case that (q2 , (b, c), q20 ) ∈ ∆2 and one of the following is true: (i) (q1 , (a, c), q10 ) ∈ ∆1 , (ii) q1 = q10 , b 6= #, and a = c = #. Observethat the construction for A3 runs in polynomial-time.
In order to construct A, we will have to perform a complementation operation on A3(to compute the complement of Y ) and apply a similar product automata construction.
The former takes exponential time (since A3 is nondeterministic), while the latter costs
an additional polynomial-time overhead.
tu
10The above algorithm runs in exponential-time even if R and S are presented as
DFA, since an automata projection operation in general yields an NFA. The situation
improves dramatically when R is functional (i.e. for all x ∈ S, there exists a uniquey ∈ S such that R(x, y)).
Theorem 3. There exists a polynomial-time algorithm which, given an automatic transition system S = hS; →i presented as a DFA and a functional regular relation
R ⊆ S × S presented as an NFA, decides whether R is a symmetry pattern for S.
Proof. Let D be the set of words over the alphabet Σ 4 of the form v1 ⊗ v2 ⊗ w1 ⊗ w2 ,for some words v1 , v2 , w1 , w2 ∈ Σ ∗ satisfying: (1) v1 → w1 , (2) (v1 , v2 ) ∈ R, (2’)(w1 , w2 ) ∈ R, and (3) v2 6→ w2 Observe that R is a symmetry pattern for S iff D isempty. The reasoning is similar to the proof of Theorem 2, but the difference now is thatgiven any w1 ∈ Σ ∗ , there is a unique w2 such that (w1 , w2 ) ∈ R since R is functional.
For this reason, we need only to make sure that v2 6→ w2 . An automaton A for D can beconstructed by first complementing the automaton for → and then a standard productautomata construction as before. The latter takes polynomial-time if → is presented as aDFA, while the latter costs an additional polynomial-time computation overhead (evenif R is presented as an NFA).
tu
Proposition 4. The following two problems are solvable in polynomial-space: givena regular relation R ⊆ S × S, check whether (1) R is functional, and (2) R is a bijective function. Furthermore, the problems are polynomial-time reducible to language
inclusion for NFA.
Observe that there are fast heuristics for checking language inclusion for NFA using antichain and simulation techniques (e.g. see [2, 10]). The proof of the above proposition
uses standard automata construction, which is relegated to the appendix.
4.2

Process symmetries for concurrent systems

We say that an automatic transition system S = hS; →i (with S ⊆ Σ ∗ ) is G-invariant
if each instance Sn = hS ∩ Γ n ; →i of S is Gn -invariant. If G is generated by regularparameterised permutations π̄ 1 , . . . , π̄ r , then G-invariance is equivalent to the condition
that, for each j ∈ [r], the bijection fπj : Σ ∗ → Σ ∗ is a regular symmetry pattern for
S. The following theorem is an immediate corollary of Theorem 3.
Theorem 4. Given an automatic transition system S = hS; →i (with S ⊆ Σ ∗ ) and a
regular parameterised symmetry group G presented by regular parameterised permutations π̄ 1 , . . . , π̄ k , we can check that S is G-invariant in polynomial-time assuming that
S is presented as DFA.
In fact, to check whether S is G-invariant, it suffices to sequentially go through eachπ̄ j and ensure that it is a symmetry pattern for S, which by Theorem 3 can be done inpolynomial-time.
11

4.3

Beyond regular symmetry patterns

Proposition 3 tells us that regular symmetry patterns do not suffice to capture parameterised reflection permutation. This leads us to our inability to check whether a parameterised system is invariant under parameterised dihedral symmetry groups, e.g., IsraeliJalfon’s self-stabilising protocol and other randomised protocols including LehmannRabin’s protocol (e.g. [26]). To deal with this problem, we extend the notion of regularlength-preserving symmetry patterns to a subclass of “context-free” symmetry patterns
that preserves some nice algorithmic properties. Proviso: All relations considered inthis subsection are length-preserving.
Recall that a pushdown automaton (PDA) is a tuple P = (Σ, Γ, Q, ∆, q0 , F ), whereΣ is the input alphabet, Γ is the stack alphabet (containing a special bottom-stack symbol, denoted by ⊥, that cannot be popped), Q is the finite set of control states, q0 ∈ Q
is an initial state, F ⊆ Q is a set of final states, and ∆ ⊆ (Q × Γ ) × Σ × (Q × Γ ≤2 )is a set of transitions, where Γ ≤2 denotes the set of all words of length at most 2. A
configuration of P is a pair (q, w) ∈ Q × Γ ∗ with stack-height |w|. For each a ∈ Σ, we
define the binary relation →a on configurations of P as follows: (q1 , w1 ) →a (q2 , w2 )if there exists a transition ((q1 , o), a, (q2 , v)) ∈ ∆ such that w1 = wo and w2 = wv forsome w ∈ Γ ∗ . A computation path π of P on input a1 . . . an is any sequence(q0 , ⊥) →a1 (q1 , w1 ) →a2 · · · →an (qn , wn )of configurations from the initial state q0 . In the following, the stack-height sequence of
π is the sequence |⊥|, |w1 |, . . . , |wn | of stack-heights. We say that a computation path
π is accepting if qn ∈ F .
We now extend Theorem 4 to a class of transducers that allows us to capture thereflection symmetry. This class consists of “height-unambiguous” pushdown transducers, which is a subclass of pushdown transducers that is amenable to synchronisation.
We say that a pushdown automaton is height-unambiguous (h.u.) if it satisfies the restriction that the stack-height sequence in an accepting computation path on an input
word w is uniquely determined by the length |w| of w. That is, given an accepting computation path π on w and an accepting computation path π 0 of w0 with |w| = |w0 |,the stack-height sequences of π and π 0 coincide. Observe that the definition allows thestack-height sequence of a non-accepting path to differ. A language L ⊆ Σ ∗ is said tobe height-unambiguous context-free (huCF) if it is recognised by a height-unambiguous
PDA. A simple example of a huCF language is the language of palindromes (i.e. the input word is the same backward as forward). A simple non-example of a huCF language
is the language of well-formed nested parentheses. This can be proved by a standard
pumping argument.
We extend the definitions of regularity of length-preserving relations, symmetry
patterns, etc. from Section 2 and Section 3 to height-unambiguous pushdown automata
in the obvious way, e.g., a length-preserving relation R ⊆ S × S is huCF if {v ⊗ w :(v, w) ∈ R} is a huCF language. We saw in Proposition 3 that parameterised dihedral
symmetry groups D are not regular. We shall show now that they are huCF.
Theorem 5. Parameterised dihedral symmetry groups D are effectively heightunambiguous context-free.
12

Proof. To show this, it suffices to show that the parameterised reflection permutationσ̄ = {σn }n≥2 , where σn := (1, n)(2, n − 1) · · · (bn/2c, dn/2e), is huCF. To this end,
given an input alphabet Σ, we construct a PDA P = (Σ 2 , Γ, Q, ∆, q0 , F ) that recognises fσ̄ : Σ ∗ → Σ ∗ such that fσ̄ (v) = σn v whenever v ∈ Σ n . The PDA P works justlike the PDA recognising the language of palindromes. We shall first give the intuition.
Given a word w of the form v1 ⊗ v2 ∈ (Σ 2 )∗ , we write w−1 to denote the word v2 ⊗ v1 .
On an input word w1 w2 w3 ∈ (Σ 2 )∗ , where |w1 | = |w3 | and |w2 | ∈ {0, 1}, the PDA
will save w1 in the stack and compares it with w3 ensuring that w3 is the reverse of w1−1 .
It will also make sure that w2 = (a, a) for some a ∈ Σ in the case when |w2 | = 1. The
formal definition of P is given in the appendix.
tu
Theorem 6. There exists a polynomial-time algorithm which, given an automatic transition system S = hS; →i presented as a DFA and a functional h.u. context-free relation
R ⊆ S × S presented as an NFA, decides whether R is a symmetry pattern for S.
To prove this theorem, let us revisit the automata construction from the proof of Theorem 3. The problematic part of the construction is that we need to show that, given an
huCF relation R, the 4-ary relation
R := (R × R) ∩ {(w1 , w2 , w3 , w4 ) ∈ (Σ ∗ )4 : |w1 | = |w2 | = |w3 | = |w4 |}(∗)

is also huCF. The rest of the construction requires only taking product with regular
relations (i.e. → or its complement), which works for unrestricted pushdown automata
since context-free languages are closed under taking product with regular languages via
the usual product automata construction for regular languages.
Lemma 1. Given an huCF relation R, we can construct in polynomial-time an h.u.
PDA recognising the 4-ary relation R.
Proof. Given a h.u. PDA P = (Σ 2 , Γ, Q, ∆, q0 , F ) recognising R, we will construct a
PDA P 0 = (Σ 4 , Γ 0 , Q0 , ∆0 , q00 , F 0 ) recognising R. Intuitively, given an input (v, w) ∈R, the PDA P 0 is required to run two copies of P at the same time, one on the input
v (to check that v ∈ R) and the other on input w (to check that w ∈ R). Since P isheight-unambiguous and |v| = |w|, we can assume that the stack-height sequences of
accepting runs of P on v and w coincide. That is, in an accepting run π1 of P on v andan accepting run of π2 of P on w, when a symbol is pushed onto (resp. popped from) the
stack at a certain position in π1 , then a symbol is also pushed onto (resp. popped from)the stack in the same position in π2 . The converse is also true. These two stacks can,therefore, be simultaneously simulated using only one stack of P 0 with Γ 0 = Γ × Γ .
For this reason, the rest of the details is a standard product automata construction for
finite-state automata. Therefore, the automaton P 0 is of size quadratic in the size of P.
The detailed definition of P 0 is given in the appendix.
tu
We shall finally pinpoint a limitation of huCF symmetry patterns, and discuss how
we can address the problem in practice. It can be proved by a simple reduction from
Post Correspondence Problem that it is undecidable to check whether a given PDA isheight-unambiguous. In practice, however, this is not a major obstacle since it is possible to manually (or semi-automatically) add a selection of huCF symmetry patterns to13

our library L of regular symmetry patterns from Section 3. Observe that this effort is independent of any parameterised system that one needs to check for symmetry. Checking
whether any huCF symmetry pattern in C is a symmetry pattern for a given automatictransition system S can then be done automatically and efficiently (cf. Theorem 6). For
example, Theorem 5 and Theorem 6 imply that we can automatically check whether an
automatic transition system is invariant under the parameterised dihedral groups:
Theorem 7. Given an automatic transition system S = hS; →i (with S ⊆ Σ ∗ ) presented as DFA, checking whether S is D-invariant can be done in polynomial-time.
Among others, this allows us to automatically confirm that Israeli-Jalfon self-stabilising
protocol is D-invariant.

5

Automatic Synthesis of Regular Symmetry Patterns

Some regular symmetry patterns for a given automatic system might not be obvious,
e.g., Gries’s coffee can example. Even in the case of process symmetries, the user mightchoose different representations for the same protocol. For example, the allocator process in Example 1 could be represented by the last (instead of the first) letter in the word,
which would mean that {(1, 2, . . . , n−1)}n≥3 and {(1, 2)(3) · · · (n)}n≥3 are symmetry
patterns for the system (instead of {(2, 3, . . . , n)}n≥2 and {(2, 3)(4) · · · (n)}n≥3 ). Although we can put reasonable variations of common symmetry patterns in our library L,
we would benefit from a systematic way of synthesising regular symmetry patterns fora given automatic transition system S. In this section, we will describe our automatic
technique for achieving this. We focus on the case of symmetry patterns that are total
functions (i.e. homomorphisms), but the approach can be generalised to other patterns.
∗
Every transducer A = (Σ# × Σ# , Q, δ, q0 , F ) over Σ#
represents a regular bi∗nary relation R over Σ . We have shown in Section 4 that we can automatically check
whether R represents a symmetry pattern, perhaps satisfying further constraints likefunctionality or bijectivity as desired by the user. Furthermore, we can also automatically check that it is a symmetry pattern for a given automatic transition system S. Our
overall approach for computing such transducers makes use of two main components,
which are performed iteratively within a refinement loop:
S YNTHESISE A candidate transducer A with n states is computed with the help of a
SAT-solver, enforcing a relaxed set of conditions encoded as a Boolean constraint ψ(Section 5.1).
V ERIFY As described in Section 4, it is checked whether the binary relation R represented by A is a symmetry pattern for S (satisfying further constraints like completeness, as desired by the user). If this check is negative, ψ is strengthened toeliminate counterexamples, and S YNTHESISE is invoked (Section 5.2).
This refinement loop is enclosed by an outer loop that increments the parameter n(initially set to some small number n0 ) when S YNTHESISE determines that no transducers satisfying ψ exist anymore. The next sections describe the S YNTHESISE step,and the generation of counterexamples in case V ERIFY fails, in more detail.
14

5.1

S YNTHESISE: Computation of a Candidate Transducer A

Our general encoding of transducers A = (Σ# × Σ# , Q, δ, q0 , F ) uses a representation
as a deterministic automaton (DFA), which is suitable for our refinement loop sincecounterexamples (in particular, words that should not be accepted) can be eliminatedusing succinct additional constraints. We assume that the states of the transducer A
to be computed are Q = {1, . . . , n}, and that q0 = 1 is the initial state. We use thefollowing variables to encode transducers with n states:– xt (of type Boolean), for each tuple t = (q, a, b, q 0 ) ∈ Q × Σ# × Σ# × Q;
– zq (of type Boolean), for each q ∈ Q.
The assignment xt = 1 is interpreted as the existence of the transition t in A. Likewise,
we use zq = 1 to represent that q is an accepting state in the automaton; since we use
DFA, it is in general necessary to have more than one accepting state.
The set of considered transducers in step S YNTHESISE is restricted by imposing a
number of conditions, selected depending on the kind of symmetry to be synthesised:
for general symmetry homomorphisms, conditions (C1)–(C8) are used, for complete
symmetry patterns (C1)–(C10), and for process symmetries (C1)–(C11).
(C1) The transducer A is deterministic.
(a,b)(C2) For every transition q −→ q 0 in A it is the case that a 6= #.6(C3) Every state of the transducer is reachable from the initial state.
(C4) From every state of the transducer an accepting state can be reached.
(C5) The initial state q0 is accepting.
(C6) The language accepted by the transducer is infinite.
(a,b0 )

(a,b)

(C7) There are no two transitions q −→ q 0 and q −→ q 0 with b 6= b0 .
(a,a)(C8) If an accepting state q has self-transitions q −→ q for every letter a ∈ Σ# , thenq has no outgoing edges.
(a,b)(C9) For every transition q −→ q 0 in A it is the case that b 6= #.
(a0 ,b)(a,b)(C10) There are no two transitions q −→ q 0 and q −→ q 0 with a 6= a0 .
Condition (C2) implies that computed transducers are length-decreasing, while (C3)and (C4) rule out transducers with redundant states. (C5) and (C6) follow from the simplifying assumption that only homomorphic symmetries patterns are computed, sincea transducer representing a total function Σ ∗ → Σ ∗ has to accept the empty word
and words of unbounded length. Note that (C5) and (C6) are necessary, but not sufficient conditions for total functions, so further checks are needed in V ERIFY. (C7)and (C8) are necessary (but again not sufficient) conditions for transducers representing total functions, given the additional properties (C3) and (C4); it can be shown thata transducer violating (C7) or (C8) cannot be a total function. Condition (C9) implies
that padding # does not occur in any accepted word, and is a sufficient condition forlength-preservation; as a result, the symbol # can be eliminated altogether from thetransducer construction.
6Note that all occurrences of # are in the end of words.

15

Finally, for process symmetries the assumption can be made that the transducer
preserves not only word length, but also the number of occurrences of each symbol:(C11) The relation R represented by the transducer only relates words with the same
Parikh vector, i.e., R(v, w) implies P(v) = P(w).
The encoding of the conditions (C1)–(C11) as Boolean constraints is mostly
straightforward. Further Boolean constraints can be useful in special cases, in particularfor Example 3 the restriction can be made that only image-finite transducers are computed. We can also constrain the search in the S YNTHESISE stage to those transducers
that accept manually defined words W = {v1 ⊗ w1 , . . . , vk ⊗ wk }, using a similar encoding as the one for counterexamples in Sect. 5.2. This technique can be used, among
others, to systematically search for symmetry patterns that generalise some known finite
symmetry.
5.2

Counterexample Generation

Once a transducer A representing a candidate relation R ⊆ Σ ∗ × Σ ∗ has been computed, Theorem 2 can be used to implement the V ERIFY step of the algorithm. Whenusing the construction from the proof of Theorem 2, one of three possible kinds ofcounterexample can be detected, corresponding to three different formulae to be added
to the constraint ψ used in the S YNTHESISE stage:∗): ∃w. R(v, w)
1. A word v has to be included in the domain R−1 (Σ#∗2. A word w has to be included in the range R(Σ# ):∃v. R(v, w)
3. One of two contradictory pairs has to be eliminated:¬R(v1 , w1 ) ∨ ¬R(v2 , w2 )Case 1 indicates relations R that are not total; case 2 relations that are not surjective;
and case 3 relations that are not functions, not injective, or not simulations.7 Each of
the formulae can be directly translated to a Boolean constraint over the vocabulary introduced in Sect. 5.1. We illustrate how the first kind of counterexample is handled,∗assuming v = a1 · · · am ∈ Σ#is the word in question; the two other cases are similar. We introduce Boolean variables ei,q for each i ∈ {0, . . . , m} and state q ∈ Q,
which will be used to identify an accepting path in the transducer with input letterscorresponding to the word v. We add constraints that ensure that exactly one ei,q is set
for each state q ∈ Q, and that the path starts at the initial state q0 = 1 and ends in an
accepting state:
n_
o
n
o

ei,q
,
¬ei,q ∨ ¬ei,q0 i∈{0,...,m} , e0,1 ,
em,q → zq q∈Q .
q∈Q

i∈{0,...,m}q6=q 0 ∈Q

For each i ∈ {1, . . . , m} a transition on the path, with input letter ai has to be enabled:no_ei−1,q ∧ ei,q0 →
x(q,ai ,b,q0 ) i∈{1,...,m} .
b∈Σ
7q,q 0 ∈Q

Note that this is for the special case of homomorphisms. Simulation counterexamples are more
complicated than case 3 when considering simulations relations that are not total functions.

16

Table 1. Experimental Results on Verifying and Generating Symmetry Patterns
Symmetry Systems (#letters)
Herman Protocol (2)Israeli-Jalfon Protocol (2)Gries’s Coffee Can (4)Resource Allocator (3)Dining Philosopher (4)6# Transducer states
5
5
8
11
17

Verif. time
0.0s
0.0s
0.1s
0.0s
0.4s

Synth. time
4s
5s
3m19s
4m56s
26m

Implementation and Evaluation

We have implemented a prototype tool based on the aforementioned approach forverifying and synthesising regular symmetry patterns. The programming language
is Java and we use SAT4J [7] as the SAT solver. The source code and the benchmarking examples can be found at https://bitbucket.org/truongkhanh/parasymmetry. The input of our tool includes a model (i.e. a textual representationof transducers), and optionally a set of finite instance symmetries (to speed up synthesisof regular symmetry patterns), which can be generated using existing tools like [32].
We apply our tool to 5 models: the Herman self-stabilising protocol [21], IsraeliJalfon self-stabilising protocol [23], the Gries’ coffee can example [20], Resource Allocator, and Dining Philosopher. For the coffee can example, the tool generates thefunctional symmetry pattern described in Section 3, whereas the tool generates rotational process symmetries for the other models (see the appendix for state diagrams).
Finite instance symmetries were added as constraints in the last three examples.
Table 1 presents the experimental results: the number of states of the synthesised
symmetry transducer, the time needed to verify that the transducer indeed represents
a symmetry pattern (using the method from Section 4), and the total time needed tocompute the transducer (using the procedure from Section 5). The data are obtainedusing a MacBook Pro (Retina, 13-inch, Mid 2014) with 3 GHz Intel Core i7 processor
and 16 GB 1600 MHz DDR3 memory. In almost all cases, it takes less than 5 minutes(primarily SAT-solving) to find the regular symmetry patterns for all these models. As
expected, the verification step is quite fast (< 1 second).

7

Future work

Describe the expressivity and nice algorithmic properties that regular symmetry patterns enjoy, we have pinpointed a limitation of regular symmetry patterns in expressing
certain process symmetry patterns (i.e. reflections) and showed how to circumvent itby extending the framework to include symmetry patterns that can be recognised byheight-unambiguous pushdown automata. One possible future research direction is togeneralise our symmetry synthesis algorithm to this more general class of symmetry
patterns. Among others, this would require coming up with a syntactic restriction ofthis “semantic” class of pushdown automata.
Acknowledgment: Lin is supported by Yale-NUS Grants, Rümmer by the Swedish Research Council. We thank Marty Weissman for a fruitful discussion.
17

References
1. P. A. Abdulla. Regular model checking. STTT, 14(2):109–118, 2012.
2. P. A. Abdulla, Y.-F. Chen, L. Holı́k, R. Mayr, and T. Vojnar. When simulation meets antichains. In TACAS, pages 158–174, 2010.
3. P. A. Abdulla, B. Jonsson, M. Nilsson, J. d’Orso, and M. Saksena. Regular model checking
for LTL(MSO). STTT, 14(2):223–241, 2012.
4. P. A. Abdulla, B. Jonsson, M. Nilsson, and M. Saksena. A survey of regular model checking.
In CONCUR, pages 35–48, 2004.
5. M. Arenas, P. Barceló, and L. Libkin. Regular languages of nested words: Fixed points, automata, and synchronization. In Automata, Languages and Programming, 34th International
Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings, pages 888–900,
2007.
6. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
7. D. L. Berre and A. Parrain. The Sat4j library, release 2.2. JSAT, 7(2-3):59–6, 2010.
8. A. Blumensath. Automatic structures. Master’s thesis, RWTH Aachen, 1999.
9. A. Blumensath and E. Grädel. Finite presentations of infinite structures: Automata and interpretations. Theory Comput. Syst., 37(6):641–674, 2004.
10. F. Bonchi and D. Pous. Checking NFA equivalence with bisimulations up to congruence. In
The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013, pages 457–468, 2013.
11. P. J. Cameron. Permutation Groups. London Mathematical Society Student Texts. Cambridge University Press, 1999.
12. E. M. Clarke, S. Jha, R. Enders, and T. Filkorn. Exploiting symmetry in temporal logic
model checking. Formal Methods in System Design, 9(1/2):77–104, 1996.
13. D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware
design aid. In Proceedings 1991 IEEE International Conference on Computer Design: VLSIin Computer & Processors, ICCD ’92, Cambridge, MA, USA, October 11-14, 1992, pages
522–525, 1992.
14. A. F. Donaldson. Automatic Techniques for Detecting and Exploiting Symmetry in Model
Checking. PhD thesis, University of Glasgow, 2007.
15. A. F. Donaldson and A. Miller. Automatic Symmetry Detection for Model Checking Using
Computational Group Theory. In FM, pages 631–631, 2005.
16. A. F. Donaldson and A. Miller. Automatic Symmetry Detection for Promela. Journal ofAutomated Reasoning, pages 251–293, 2008.
17. E. A. Emerson and V. Kahlon. Reducing model checking of the many to the few. In Automated Deduction - CADE-17, 17th International Conference on Automated Deduction,
Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, pages 236–254, 2000.
18. E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In POPL, pages 85–94, 1995.
19. E. A. Emerson and A. P. Sistla. Symmetry and model checking. Formal Methods in System
Design, 9(1/2):105–131, 1996.
20. D. Gries. The Science of Programming. Springer-Verlag, 1981.
21. T. Herman. Probabilistic self-stabilization. Inf. Process. Lett., 35(2):63–67, 1990.
22. C. N. Ip and D. L. Dill. Better Verification through Symmetry. Formal Methods in System
Design, pages 41–75, 1996.
23. A. Israeli and M. Jalfon. Token management schemes and random walks yield selfstabilizing mutual exclusion. In PODC, pages 119–131, 1990.
24. 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.

18

25. 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.
26. D. Lehmann and M. Rabin. On the advantage of free choice: A symmetric and fully distributed solution to the dining philosophers problem (extended abstract). In Proc. 8th Annual
ACM Symposium on Principles of Programming Languages (POPL’81), pages 133–138,
1981.
27. A. W. Lin. Accelerating tree-automatic relations. In FSTTCS, pages 313–324, 2012.
28. 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 Engineeringand Methodology, pages 133–166, 2000.
29. C. Spermann and M. Leuschel. ProB Gets Nauty: Effective Symmetry Reduction for B and
Z Models. In TASE, pages 15–22, 2008.
30. T. Vojnar. Cut-offs and automata in formal verification of infinite-state systems, 2007. Habilitation Thesis, Faculty of Information Technology, Brno University of Technology.
31. T. Wahl and A. F. Donaldson. Replication and abstraction: Symmetry in automated formal
verification. Symmetry, 2:799–847, 2010.
32. S. J. Zhang, J. Sun, C. Sun, Y. Liu, J. Ma, and J. S. Dong. Constraint-based automatic
symmetry detection. In ASE, pages 15–25, 2013.

A

Transducer Representation for Gries’s Coffee Can Example

We shall first build basic transitions. Firstly, for each i, j ∈ N, we define DECi,≥j (resp.
INCi,≥j ) to be a transducer over {1, ⊥} which checks that the current value (i.e. thenumber of 1s) is at least j and decrements (resp. increments) it by i. For example, thetransducer for DEC1,≥2 can be defined as follows:
⊥/⊥

1/1
1/⊥
1/1

For INCi,≥j , we will make the assumption that if the buffer has reached its maximum
capacity (i.e. there is not enough padding symbol ⊥ in the suffix), then the value stays
as is. For example, the transducer for INC1,≥0 is:
⊥/⊥

1/1
⊥/1

For each z ∈ {x, y}, we let DECi,≥j [z] (resp. INCi,≥j [z]) denote the transducer obtained from DECi,≥j (resp. INCi,≥j ) by replacing every occurrence of 1 and ⊥ by 1z
and ⊥z .
The transducer for the example can then be obtained by connecting these basic
components. For example, the transducer for case (b) is simply the transducer INC1,≥0 ◦DEC2,≥2 , where ◦ is simply the language concatenation operator (i.e. connecting thefinal state of INC1,≥0 with the initial state of DEC2,≥2 ).
19

B

Proof of Proposition 2

The proof of this proposition is a simple automata construction that relies on the factthat regular relations are closed under projections. For simplicity, we shall illustrate
this only in the case when S = Σ ∗ (for a general regular set S, we simply need to
do a simple product construction). Suppose that the transducer for → is A and that the2transducer for R is A0 = (Σ#, Q0 , ∆0 , q00 , F 0 ). Let S1 = hR(S); →1 i be the imageof S under R. Let λ : (Σ ∪ {}) → Σ# be a function such that λ(a) = a, for eacha ∈ Σ, and λ() = #. The set R(S) is regular and can be constructed by a simple
projection operation of ∆0 onto the second component, i.e., define the new transition
relation ∆01 ⊆ Q0 × (Σ ∪ {}) × Q0 such that, for each a ∈ Σ ∪ {}, (p, a, q) ∈ ∆01 iff(p, (b, λ(a)), q) ∈ ∆0 for some b ∈ Σ. The transducer for →1 can then be obtained by
restricting → to R(S) by means of product automata construction. The construction of
automata presentation of S1 in fact runs in polynomial-time.

C

Finishing proof of Theorem 1

We first show that F is effectively regular. Given an alphabet Σ, the function fF maps
the word a1 . . . an ∈ Σ n to a2 a1 a3 a4 . . . an , i.e., the first two letters are swapped.
The transducer for fF is (Σ 2 , Q, ∆, q0 , F ), where Q = {q0 , p} ∪ {qv : v ∈ Σ 2 },F = {p}, and ∆ consists of the following transitions: (1) (q0 , v, qv ) for each v ∈ Σ 2 ,(2) (q(a,b) , (b, a), p) for each (a, b) ∈ Σ 2 , and (3) (p, (a, a), p) for each a ∈ Σ. This
construction is effective (in fact, can be performed in O(|Σ|2 ).
We now show that F 0 is effectively regular. Given an alphabet Σ, the function fF 0 maps the word a1 . . . an to an a1 a2 . . . an−1 . The transducer for fF 0 is(Σ 2 , Q, ∆, q0 , F ), where Q = {q0 } ∪ {qv : v ∈ Σ 2 }, F = {qF }, and ∆ consists of the following transitions: (1) (q0 , v, qv ) ∈ ∆ for each v ∈ Σ 2 , and (2)(q(a,b) , (a0 , a), q(a0 ,b) ) ∈ ∆ for each a0 ∈ Σ, and (3) (q(a,b) , (b, a), qF ) for each(a, b) ∈ Σ 2 .

D

Proof of Proposition 3

The proof is by contradiction. Suppose that D = {Dn }n≥2 are generated by finitely
many regular parameterised permutations π̄ 1 , . . . , π̄ k , say, with π̄ j = {πnj }n≥2 . Let
Σ = {a, b}. Then, for each j ∈ [k], there is a transducer Aj recognising fπj : Σ ∗ →Σ ∗ such that fπj (v) = πnj v whenever v ∈ Σ n . Let m the maximum number of statesamong all the transducers Aj . Let N := (m + 1)3 , which as we shall see will make our
pumping argument works.
Let r = (1, 2, . . . , n) and s = (1, n)(2, n − 1) · · · (bn/2c, dn/2e). Each instance
Dn in D = {Dn }n≥2 is generated by r and s. The group consists of the elements
r0 , r1 , . . . , rn−1 , s, sr1 , . . . , srn−1 .
Any generating set X for Dn must contains at least one of s, sr1 , . . . , srn−1 . Let M =j
4N . Then, for some j ∈ [k], the permutation πM
is srl for some l ∈ [0, M − 1]. There
are two cases:20

– l is even, i.e., l = 2h for some integer h. Then,srl = (h, h + 1)(h − 1(mod M ), h + 2) · · · (h −M2(mod M ), h +

M
+ 1).
2

Visually, this symmetry is simply a reflection symmetry on an M -gon with vertices
labeled 1, . . . , M along the line connecting the middle point between h and h + 1
and the center of the polygon.
– l is odd, i.e., l = 2h + 1 for some integer h. Then,srl = (h, h+2)(h−1(mod M ), h+3) · · · (h−M−12(mod M ), h+

M
+1).
2

Visually, this symmetry is simply a reflection symmetry on an M -gon with vertices
labeled 1, . . . , M along the line connecting h + 1 and the center of the polygon.
In the following, we will consider only the first case since the second case can be dealt
with using the same argument. In this case, observe that srl maps h + N + 1 to h − N(mod M ) and vice versa. We assume that h + N + 1 < h − N (mod M ). The othercase can be dealt with using the same argument. In this case, let t1 = h + N + 1 andt2 = h − N (mod M ). Consider the word w = a1 · · · aM ∈ Σ ∗ such that
 (b, a) if i = t1 ,ai = (a, b) if i = t2 ,
(a, a) otherwise.
Therefore, w = w1 (b, a)w2 (a, b)w3 , for some w1 , w2 , w3 ∈ (a, a)∗ . Notice also thatby definition |w2 | = N and |w1 | + |w3 | = 3N − 2. There are two cases: |w1 | < |w3 |or |w1 | ≥ |w3 |. We shall consider only |w1 | < |w3 |; the other case can be treated in thesame way. Consider an accepting run σ of Aj on w. The run can be divided into fivesegments: σ = σ1 γ1 σ2 γ2 σ3 , where σi is a run segment of Aj on wi (wheni = 1, from the initial state), γ1 is a transition on input (b, a), and γ2 is a transition on
input (a, b).
In the following, we shall show that, for some w20 , w30 ∈ (a, a)∗ with wi0 6= wi , theword w1 (b, a)w20 (a, b)w30 is also accepted by Aj , contradicting that fπ̄j is a bijectivefunction. This is done by a pumping argument. Since |w2 | > m, then a state q of thetransducer is visited twice in σ2 (e.g. after consuming m0 ≤ m number of as). Let us
now analyse the path σ3 , which is of length > N . Let us further subdivide σ3 into atleast m2 contiguous segments of length m + 1. Since one state of the transducer isvisited twice in each segment (after consuming at most m number of as) and that there
are at least m2 disjoint segments, we can infer that at least m0 of these segments havecycles of the same length L. We can construct w20 , w30 and their accepting runs σ20 andσ30 by simply removing m0 cycles of length L from σ3 and repeating the cycle of length
m0 in σ2 precisely L times.

E

Boolean encoding of the conditions in Section 5.1(C3), (C4) We assume additional variables yq , yq0 (for each q ∈ Q) ranging over theinterval [0, n − 1] to encode the distance of state from an accepting or from the initial
21

state. The following formulae (instantiated for each q ∈ Q) define the value of thevariables, and imply that every state is only finitely many transitions away from theinitial and some accepting state:_zq → yq = 0,¬zq →x(q,a,b,q0 ) ∧ yq = yq0 + 1
a,b∈Σ,q 0 ∈Q

q = 1 → yq0 = 0,_q 6= 1 →x(q0 ,a,b,q) ∧ yq0 = yq0 0 + 1

a,b∈Σ,q 0 ∈Q

In the third constraint, recall that q0 = 1 is the initial state. The integer variables canfurther be encoded as a vector of Boolean variables and unary or binary representation.
(C6) Since we search for transducers in which every state is reachable from the initialstate, and in which an accepting state is reachable from every state, (C6) reduces tothe existence of some cycle in the automaton. Because the transducer is furthermore
supposed to represent a total function, the input letters of the transitions on the cycle
can even be fixed to an arbitrary letter a0 ∈ Σ. To encode the condition, we assume
additional Boolean variables c(q,b,q0 ) for each tuple (q, b, q 0 ) ∈ Q × Σ × Q; the assignment c(q,b,q0 ) = 1 will represent the fact that the transition t = (q, a0 , b, q 0 ) occurs onsome infinite path in the automaton (i.e., on a path on which at least one state occurs
infinitely often). This is expressed by the following set of Boolean formulae, stating thatat least one c(q,b,q0 ) is set, that each c(q,b,q0 ) implies that the corresponding transition ispresent in the transducer, and that each c(q,b,q0 ) has a successor transition:no_c(q,b,q0 ) ,c(q,b,q0 ) → x(q,a0 ,b,q0 ),0q,q ∈Q,b∈Σ(q,b,q 0 )nc(q,b,q0 ) →_c(q0 ,b0 ,q00 )q 00 ∈Q,b0 ∈Σoq,q 0 ∈Q,b∈Σ(C11) The main idea when encoding (C11) as a set of Boolean formulae is to consider
the Parikh difference between input and output letters on paths in the transducer A;
importantly, we can observe that this difference, for paths starting in the initial state, isindependent of the path itself and only depends on the last state of the path:Lemma 2. Suppose A is a deterministic transducer satisfying (C4) and (C11), andlet ρ1 and ρ2 be paths in A that start in the initial state q0 and end in the same (notnecessarily accepting) state q. Let v1 ⊗ w1 and v2 ⊗ w2 be the words generated by ρ1and ρ2 , respectively. Then P(w1 ) − P(v1 ) = P(w2 ) − P(v2 ).
Proof. Thanks to (C4), there is a path ρ from q to some accepting state; i.e., ρ1 · ρ
and ρ2 · ρ are two accepting paths of A. Let v1 · v ⊗ w1 · w and v2 · v ⊗ w2 · w be
the corresponding accepted words. Due to (C11), we have P(vi · v) = P(wi · w) fori ∈ {1, 2}, and thus P(vi · v) − P(wi · w) = P(vi ) + P(v) − P(wi ) − P(w) = 0, which
implies the conjecture.
tuThis means that every state q in a transducer A satisfying (C11) has a fixed vector dq
of Parikh differences, which can be determined by looking at an arbitrary path from the22

initial state to q (and then computed as dq = P(w) − P(v), for the word v ⊗ w acceptedby the path). The initial and every accepting state has Parikh difference dq = 0.
This leads to a simple encoding of (C11): we introduce variables daq for every
state q ∈ Q and every character a ∈ Σ, ranging over the set {−n + 1, . . . , n − 1}of integers. Variable daq will represent the Parikh difference for letter a in state q ∈ Q,
which is uniquely determined by a set of constraints about the Parikh difference for
initial and final states, as well as the effect of transitions: a
dq0 = 0 a∈Σ ,zq → daq = 0 a∈Σ, q∈Q ,nox(q,a,b,q0 ) → daq0 = daq + 1 ∧ dbq0 = dbq − 1 q,q0 ∈Q ,a6=b∈Σ

nox(q,a,a,q0 ) → daq0 = daq q,q0 ∈Q ,nox(q,a,b,q0 ) → dcq0 = dcq q,q0 ∈Q .
a,b∈Σc∈Σ\{a,b}a∈Σ

F

Descriptions of protocols

F.1

Herman’s protocol

Here is an example based on a nondeterministic version of Herman’s self-stabilising
protocol (only for odd numbers of processes). Again, it is very similar to before (i.e. ina ring) and passes tokens around. The variation here is that a process can pass a token
to its right neighbour or keep it, but not to the left neighbour. Two tokens are merged assoon as they are held by the same process (i.e. same as before). A formalisation of thisprotocol as a transducer goes as before, i.e., it is a union of: > ∗– I∗ ⊥> ⊥I> ∗– I∗ >> ⊥ I∗ ⊥– >⊥I >> ∗ >– ⊥ I >
Notice that here you only have the rotation symmetry, but not the reflection symmetry.

G

Transducers Found From Our Program

Figures 2-3 show the transducers generated from our program for all the systems usedin our experiments.

23

⊤/⊤

⊤/⊤

3

⊥/⊤
⊤/⊥

⊥/⊥
5

⊥/⊤
1
⊤/⊥

⊤/⊤

⊥/⊥
⊥/⊥
4

⊥/⊤

2

⊤/⊥

Fig. 1. Transducer of Herman Protocol Example

⊤/⊤

⊤/⊤

3

⊥/⊤
⊤/⊥

⊥/⊤

⊥/⊥
2

1
⊤/⊥

⊤/⊤

⊥/⊥
⊥/⊥
4

⊥/⊤

5

⊤/⊥

Fig. 2. Transducer of Israeli-Jalfon Protocol Example

24

3/3

2/2

0/1
1

2/2
1/1

1/0

1/0

3

7

0/1
3/3

2/2
1/1
0/1

0/0
1/0

2/2
1/0
6

3/3

3/2
0/0

5

3/2
2

3/3

0/1
2/2
8

4

0/1

1/1

Fig. 3. Transducer of Griess Coffee Can Example

25

r/c
r/r
r/c

c/c

4

c/r
5
c/c

c/i

i/i

i/r

i/c
i/c

r/i

2

c/i
c/c
i/i

c/i

i/i
1

r/r

8

i/i

i/c
6

c/c
r/i

i/r

r/r

r/i

11
c/r
r/c

10
c/r
r/r
r/r

r/c

7
i/r

c/c

c/r

r/i
i/i
i/r

9
c/i
i/c

3

Fig. 4. Transducer of the Resource Allocator Example

26

0/1
3/1
2/0

2/2
2/1

1/2

15

3/2
2/3

2/1

3/3
0/0
17

3/0

3/1

1/1

0/3

0/2

16

1/3
1/0

8

1/1

0/1
2/0
3/0
1/2

1/1
1/0

0/1
1/0

0/0

3

3/1
1/3

3/3
12

2/3
3/2

3/0
2/1

2/2
6

0/3
9

0/2
2/0

0/0

1
0/2
3/2
1/2
2/2
2/2

1/0

1/1
2/1

4

1/2

3/2

3/1
1/3

0/0
14

0/3
3/0

2/3

10

3/3

2/0

0/1

13

0/2
2/3
0/3
1/3
3/3
3/3

1/2

1/1
3/1
1/3

2

0/1
1/0

0/3

0/0
7
2/1

11

2/0
0/2

2/2
5

3/0
3/2
2/3

Fig. 5. Transducer of Dining Philosopher Example

27