Regular Symmetry
Patterns
Anthony W. Lin (Yale-NUS), Khanh Nguyen (Autocad)
Philipp Ruemmer (Uppsala), Jun Sun (SUTD)

Symmetries in systems

Symmetry examples
Reflection

RotationSymmetries are closed
under composition

Symmetries as
automorphisms
Automorphism: structure-preserving bijection on
system configurations by permuting indices(Critical)(Idle)(Idle) ——> (Idle)(Critical)(Idle)
The behaviour of systems is indistinguishable
under an automorphism

Automorphism example
Idle,Idle
Idle,Try

Idle,Critical

Try,Idle

Try,Try

Critical,Try

Critical,IdleTry,Critical

Symmetry: 1 —> 2 —> 1

Symmetries help model
checking
Gist: Prune branches from states in the sameequivalence class as visited states~~

The space reduction can be exponential!
Works on all properties (safety, liveness, …)

Two problems

Say, we mainly attack the first problem
and, to some extent, the secondproblem.

•Symmetry identification: how to identify
symmetries in a given system•

Symmetry exploitation: (1) once symmetries areidentified, check two states are similar (up tosymmetries), (2) compute the “quotient” systems
Both problems are in general computationallydifficult!

Challenge: devise practical solutions to the problems

Concurrency by Replication
Think

Drop

Think

Drop

Left

RightRightLeft

Template 1

Template 2

Parameterised systems
Instance with any number of processes can beobtained by replicating templates (a.k.a. parameterisedsystems)
Definition: an infinite family of finite-state systems……..

Parameterised Systems
Help Verification
Instance-by-instance (using finite-state model checkers):
Size 10.1s
Size 20.1s…
Size 51.5s…
Size 1062s…
Size 15TimeoutParameterised verification (regular model checking, etc.):
Replication tends to produce “similar correctness proofs” for each sizeand can be symbolically represented

Success on safety, but not so on other properties (e.g. liveness)

Can Parameterised Systems
Help for Symmetry Finding?
Instance-by-instance (using finite-state symmetry finders):
Size 10.01s
Size 20.01s…
Size 50.2s…
Size 1580s…
Size 20
Timeout
Parameterised:??

Symmetry “Patterns” forParameterised Systems
Observation:
Instances of parameterised systems (obtained by)
replications tend to exhibit similar-looking symmetries

Pattern Example: Rotation

These 5 symmetries (case n=5) can be generated by

For general n, this rotation symmetry pattern isPattern Example: Reflection

These 2 symmetries (case n=5) can be generated by(in cycle notation)
For general n, the reflection pattern isOther patterns
Full symmetry (all permutationson {1,…,n})Broadcast protocol

1
Resource allocator

Full symmetry on subsystem(all permutations on {1,…,n}that fix the center point 1)

Contributions
Symbolic Framework for Symmetry Patterns inParameterised Systems
Language for Describing Systems: letter-to-lettertransducers (standard in regular model checking)Language for Describing Symmetries: letter-to-lettertransducers (NEW)Expressive for describing practical symmetry patterns
automatic verification and synthesis of symmetry patterns

Symmetry verification
Does the given parameterised system exhibit …?
• Rotations• Reflections• Full symmetries• Above symmetries in a subsystem …

Key Contribution: Each can be expressed and automaticallychecked in our framework!
Good news: there is a “library” of common symmetries

Symmetry synthesisSymmetries in parameterised systems may not be
obvious …
• Data symmetries (e.g. fork position swapped)•Symmetries in a subsystem (but which?)
Contribution: a CEGAR method for synthesising
symmetry patterns in a parameterised system

The symbolic framework:
more technical details

Transducers(Finite) Automata over the alphabet
Symbolic representations of infinite binary relations
Example:Automaton:

a b c
a a c

Automatic transition systems(Regular Model Checking)Set of states:(or a regular subset thereof)

Labelled transitions: defined by a finite family oftransducers (one transducer for each action label)

Example: DiningPhilosopher (pick left first)
0 - Thinking

3 - Drop Left

1 - Pick Left

2 - Pick Right

000
100

Symmetry Pattern

Bijection, Homomorphism, …

