Behavioural equivalences on finite-state systems are PTIME-hard. (English) Zbl 1109.68052

Sawa, Zdeněk; Jančar, Petr

Comput. Inform. 24, No. 5, 513-528 (2005).

Summary: The paper shows a LOGSPACE-reduction from the Boolean circuit value problem which demonstrates that any relation subsuming bisimilarity and being subsumed by trace preorder (i.e., language inclusion) is PTIME-hard, even for finite acyclic labelled transition systems. This reproves and substantially extends the result of J. Balcázar, J. Gabarró and M. Sántha [Formal Asp. Comput. 4, 638–648 (1992; Zbl 0758.68033)] for bisimilarity.

MSC:

68Q25	Analysis of algorithms and problem complexity
68Q10	Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
93A30	Mathematical modelling of systems (MSC2010)

Keywords:

verification; finite transition systems; bisimulation equivalence; trace equivalence; computational complexity; PTIME-hardness