Techniques for Distributed Reachability Analysis with Partial Order and Symmetry based Reductions

TL;DR

This paper introduces distributed techniques combining partial order and symmetry reductions to improve reachability analysis efficiency in explicit state space model checkers like SPIN, applicable to both depth-first and breadth-first searches.

Contribution

It presents novel methods for integrating partial order and symmetry reductions in a distributed environment for on-the-fly state space exploration.

Findings

Enhanced efficiency in reachability analysis

Applicable to both depth-first and breadth-first search

Improved state space reduction in distributed model checking

Abstract

In this work we propose techniques for efficient reachability analysis of the state space (e.g., detection of bad states) using a combination of partial order and symmetry based reductions in a distributed setting. The proposed techniques are focused towards explicit state space enumeration based model-checkers like SPIN. We consider variants for both depth-first as well as breadth-first based generation of the reduced state graphs on-the-fly.