Naslov
BDD-based Algorithms for Computing State Transitions

Autori
Grudenić, Igor ; Bogunović, Nikola

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Computers in technical systems and intelligent systems / Budin, Leo ; Ribarić, Slobodan - Rijeka : Linia Vera, 2003, 50-54

Skup
XXVI International Convention MIPRO 2003

Mjesto i datum
Opatija, Hrvatska, 19.05.2003. - 23.05.2003

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
formal methods; BDD-based algorithms; formal verification

Sažetak
Symbolic model checking is used extensively to verify finite-state systems by examining state-graph models of the system behavior. The algorithmic nature of model checking procedure makes it fully automatic but at the same time sensitive to the size of the formal model of the system. The binary decision diagram (BDD) is a powerful data structure for the representation of many mathematical objects and specifically suitable for the valid state space computation. The aim of the paper is to identify the computationally expensive BDD operations with respect to the size of the state graph. Based on these operations the paper presents a study of performance issues and possible improvements in BDD construction and manipulation.

Izvorni jezik
Engleski

Znanstvena područja
Računarstvo

POVEZANOST RADA