P-hardness of equivalence testing on finite-state processes

Abstract

The paper shows a simple LOGSPACE-reduction from the boolean circuit value problem which demonstrates that, on finite labelled transition systems, deciding an arbitrary relation which subsumes bisimulation equivalence and is subsumed by trace preorder is a polynomial time- hard problem (and thus can not be expected to be efficiently parallelizable). By this, the result of Balcàzar, Gabarrò and Sàntha (1992) for bisimilarity is substantially extended.