--- abstract: "Symmetry reduction holds great promise to counter the state explosion problem. However, currently it is ``conducting a life on the fringe'', and is not widely applied, mainly due to the restricted applicability of many of the techniques.\r\nIn this paper we propose a symmetry reduction technique applied to high-level formal specification languages (B and Z).\r\nNot only does symmetry arise naturally in most models, it can also be exploited without restriction by our method.\r\nThis method translates states of a formal model into directed graphs, and then uses graph canonicalisation to detect symmetries.\r\nWe use the tool nauty to efficiently perform graph canonicalisation, which we have interfaced with the model checker ProB.\r\n\r\nIn this paper we present the general technique, show how states can be translated first into vertex-coloured graphs suitable for nauty.\r\nWe present empirical results, showing the effectiveness of our method as well as analysing the cost of graph canonicalisation.\r\n" accompaniment: [] book_title: Proceedings of TASE 2008 commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - ~ - leuschel@cs.uni-duesseldorf.de creators_name: - family: Spermann given: Corinna honourific: '' lineage: '' - family: Leuschel given: Michael honourific: '' lineage: '' data_type: ~ date: 2008 date_type: published datestamp: 2008-11-04 09:08:49 department: ~ dir: disk0/00/00/00/45 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 45 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/45/1/nauty_symIEEE.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-04-19 15:05:51 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://www2.computer.org/portal/web/csdl/doi/10.1109/TASE.2008.33 output_media: ~ pagerange: 15-22 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: ~ producers_id: [] producers_name: [] projects: [] publication: ~ publisher: IEEE Press refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 19 series: ~ skill_areas: [] source: ~ status_changed: 2008-11-04 09:08:49 subjects: - deploy_tooldev - deploy_tooldev_modela succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: 'ProB gets Nauty: Effective Symmetry Reduction for B and Z Models' type: book_section userid: 12 volume: ~