Manual and automatic exploitation of symmetries in SPN models

Abstract

The exploitation of symmetries for the reachability analysis of SPNs was recognized as a necessary step to handle reasonably complex models right from the beginning. Initially this step was performed manually by the modeler, and required a great deal of experience and ingenuity. Subsequently, the research has focused on techniques to automate such symmetries exploitation to simplify the modeler's task and still allow the solution of reasonably complex models. We recall some of the steps of this evolution, that has now simplified the definition of efficiently solvable models. We also attempt to devise some future perspectives to work on.