Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Lowerbounds for Bisimulation by Partition Refinement

Jan Friso Groote, Jan Martens, Erik. P. de Vink

TL;DR

This work proves fundamental lower bounds for bisimulation decision via partition refinement on labelled transition systems. The authors construct deterministic LTS families (notably the bisplitters B_k and their layered variant C_k) to show sequential partition-refinement algorithms incur Ω((m+n) log n) work, and that even augmenting with an end-structure oracle does not improve this bound. They further establish an Ω(n) lower bound for parallel partition-refinement algorithms, and discuss connections and contrasts with colour refinement literature. The results delineate the limitations of partition-refinement approaches and suggest that faster, generic bisimulation algorithms would need techniques beyond partition refinement, especially for multi-action settings; the singleton-action Roberts' linear algorithm remains a sharp contrast in that restricted regime. Overall, the paper clarifies the computational barriers to optimal partition-refinement-based bisimulation and frames open questions about faster non-partition-based methods, particularly in parallel contexts.

Abstract

We provide time lower bounds for sequential and parallel algorithms deciding bisimulation on labeled transition systems that use partition refinement. For sequential algorithms this is $Ω((m \mkern1mu {+} \mkern1mu n ) \mkern-1mu \log \mkern-1mu n)$ and for parallel algorithms this is $Ω(n)$, where $n$ is the number of states and $m$ is the number of transitions. The lowerbounds are obtained by analysing families of deterministic transition systems, ultimately with two actions in the sequential case, and one action for parallel algorithms. For deterministic transition systems with one action, bisimilarity can be decided sequentially with fundamentally different techniques than partition refinement. In particular, Paige, Tarjan, and Bonic give a linear algorithm for this specific situation. We show, exploiting the concept of an oracle, that this approach is not of help to develop a faster generic algorithm for deciding bisimilarity. For parallel algorithms there is a similar situation where these techniques may be applied, too.

Lowerbounds for Bisimulation by Partition Refinement

TL;DR

This work proves fundamental lower bounds for bisimulation decision via partition refinement on labelled transition systems. The authors construct deterministic LTS families (notably the bisplitters B_k and their layered variant C_k) to show sequential partition-refinement algorithms incur Ω((m+n) log n) work, and that even augmenting with an end-structure oracle does not improve this bound. They further establish an Ω(n) lower bound for parallel partition-refinement algorithms, and discuss connections and contrasts with colour refinement literature. The results delineate the limitations of partition-refinement approaches and suggest that faster, generic bisimulation algorithms would need techniques beyond partition refinement, especially for multi-action settings; the singleton-action Roberts' linear algorithm remains a sharp contrast in that restricted regime. Overall, the paper clarifies the computational barriers to optimal partition-refinement-based bisimulation and frames open questions about faster non-partition-based methods, particularly in parallel contexts.

Abstract

We provide time lower bounds for sequential and parallel algorithms deciding bisimulation on labeled transition systems that use partition refinement. For sequential algorithms this is and for parallel algorithms this is , where is the number of states and is the number of transitions. The lowerbounds are obtained by analysing families of deterministic transition systems, ultimately with two actions in the sequential case, and one action for parallel algorithms. For deterministic transition systems with one action, bisimilarity can be decided sequentially with fundamentally different techniques than partition refinement. In particular, Paige, Tarjan, and Bonic give a linear algorithm for this specific situation. We show, exploiting the concept of an oracle, that this approach is not of help to develop a faster generic algorithm for deciding bisimilarity. For parallel algorithms there is a similar situation where these techniques may be applied, too.
Paper Structure (11 sections, 11 theorems, 16 equations, 7 figures)

This paper contains 11 sections, 11 theorems, 16 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Roberts' algorithm
  4. Example
  5. $\mathscr{B}_k$ is $\Omega(n \log n)$ for partition refinement
  6. $\mathscr{B}_k$ is $\Omega(n\log n)$ for partition refinement with an oracle
  7. Example
  8. $\mathscr{C}_k$ is $\Omega((m+n)\log n)$ for partition refinement
  9. An $\Omega(n)$ lowerbound for parallel partitioning algorithms
  10. Colour refinement
  11. Conclusion

Key Result

Lemma 4.3

Let $k \geqslant 1$ and consider the LTS with initial partition $\mathscr{B}_k = (\mathbb{B}^k, \mathscr{A}_k, {\rightarrow}, \pi_0^{k})$, i.e. the $k$-th bisplitter. Let the sequence $\Pi = ( \pi_0^{k}, \ldots, \pi_n )$ be a valid refinement sequence for $\mathscr{B}_k$. Then it holds that

Figures (7)

  • Figure 1: An example of a deterministic LTS with initial partition (action label suppressed).
  • Figure 2: The bisplitters $\mathscr{B}_1$, $\mathscr{B}_2$, and $\mathscr{B}_3$. Initial partitions are indicated by single-circled and double circled states.
  • Figure 3: The partial layered bisplitter $\mathscr{C}_3$ with tree gadgets, the colours represent the initial partition.
  • Figure 4: The example of the outgoing tree for $\mathscr{C}_6$ from the root $\lbrack \mkern1mu {\textup{011010}}, {\varepsilon} \mkern1mu \rbrack\in S^{\mathscr{C}}_6$ .
  • Figure 5: A transition system with a parallel refinement cost of $1$
  • ...and 2 more figures

Theorems & Definitions (30)

  • Definition 2.1
  • Definition 2.2
  • Definition 4.1
  • Definition 4.2
  • Lemma 4.3
  • proof
  • Theorem 4.4
  • proof
  • Definition 5.1
  • Lemma 5.2
  • ...and 20 more