Approximate Partial Order Reduction

We present a new partial order reduction method for reachability analysis of nondeterministic labeled transition systems over metric spaces. Nondeterminism arises from both the choice of the initial state and the choice of actions, and the number of executions to be explored grows exponentially with their length. We introduce a notion of epsilon-independence relation over actions that relates approximately commutative actions; epsilon-equivalent action sequences are obtained by swapping epsilon-independent consecutive action pairs. Our reachability algorithm generalizes individual executions to cover sets of executions that start from different, but delta-close initial states, and follow different, but epsilon-independent, action sequences. The constructed over-approximations can be made arbitrarily precise by reducing the delta, epsilon parameters. Exploiting both the continuity of actions and their approximate independence, the algorithm can yield an exponential reduction in the number of executions explored. We illustrate this with experiments on consensus, platooning, and distributed control examples.