$\xor$-OBDD in Symbolic Model Checking

ŘEHÁK, Vojtěch. $\xor$-OBDD in Symbolic Model Checking. In SOFSEM 2002: Student Research Forum. Milovy (Czech Republic): Slovak University of Technology, 2002, s. 41-46.

Základní údaje

Originální název

$\xor$-OBDD in Symbolic Model Checking

Autoři

ŘEHÁK, Vojtěch (203 Česká republika, garant)

Vydání

Milovy (Czech Republic), SOFSEM 2002: Student Research Forum, s. 41-46, 2002

Nakladatel

Slovak University of Technology

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

20206 Computer hardware and architecture

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/02:00006715

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

Data structures; $\xor$-OBDD; symbolic model checking;

Štítky

$\xor$-OBDD, data structures, symbolic model checking

Příznaky

Recenzováno

---

Anotace

V originále

We present a feasibility study of using $\oplus$-OBDD data structure in symbolic model checking (SMC). $\xor$-OBDD has been proposed as a more succinct modification of well known OBDD data structure which is of common use in nowadays SMC. We introduce three modifications of $\xor$-OBDD, analyze their respective efficiency, and present some experimental results based on implementations of $\xor$-OBDD within a symbolic model checker NuSMV.

---

Návaznosti

GA201/00/1023, projekt VaV	Název: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů Investor: Grantová agentura ČR, Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
MSM 143300001, záměr	Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů