Ackermann Encoding, Bisimulations, and OBDDs

TL;DR

This paper introduces a novel graph representation method using OBDDs based on node partitions and presents a simultaneous computation technique for graph quotients and OBDD representations utilizing Ackermann encoding.

Contribution

It offers a new approach to graph encoding with OBDDs and a method to compute bisimulation quotients and OBDD representations simultaneously.

Findings

Efficient graph representation via OBDDs using node partitions.

A novel method for simultaneous bisimulation quotient and OBDD computation.

Application of Ackermann encoding to improve graph encoding processes.

Abstract

We propose an alternative way to represent graphs via OBDDs based on the observation that a partition of the graph nodes allows sharing among the employed OBDDs. In the second part of the paper we present a method to compute at the same time the quotient w.r.t. the maximum bisimulation and the OBDD representation of a given graph. The proposed computation is based on an OBDD-rewriting of the notion of Ackermann encoding of hereditarily finite sets into natural numbers.