×

Some notes on the abstraction operation for multi-terminal binary decision diagrams. (English) Zbl 1291.68258

Summary: The starting point of this work are inaccurate statements found in the literature for Multi-terminal Binary Decision Diagrams (MTBDDs) regarding the well-definedness of the MTBDD abstraction operation. The statements try to relate an operation \(\ast\) on a set of terminal values \(M\) to the property that the abstraction over this operation does depend on the order of the abstracted variables. This paper gives a necessary and sufficient condition for the independence of the abstraction operation of the order of the abstracted variables in the case of an underlying monoid and it treats the more general setting of a magma.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68P05 Data structures
08A70 Applications of universal algebra in computer science

Software:

PRISM
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Bahar R, Frohm E, Ganoa CM, Hachtel G, Macii E, Pardo A, Somenzi F (1997) Algebraic decision diagrams and their applications. Form Methods Syst Des 10(2/3):171-206 · doi:10.1023/A:1008699807402
[2] Bourbaki N (1974) Algebra I, Chaps. 1-3. Springer, Berlin · Zbl 0281.00006
[3] Fujita M, McGeer PC, Yang JC-Y (1997) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form Methods Syst Des 10(2-3):149-169 · doi:10.1023/A:1008647823331
[4] Jezek J, Kepka T (1983) Medial groupoids. Rozpravy Ceskoslovenske Akademie Ved, Rada matematickych a prirodnch ved. Rocnik 93, Sesit 2, Prague
[5] Kuntz M (2006) Symbolic semantics and verification of stochastic process algebras. Dissertation, Institut für Informatik der FAU, Erlangen
[6] PRISM website. http://www.prismmodelchecker.org/
[7] Shcherbacov V (2005) On the structure of finite medial quasigroups. Bul Acad Ştiinţe Repub Mold Mat 1(47):11-18 · Zbl 1078.20063
[8] Siegle M (2002) Behaviour analysis of communication systems: compositional modelling, compact representation and analysis of performability properties. Shaker, Aachen
[9] Strecker R (1974) Über entropische Gruppoide. Math Nachr 64(1):363-371 · Zbl 0294.20067 · doi:10.1002/mana.19740640124
[10] Tamura T (1956) The theory of construction of finite semigroups I. Osaka Math J 8(2) · Zbl 0073.01003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.