The equivalence checking of systems that are given as a composition of interacting finite-state systems is considered. It is shown that the problem is EXPTIME-hard for any notion of equivalence that lies between bisimulation equivalence and trace equivalence, as conjectured by Rabinovich (1997). The result is proved for parallel composition of finite-state systems where hiding of actions is allowed, and for 1-safe Petri nets. The technique of the proof allows to extend this result easily to other types of 'non-flat' systems. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Sawa, Z. (2003). Equivalence checking of non-flat systems is EXPTIME-hard. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2761, 237–250. https://doi.org/10.1007/978-3-540-45187-7_16
Mendeley helps you to discover research relevant for your work.