Lowerbounds for Bisimulation by Partition Refinement

DOI10.46298/LMCS-19(2:10)2023MaRDI QIDQ6135758zbMATH OpenOpenAlexFDO

Authors Jan Friso Groote, Jan Martens, Erik de Vink

Publication date 26 August 2023

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2203.07158

zbMATH Keywords

bisimilaritylabelled transition systemlowerboundpartition refinement

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

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 $Omega((mmkern1mu+mkern1mun)mkern-1mulogmkern-1mun)$ and for parallel algorithms this is $Omega(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.

Recommendations

• An implementation of an efficient algorithm for bisimulation equivalence
• Deciding orthogonal bisimulation
• An efficient algorithm for computing bisimulation equivalence
• scientific article; zbMATH DE number 1796125
• Bisimilarity Minimization in O(m logn) Time

Cites work

• A calculus of communicating systems
• A linear time solution to the single function coarsest partition problem
• An O(m n) algorithm for branching bisimilarity on labelled transition systems
• An efficient algorithm for computing bisimulation equivalence
• An efficient algorithm to determine probabilistic bisimulation
• An efficient parallel algorithm for the single function coarsest partition problem
• Bisimulation by Partitioning Is Ω((m+n)log n).
• CCS expressions, finite state processes, and three problems of equivalence
• Efficient and modular coalgebraic partition refinement
• Exact performance equivalence: An equivalence relation for stochastic automata
• Fast Pattern Matching in Strings
• Hopcroft’s Algorithm and Cyclic Automata
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 3460178 (Why is no real title available?)
• Implementation and Application of Automata
• Partitioning a graph in \(O(|A|\log_ 2|V|)\)
• Simulation of Parallel Random Access Machines by Circuits
• Three Partition Refinement Algorithms
• Tight lower and upper bounds for the complexity of canonical colour refinement

Cited in

(4)

• From bisimulation to simulation: Coarsest partition problems
• On domain-partitioning induction criteria: worst-case bounds for the worst-case based
• Incremental NFA minimization
• An evaluation of massively parallel algorithms for DFA minimization

This page was built for publication: Lowerbounds for Bisimulation by Partition Refinement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135758)