Skip to main navigation Skip to search Skip to main content

A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

424 Downloads (Pure)

Abstract

The most efficient way to calculate strong bisimilarity is by finding the relational coarsest partition of a transition system. We provide the first linear-time algorithm to calculate strong bisimulation using parallel random access machines (PRAMs). More precisely, with n states, m transitions and | Act| ≤ m action labels, we provide an algorithm for max (n, m) processors that calculates strong bisimulation in time O(n+ | Act| ) and space O(n+ m). The best-known PRAM algorithm has time complexity O(nlog n) on a smaller number of processors making it less suitable for massive parallel devices such as GPUs. An implementation on a GPU shows that the linear time-bound is achievable on contemporary hardware.

Original languageEnglish
Title of host publicationFormal Aspects of Component Software
Subtitle of host publication17th International Conference, FACS 2021, Virtual Event, October 28–29, 2021, Proceedings
EditorsGwen Salaün, Anton Wijs
Place of PublicationCham
PublisherSpringer
Pages115-133
Number of pages19
ISBN (Electronic)978-3-030-90636-8
ISBN (Print)978-3-030-90635-1
DOIs
Publication statusPublished - 28 Oct 2021
Event17th International Conference on Formal Aspects of Component Software, FACS 2021 - Virtual, Online
Duration: 28 Oct 202129 Oct 2021

Publication series

NameLecture Notes in Computer Science (LNCS)
Volume13077
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameProgramming and Software Engineering (LNPSE)
Volume13077
ISSN (Print)2945-915X
ISSN (Electronic)2945-9168

Conference

Conference17th International Conference on Formal Aspects of Component Software, FACS 2021
CityVirtual, Online
Period28/10/2129/10/21

Keywords

  • Bisimulation
  • Relational Coarsest Partition

Fingerprint

Dive into the research topics of 'A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions'. Together they form a unique fingerprint.

Cite this