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

#### 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.
##### Scheda breve Scheda completa
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
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)
Dimensione 117.08 kB
Ferrara_The -size-of-BDDs_2016.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)