×

Partially-shared zero-suppressed multi-terminal BDDs: Concept, algorithms and applications. (English) Zbl 1214.68219

Summary: Multi-Terminal Binary Decision Diagrams (MTBDDs) are a well accepted technique for the state graph 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68W05 Nonnumerical algorithms
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

CUDD; CASPA; PRISM
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] Formal Methods in System Design (1997) 10(2–3). Special Issue on Multi-Terminal Binary Decision Diagrams
[2] Akers SB (1978) Binary decision diagrams. IEEE Trans Comput C-27(6):509–516 · Zbl 0377.94038
[3] Balbo G, Conte G, Donatelli S, Franceschinis G, Ajmone Marsan M, Ajmone Marsan M (1995) Modelling with generalized stochastic Petri nets. Wiley, New York · Zbl 0843.68080
[4] Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C-35(8):677–691 · Zbl 0593.94022
[5] Ciardo G, Lüttgen G, Miner AS (2007) Exploiting interleaving semantics in symbolic state-space generation. Form Methods Syst Des 31(1):63–100 · Zbl 1118.68533
[6] de Alfaro L, Kwiatkowska M, Norman G, Parker D, Segala R (2000) Symbolic model checking for probabilistic processes using MTBDDs and the Kronecker representation. In: Graf S, Schwartzbach M (eds) Proc. of the 6th int. conference on tools and algorithms for the construction and analysis of systems (TACAS’00). LNCS, vol 1785. Springer, Berlin, pp 395–410 · Zbl 0960.68109
[7] Hermanns H, Herzog U, Mertsiotakis V (1998) Stochastic process algebras–between LOTOS and Markov chains. Comput Netw ISDN Syst 30(9–10):901–924
[8] Hermanns H, Kwiatkowska M, Norman G, Parker D, Siegle M (2003) On the use of MTBDDs for performability analysis and verification of stochastic systems. J Log Algebr Program 56(1–2):23–67 · Zbl 1054.68018
[9] JINC BDD package. www.jossowski.de
[10] Kam T, Villa T, Brayton R, Sangiovanni-Vincentelli A (1998) Multi-valued decision diagrams: theory and applications. Mult Valued Log 4(1–2):9–62 · Zbl 1025.94515
[11] Kuntz M, Siegle M, Werner E (2004) Symbolic performance and dependability evaluation with the tool CASPA. In: Proc. of EPEW. LNCS, vol 3236. Springer, Berlin, pp 293–307
[12] Lampka K, Siegle M (2006) Activity-local state graph generation for high-level stochastic models. In: Meassuring, modeling, and evaluation of systems 2006, April 2006, pp 245–264
[13] Lampka K, Siegle M (2006) Analysis of Markov reward models using zero-supressed multi-terminal decision diagrams. In: Proceedings of VALUETOOLS 2006 (CD-edition), October 2006
[14] Lee CY (1959) Representation of switching circuits by binary-decision programs. Bell Syst Tech J 38:985–999
[15] Minato S (1993) Zero-suppressed BDDs for set manipulation in combinatorial problems. In: Proc. of the 30th ACM/IEEE design automation conference (DAC), Dallas (Texas), USA, June 1993, pp 272–277
[16] Minato S (2001) Zero-suppressed BDDs and their applications. Int J Softw Tools Technol Transf 3(2):156–170 · Zbl 1002.68589
[17] Miner A, Parker D (2004) Symbolic representations and analysis of large state spaces. In: Baier Ch, Haverkort B, Hermanns H, Katoen J-P, Siegle M (eds) Validation of stochastic systems, Dagstuhl (Germany), 2004. LNCS, vol 2925. Springer, Berlin, pp 296–338 · Zbl 1203.68117
[18] Möbius web page. www.moebius.crhc.uiuc.edu
[19] Ossowski J, Baier C (2008) A uniform framework for weighted decision diagrams and its implementation. Int J Softw Tools Technol Transf 10(5):425–441 · Zbl 05536145
[20] PRISM. www.prismmodelchecker.org
[21] PROMOC modeling tool. www.jossowski.de
[22] Sasao T, Fujita M (eds) (1996) Representations of discrete functions, vol 1. Kluwer Academic, Dordrecht · Zbl 0841.00020
[23] Shannon CS (2000) Eine symbolische Analyse von Relaisschaltkreisen. In: Ein/Aus. Brinkmann und Bose, Berlin. The article originally appeared with the title: A symbolic analysis of switching circuits in Trans. AIEE 57 (1938), 713
[24] Siegle M (2001) Advances in model representation. In: de Alfaro L, Gilmore S (eds) Proc. of the joint int. workshop, PAPM-PROBMIV 2001, Aachen (Germany). LNCS, vol 2165. Springer, Berlin, pp 1–22 · Zbl 1010.68524
[25] SMART. www.cs.ucr.edu/\(\sim\)ciardo/SMART
[26] Somenzi F (1998) CUDD: Colorado University decision diagram package release
[27] Wegener I (2000) Branching programs and binary decision diagrams. SIAM, Philadelphia · Zbl 0956.68068
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.