Bisimilarity Problems Requiring Exponential Time

Abstract We study the complexity of deciding bisimilarity between non-deterministic processes. In particular, we consider a calculus with recursive definitions of processes, value passing (i. e. input/output of data) and an equality test over data. We show that the bisimilarity problem is EXP-complete over this calculus and thus that exponential time is provably necessary in order to solve it. We then prove that, if we add a parallel composition operator to the calculus, and we impose that parallel composition is never used inside recursive definitions, then the bisimilarity problem is still EXP-complete, thus no harder than in the fragment without parallel composition.

Authors

• Michele Boreale
• Luca Trevisan 0001

Keywords

No keywords are indexed for this paper.