Model checking is an automated approach to verification of systems, e.g., software systems, hardware systems, communication protocols, etc. This is done via representing the system as a transition system, that is, representing different situations that the system can be in as a number of states and their relations, while representing properties that have to be verified as temporal logic formulas. Unfortunately, when the system at hand is comprised of a number of sub-systems (processes or components) that run in parallel, the number of states of the system grows exponentially in the number of sub-systems that run in parallel. For tackling the phenomenon, called state space explosion problem, there have been several approaches developed. A well known and widely practiced approach is symmetry reduction that makes use of symmetry of sub-systems running in parallel to reduce the number of states of the composite system.

Constraint automata are a variation of transition systems where, there are a number of data-flow locations allowing transmutation of data. The name constraint automata refers to the fact that each transition puts a number of restrictions (constraints) on the data flow throughout constraint automata as that transition is being executed. Reo is an exogenous channel based communication language providing orchestration among components of a system. The semantics underlying Reo circuits can be expressed as constraint automata. In this thesis, we adapt the technique of symmetry reduction to the case of systems expressed in constraint automata and discuss how Reo circuits can be helpful in isolating symmetrical parts of the system, facilitating more efficient dealing with symmetry reduction.