Symmetry Reductions for a Class of Discrete-Event Systems

Issues related to the control and verification of isomorphic modular discrete-event systems are investigated.  A finite state automaton system model is considered for the system modules where a set of atomic propositions are defined on the states.  A type of symmetry is defined for these modular systems and a restriction of the  &mu-calculus designed for these systems is introduced.  A procedure is shown to reduce the cost in computation time and memory for testing if symmetric modular systems satisfy propositions in this &mu-calculus.  An example of a symmetric modular UAV platoon leader system
is then shown and discussed.