Hardness of equivalence checking for composed finite-state systems |
| |
Authors: | Zdeněk Sawa Petr Jan?ar |
| |
Affiliation: | 1.FEI,Technical University of Ostrava,Ostrava-Poruba,Czech Republic |
| |
Abstract: | 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, to labelled 1-safe Petri nets. Further hardness results are shown
for special cases of acyclic systems. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|