Lattice-Valued Binary Decision Diagrams

被引：0

作者：

Geeraerts, Gilles ^{[1
]}

Kalyon, Gabriel ^{[1
]}

Le Gall, Tristan ^{[1
]}

Maquet, Nicolas ^{[1
]}

Raskin, Jean-Francois ^{[1
]}

机构：

[1] Univ Libre Bruxelles, Dept Informat Methodes Formelles & Verificat, Brussels, Belgium

来源：

AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS | 2010年 / 6252卷

关键词：

LTL SATISFIABILITY; MODEL-CHECKING; AUTOMATA; ALGORITHMS; ANTICHAINS;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This work introduces a new data structure, called Lattice-Valued Binary Decision Diagrams (or LVBDD for short), for the compact representation and manipulation of functions of the form theta : 2(P) bar right arrow L where P is a finite set of Boolean propositions and L is a finite distributive lattice. Such functions arise naturally in several verification problems. LVBDD are a natural generalisation of multi-terminal ROBDD which exploit the structure of the underlying lattice to achieve more compact representations. We introduce two canonical forms for LVBDD and present algorithms to symbolically compute their conjunction, disjunction and projection. We provide experimental evidence that this new data structure can outperform ROBDD for solving the finite-word LTL satisfiability problem.

引用

页码：158 / 172

页数：15

共 23 条

[1]

ANDERSEN HR, 1997, LICS

[2]

[Anonymous], NUSMV MODEL CHECKER

[3]

[Anonymous], 2001, Model checking

[4]

BIRKHOFF G, 1999, C PUBLICATIONS AM MA

[5]

Bryant RE, 1986, IEEE T COMPUT, VC-35, P8

[6]

BURCH JR, 1990, LICS 1990

[7]

CHECHIK M, 2001, LNCS, V2154, P441

[8]

CIMATTI A, 1999, LECT NOTES COMPUTER, V1633, P495, DOI DOI 10.1007/3-540-48683-6_44

[9]

Cousot P., 1977, POPL 1977

[10]

De Wulf M, 2008, LECT NOTES COMPUT SC, V4963, P63, DOI 10.1007/978-3-540-78800-3_6

← 1 2 3 →