Jan Martens: Lowerbounds for partition refinement algorithms that decide bisimilarity

Event Details

Most of the algorithms that decide strong bisimilarity for LTSs can be classified as partition refinement algorithms. This includes the most efficient and well-known Paige-Tarjan algorithm. In recent work we establish an Omega((m+n) log n) lowerbound for the time complexity of these partition refinement algorithms, matching the time complexity of the Paige-Tarjan algorithm. However there is a catch: some techniques used for efficiently deciding bisimilarity on restricted LTSs that are deterministic and only have a one-letter alphabet are not captured by the partition refinement assumptions. Although it seems unlikely, these techniques could improve the run-time complexity for deciding bisimilarity on less restricted LTSs. In this talk I’ll discuss the lowerbound for partition refinement algorithms and sketch the contradictory results that come with partition refinement on restricted LTSs.