The Bisimulation Problem for equational graphs of finite out-degree

TL;DR

This paper proves the decidability of the bisimulation problem for equational graphs with finite out-degree by reducing it to a known problem and providing a complete formal system for equivalence deduction.

Contribution

It introduces a reduction of the bisimulation problem to deterministic rational boolean series and develops a formal system for equivalence reasoning.

Findings

Decidability of the bisimulation problem for equational graphs of finite out-degree.

A reduction to bisimulation for deterministic rational boolean series.

A complete formal system for deducing equivalence of such series.

Abstract

The "bisimulation problem" for equational graphs of finite out-degree is shown to be decidable. We reduce this problem to the bisimulation problem for deterministic rational (vectors of) boolean series on the alphabet of a dpda M. We then exhibit a complete formal system for deducing equivalent pairs of such vectors.