The Taub Faculty of Computer Science Events and Talks

In model checking, we work toward deciding whether a system satisfies a given specification. Often, a system exhibits some type of symmetry in its structure or in its behaviour. Such symmetries can be exploited by a designer to alleviate some of the complexity of model checking, as well as to gain insight into the behaviour of the system. Thus, we want to decide whether a given system exhibits symmetry. Symmetry is not a well-defined concept and might come in various forms, each capturing a different characteristic behaviour. In this talk, I introduce several notions of semantic symmetry in transducers, and demonstrate the definitions and the behaviours they capture, as well as pose the algorithmic questions pertaining to them and their solutions. In particular, I present the notion of simulation by rounds, whose usefulness is in that it can be applied to process symmetry. In this setting, words are partitioned into rounds, and a transducer is round simulated by another if for every input word, we can shuffle the letters within each round such that the output of the simulating transducer on the shuffled word is itself a shuffle of the output of the simulated transducer. We use tools and techniques from logic, algebra and automata theory.