×

zbMATH — the first resource for mathematics

On the use of MTBDDs for performability analysis and verification of stochastic systems. (English) Zbl 1054.68018
Summary: This paper describes how to employ Multi-Terminal Binary Decision Diagrams (MTBDDs) for the construction and analysis of a general class of models that exhibit stochastic, probabilistic and non-deterministic behaviour. It is shown how the notorious problem of state space explosion can be circumvented by compositionally constructing symbolic (i.e. MTBDD-based) representations of complex systems from small-scale components. We emphasise, however, that compactness of the representation can only be achieved if heuristics are applied with insight into the structure of the system under investigation. We report on our experiences concerning compact representation, performance analysis and verification of performability properties.

MSC:
68M20 Performance evaluation, queueing, and scheduling in the context of computer systems
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
CUDD; LOTOS; PRISM
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Puterman, M., Markov decision processes, (1994), Wiley
[2] Courcoubetis, C.; Yannakakis, M., The complexity of probabilistic verification, Journal of the ACM, 42, 4, 857-907, (1995) · Zbl 0885.68109
[3] R. Segala, Modelling and verification of randomized distributed real time systems, Ph.D. thesis, Massachusetts Institute of Technology, 1995
[4] Milner, R., Communication and concurrency, (1989), Prentice Hall · Zbl 0683.68008
[5] Bolognesi, T.; Brinksma, E., Introduction to the ISO specification language LOTOS, (), 23-73
[6] N. Götz, U. Herzog, M. Rettelbach, Multiprocessor and distributed system design: The integration of functional specification and performance analysis using stochastic process algebras, in: Proceedings of the 16th International Symposium on Computer Performance Modelling, Measurement and Evaluation, PERFORMANCE 1993, Tutorial, vol. 729 of Lecture Notes in Computer Science, Springer, 1993, pp. 121-146
[7] Hillston, J., A compositional approach to performance modelling, (1996), Cambridge University Press
[8] Hermanns, H.; Herzog, U.; Katoen, J.-P., Process algebra for performance evaluation, Theoretical computer science, 274, 1-2, 43-87, (2002) · Zbl 0992.68149
[9] P. Courtois, Decomposability, queueing and computer system applications, ACM monograph series, 1977 · Zbl 0368.68004
[10] B. Plateau, On the synchronization structure of parallelism and synchronization models for distributed algorithms, in: Proceedings of the ACM Sigmetrics Conference on Measurement and Modeling of Computer Systems, Austin, TX, 1985, pp. 147-154
[11] Buchholz, P., A class of hierarchical queueing networks and their analysis, Queueing systems, 15, 59-80, (1994) · Zbl 0789.60067
[12] Hermanns, H.; Katoen, J., Automated compositional Markov chain generation for a plain-old telephony system, Science of computer programming, 36, 1, 97-127, (1999) · Zbl 0941.68649
[13] M. Siegle, Structured Markovian performance modelling with automatic symmetry exploitation, in: G. Haring, H. Wabnig (Eds.), Short Papers and Tool Descriptions Proceedings of the 7th International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, Vienna, Austria, 1994, pp. 77-81
[14] Bryant, R., Graph-based algorithms for Boolean function manipulation, Ieee toc, C-35, 8, 677-691, (1986) · Zbl 0593.94022
[15] R. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, F. Somenzi, Algebraic decision diagrams and their applications, in: ICCAD-93: International Conference on Computer-Aided Design, ACM/IEEE, Santa Clara, CA, 1993, pp. 188-191, also available in Formal Methods in System Design 10 (2/3) 1997
[16] E. Clarke, M. Fujita, P. McGeer, K. McMillan, J. Yang, X. Zhao, Multi-terminal binary decision diagrams: an efficient data structure for matrix representation, in: Proceedings of International Workshop on Logic Synthesis (IWLS’93), Tahoe City, 1993, pp. 6a:1-15, also available in Formal Methods in System Design 10 (2/3) (1997) 149-169
[17] Hansson, H.; Jonsson, B., A framework for reasoning about time and reliability, (), 102-111
[18] C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, On the logical characterisation of performability properties, in: ICALP, vol. 1853 of Lecture Notes in Computer Science, Springer, 2000, pp. 780-792 · Zbl 0973.68014
[19] Hermanns, H.; Herzog, U.; Mertsiotakis, V., Stochastic process algebras–between LOTOS and Markov chains, Computer networks and ISDN (CNIS), 30, 9-10, 901-924, (1998)
[20] H. Hermanns, Interactive Markov chains, Lecture Notes in Computer Science, vol. 2428, Springer, 2002 · Zbl 1012.68142
[21] Bernardo, M.; Gorrieri, R., A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time, Theoretical computer science, 202, 1-54, (1998) · Zbl 0902.68075
[22] M. Bravetti, M. Bernardo, Compositional asymmetric cooperations for process algebras with probabilities, priorities, and time, in: Proceedings of the 1st International Workshop on Models for Time Critical Systems (MTCS 2000), Electronic Notes in Theoretical Computer Science 39 (3), State College (PA), 2000 · Zbl 0970.68114
[23] Olderog, E.-R.; Hoare, C., Specification-oriented semantics for communicating processes, Acta informatica, 23, 1, 9-66, (1986) · Zbl 0569.68019
[24] G. Plotkin, A structural approach to operational semantics, technical report, Computer Science Department FN-19, DAIMI, Aarhus University, September 1981
[25] A. Bianco, L. de Alfaro, Model checking of probabilistic and nondeterministic systems, in: P. Thiagarajan (Ed.), Proceedings of Foundations of Software Technology and Theoretical Computer Science, vol. 1026 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 499-513 · Zbl 1354.68167
[26] Baier, C.; Kwiatkowska, M., Model checking for a probabilistic branching time logic with fairness, Distributed computing, 11, 125-155, (1998)
[27] Hart, S.; Sharir, M.; Pnueli, A., Termination of probabilistic concurrent programs, ACM transactions on programming languages and systems, 5, 356-380, (1983) · Zbl 0511.68009
[28] L. de Alfaro, From fairness to chance, in: C. Baier, M. Huth, M. Kwiatkowska, M. Ryan (Eds.), Proceedings of First International Workshop on Probabilistic Methods in Verification (PROBMIV’98), vol. 22 of Electronic Notes in Theoretical Computer Science, 1998 · Zbl 0920.68075
[29] E. Clarke, E. Emerson, A. Sistla, Automatic verification of finite-state concurrent systems using temporal logics, in: 10th ACM Symposium on Principles of Programming Languages, 1983, pp. 24-26, the full version is available in ACM Transactions on Programming Languages and Systems 1(2), 1986
[30] C. Baier, On algorithmic verification methods for probabilistic systems, Habilitation thesis, Fakultät für Mathematik & Informatik, Universität Mannheim, 1999
[31] L. de Alfaro, Stochastic transition systems, in: D. Sangiorgi, R. de Simone (Eds.), Proceedings of CONCUR’98, Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 423-438
[32] L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, R. Segala, Symbolic model checking for probabilistic processes using MTBDDs and the Kronecker representation, in: S. Graf, M. Schwartzbach (Eds.), TACAS’2000, LNCS 1785, Berlin, 2000, pp. 395-410 · Zbl 0960.68109
[33] G. Ciardo, R. Zijal, Well-defined stochastic Petri nets, in: MASCOTS, 1996, pp. 278-284
[34] Qureshi, M.; Sanders, W.; van Moorsel, A.; German, R., Algorithms for the generation of state-level representations of stochastic activity networks with general reward structures, IEEE transactions on software engineering, 22, 9, 603-614, (1996)
[35] D. Deavours, W. Sanders, An efficient well-specified check, in: P. Bucholz, M. Silva (Eds.), Proceedings of the 8th International Workshop on Petri Nets and Performance Models (PNPM ’99), Zaragoza, Spain, 1999, pp. 124-133
[36] H. Hermanns, M. Siegle, Bisimulation algorithms for stochastic process algebras and their BDD-based implementation, in: J.-P. Katoen (Ed.), ARTS’99, 5th International AMAST Workshop on Real-Time and Probabilistic Systems, vol. 1601 of Lecture Notes in Computer Science, Springer, 1999, pp. 144-264
[37] Ajmone Marsan, M.; Balbo, G.; Conte, G., A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems, ACM transactions on computer systems, 2, 2, 93-122, (1984)
[38] Ajmone Marsan, M.; Balbo, G.; Conte, G.; Donatelli, S.; Franceschinis, G., Modelling with generalized stochastic Petri nets, (1995), Wiley · Zbl 0843.68080
[39] A. Shiryaev, Probability, 2nd edition, vol. 95 of Graduate Texts in Mathematics, Springer, 1996
[40] Stewart, W., Introduction to the numerical solution of Markov chains, (1994), Princeton University Press
[41] Jensen, A., Markoff chains as an aid in the study of markoff processes, Skand. aktuarietiedskr., 36, 87-91, (1953) · Zbl 0051.35607
[42] Grassmann, W., Transient solutions in Markovian queues, European journal of operational research, 1, 396-402, (1977) · Zbl 0371.60110
[43] E. Clarke, K. McMillan, X. Zhao, M. Fujita, J. Yang, Spectral transforms for large boolean functions with applications to technology mapping, in: 30th Design Automation Conference, ACM/IEEE, 1993, pp. 54-60
[44] K. Brace, R. Rudell, R. Bryant, Efficient implementation of a BDD package, in: 27th ACM/IEEE Design Automation Conference, 1990, pp. 40-45
[45] Enders, R.; Filkorn, T.; Taubner, D., Generating BDDs for symbolic model checking in CCS, Distributed computing, 6, 3, 155-164, (1993) · Zbl 0778.68063
[46] McMillan, K., Symbolic model checking, (1993), Kluwer Academic Publishers · Zbl 0784.68004
[47] M. Kwiatkowska, G. Norman, D. Parker, R. Segala, Symbolic model checking of concurrent probabilistic systems using MTBDDs and Simplex, Tech. rep., School of Computer Science, University of Birmingham, 1999
[48] M. Kwiatkowska, G. Norman, D. Parker, PRISM: Probabilistic symbolic model checker, in: T. Field, P. Harrison, J. Bradley, U. Harder (Eds.), Proceedings of 12th International Conference on Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS’02), vol. 2324 of LNCS, Springer, 2002, pp. 200-204 · Zbl 1047.68533
[49] F. Somenzi, Cudd: Colorado university decision diagram package, release 2.3.0, user’s Manual and Programmer’s Manual, http://vlsi.colorado.edu/ fabio, September 1998
[50] R. Alur, T. Henzinger, Reactive modules, in: Proceedings of 11th Annual IEEE Symposium on Logic in Computer Science (LICS’96), IEEE Computer Society Press, 1006, pp. 207-218
[51] E. Frank, Codierung und numerische analyse von transitionssystemen unter verwendung von MTBDDs, student’s thesis, Universität Erlangen-Nürnberg, IMMD 7, 1999 (in German)
[52] E. Frank, Erweiterung eines MTBDD-basierten Werkzeugs für die Analyse stochastischer Transitionssysteme, Tech. Report Informatik 7, no. 01/00, Universität Erlangen-Nürnberg, January 2000 (in German)
[53] Hermanns, H.; Herzog, U.; Klehmet, U.; Mertsiotakis, V.; Siegle, M., Compositional performance modelling with the tipptool, Performance evaluation, 39, 1-4, 5-35, (2000) · Zbl 1052.68553
[54] C. Kelley, Iterative Methods for linear and nonlinear systems, Series on Frontiers in Applied Mathematics, SIAM, 1995 · Zbl 0832.65046
[55] Ibe, O.; Trivedi, K., Stochastic Petri net models of polling systems, IEEE journal on selected areas in communications, 8, 9, 1649-1657, (1990)
[56] H. Hermanns, J. Meyer-Kayser, M. Siegle, Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains, in: B. Plateau, W. Stewart, M. Silva (Eds.), 3rd International Workshop on the Numerical Solution of Markov Chains, Prensas Universitarias de Zaragoza, 1999, pp. 188-207
[57] Aspnes, J.; Herlihy, M., Fast randomized consensus using shared memory, Journal of algorithms, 11, 3, 441-460, (1990) · Zbl 0705.68016
[58] M. Vardi, Automatic verification of probabilistic concurrent finite state programs, in: Proceedings of IEEE Symposium on Foundations of Computer Science (FOCS’85), 1985, pp. 327-338
[59] Bollig, B.; Wegener, I., Improving the variable ordering of OBDDs is npcomplete, IEEE transactions on computers, 45, 9, 993-1006, (1996) · Zbl 1048.68571
[60] S. Tani, K. Hamaguchi, S. Yajima, The complexity of optimal variable ordering of a shared binary decision diagram, in: Proceedings of 45th ISAAC, vol. 762 of Lecture Notes in Computer Science, Springer, 1993, pp. 389-398 · Zbl 0925.68198
[61] R. Rudell, Dynamic variable ordering for ordered binary decision diagrams, in: Proceedings of IEEE ICCAD’93, 1993, pp. 42-47
[62] M. Fujita, Y. Matsunaga, T. Kakuda, On variable ordering of binary decision diagrams for the application of multi-level logic synthesis, in: Proceedings of European Design Automation Conference (EDAC 91), IEEE Computer Society Press, 1991, pp. 50-54
[63] J. Bern, C. Meinel, A. Slobodova, Global rebuilding of OBDD’s–tunneling memory requirement maxima, in: P. Wolper (Ed.), Proceedings of International Conference On Computer Aided Verification, vol. 939 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 4-15
[64] D. Parker, Implementation of symbolic model checking for probabilistic systems, Ph.D. thesis, School of Computer Science, University of Birmingham, submitted
[65] Kemeny, J.; Snell, J., Finite Markov chains, (1976), Springer · Zbl 0328.60035
[66] Larsen, K.; Skou, A., Bisimulation through probabilistic testing, Information and computation, 94, 1, 1-28, (1991) · Zbl 0756.68035
[67] Clarke, E.M.; Jha, S.; Enders, R.; Filkorn, T., Exploiting symmetry in temporal logic model checking, Formal methods in system design, 9, 1/2, 77-104, (1996)
[68] J. Katoen, M. Kwiatkowska, G. Norman, D. Parker, Faster and symbolic CTMC model checking, in: L. de Alfaro, S. Gilmore (Eds.), Proceedings of Process Algebra and Probabilistic Methods (PAPM-PROBMIV 2001), vol. 2165 of Lecture Notes in Computer Science, Springer, 2001, pp. 23-38 · Zbl 1007.68517
[69] M. Kwiatkowska, G. Norman, D. Parker, Probabilistic symbolic model checking with PRISM: a hybrid approach, in: J.-P. Katoen, P. Stevens (Eds.), Proceedings of 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02), vol. 2280 of LNCS, Springer, 2002, pp. 52-66 · Zbl 1043.68576
[70] P. D’Argenio, B. Jeannet, H. Jensen, K. Larsen, Reachability Analysis of Probabilistic Systems by Successive Refinements, in: L. de Alfaro, S. Gilmore (Eds.), Process Algebra and Probabilistic Methods. Joint International Workshop PAPMPROBMIV 2001, Springer, LNCS 2165, 2001, pp. 39-56 · Zbl 1007.68131
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.