Advertisement

The Benefits of Sometimes Not Being Discrete

  • Jane Hillston
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)

Abstract

Discrete representations of systems are usual in theoretical computer science and they have many benefits. Unfortunately they also suffer from the problem of state space explosion, sometimes termed the curse of dimensionality. In recent years, research has shown that there are cases in which we can reap the benefits of discrete representation during system description but then gain from more efficient analysis by approximating the discrete system by a continuous one. This paper will motivate this approach, explaining the theoretical foundations and their practical benefits.

Keywords

Model Check Process Algebra Discrete Representation Discrete Time Markov Chain Model Check Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  2. 2.
    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358–372. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Bakhshi, R., Cloth, L., Fokkink, W., Haverkort, B.R.: Mean-field analysis for the evaluation of gossip protocols. In: Proceedings of 6th Int. Conference on the Quantitative Evaluation of Systems (QEST 2009), pp. 247–256 (2009)Google Scholar
  4. 4.
    Bakhshi, R., Cloth, L., Fokkink, W., Haverkort, B.R.: Mean-field framework for performance evaluation of push-pull gossip protocols. Perform. Eval. 68(2), 157–179 (2011)CrossRefGoogle Scholar
  5. 5.
    Benaïm, M., Le Boudec, J.: A class of mean field interaction models for computer and communication systems. In: Performance Evaluation (2008)Google Scholar
  6. 6.
    Benaïm, M., Le Boudec, J.Y.: On mean field convergence and stationary regime. CoRR, abs/1111.5710 (2011)Google Scholar
  7. 7.
    Bernardo, M., Gorrieri, R.: A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. Theor. Comput. Sci. 202(1-2), 1–54 (1998)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Bhat, G., Cleaveland, R., Grumberg, O.: Efficient On-the-Fly Model Checking for CTL*. In: Logic in Computer Science (LICS 1995), pp. 388–397 (1995)Google Scholar
  9. 9.
    Bortolussi, L.: On the approximation of stochastic concurrent constraint programming by master equation, vol. 220, pp. 163–180 (2008)Google Scholar
  10. 10.
    Bortolussi, L., Hayden, R.A.: Bounds on the deviation of discrete-time Markov chains from their mean-field model. Perform. Eval. 70(10), 736–749 (2013)CrossRefGoogle Scholar
  11. 11.
    Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 333–347. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  12. 12.
    Bortolussi, L., Hillston, J.: Fluid model checking. CoRR, 1203.0920 (2012)Google Scholar
  13. 13.
    Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective systems behaviour: A tutorial. In: Performance Evaluation (2013)Google Scholar
  14. 14.
    Bortolussi, L., Hillston, J.: Checking Individual Agent Behaviours in Markov Population Models by Fluid Approximation. In: Bernardo, M., de Vink, E., Di Pierro, A., Wiklicky, H. (eds.) SFM 2013. LNCS, vol. 7938, pp. 113–149. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  15. 15.
    Bortolussi, L., Lanciani, R.: Model Checking Markov Population Models by Central Limit Approximation. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 123–138. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  16. 16.
    Bortolussi, L., Policriti, A.: Dynamical systems and stochastic programming: To ordinary differential equations and back. In: Priami, C., Back, R.-J., Petre, I. (eds.) Transactions on Computational Systems Biology XI. LNCS, vol. 5750, pp. 216–267. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  17. 17.
    Calder, M., Gilmore, S., Hillston, J.: Automatically deriving ODEs from process algebra models of signalling pathways. In: Proceedings of Computational Methods in Systems Biology (CMSB 2005), pp. 204–215 (2005)Google Scholar
  18. 18.
    Cardelli, L.: Brane Calculi. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS (LNBI), vol. 3082, pp. 257–278. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    Cardelli, L.: On process rate semantics. Theor. Comput. Sci. 391(3), 190–215 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  20. 20.
    Cardelli, L.: From Processes to ODEs by Chemistry. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) 5th IFIP International Conference On Theoretical Computer Science - TCS 2008. IFIP, vol. 273, pp. 261–281. Springer, Boston (2008)CrossRefGoogle Scholar
  21. 21.
    Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: LTL model checking of time-inhomogeneous markov chains. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 104–119. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  22. 22.
    Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Logical Methods in Computer Science 7(1) (2011)Google Scholar
  23. 23.
    Ciardo, G., Trivedi, K.S.: A Decomposition Approach for Stochastic Reward Net Models. Perform. Eval. 18(1), 37–59 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  24. 24.
    Ciocchetta, F., Hillston, J.: Bio-PEPA: A framework for the modelling and analysis of biological systems. Theor. Comput. Sci. 410(33-34), 3065–3085 (2009)CrossRefzbMATHMathSciNetGoogle Scholar
  25. 25.
    Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties Form. Methods Syst. Des. 1(2-3), 275–288 (1992)CrossRefGoogle Scholar
  26. 26.
    Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Abstracting the Differential Semantics of Rule-Based Models: Exact and Automated Model Reduction. In: Proceedings of Logic in Computer Science (LICS 2010), pp. 362–381 (2010)Google Scholar
  27. 27.
    Darling, R.W.R.: Fluid limits of pure jump Markov processes: A practical guide (2002), http://arXiv.org
  28. 28.
    Darling, R.W.R., Norris, J.R.: Differential equation approximations for Markov chains. Probability Surveys 5 (2008)Google Scholar
  29. 29.
    Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSLTA. IEEE Trans. Software Eng. 35(2), 224–240 (2009)CrossRefGoogle Scholar
  30. 30.
    Gast, N., Gaujal, B.: A mean field model of work stealing in large-scale systems. In: Proceedings of ACM SIGMETRICS 2010, pp. 13–24 (2010)Google Scholar
  31. 31.
    Geisweiller, N., Hillston, J., Stenico, M.: Relating continuous and discrete PEPA models of signalling pathways. Theor. Comput. Sci. 404(1-2), 97–111 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  32. 32.
    Gillespie, D., Petzold, L.: Numerical simulation for biochemical kinetics. In: System Modeling in Cellular Biology, pp. 331–353. MIT Press (2006)Google Scholar
  33. 33.
    Gnesi, S., Mazzanti, F.: An Abstract, on the Fly Framework for the Verification of Service-Oriented Systems. In: Results of the SENSORIA Project, pp. 390–407 (2011)Google Scholar
  34. 34.
    Hayden, R.A., Bradley, J.T.: A fluid analysis framework for a Markovian process algebra. Theor. Comput. Sci. 411(22-24), 2260–2297 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  35. 35.
    Hayden, R.A., Bradley, J.T., Clark, A.D.: Performance specification and evaluation with unified stochastic probes and fluid analysis. IEEE Trans. Software Eng. 39(1), 97–118 (2013)CrossRefGoogle Scholar
  36. 36.
    Hayden, R.A., Stefanek, A., Bradley, J.T.: Fluid computation of passage-time distributions in large Markov models. Theor. Comput. Sci. 413(1), 106–141 (2012)CrossRefzbMATHMathSciNetGoogle Scholar
  37. 37.
    Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theor. Comput. Sci. 274(1-2), 43–87 (2002)CrossRefzbMATHMathSciNetGoogle Scholar
  38. 38.
    Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press (1995)Google Scholar
  39. 39.
    Hillston, J.: Exploiting Structure in Solution: Decomposing Compositional Models. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 278–314. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  40. 40.
    Hillston, J.: Fluid flow approximation of PEPA models. In: Proceedings of the Second International Conference on the Quantitative Evaluation of SysTems, QEST 2005, pp. 33 – 42 (2005)Google Scholar
  41. 41.
    Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov Reward Model Checker. In: Proceedings of Quantitative Evaluation of Systems, QEST 2005, pp. 243–244 (2005)Google Scholar
  42. 42.
    Katoen, J.-P., Mereacre, A.: Model checking HML on piecewise-constant inhomogeneous markov chains. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 203–217. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  43. 43.
    Kolesnichenko, A., Remke, A., de Boer, P.T., Haverkort, B.R.: Comparison of the mean-field approach and simulation in a peer-to-peer botnet case study. In: Thomas, N. (ed.) EPEW 2011. LNCS, vol. 6977, pp. 133–147. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  44. 44.
    Kolesnichenko, A., Remke, A., de Boer, P.-T., Haverkort, B.R.: A logic for model-checking of mean-field models. In: Proceedings of 43rd Int. Conference on Dependable Systems and Networks, DSN 2013 (2013)Google Scholar
  45. 45.
    Kurtz, T.G.: Solutions of ordinary differential equations as limits of pure jump Markov processes. Journal of Applied Probability 7, 49–58 (1970)CrossRefzbMATHMathSciNetGoogle Scholar
  46. 46.
    Kurtz, T.G.: Approximation of population processes. SIAM (1981)Google Scholar
  47. 47.
    Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer 6(2), 128–142 (2004)CrossRefGoogle Scholar
  48. 48.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  49. 49.
    Latella, D., Loreti, M., Massink, M.: On-the-fly Fast Mean-Field Model-Checking. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 297–314. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  50. 50.
    Le Boudec, J.-Y., McDonald, D., Mundinger, J.: A Generic Mean Field Convergence Result for Systems of Interacting Objects. In: Proceedings of Quantitative Evaluation of Systems (QEST 2007), pp. 3–18 (2007)Google Scholar
  51. 51.
    McCaig, C.: From individuals to populations: changing scale in process algebra models of biological systems. PhD thesis, University of Stirling (2008)Google Scholar
  52. 52.
    McCaig, C., Norman, R., Shankland, C.: Process Algebra Models of Population Dynamics. In: Horimoto, K., Regensburger, G., Rosenkranz, M., Yoshida, H. (eds.) AB 2008. LNCS, vol. 5147, pp. 139–155. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  53. 53.
    McCaig, C., Norman, R., Shankland, C.: From Individuals to Populations: A Symbolic Process Algebra Approach to Epidemiology. Mathematics in Computer Science 2(3), 535–556 (2009)CrossRefzbMATHMathSciNetGoogle Scholar
  54. 54.
    Norman, R., Shankland, C.: Developing the Use of Process Algebra in the Derivation and Analysis of Mathematical Models of Infectious Disease. In: Moreno-Díaz Jr., R., Pichler, F. (eds.) EUROCAST 2003. LNCS, vol. 2809, pp. 404–414. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  55. 55.
    Norris, J.R.: Markov Chains. Cambridge University Press (1997)Google Scholar
  56. 56.
    Priami, C.: Stochastic pi-Calculus. Comput. J. 38(7), 578–589 (1995)CrossRefGoogle Scholar
  57. 57.
    Regev, A., Panina, E.M., Silverman, W., Cardelli, L., Shapiro, E.Y.: BioAmbients: an abstraction for biological compartments. Theor. Comput. Sci. 325(1), 141–167 (2004)CrossRefzbMATHMathSciNetGoogle Scholar
  58. 58.
    Regev, A., Shapiro, E.: Cellular Abstractions: Cells as computation. Nature 419(6905), 343–343 (2002)CrossRefGoogle Scholar
  59. 59.
    Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. CRM Monograph Series, vol. 23. American Mathematical Society (2004)Google Scholar
  60. 60.
    Silva, M., Recalde, L.: Petri nets and integrality relaxations: A view of continuous Petri net models. IEEE Trans. on Systems, Man, and Cybernetics, Part C 32(4), 314–327 (2002)CrossRefGoogle Scholar
  61. 61.
    Silva, M., Recalde, L.: On fluidification of Petri Nets: from discrete to hybrid and continuous models. Annual Reviews in Control 28(2), 253–266 (2004)CrossRefGoogle Scholar
  62. 62.
    Sumpter, D.T.J.: From Bee to Society: An Agent-based Investigation of Honey Bee Colonies. PhD thesis, University of Manchester (2000)Google Scholar
  63. 63.
    Tofts, C.M.N.: A Synchronous Calculus of Relative Frequency. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 467–480. Springer, Heidelberg (1990)Google Scholar
  64. 64.
    Tribastone, M., Ding, J., Gilmore, S., Hillston, J.: Fluid rewards for a stochastic process algebra. IEEE Trans. Software Eng. 38(4), 861–874 (2012)CrossRefGoogle Scholar
  65. 65.
    Tribastone, M., Gilmore, S., Hillston, J.: Scalable differential analysis of process algebra models. IEEE Trans. Software Eng. 38(1), 205–219 (2012)CrossRefGoogle Scholar
  66. 66.
    Trivedi, K.S., Kulkarni, V.G.: FSPNs: Fluid Stochastic Petri Nets. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 24–31. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  67. 67.
    Tschaikowski, M., Tribastone, M.: Tackling continuous state-space explosion in a Markovian process algebra. Theor. Comput. Sci. 517, 1–33 (2014)CrossRefzbMATHMathSciNetGoogle Scholar
  68. 68.
    Van Kampen, N.G.: Stochastic Processes in Physics and Chemistry. Elsevier (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Jane Hillston
    • 1
  1. 1.LFCS, School of InformaticsUniversity of EdinburghUK

Personalised recommendations