Sciweavers

Share
LPAR
2010
Springer

Hardness of Preorder Checking for Basic Formalisms

8 years 3 months ago
Hardness of Preorder Checking for Basic Formalisms
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.
Laura Bozzelli, Axel Legay, Sophie Pinchinat
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where LPAR
Authors Laura Bozzelli, Axel Legay, Sophie Pinchinat
Comments (0)
books