Abstract
We review high-level specification formalisms for Markovian performability models, thereby emphasising the role of structuring concepts as realised par excellence by stochastic process algebras. Symbolic representations based on decision diagrams are presented, and it is shown that they quite ideally support compositional model construction and analysis.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Ajmone Marsan, G. Balbo, and G. Conte. A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems. ACM Transactions on Computer Systems, 2(2):93–122, May 1984.
M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with generalized stochastic Petri nets. Wiley, 1995.
F. Baccelli, W.A. Massey, and D. Towsley. Acyclic Fork-Join Queuing Networks. Journal of the ACM, 36(3):615–642, 1989.
R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic Decision Diagrams and their Applications. Formal Methods in System Design, 10(2/3):171–206, April/May 1997.
F. Baskett, K.M. Chandy, R.R. Muntz, and F.G. Palacios. Open, Closed and Mixed Networks of Queues with Different Classes of Customers. Journal of the ACM, 22(2):248–260, 1975.
M. Bernardo and R. Gorrieri. A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. Theoretical Computer Science, 202:1–54, 1998.
H. Bohnenkamp and B. Haverkort. Semi-Numerical Solution of Stochastic Process Algebra Models. In J.-P. Katoen, editor, ARTS’99, pages 228–243. Springer, LNCS 1601, 1999.
G. Bolch and S. Greiner. Modeling and Performance Evaluation of Production Lines Using the Modeling Language MOSEL. In Proc. of the 2nd IEEE/ECLA/IFIP Int. Conf. on Architectures and Design Methods for Balanced Automation Systems, pages 163–174, June 1996.
A. Bouali and R. de Simone. Symbolic Bisimulation Minimisation. In Computer Aided Verification, pages 96–108, 1992. LNCS 663.
M. Bozga and O. Maler. On the Representation of Probabilities over Structured Domains. In N. Halbwachs and D. Peled, editors, Int. Conf. on Computer-Aided Verification (CAV’99), pages 261–273. Springer, LNCS 1633, July 1999.
K.S. Brace, R.L. Rudell, and R.E. Bryant. Efficient Implementation of a BDD Package. In 27th ACM/IEEE Design Automation Conf., pages 40–45, 1990.
R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
P. Buchholz. Die strukturierte Analyse Markovscher Modelle. PhD thesis, Universität Dortmund, 1991 (in German).
P. Buchholz. A Hierarchical View of GCSPNs and Its Impact on Qualitative and Quantitative Analysis. Journal of Parallel and Distributed Computing, 15(3):207–224, July 1992.
P. Buchholz. Aggregation and Reduction Techniques for Hierarchical GCSPNs. In Proc. of PNPM’ 93, pages 216–225, Tolouse, October 1993.
P. Buchholz. Hierarchies in Colored GSPNs. In M. Ajmone Marsan, editor, 14th Int. Conf. on Application and Theory of Petri Nets, pages 106–125. Springer, LNCS 691, 1993.
P. Buchholz. A class of hierarchical queueing networks and their analysis. Queueing Systems, 15: 59–80, 1994.
P. Buchholz. Markovian Process Algebra: Composition and Equivalence. In U. Herzog and M. Rettelbach, editors, Proc. of the 2nd Workshop on Process Algebras and Performance Modelling, pages 11–30. Arbeitsberichte des IMMD No. 27/4, Universität Erlangen-Nürnberg, July 1994.
P. Buchholz. A Framework for the Hierarchical Analysis of Discrete Event DynamicSystems. Habilitation thesis, Universität Dortmund, 1996.
P. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS Journal of Computing, 12(3):203–222, Summer 2000.
P. Buchholz and P. Kemper. On Generating a Hierarchy for GSPN Analysis. Performance Evaluation Review (ACM Sigmetrics), 26(2):5–14, August 1998.
P. Buchholz and P. Kemper. A Toolbox for the Analysis of Discrete Event Dynamic Systems. In N. Halbwachs and D. Peled, editors, Computer Aided Verification, pages 483–486. Springer, LNCS 1633, 1999.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. Information and Computation, (98):142–170, 1992.
J.P. Buzen. Computational Algorithms for Closed Queueing Networks with Exponential Servers. Communications of the ACM, 16:527–531, 1973.
W.L. Cao and W.J. Stewart. Iterative Aggregation/Disaggregation Techniques for Nearly Uncoupled Markov Chains. Journal of the ACM, 32(3):702–719, July 1985.
G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. On Well-Formed Coloured Nets and their Symbolic Reachability Graph. In Proc. of the 11th Int. Conf. on Application and Theory of Petri Nets, pages 387–410, Paris, June 1990. Reprinted in High-level Petri Nets, K. Jensen, G. Rozenberg, eds., Springer 1991.
G. Ciardo. Analysis of Large Stochastic Petri Net Models. PhD thesis, Duke University, Durham, NC, USA, 1989.
G. Ciardo and A.S. Miner. A data structure for the e.cient Kronecker solution of GSPNs. In P. Buchholz and M. Silva, editors, PNPM’99, pages 22–31. IEEE computer society, 1999.
G. Ciardo and M. Tilgner. Parametric State Space Structuring. Technical Report ICASE Report No. 97-67, ICASE, 1997.
G. Ciardo and K.S. Trivedi. A decomposition approach for stochastic reward net models. Performance Evaluation, 18(1):37–59, July 1993.
E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang. Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. In 30th Design Automation Conf., pages 54–60. ACM/IEEE, 1993.
A.E. Conway and N.D. Georganas. Queueing Networks — Exact Computational Algorithms. MIT Press, 1989.
P.J. Courtois. Decomposability, queueing and computer system applications. ACM monograph series, 1977.
P.J. Courtois. On Time and Space Decomposition of Complex Structures. Communications of the ACM, 28(6):590–603, June 1985.
J. Couvillion, R. Freire, R. Johnson, W.D. Obal II, M.A. Qureshi, M. Rai, W.H. Sanders, and J. Tvedt. Performability modeling with UltraSAN. IEEE Software, 8(5):69–80, September 1991.
I. Davies. Symbolic techniques for the performance analysis of generalised stochastic Petri nets. Master’s thesis, University of Cape Town, Department of Computer Science, January 2001.
M. Davio. Kronecker Products and Shuffle Algebra. IEEE Transactions on Computers, C-30(2): 116–125, February 1981.
L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic Model Checking for Probabilistic Processes using MTBDDs and the Kronecker Representation. In S. Graf and M. Schwartzbach, editors, TACAS’2000, pages 395–410, Berlin, 2000. Springer, LNCS 1785.
S. Donatelli. Superposed stochastic automata: a class of stochastic Petri nets with parallel solution and distributed state space. Performance Evaluation, 18(1):21–36, July 1993.
S. Donatelli. Superposed Generalized Stochastic Petri Nets: Definition and Efficient Solution. In M. Silva, editor, 15th Int. Conf. on Application and Theory of Petri Nets, Zaragoza, June 1994.
R. Enders, T. Filkorn, and D. Taubner. Generating BDDs for symbolicmo del checking in CCS. Distributed Computing, (6):155–164, 1993.
P. Fernandes, B. Plateau, and W.J. Stewart. Efficient Descriptor-Vector Multiplications in Stochastic Automata Networks. Journal of the ACM, 45(3):381–414, May 1998.
G. Franceschinis and M. Ribaudo. Efficient Performance Analysis Techniques for Stochastic Well-Formed Nets and Stochastic Process Algebras. In W. Reisig and G. Rozenberg, editors, Lectures on Petri Nets II: Applications, pages 386–437. Springer, LNCS 1492, 1998.
E. Frank. Codierung und numerische Analyse von Transitionssystemen unter Verwendung von MTBDDs. Student’s thesis, Universität Erlangen-Nürnberg, October 1999 (in German).
E. Frank. Erweiterung eines MTBDD-basierten Werkzeugs für die Analyse stochastischer Transitionssysteme. Technical Report Inf 7, 01/00, Universität Erlangen-Nürnberg, January 2000 (in German).
M. Fujita, P. McGeer, and J.C.-Y. Yang. Multi-terminal Binary Decision Diagrams: An efficient data structure for matrix representation. Formal Methods in System Design, 10(2/3):149–169, April/May 1997.
R. German. Performance Analysis of Communication Systems — Modelling with Non-Markovian Stochastic Petri Nets. Wiley, 2000.
N. Götz, U. Herzog, and M. Rettelbach. Multiprocessor and Distributed System Design: The Integration of Functional Specification and Performance Analysis Using Stochastic Process Algebras. In Proc. of PERFORMANCE 1993, Tutorial, pages 121–146. Springer LNCS 729, 1993.
G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Probabilistic Analysis of Large Finite State Machines. In 31st Design Automation Conf., pages 270–275, San Diego, CA, June 1994. ACM/IEEE.
G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Symbolic Algorithms to Calculate Steady-State Probabilities of a Finite State Machine. In European Design Automation Conf., pages 214–218, Paris, February 1994. IEEE.
G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Markovian Analysis of Large Finite State Machines. IEEE Transactions on CAD, 15(12):1479–1493, Dec. 1996.
H. Hermanns. Interactive Markov Chains. PhD thesis, Universität Erlangen-Nürnberg, September 1998. Arbeitsberichte des IMMD No. 32/7.
H. Hermanns, U. Herzog, and J.-P. Katoen. Process algebra for performance evaluation. Theoretical Computer Science, 2001. to appear.
H. Hermanns, U. Herzog, U. Klehmet, V. Mertsiotakis, and M. Siegle. Compositional performance modelling with the TIPPtool. Performance Evaluation, 39(1–4):5–35, January 2000.
H. Hermanns, U. Herzog, and V. Mertsiotakis. Stochastic Process Algebras-Between LOTOS and Markov Chains. Computer Networks and ISDN systems (CNIS), 30(9–10):901–924, 1998.
H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov Chain Model Checker. In S. Graf and M. Schwartzbach, editors, TACAS’2000, pages 347–362, Berlin, 2000. Springer, LNCS 1785.
H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. Towards model checking stochastic process algebra. In W. Grieskamp, T. Santen, and B. Stoddart, editors, 2nd Int. Conf. on Integrated Formal Methods, pages 420–439, Dagstuhl, November 2000. Springer, LNCS 1945.
H. Hermanns, M. Kwiatkowska, G. Norman, D. Parker, and M. Siegle. On the use of MTBDDs for performability analysis and verification of stochastic systems. (in preparation).
H. Hermanns, J. Meyer-Kayser, and M. Siegle. Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains. In B. Plateau, W.J. Stewart, and M. Silva, editors, 3rd Int. Workshop on the Numerical Solution of Markov Chains, pages 188–207. Prensas Universitarias de Zaragoza, 1999.
H. Hermanns and M. Rettelbach. Syntax, Semantics, Equivalences, and Axioms for MTIPP. In U. Herzog and M. Rettelbach, editors, Proc. of the 2nd Workshop on Process Algebras and Performance Modelling, pages 71–88. Arbeitsberichte des IMMD No. 27/4, Universität Erlangen-Nürnberg, July 1994.
H. Hermanns and M. Siegle. Bisimulation Algorithms for Stochastic Process Algebras and their BDD-based Implementation. In J.-P. Katoen, editor, ARTS’99, 5th Int. AMAST Workshop on Real-Time and Probabilistic Systems, pages 144–264. Springer, LNCS 1601, 1999.
U. Herzog. Leistungsbewertung und Modellbildung für Parallelrechner. Informationstechnik (it), 31(1):31–38, 1989. (in German).
U. Herzog. Performance Evaluation and Formal Description. In V.A. Monaco and R. Negrini, editors, Advanced Computer Technology, Reliable Systems and Applications, Proceedings, pages 750–756. IEEE Comp. Soc. Press, 1991.
J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.
J. Hillston and V. Mertsiotakis. A Simple Time Scale Decomposition Technique for Stochastic Process Algebras. The Computer Journal, 38(7):566–577, December 1995. Special issue: Proc. of the 3rd Workshop on Process Algebras and Performance Modelling.
O.C. Ibe and K.S. Trivedi. Stochastic Petri Net Models of Polling Systems. IEEE Journal on Selected Areas in Communications, 8(9):1649–1657, December 1990.
P. Kemper. Reachability analysis based on structured representation. In J. Billington and W. Reisig, editors, Application and Theory of Petri Nets, pages 269–288. Springer, LNCS 1091, 1999.
C. Kim and A.K. Agrawala. Analysis of the Fork-Join Queue. IEEE Transactions on Computers, 38(2): 250–255, 1989.
W. Kleinöder. Stochastische Bewertung von Aufgabenstrukturen fur hierarchische Mehrrechnersysteme. PhD thesis, Universität Erlangen-Nürnberg, Arbeitsberichte des IMMD No. 15/10, August 1982 (in German).
W. Knottenbelt. Generalized Markovian Analysis of Timed Transition Systems. Master’s thesis, University of Cape Town, June 1996.
M. Kwiatkowska, G. Norman, and R. Segala. Automated Verification of a Randomised Distributed Consensus Protocol Using Cadence SMV and PRISM. Technical Report CSR-01-1, School of Computer Science, University of Birmingham, January 2001.
V. Mertsiotakis. Time Scale Decomposition of Stochastic Process Algebra Models. In E. Brinksma and A. Nymeyer, editors, Proc. of 5th Workshop on Process Algebras and Performance Modelling. CTIT Technical Report series, No. 97–14, University of Twente, June 1997.
V. Mertsiotakis. Approximate Analysis Methods for Stochastic Process Algebras. PhD thesis, Universität Erlangen-Nürnberg, 1998.
V. Mertsiotakis and M. Silva. Throughput Approximation of Decision Free Processes Using Decomposition. In Proc. of the 7th Int. Workshop on Petri Nets and Performance Models, pages 174–182, St. Malo, June 1997. IEEE CS-Press.
M. Meyer. Entwurf eines spezialisierten Coprozessors für die Manipulation von Binären Entscheidungsdiagrammen. Student’s thesis, Universität Erlangen-Nürnberg, January 2001 (in German).
A. Miner. Efficient solution of GSPNs using matrix diagrams. In Petri Nets and Performance models (PNPM). IEEE Computer Society Press, 2001. (to appear).
A. Miner and G. Ciardo. Efficient reachability set generation and storage using decision diagrams. In H. Kleijn and S. Donatelli, editors, Application and Theory of Petri Nets 1999, pages 6–25. Springer, LNCS 1639, 1999.
A.S. Miner, G. Ciardo, and S. Donatelli. Using the exact state space of a Markov model to compute approximate stationary measures. Performance Evaluation Review, 28(1):207–216, June 2000. Proc. of ACM SIGMETRICS 2000.
M.K. Molloy. Performance Analysis Using Stochastic Petri Nets. IEEE Transactions on Computers, C-31: 913–917, September 1982.
R. Nelson and A.N. Tantawi. Approximate Analysis of Fork/Join Synchronization in Parallel Queues. IEEE Transactions on Computers, 37(6):739–743, 1988.
D. Parker. Implementation of symbolic model checking for probabilistic systems. PhD thesis, School of Computer Science, University of Birmingham, 2001. (to appear).
B. Plateau. On the Synchronization Structure of Parallelism and Synchronization Models for Distributed Algorithms. In Proc. of ACM SIGMETRICS, pages 147–154, Austin, TX, August 1985.
B. Plateau and K. Atif. Stochastic Automata Network for Modeling Parallel Systems. IEEE Transactions on Software Engineering, 17(10):1093–1108, 1991.
B. Plateau and J.-M. Fourneau. A Methodology for Solving Markov Models of Parallel Systems. Journal of Parallel and Distributed Computing, 12:370–387, 1991.
B. Plateau, J.-M. Fourneau, and K.-H. Lee. PEPS: A Package for Solving Complex Markov Models of Parallel Systems. In Proc. of the 4th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, pages 341–360, Palma (Mallorca), September 1988.
M. Reiser and S. Lavenberg. Mean Value Analysis of Closed Multichain Queueing Networks. Journal of the ACM, 27(2):313–322, 1980.
J.A. Rolia and K.C. Sevcik. The Method of Layers. IEEE Transactions on Software Engineering, 21(8):689–700, August 1995.
W.H. Sanders and J.F. Meyer. Reduced Base Model Construction Methods for Stochastic Activity Networks. IEEE Journal on Selected Areas in Communications, 9(1):25–36, January 1991.
C. Sauer and E. McNair. The Evolution of the Research Queueing Package RESQ. In Proc. of the First Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, Paris, May 1984.
M. Sczittnick. Techniken zur funktionalen und quantitativen Analyse von Markoffschen Rechensystemmodellen. Master’s thesis, Universitat Dortmund, August 1987 (in German).
M. Siegle. Using Structured Modelling for Efficient Performance Prediction of Parallel Systems. In G.R. Joubert, D. Trystram, F.J. Peters, and D.J. Evans, editors, Parallel Computing: Trends and Applications, Proc. of the Int. Conf. ParCo93, pages 453–460. North-Holland, 1994.
M. Siegle. Beschreibung und Analyse von Markovmodellen mit großem Zustandsraum. PhD thesis, Universität Erlangen-Nürnberg, 1995 (in German).
M. Siegle. Compositional Representation and Reduction of Stochasitic Labelled Transition Systems based on Decision Node BDDs. In D. Baum, N. Müller, and R. Rödler, editors, MMB’99, pages 173–185, Trier, September 1999. VDE Verlag.
M. Siegle. Behaviour analysis of communication systems: Stochastic modelling and analysis. Habilitation thesis, University of Erlangen-Nürnberg, 2001 (to appear).
H.A. Simon and A. Ando. Aggregation of Variables in Dynamic Systems. Econometrica, 29:111–138, 1961.
F. Somenzi. CUDD: Colorado University Decision Diagram Package, Release 2.3.0. User’s Manual and Programmer’s Manual, September 1998.
W. Stewart, K. Atif, and B. Plateau. The Numerical Solution of Stochastic Automata Networks. Rapport Apache 6, Institut IMAG, LGI, LMC, Grenoble, November 1993.
W.J. Stewart. MARCA: Markov Chain Analyzer, A Software Package for Markov Modeling. In W.J. Stewart, editor, Numerical Solution of Markov Chains. Marcel Dekker, 1991.
W.J. Stewart. Introduction to the numerical solution of Markov chains. Princeton University Press, 1994.
M. Veran and D. Potier. QNAP2: A Portable Environment for Queueing Systems Modelling. In Proc. of the First Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, Paris, May 1984.
M. Woodside, J.E. Neilson, D.C. Petriu, and S. Majumdar. The Stochastic Rendezvous Network Model for Performance of Synchronous Client-Server-like Distributed Software. IEEE Transactions on Computers, 44(1): 20–34, January 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Siegle, M. (2001). Advances in Model Representations. In: de Alfaro, L., Gilmore, S. (eds) Process Algebra and Probabilistic Methods. Performance Modelling and Verification. PAPM-PROBMIV 2001. Lecture Notes in Computer Science, vol 2165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44804-7_1
Download citation
DOI: https://doi.org/10.1007/3-540-44804-7_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42556-4
Online ISBN: 978-3-540-44804-4
eBook Packages: Springer Book Archive