Hardness of preorder checking for basic formalisms |
| |
Authors: | Laura Bozzelli Axel Legay |
| |
Affiliation: | a Technical University of Madrid, 28660 Boadilla del Monte, Madrid, Spainb IRISA, Campus de Beaulieu, 35042 Rennes Cedex, France |
| |
Abstract: | We investigate the complexity of preorder checking when the specification is a flat finite-state system whereas the implementation is either a non-flat finite-state system or a standard timed automaton. In both cases, we show that simulation checking is Exptime-hard, and for the case of a non-flat implementation, the result holds even if there is no synchronization between the parallel components and their alphabets of actions are pairwise disjoint. Moreover, we show that the considered problems become Pspace-complete when the specification is assumed to be deterministic. Additionally, we establish that comparing a synchronous non-flat system with no hiding and a flat system is Pspace-hard for any relation between trace containment and bisimulation equivalence, even if the flat system is assumed to be fixed. |
| |
Keywords: | Behavioral preorders and equivalences Preorder and equivalence checking Non-flat finite-state systems Timed automata Computational complexity |
本文献已被 ScienceDirect 等数据库收录! |
|