UNIGE document Chapitre d'actes
previous document  unige:12331  next document
add to browser collection

Sigma Decision Diagrams

Published in TERMGRAPH 2009 : Preliminary proceedings of the 5th International Workshop on Computing with Terms and Graphs. 2009
Abstract Encoding and rewriting of large set of terms is very useful in a number of domains, such as model checking and theorem proving. The challenge of encoding and normalizing several billions of terms requires efficient ways of representing and manipulating them. Term Graph Rewriting is a well-known technique to share common sub-terms and thus to save both memory and processing time. However, this does not always fit well to the operational framework since it destroys the original structure and replaces it by a new one. This paper introduces a new kind of Decision Diagrams (DD), especially designed to handle set of terms in an efficient way. Based on the Set Decision Diagrams(SDD), an evolution of the well-known Binary Decision Diagrams(BDD), we propose the Sigma Decision Diagrams (ΣDD), a new approach to perform Term Rewriting on a set of terms in order to compute the image of that set efficiently.
Keywords Term RewritingSet Decision DiagramsΣ Decision DiagramsSet of terms
Stable URL https://archive-ouverte.unige.ch/unige:12331
Full text
Proceedings chapter (349 Kb) - public document Free access

241 hits



Deposited on : 2010-11-05

Export document
Format :
Citation style :