Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
Hardness of Preorder Checking for Basic Formalisms
verfasst von : Laura Bozzelli, Axel Legay, Sophie Pinchinat
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.