Temporal Logic Model Checking is a verification method in which we describe a system, the model, and then we verify whether important properties, expressed in a temporal logic formula, hold in the system. Many Model Checking tools employ BDDs or some other data structure to represent sets of states. It has been empirically observed that the BDDs used in these algorithms may grow exponentially as the model and formula increase in size. We formally prove that no kind of data structure of polynomial size can represent the set of valid initial states for all models and all formulae. This result holds for all data structures where a state can be checked in polynomial time. Therefore, it holds not only for all types of BDDs regardless of variable ordering, but also for more powerful data structures, such as RBCs, MTBDDs, ADDs and SDDs. Thus, the size explosion of BDDs is not a limit of these specific data representation structures, but is unavoidable: every formalism used in the same way would lead to an exponential size blow up.

The size of BDDs and other data structures in temporal logics model checking / Ferrara, Andrea; Liberatore, Paolo; Schaerf, Marco. - STAMPA. - 65:10(2016), pp. 3148-3156. [10.1109/TC.2015.2512872]

The size of BDDs and other data structures in temporal logics model checking

FERRARA, Andrea;LIBERATORE, Paolo
;
SCHAERF, Marco
2016

Abstract

Temporal Logic Model Checking is a verification method in which we describe a system, the model, and then we verify whether important properties, expressed in a temporal logic formula, hold in the system. Many Model Checking tools employ BDDs or some other data structure to represent sets of states. It has been empirically observed that the BDDs used in these algorithms may grow exponentially as the model and formula increase in size. We formally prove that no kind of data structure of polynomial size can represent the set of valid initial states for all models and all formulae. This result holds for all data structures where a state can be checked in polynomial time. Therefore, it holds not only for all types of BDDs regardless of variable ordering, but also for more powerful data structures, such as RBCs, MTBDDs, ADDs and SDDs. Thus, the size explosion of BDDs is not a limit of these specific data representation structures, but is unavoidable: every formalism used in the same way would lead to an exponential size blow up.
2016
BDDs; compilability; complexity; Model checking; succinctness; Theoretical Computer Science; Software; Hardware and Architecture; Computational Theory and Mathematics
01 Pubblicazione su rivista::01a Articolo in rivista
The size of BDDs and other data structures in temporal logics model checking / Ferrara, Andrea; Liberatore, Paolo; Schaerf, Marco. - STAMPA. - 65:10(2016), pp. 3148-3156. [10.1109/TC.2015.2512872]
File allegati a questo prodotto
File Dimensione Formato  
Ferrara_Postprint_The -size-of-BDDs_2016.pdf

accesso aperto

Note: https://ieeexplore.ieee.org/document/7366751
Tipologia: Documento in Post-print (versione successiva alla peer review e accettata per la pubblicazione)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 117.08 kB
Formato Adobe PDF
117.08 kB Adobe PDF
Ferrara_The -size-of-BDDs_2016.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 182.51 kB
Formato Adobe PDF
182.51 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/912746
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact