Behavioural Equivalences on Finite-State Systems are PTIME-hard
keywords: Verification, finite transition systems, bisimulation equivalence, trace equivalence, computational complexity, PTIME-hardness
The paper shows a ŁOGSPACE-reduction from the Boolean circuit value problem which demonstrates that any relation subsuming bisimilarity and being subsumed by trace preorder (ie, language inclusion) is PTIME-hard, even for finite acyclic labelled transition systems. This reproves and substantially extends the result of Balcazar, Gabarro and Santha (1992) for bisimilarity.
reference: Vol. 24, 2005, No. 5, pp. 513–528
