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. © Springer-Verlag Berlin Heidelberg 2007.
Model Checking and Preprocessing / Andrea, Ferrara; Liberatore, Paolo; Schaerf, Marco. - 4733:(2007), pp. 48-59. (Intervento presentato al convegno 10th Congress of the Italian Association for Artificial Intelligence tenutosi a Rome; Italy nel September 10-13, 2007) [10.1007/978-3-540-74782-6_6].
Model Checking and Preprocessing
LIBERATORE, Paolo;SCHAERF, Marco
2007
Abstract
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. © Springer-Verlag Berlin Heidelberg 2007.File | Dimensione | Formato | |
---|---|---|---|
VE_2007_11573-188010.pdf
solo gestori archivio
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
5.03 MB
Formato
Adobe PDF
|
5.03 MB | Adobe PDF | Contatta l'autore |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.