Show simple item record

dc.contributor.author
Lampka, Kai
dc.contributor.author
Siegle, Markus
dc.contributor.author
Ossowski, Jörn
dc.contributor.author
Baier, Christel
dc.date.accessioned
2022-08-11T13:28:31Z
dc.date.available
2017-06-08T20:49:45Z
dc.date.available
2022-08-11T13:28:31Z
dc.date.issued
2008
dc.identifier.uri
http://hdl.handle.net/20.500.11850/13019
dc.description.abstract
Multi-Terminal Binary Decision Diagrams (MTBDDs) are a well accepted technique for the state graph (SG) based quantitative analysis of large and complex systems specified by means of high-level model description techniques. However, this type of Decision Diagram (DD) is not always the best choice, since finite functions with small satisfaction sets, and where the fulfilling assignments possess many 0-assigned positions, may yield relatively large MTBDD based representations. Therefore, this article introduces zero-suppressed MTBDDs and proves that they are canonical representations of multi-valued functions on finite (input) sets. For manipulating DDs of this new type, possibly defined over different sets of function variables, the concept of partially-shared zero-suppressed MTBDDs and respective algorithms are developed. The efficiency of this new approach is demonstrated by comparing it to the well-known standard type of MTBDDs, where both types of DDs have been implemented by us within the C++-based DD-package Jinc. The benchmarking takes place in the context of Markovian analysis and probabilistic model checking of systems. In total, the presented work extends existing approaches, since it not only allows one to directly employ (multi-terminal) zero-suppressed DDs in the field of quantitative verification, but also clearly demonstrates their efficiency.
en_US
dc.language.iso
en
en_US
dc.publisher
ETH Zurich, Computer Engineering and Networks Laboratory
en_US
dc.subject
Binary Decision Diagrams and their algorithms
en_US
dc.subject
quantitative verification of systems
en_US
dc.subject
symbolic data structures for performance analysis
en_US
dc.title
Partially-shared Zero-Suppressed Multi-Terminal BDDs: Concept, Algorithms and Applications
en_US
dc.type
Report
ethz.journal.title
TIK Report
ethz.journal.volume
289
en_US
ethz.size
23 p.
en_US
ethz.publication.place
Zurich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02140 - Dep. Inf.technologie und Elektrotechnik / Dep. of Inform.Technol. Electrical Eng.::02640 - Inst. f. Technische Informatik und Komm. / Computer Eng. and Networks Lab.::03234 - Plattner, Bernhard (emeritus) / Plattner, Bernhard (emeritus)
en_US
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02140 - Dep. Inf.technologie und Elektrotechnik / Dep. of Inform.Technol. Electrical Eng.::02640 - Inst. f. Technische Informatik und Komm. / Computer Eng. and Networks Lab.::03234 - Plattner, Bernhard (emeritus) / Plattner, Bernhard (emeritus)
ethz.date.deposited
2017-06-08T20:49:51Z
ethz.source
ECIT
ethz.identifier.importid
imp59364c21f3cc572493
ethz.ecitpid
pub:24394
ethz.eth
yes
en_US
ethz.availability
Metadata only
en_US
ethz.rosetta.installDate
2017-07-12T14:11:04Z
ethz.rosetta.lastUpdated
2023-02-07T05:14:07Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Partially-shared%20Zero-Suppressed%20Multi-Terminal%20BDDs:%20Concept,%20Algorithms%20and%20Applications&rft.jtitle=TIK%20Report&rft.date=2008&rft.volume=289&rft.au=Lampka,%20Kai&Siegle,%20Markus&Ossowski,%20J%C3%B6rn&Baier,%20Christel&rft.genre=report&
 Search print copy at ETH Library

Files in this item

FilesSizeFormatOpen in viewer

There are no files associated with this item.

Publication type

Show simple item record