Branching time and abstraction in bisimulation semantics
Journal of the ACM
Rob J. van Gabbeek
A theory of normed simulations
Branching Bisimilarity of Normed BPA Processes Is in NEXPTIME
Branching Bisimilarity on Normed BPA Is EXPTIME-Complete