Regular Symmetry Pattern

View a function as a binary relation

Examples (next few slides): rotation, swap, …

Rotation is regular
I C I I I I I I I I
I I C I I I I I I IAutomaton remembers when reading ith position:
1. ith position, 1st letter
2. 1st position, 2nd letter

Symmetry PatternVerification

Verifying Regular Symmetry
Patterns
Theorem: Checking whether a given automatic system
exhibits a given regular symmetry pattern is PTIME checkable

Proof Idea: automata construction
Corollary: Checking whether a given automatic system
exhibits a rotation symmetry is PTIME checkable

Full Symmetry Pattern
All permutations on {1,…,n}This corresponds to n! automorphisms
Key: the set of automorphisms forms a group under functional
composition generated by:(1,2) —— a swap
(1,…,n) ——— a rotation
Swap is also regular!

Full Symmetry in aSubsystem
1

All permutations on {1,…,n} that fix 1
This corresponds to (n-1)! automorphisms

These can be generated by (2,3) and (2,3,….,n)Verifying full symmetry
Corollary: Checking whether a given automatic system
exhibits a full symmetry pattern (in a fixed subsystem) isPTIME checkable

What about reflection?
Unfortunately, it is NOT regular!
abcdeedcba
You have to compare the first half of the stringwith the second half of the string

Verifying reflection symmetry
Theorem: Checking whether a given automatic system
exhibits a given reflection symmetry pattern is PTIME
checkable
Proof idea: introduce a subclass of pushdown automata called

Key Property: they can be synchronised (unlike general PDA)
Automatic symmetry verification extends to huCF patterns

Symmetry Pattern
Synthesis

Synthesise-Verify Loop
Verify (automata method)

Synthesise (SAT-solver)
1. Encode Transducers as
Boolean Formulas
2. Maintain a set of boolean
constraints that has to satisfy
3. Initialise to constraints likeis not trivial, is infinite, …

NO

1. Is
2. Is
3. Is
4. Is
5. Isa (partial) function?
total?
injective?
surjective?
a homomorphism?

YES
FINISH“Smart” enumeration of regular symmetry patterns:
guess a transducer with 1 state, 2 states, 3 states,
4 states, …

Counterexamples
Three forms of counterexamples:
1. has to be included in the domain of
2. has to be included in the range of
3. One of two contradictory pairs
andeliminated.

must beEach can be encoded as a boolean constraint!

Synthesis of Finite ExistentialAbstractions (for Proving Safety)
Verify (automata method)
1. Is
2. Is
3. Is
4. Is
5. Is

a (partial) function?
total?
injective?
surjective?
a homomorphism?

Relax (3) and (4) in oursynthesis-verify loop
Add to Synthesis (boolean constraint):- “The range offinite?”
Add to Verify:- “Does the abstraction satisfy safety?”

Can automatically check safety with a simple fixpointcomputation (will terminate since range of is finite)Experiments andExamples

1

3/3

2/2

0/0

1/1

11

3/3

1/3

10

2/2

1/2

9

0/0

1/0

8

1/1

2/1

1/3

3/1

0/3

3/2

1/2

3/0

0/3

2

1/1

2/3

2/3

41/1

0/2

0/3

3/0

3

1/1

2/0

1/3

3/1

15

2/2

2/1

3/2

1/0

0/1

3/0

2/1

1/2

3/1

0/1

2/3

3/2

1/0

0/1

0/2

2/0

1/3

3/1

2/0

0/2

1/3

3/1

0/1

1/0

2/3

3/2

2/1

7

0/0

1/2

0/1

14

3/3

1/0

2/1

12

3/3

1/2

0/2

17

3/3

2/0

0/2

2/0

3/0

0/3

3/2

2/3

3/0

0/3

5

2/2

13

0/0

6

2/2

16

0/0

Synthesised Transducer for
Dining Philosopher

Conclusion and Future
Work

Conclusion
Look for symmetry patterns instead of symmetries (foran individual instance)• Expressive symbolic framework for automaticallyverifying and synthesising symmetry patterns•

Future WorkSynthesis of huCF symmetry patterns• Synthesis of multiple symmetry patterns•