Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Model Checking and Preprocessing
verfasst von : Andrea Ferrara, Paolo Liberatore, Marco Schaerf
Erschienen in: AI*IA 2007: Artificial Intelligence and Human-Oriented Computing
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
Temporal Logic Model Checking is a verification method having many industrial applications. This method describes a system as a formal structure called model; some properties, expressed in a temporal logic formula, can be then checked over this model. In order to improve performance, some tools allow to preprocessing the model so that a set of properties can be verified reusing the same preprocessed model. In this article, we prove that this preprocessing cannot possibly reduce complexity, if its result is bound to be of size polynomial in the size of the input. This result also holds if the formula is the part of the data that is preprocessed, which has similar practical implications.