"Computational complexity of comparing behaviours of systems composed from interacting finite-state components is considered. The main result shows that the respective problems are EXPTIME-hard for all relations between bisimulation equivalence and trace preorder, as conjectured by Rabinovich (Inf Comput 139(2):111?129, 1997). The result is proved for a specific model of parallel compositions where the components synchronize on shared actions but it can be easily extended to other similar models, e.g., to labelled 1-safe Petri nets. Further hardness results are shown for special cases of acyclic systems."@en . . "Hardness of equivalence checking for composed finite-state systems"@en . "2"^^ . "P(1M0567)" . . "DE - Spolkov\u00E1 republika N\u011Bmecko" . "2"^^ . "Hardness of equivalence checking for composed finite-state systems" . . . . . . "[AB1BDEE2B2FB]" . . "27240" . . "Jan\u010Dar, Petr" . . "Acta Informatica" . "RIV/61989100:27240/09:00021390" . "Hardness of equivalence checking for composed finite-state systems" . . "Hardness of equivalence checking for composed finite-state systems"@en . "316849" . "0001-5903" . . . "Sawa, Zden\u011Bk" . . "3" . "23"^^ . . . "000265216000001" . "Computational complexity of comparing behaviours of systems composed from interacting finite-state components is considered. The main result shows that the respective problems are EXPTIME-hard for all relations between bisimulation equivalence and trace preorder, as conjectured by Rabinovich (Inf Comput 139(2):111?129, 1997). The result is proved for a specific model of parallel compositions where the components synchronize on shared actions but it can be easily extended to other similar models, e.g., to labelled 1-safe Petri nets. Further hardness results are shown for special cases of acyclic systems." . "RIV/61989100:27240/09:00021390!RIV10-MSM-27240___" . . "46" . "verification; eqivalence checking; computational complexity; parallel composition; finite-state systems"@en . .