A quasi-local algorithm for checking bisimilarity

  • Wenjie Du*
  • , Yuxin Deng
  • *Corresponding author for this work

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

4 Scopus citations

Abstract

Bisimilarity is one of the most important relations for comparing the behaviour of formal systems in concurrency theory. Decision algorithms for bisimilarity in finite state systems are usually classified into two kinds: global algorithms are generally efficient but require to generate the whole state spaces in advance, local algorithms combine the verification of a system's behaviour with the generation of the system's state space, which is often more effective to determine that one system fails to be related to another. In this paper we propose a quasi-local algorithm with worst case time complexity O(m1m2), where m1 and m2 are the numbers of transitions in two labelled transition systems. With mild modifications, the algorithm can be easily adapted to decide similarity with the same time complexity. For deterministic systems, the algorithm can be simplified and runs in time O(min(m1,m2)).

Original languageEnglish
Title of host publicationProceedings - 2011 IEEE International Conference on Computer Science and Automation Engineering, CSAE 2011
Pages1-5
Number of pages5
DOIs
StatePublished - 2011
Externally publishedYes
Event2011 IEEE International Conference on Computer Science and Automation Engineering, CSAE 2011 - Shanghai, China
Duration: 10 Jun 201112 Jun 2011

Publication series

NameProceedings - 2011 IEEE International Conference on Computer Science and Automation Engineering, CSAE 2011
Volume2

Conference

Conference2011 IEEE International Conference on Computer Science and Automation Engineering, CSAE 2011
Country/TerritoryChina
CityShanghai
Period10/06/1112/06/11

Keywords

  • Concurrency
  • algorithm
  • bisimilarity
  • labelled transition systems

Fingerprint

Dive into the research topics of 'A quasi-local algorithm for checking bisimilarity'. Together they form a unique fingerprint.

Cite this