In our previous research developing the TopSPIN symmetry reduction
package for SPIN, we have cultivated a unique framework of techniques
and tools for symmetry reduced explicit state model checking. We
propose to extend TopSPIN and construct a new, purpose-built explicit
state model checker as a test-bed for explicit state symmetry
reduction techniques for probabilistic systems.
We are part of the Formal Analysis, Theory and Algorithms Group (FATA).
ARTE is funded by the Engineering and Physical
Sciences Research Council, number EP/E032354/1.