Skip to main content
SpringerLink
Log in

Distributed and Structured Analysis Approaches to Study Large and Complex Systems⋆

  • Chapter
  • First Online:
Lectures on Formal Methods and PerformanceAnalysis (EEF School 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2090))

Included in the following conference series:

Abstract

Both the logic and the stochastic analysis of discrete-state systems are hindered by the combinatorial growth of the state space underlying a high-level model. In this work, we consider two orthogonal approaches to cope with this “state-space explosion”. Distributed algorithms that make use of the processors and memory overall available on a network of N workstations can manage models with state spaces approximately N times larger than what is possible on a single workstation. A second approach, constituting a fundamental paradigm shift, is instead based on decision diagrams and related implicit data structures that efficiently encode the state space or the transition rate matrix of a model, provided that it has some structure to guide its decomposition; with these implicit methods, enormous sets can be managed efficiently, but the numerical solution of the stochastic model, if desired, is still a bottleneck, as it requires vectors of the size of the state space.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S.C. Allmaier, M. Kowarschik, and G. Horton. State space construction and steady-state solution of GSPNs on a shared-memory multiprocessor. In Proc. 7th Int. Workshop on Petri Nets and Performance Models (PNPM’97), pages 112–121, St. Malo, France, June 1997. IEEE Comp. Soc. Press.

    Google Scholar 

  2. V. Amoia, G. De Micheli, and M. Santomauro. Computer-oriented formulation of transition-rate matrices via Kronecker algebra. IEEE Trans. Rel., 30:123–132, June 1981.

    Article  MATH  Google Scholar 

  3. J.A. Bergstra, A. Ponse, and S.A. Smolka. Handbook of Process Algebra. North-Holland, 2001.

    Google Scholar 

  4. J.W. Brewer. Kronecker products and matrix calculus in system theory. IEEE Trans. Circ. and Syst., CAS-25:772–781, Sept. 1978.

    Article  MathSciNet  Google Scholar 

  5. R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp., 35(8):677–691, Aug. 1986.

    Article  MATH  Google Scholar 

  6. R.E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comp. Surv., 24(3):393–318, 1992.

    Article  Google Scholar 

  7. P. Buchholz. Numerical solution methods based on structured descriptions of Markovian models. In G. Balbo and G. Serazzi, editors, Computer performance Evaluation, pages 251–267. Elsevier Science Publishers B.V. (North-Holland), 1991.

    Google Scholar 

  8. P. Buchholz. Hierarchical Markovian models-Symmetries and Reduction. In Modelling Techniques and Tools for Computer Performance Evaluation. Elsevier Science Publishers B.V. (North-Holland), 1992.

    Google Scholar 

  9. P. Buchholz. A class of hierarchical queueing networks and their analysis. Queueing Systems., 15:59–80, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  10. P. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of memoryefficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp., 12(3):203–222, Summer 2000.

    Article  MATH  MathSciNet  Google Scholar 

  11. P. Buchholz, M. Fischer, and P. Kemper. Distributed steady state analysis using Kronecker algebra. In B. Plateau, W.J. Stewart, and M. Silva, editors, Numerical Solution of Markov Chains, pages 76–95. Prensas Universitarias de Zaragoza, Zaragoza, Spain, Sept. 1999.

    Google Scholar 

  12. P. Buchholz and P. Kemper. Numerical analysis of stochastic marked graphs. In Proc. 6th Int. Workshop on Petri Nets and Performance Models (PNPM’95), pages 32–41, Durham, NC, Oct. 1995. IEEE Comp. Soc. Press.

    Google Scholar 

  13. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020_states and beyond. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428–439, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.

    Google Scholar 

  14. S. Caselli, G. Conte, and P. Marenzoni. Parallel state space exploration for GSPN models. In G. De Michelis and M. Diaz, editors, Application and Theory of Petri Nets 1995 (Proc. 16th Int. Conf. on Applications and Theory of Petri Nets, Turin, Italy), Lecture Notes in Computer Science 935, pages 181–200. Springer-Verlag, June 1995.

    Google Scholar 

  15. G. Ciardo, J. Gluckman, and D. Nicol. Distributed state-space generation of discrete-state stochastic models. INFORMS J. Comp., 10(1):82–93, 1998.

    Article  Google Scholar 

  16. G. Ciardo, G. Luettgen, and R. Siminiceanu. Efficient symbolic state-space construction for asynchronous systems. In M. Nielsen and D. Simpson, editors, Application and Theory of Petri Nets 2000 (Proc. 21th Int. Conf. on Applications and Theory of Petri Nets, Aarhus, Denmark), Lecture Notes in Computer Science 1825, pages 103–122. Springer-Verlag, June 2000.

    Google Scholar 

  17. G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: an efficient iteration strategy for symbolic state space generation. In T. Margaria and W. Yi, editors, Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer-Verlag, Apr. 2001.To appear.

    Google Scholar 

  18. G. Ciardo and A.S. Miner. SMART: Simulation and Markovian Analyzer for Reliability and Timing. In Proc. IEEE International Computer Performance and Dependability Symposium (IPDS’96), page 60, Urbana-Champaign, IL, USA, Sept. 1996. IEEE Comp. Soc. Press.

    Google Scholar 

  19. G. Ciardo and A.S. Miner. Storage alternatives for large structured state spaces. In R. Marie, B. Plateau, M. Calzarossa, and G. Rubino, editors, Proc. 9th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, Lecture Notes in Computer Science 1245, pages 44–57, St. Malo, France, June 1997. Springer-Verlag.

    Chapter  Google Scholar 

  20. G. Ciardo and A.S. Miner. A data structure for the efficient Kronecker solution of GSPNs. In P. Buchholz, editor, Proc. 8th Int. Workshop on Petri Nets and Performance Models (PNPM’99), pages 22–31, Zaragoza, Spain, Sept. 1999. IEEE Comp. Soc. Press.

    Google Scholar 

  21. G. Ciardo and M. Tilgner. On the use of Kronecker operators for the solution of generalized stochastic Petri nets. ICASE Report 96-35, Institute for Computer Applications in Science and Engineering, Hampton, VA, May 1996.

    Google Scholar 

  22. E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 1999.

    Google Scholar 

  23. M. Davio. Kronecker products and shuffle algebra. IEEE Trans. Comp., C-30: 116–125, Feb. 1981.

    Article  MathSciNet  Google Scholar 

  24. E.W. Dijkstra, W.H. Feijen, and A. Van Gasteren. Derivation of a termination detection algorithm for a distributed computation. Inf. Proc. Letters, 16:217–219, June 1983.

    Article  Google Scholar 

  25. S. Donatelli. Superposed Stochastic Automata: a class of stochastic Petri nets with parallel solution and distributed state space. Perf. Eval., 18:21–26, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  26. P. Fernandes, B. Plateau, and W.J. Stewart. Efficient descriptor-vector multiplication in stochastic automata networks. Journal of the ACM, 45(3):381–414, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  27. A. Graham. Kronecker Products and Matrix Calculus: with Applications. Halsted Press / John Wiley, New York, 1981.

    MATH  Google Scholar 

  28. B.R. Haverkort, A. Bell, and H. Bohnenkamp. On the efficient sequential and distributed generation of very large Markov chains from stochastic Petri nets. In P. Buchholz, editor, Proc. 8th Int. Workshop on Petri Nets and Performance Models (PNPM’99), pages 12–21, Zaragoza, Spain, Sept. 1999. IEEE Comp. Soc. Press.

    Google Scholar 

  29. T. Kam, T. Villa, R. Brayton, and A. Sangiovanni-Vincentelli. Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic, 4(1-2):9–62, 1998.

    MATH  MathSciNet  Google Scholar 

  30. K.G. Larsen, P. Pettersson, and W. Yi. Uppaal: Status and developments. In O. Grumberg, editor, 9th Int. Conf. on Computer Aided Verification (CAV’ 97), volume 1254 of Lecture Notes in Computer Science, pages 456–459. Springer-Verlag, June 1997.

    Google Scholar 

  31. P. Marenzoni, S. Caselli, and G. Conte. Analysis of large GSPN models: a distributed solution tool. In Proc. 7th Int. Workshop on Petri Nets and Performance Models (PNPM’97), pages 122–131, St. Malo, France, June 1997. IEEE Comp. Soc. Press.

    Google Scholar 

  32. V. Migallón, J. Penadés, and D.B. Szyld. Experimental study of parallel iterative solutions of Markov chains with block partitions. In B. Plateau, W.J. Stewart, and M. Silva, editors, Numerical Solution of Markov Chains, pages 96–110. Prensas Universitarias de Zaragoza, Zaragoza, Spain, Sept. 1999.

    Google Scholar 

  33. A.S. 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 (Proc. 20th Int. Conf. on Applications and Theory of Petri Nets, Williamsburg, VA, USA), Lecture Notes in Computer Science 1639, pages 6–25. Springer-Verlag, June 1999.

    Google Scholar 

  34. T. Murata. Petri Nets: properties, analysis and applications. Proc. of the IEEE, 77(4):541–579, Apr. 1989.

    Article  Google Scholar 

  35. D. Nicol and G. Ciardo. Automated parallelization of discrete state-space generation. J. Par. and Distr. Comp., 47:153–167, 1997.

    Article  Google Scholar 

  36. D.M. Nicol. Non-commital barrier synchronization. Parallel Computing, 21: 529–549, 1995.

    Article  MATH  Google Scholar 

  37. E. Pastor and J. Cortadella. Efficient encoding schemes for symbolic analysis of Petri nets. In Proc. Design Automation and Test in Europe, Feb. 1998.

    Google Scholar 

  38. E. Pastor and J. Cortadella. Structural methods applied to the symbolic analysis of Petri nets. In Proc. IEEE/ACM International Workshop on Logic Synthesis, June 1998.

    Google Scholar 

  39. E. Pastor, O. Roig, J. Cortadella, and R. Badia. Petri net analysis using Boolean manipulation. In R. Valette, editor, Application and Theory of Petri Nets 1994, (Proc. 15th Int. Conf. on Applications and Theory of Petri Nets, Zaragoza, Spain), Lecture Notes in Computer Science 815, pages 416–435. Springer-Verlag, June 1994.

    Google Scholar 

  40. S. Pissanetzky. Sparse Matrix Technology. Academic Press, 1984.

    Google Scholar 

  41. B. Plateau. On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In Proc. 1985 ACM SIGMETRICS Conf. on Measurement and Modeling of Computer Systems, pages 147–153, Austin, TX, USA, May 1985.

    Google Scholar 

  42. W.J. Stewart, K. Atif, and B. Plateau. The numerical solution of stochastic automata networks. Eur. J. of Oper. Res., 86:503–525, 1995.

    Article  MATH  Google Scholar 

  43. K. Varpaaniemi, J. Halme, K. Hiekkanen, and T. Pyssysalo. PROD reference manual. Technical Report B13, Helsinki Univ. of Technology, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, College of William and Mary, Williamsburg, VA, 23187, USA

    Gianfranco Ciardo

Authors
  1. Gianfranco Ciardo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Computer Science, Formal Methods and Tools Group, University of Twente, 217, 7500, AE, Enschede, The Netherlands

    Ed Brinksma , Holger Hermanns  & Joost-Pieter Katoen ,  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Ciardo, G. (2001). Distributed and Structured Analysis Approaches to Study Large and Complex Systems⋆. In: Brinksma, E., Hermanns, H., Katoen, JP. (eds) Lectures on Formal Methods and PerformanceAnalysis. EEF School 2000. Lecture Notes in Computer Science, vol 2090. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44667-2_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-44667-2_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42479-6

  • Online ISBN: 978-3-540-44667-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation