×

zbMATH — the first resource for mathematics

Quantitative abstractions for collective adaptive systems. (English) Zbl 1346.68219
Bernardo, Marco (ed.) et al., Formal methods for the quantitative evaluation of collective adaptive systems. 16th international school on formal methods for the design of computer, communication, and software systems, SFM 2016, Bertinoro, Italy, June 20–24, 2016. Advanced lectures. Cham: Springer (ISBN 978-3-319-34095-1/pbk; 978-3-319-34096-8/ebook). Lecture Notes in Computer Science 9700, 202-232 (2016).
Summary: Collective adaptive systems (CAS) consist of a large number of possibly heterogeneous entities evolving according to local interactions that may operate across multiple scales in time and space. The adaptation to changes in the environment, as well as the highly dispersed decision-making process, often leads to emergent behaviour that cannot be understood by simply analysing the objectives, properties, and dynamics of the individual entities in isolation.
As with most complex systems, modelling is a phase of crucial importance for the design of new CAS or the understanding of existing ones. Elsewhere in this volume the typical workflow of formal modelling, analysis, and evaluation of a CAS has been illustrated in detail. In this chapter we treat the problem of efficiently analysing large-scale CAS for quantitative properties. We review algorithms to automatically reduce the dimensionality of a CAS model preserving modeller-defined state variables, with focus on descriptions based on systems of ordinary differential equations. We illustrate the theory in a tutorial fashion, with running examples and a number of more substantial case studies ranging from crowd dynamics, epidemiology and biological systems.
For the entire collection see [Zbl 1337.68006].

MSC:
68T42 Agent technology and artificial intelligence
68T05 Learning and adaptive systems in artificial intelligence
93A15 Large-scale systems
93A30 Mathematical modelling of systems (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aldini, A., Bravetti, M., Gorrieri, R.: A process-algebraic approach for the analysis of probabilistic noninterference. J. Comput. Secur. 12(2), 191–245 (2004) · Zbl 05430208 · doi:10.3233/JCS-2004-12202
[2] Aoki, M.: Control of large-scale dynamic systems by aggregation. IEEE Trans. Autom. Control 13(3), 246–253 (1968) · doi:10.1109/TAC.1968.1098900
[3] Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187–231 (2000) · Zbl 1073.68690 · doi:10.1006/jcss.1999.1683
[4] Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, IOS Press, Amsterdam (2009)
[5] Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. Technical report, Department of Computer Science, The University of Iowa (2010). www.SMT-LIB.org
[6] Barua, D., Hlavacek, W.S.: Modeling the effect of APC truncation on destruction complex function in colorectal cancer cells. PLoS Comput. Biol. 9(9), e1003217 (2013) · doi:10.1371/journal.pcbi.1003217
[7] Berdine, J., Bjørner, N.: Computing all implied equalities via SMT-based partition refinement. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 168–183. Springer, Heidelberg (2014) · Zbl 1423.68408 · doi:10.1007/978-3-319-08587-6_12
[8] Blinov, M.L., Faeder, J.R., Goldstein, B., Hlavacek, W.S.: BioNetGen: software for rule-based modeling of signal transduction based on the interactions of molecular domains. Bioinformatics 20(17), 3289–3291 (2004) · doi:10.1093/bioinformatics/bth378
[9] Bortolussi, L., De Nicola, R., Galpin, V., Gilmore, S., Hillston, J., Latella, D., Loreti, M., Massink, M.: CARMA: collective adaptive resource-sharing Markovian agents. In: QAPL, pp. 16–31 (2015) · doi:10.4204/EPTCS.194.2
[10] Bortolussi, L., Gast, N.: Scalable quantitative analysis: fluid and hybrid approximations. In: SFM (2016)
[11] Bortolussi, L., Latella, D., Massink, M.: Stochastic process algebra and stability analysis of collective systems. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 1–15. Springer, Heidelberg (2013) · Zbl 06267969 · doi:10.1007/978-3-642-38493-6_1
[12] Bortolussi, L., Le Boudec, J.Y., Latella, D., Massink, M.: Revisiting the limit behaviour of ”El Botellon”. Technical report (2012). http://infoscience.epfl.ch/record/179935/
[13] van Breugel, F., Worrell, J.: Approximating and computing behavioural distances in probabilistic transition systems. Theor. Comput. Sci. 360(1–3), 373–385 (2006) · Zbl 1097.68102 · doi:10.1016/j.tcs.2006.05.021
[14] Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. Appl. Probab. 31(1), 59–75 (1994) · Zbl 0796.60073 · doi:10.2307/3215235
[15] Camporesi, F., Feret, J.: Formal reduction for rule-based models. Electron. Notes Theoret. Comp. Sci. 276, 29–59 (2011) · Zbl 1342.68076 · doi:10.1016/j.entcs.2011.09.014
[16] Camporesi, F., Feret, J., Koeppl, H., Petrov, T.: Combining model reductions. Electron. Notes Theoret. Comp. Sci. 265, 73–96 (2010) · Zbl 1342.68077 · doi:10.1016/j.entcs.2010.08.006
[17] Cardelli, L.: Morphisms of reaction networks that couple structure to function. BMC Syst. Biol. 8(1), 84 (2014) · doi:10.1186/1752-0509-8-84
[18] Cardelli, L., Csikász-Nagy, A., Dalchau, N., Tribastone, M., Tschaikowski, M.: Noise reduction in complex biological switches. Scientific reports 6, 20214 EP (February 2016). http://dx.doi.org/10.1038/srep20214 · doi:10.1038/srep20214
[19] Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Forward and backward bisimulations for chemical reaction networks. In: CONCUR (2015) · Zbl 1374.68204
[20] Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Efficient syntax-driven lumping of differential equations. In: TACAS (2016, to appear) · Zbl 1347.68258 · doi:10.1007/978-3-662-49674-9_6
[21] Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Symbolic computation of differential equivalences. In: POPL (2016) · Zbl 1347.68258 · doi:10.1145/2837614.2837649
[22] Ciocchetta, F., Hillston, J.: Bio-PEPA: a framework for the modelling and analysis of biological systems. TCS 410(33–34), 3065–3084 (2009) · Zbl 1173.68041 · doi:10.1016/j.tcs.2009.02.037
[23] Conzelmann, H., Fey, D., Gilles, E.: Exact model reduction of combinatorial reaction networks. BMC Syst. Biol. 2(1), 78 (2008) · doi:10.1186/1752-0509-2-78
[24] Conzelmann, H., Saez-Rodriguez, J., Sauter, T., Kholodenko, B., Gilles, E.: A domain-oriented approach to the reduction of combinatorial complexity in signal transduction networks. BMC Bioinform. 7(1), 34 (2006) · doi:10.1186/1471-2105-7-34
[25] Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Abstracting the differential semantics of rule-based models: exact and automated model reduction. In: LICS, pp. 362–381 (2010)
[26] de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · Zbl 05262379 · doi:10.1007/978-3-540-78800-3_24
[27] De Nicola, R., Latella, D., Loreti, M., Massink, M.: Rate-based transition systems for stochastic process calculi. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 435–446. Springer, Heidelberg (2009) · Zbl 1248.68350 · doi:10.1007/978-3-642-02930-1_36
[28] De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A formal approach to autonomic systems programming: the SCEL language. TAAS 9(2), 7:1–7:29 (2014)
[29] Dehnert, C., Katoen, J.-P., Parker, D.: SMT-based bisimulation minimisation of Markov models. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 28–47. Springer, Heidelberg (2013) · Zbl 1426.68168 · doi:10.1007/978-3-642-35873-9_5
[30] DeMaio, P.: Bike-sharing: history, impacts, models of provision, and future. J. Publ. Transp. 14(4), 41–56 (2009) · doi:10.5038/2375-0901.12.4.3
[31] Derisavi, S., Hermanns, H., Sanders, W.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309–315 (2003) · Zbl 1189.68039 · doi:10.1016/S0020-0190(03)00343-0
[32] Feng, C., Hillston, J.: Automatic moment-closure approximation of spatially distributed collective adaptive systems. ACM Trans. Model. Comput. Simul. (to appear) · Zbl 1368.68316 · doi:10.1145/2883608
[33] Feng, C., Hillston, J.: PALOMA: a process algebra for located Markovian agents. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 265–280. Springer, Heidelberg (2014) · Zbl 06461607 · doi:10.1007/978-3-319-10696-0_22
[34] Feret, J.: Fragments-based model reduction: some case studies. Electron. Notes Theoret. Comput. Sci. 268, 77–96 (2010) · Zbl 1283.92062 · doi:10.1016/j.entcs.2010.12.007
[35] Feret, J., Danos, V., Krivine, J., Harmer, R., Fontana, W.: Internal coarse-graining of molecular systems. Proc. Nat. Acad. Sci. 106(16), 6453–6458 (2009) · doi:10.1073/pnas.0809908106
[36] Feret, J., Henzinger, T., Koeppl, H., Petrov, T.: Lumpability abstractions of rule-based systems. Theoret. Comput. Sci. 431, 137–164 (2012) · Zbl 1267.68153 · doi:10.1016/j.tcs.2011.12.059
[37] Fricker, C., Gast, N.: Incentives and redistribution in homogeneous bike-sharing systems with stations of finite capacity. EURO J. Transp. Logist. 1–31 (2014). doi: 10.1007/s13676-014-0053-5 · doi:10.1007/s13676-014-0053-5
[38] Galpin, V.: Spatial representations and analysis techniques. In: SFM (2016) · Zbl 06632412 · doi:10.1007/978-3-319-34096-8_5
[39] Gao, S., Kong, S., Clarke, E.: Satisfiability modulo ODEs. In: FMCAD, pp. 105–112 (2013)
[40] Grosu, R., Bartocci, E.: Spatio-temporal model checking. In: SFM (2016)
[41] Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI, pp. 62–73 (2011) · doi:10.1145/1993498.1993506
[42] Gupta, V., Jagadeesan, R., Panangaden, P.: Approximate reasoning for real-time probabilistic processes. Log. Methods Comput. Sci. 2(1) (2006) · Zbl 1126.68055
[43] Hayden, R.A., Bradley, J.T.: A fluid analysis framework for a Markovian process algebra. Theoret. Comput. Sci. 411(22–24), 2260–2297 (2010) · Zbl 1334.68151 · doi:10.1016/j.tcs.2010.02.001
[44] Hillston, J.: A compositional approach to performance modelling. In: CUP (1996) · Zbl 1080.68003 · doi:10.1017/CBO9780511569951
[45] Hillston, J.: Fluid flow approximation of PEPA models. In: QEST, pp. 33–43, September 2005 · doi:10.1109/QEST.2005.12
[46] Iacobelli, G., Tribastone, M.: Lumpability of fluid models with heterogeneous agent types. In: DSN, pp. 1–11 (2013) · doi:10.1109/DSN.2013.6575346
[47] Iacobelli, G., Tribastone, M., Vandin, A.: Differential bisimulation for a Markovian process algebra. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 293–306. Springer, Heidelberg (2015) · Zbl 06482743 · doi:10.1007/978-3-662-48057-1_23
[48] Iwasa, Y., Andreasen, V., Levin, S.: Aggregation in model ecosystems. I. Perfect aggregation. Ecol. Model. 37(3–4), 287–302 (1987) · Zbl 0659.92023 · doi:10.1016/0304-3800(87)90030-5
[49] Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339–354. Springer, Heidelberg (2012) · Zbl 1358.68257 · doi:10.1007/978-3-642-31365-3_27
[50] Katoen, J., Khattri, M., Zapreev, I.: A Markov reward model checker. In: QEST, pp. 243–244 (2005) · doi:10.1109/QEST.2005.2
[51] Kermack, W.O., McKendrick, A.: Contribution to the mathematical theory of epidemics. Proc. Roy. Soc. Lond. Ser. A Containing Papers Math. Phys. Charact. 115(772), 700–721 (1927) · JFM 53.0517.01 · doi:10.1098/rspa.1927.0118
[52] Kocieniewski, P., Faeder, J.R., Lipniacki, T.: The interplay of double phosphorylation and scaffolding in MAPK pathways. J. Theor. Biol. 295, 116–124 (2012) · Zbl 1336.92033 · doi:10.1016/j.jtbi.2011.11.014
[53] Köksal, A.S., Kuncak, V., Suter, P.: Constraints as control. In: POPL, pp. 151–164 (2012) · Zbl 06481244 · doi:10.1145/2103656.2103675
[54] 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) · Zbl 05940745 · doi:10.1007/978-3-642-22110-1_47
[55] Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991) · Zbl 0756.68035 · doi:10.1016/0890-5401(91)90030-6
[56] Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL, pp. 607–618 (2014) · Zbl 1284.68410 · doi:10.1145/2535838.2535857
[57] Loreti, M., Hillston, J.: Modeling and analysis of collective adaptive systems with CARMA and its tools. In: SFM (2016)
[58] Massink, M., Latella, D., Bracciali, A., Hillston, J.: Modelling non-linear crowd dynamics in Bio-PEPA. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 96–110. Springer, Heidelberg (2011) · Zbl 05905712 · doi:10.1007/978-3-642-19811-3_8
[59] Mover, S., Cimatti, A., Tiwari, A., Tonetta, S.: Time-aware relational abstractions for hybrid systems. In: EMSOFT, pp. 1–10 (2013) · doi:10.1109/EMSOFT.2013.6658592
[60] Nelson, D.L., Cox, M.M.: Lehninger Principles of Biochemistry, 6th edn. Palgrave Macmillan, Basingstoke (2013)
[61] Norris, J.: Markov Chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (1998)
[62] Okino, M.S., Mavrovouniotis, M.L.: Simplification of mathematical models of chemical reaction systems. Chem. Rev. 2(98), 391–408 (1998) · doi:10.1021/cr950223l
[63] Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987) · Zbl 0654.68072 · doi:10.1137/0216062
[64] Pappas, G.J.: Bisimilar linear systems. Automatica 39(12), 2035–2047 (2003) · Zbl 1045.93033 · doi:10.1016/j.automatica.2003.07.003
[65] Di Pierro, A., Hankin, C., Wiklicky, H.: Quantitative relations and approximate process equivalences. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 508–522. Springer, Heidelberg (2003) · Zbl 1274.68227 · doi:10.1007/978-3-540-45187-7_33
[66] Rowe, J.E., Gomez, R.: El Botellon: modeling the movement of crowds in a city. Complex Syst. 14, 363–370 (2003)
[67] Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 686–702. Springer, Heidelberg (2011) · Zbl 05940754 · doi:10.1007/978-3-642-22110-1_56
[68] Sattenspiel, L., Herring, D.A.: Simulating the effect of quarantine on the spread of the 1918–19 flu in Central Canada. Bull. Math. Biol. 65(1), 1–26. http://dx.doi.org/10.1006/bulm.2002.0317 · Zbl 1334.92427 · doi:10.1006/bulm.2002.0317
[69] van der Schaft, A.J.: Equivalence of dynamical systems by bisimulation. IEEE Trans. Autom. Control 49(12), 2160–2172 (2004) · Zbl 1365.93212 · doi:10.1109/TAC.2004.838497
[70] Sproston, J., Donatelli, S.: Backward bisimulation in Markov chain model checking. IEEE Trans. Softw. Eng. 32(8), 531–546 (2006) · Zbl 05341860 · doi:10.1109/TSE.2006.74
[71] Suderman, R., Deeds, E.J.: Machines vs. ensembles: effective MAPK signaling through heterogeneous sets of protein complexes. PLoS Comput. Biol. 9(10), e1003278 (2013) · doi:10.1371/journal.pcbi.1003278
[72] Toth, J., Li, G., Rabitz, H., Tomlin, A.S.: The effect of lumping and expanding on kinetic differential equations. SIAM J. Appl. Math. 57(6), 1531–1556 (1997) · Zbl 0891.34030 · doi:10.1137/S0036139995293294
[73] Tribastone, M., Gilmore, S., Hillston, J.: Scalable differential analysis of process algebra models. IEEE Trans. Softw. Eng. 38(1), 205–219 (2012) · doi:10.1109/TSE.2010.82
[74] Tschaikowski, M., Tribastone, M.: Exact fluid lumpability for Markovian process algebra. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 380–394. Springer, Heidelberg (2012) · Zbl 1364.68297 · doi:10.1007/978-3-642-32940-1_27
[75] Tschaikowski, M., Tribastone, M.: Approximate reduction of heterogenous nonlinear models with differential hulls. IEEE Trans. Autom. Control. (2015, to appear) · Zbl 1359.93084
[76] Tschaikowski, M., Tribastone, M.: A unified framework for differential aggregations in Markovian process algebra. J. Log. Algebraic Methods Program. 84(2), 238–258 (2015) · Zbl 1319.68151 · doi:10.1016/j.jlamp.2014.10.004
[77] Valmari, A., Franceschinis, G.: Simple O(m logn) time Markov chain lumping. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 38–52. Springer, Heidelberg (2010) · Zbl 1284.68437 · doi:10.1007/978-3-642-12002-2_4
[78] Voit, E.O.: Biochemical systems theory: a review. ISRN Biomath. 1–53 (2013). http://dx.doi.org/10.1155/2013/897658897658
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.