nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

How Adaptive and Reliable is Your Program?

verfasst von : Valentina Castiglioni, Michele Loreti, Simone Tini

Erschienen in: Formal Techniques for Distributed Objects, Components, and Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We consider the problem of modelling and verifying the behaviour of systems characterised by a close interaction of a program with the environment. We propose to model the program-environment interplay in terms of the probabilistic modifications they induce on a set of application-relevant data, called data space. The behaviour of a system is thus identified with the probabilistic evolution of the initial data space. Then, we introduce a metric, called evolution metric, measuring the differences in the evolution sequences of systems and that can be used for system verification as it allows for expressing how well the program is fulfilling its tasks. We use the metric to express the properties of adaptability and reliability of a program, which allow us to identify potential critical issues of it w.r.t. changes in the initial environmental conditions. We also propose an algorithm, based on statistical inference, for the evaluation of the evolution metric.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Formalisation of SysML State Machines in mCRL2

Nächstes Kapitel Branching Place Bisimilarity: A Decidable Behavioral Equivalence for Finite Petri Nets with Silent Moves

Abate, A., D’Innocenzo, A., Benedetto, M.D.D.: Approximate abstractions of stochastic hybrid systems. IEEE Trans. Automat. Contr. 56(11), 2688–2694 (2011)MathSciNetCrossRef

Abate, A., Katoen, J., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control. 16(6), 624–641 (2010)MathSciNetCrossRef

Abate, A., Prandini, M.: Approximate abstractions of stochastic systems: a randomized method. In: Proceedings of CDC-ECC 2011, pp. 4861–4866 (2011)

Arjovsky, M., Chintala, S., Bottou, L.: Wasserstein generative adversarial networks. In: Proceedings of ICML 2017, pp. 214–223 (2017)

Bernardo, M., Nicola, R.D., Loreti, M.: A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences. Inf. Comput. 225, 29–82 (2013)MathSciNetCrossRef

Bloom, H.A.P., Lygeros, J. (eds.): Stochastic Hybrid Systems: Theory and Safety Critical Applications. Lecture Notes in Control and Information Sciences, vol. 337. Springer, Heidelberg (2006). https://doi.org/10.1007/11587392CrossRef

Breugel, F.: A behavioural pseudometric for metric labelled transition systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 141–155. Springer, Heidelberg (2005). https://doi.org/10.1007/11539452_14CrossRef

Cassandras, C.G., Lygeros, J. (eds.): Stochastic Hybrid Systems. Control Engineering, vol. 24, 1st edn. CRC Press, Boca Raton (2007)MATH

Castiglioni, V., Chatzikokolakis, K., Palamidessi, C.: A logical characterization of differential privacy via behavioral metrics. In: Bae, K., Ölveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 75–96. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02146-7_4CrossRef

10.

Castiglioni, V., Chatzikokolakis, K., Palamidessi, C.: A logical characterization of differential privacy. Sci. Comput. Program. 188, 102388 (2020)CrossRef

11.

Castiglioni, V., Loreti, M., Tini, S.: Measuring adaptability and reliability of large scale systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12477, pp. 380–396. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-61470-6_23CrossRef

12.

Castiglioni, V., Loreti, M., Tini, S.: The metric linear-time branching-time spectrum on nondeterministic probabilistic processes. Theor. Comput. Sci. 813, 20–69 (2020)MathSciNetCrossRef

13.

Castro, P.F., D’Argenio, P.R., Demasi, R., Putruele, L.: Measuring masking fault-tolerance. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019, Part II. LNCS, vol. 11428, pp. 375–392. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_21CrossRef

14.

Cerný, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. Theor. Comput. Sci. 413(1), 21–35 (2012)MathSciNetCrossRef

15.

Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized bisimulation metrics. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 32–46. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44584-6_4CrossRef

16.

Ciocchetta, F., Hillston, J.: Bio-PEPA: an extension of the process algebra PEPA for biochemical networks. Electron. Notes Theor. Comput. Sci. 194(3), 103–117 (2008)CrossRef

17.

Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)MathSciNetCrossRef

18.

Deshmukh, J.V., Majumdar, R., Prabhu, V.S.: Quantifying conformance using the skorokhod metric. Formal Methods Syst. Design 50(2–3), 168–206 (2017)CrossRef

19.

Faugeras, O.P., Rüschendorf, L.: Risk excess measures induced by hemi-metrics. Probab. Uncertain. Quant. Risk 3(1), 1–35 (2018). https://doi.org/10.1186/s41546-018-0032-0MathSciNetCrossRefMATH

20.

Gebler, D., Larsen, K.G., Tini, S.: Compositional bisimulation metric reasoning with probabilistic process calculi. Log. Methods Comput. Sci. 12(4) (2016)

21.

Ghosh, S., Bansal, S., Sangiovanni-Vincentelli, A.L., Seshia, S.A., Tomlin, C.: A new simulation metric to determine safe environments and controllers for systems with unknown dynamics. In: Proceedings of HSCC 2019, pp. 185–196 (2019)

22.

Giacalone, A., Jou, C.C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of IFIP Work, Conference on Programming, Concepts and Methods, pp. 443–458 (1990)

23.

Girard, A., Gößler, G., Mouelhi, S.: Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models. IEEE Trans. Automat. Contr. 61(6), 1537–1549 (2016)MathSciNetCrossRef

24.

van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121(1), 59–80 (1995)MathSciNetCrossRef

25.

Gulrajani, I., Ahmed, F., Arjovsky, M., Dumoulin, V., Courville, A.C.: Improved training of Wasserstein GANs. In: Proceedings of Advances in Neural Information Processing Systems, pp. 5767–5777 (2017)

26.

Heredia, G., et al.: Control of a multirotor outdoor aerial manipulator. In: Proceedings of IROS 2014, pp. 3417–3422. IEEE (2014)

27.

Hillston, J., Hermanns, H., Herzog, U., Mertsiotakis, V., Rettelbach, M.: Stochastic process algebras: integrating qualitative and quantitative modelling. In: Proceedings of International Conference on Formal Description Techniques 1994. IFIP, vol. 6, pp. 449–451 (1994)

28.

Hu, J., Lygeros, J., Sastry, S.: Towards a theory of stochastic hybrid systems. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 160–173. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46430-1_16CrossRefMATH

29.

Kwiatkowska, M., Norman, G.: Probabilistic metric semantics for a simple language with recursion. In: Penczek, W., Szałas, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 419–430. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61550-4_167CrossRef

30.

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12CrossRefMATH

31.

Malhame, R., Yee Chong, C.: Electric load model synthesis by diffusion approximation of a high-order hybrid-state stochastic system. IEEE Trans. Automat. Contr. 30(9), 854–660 (1985)CrossRef

32.

Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, USA (2005)MATH

33.

Rachev, S.T., Klebanov, L.B., Stoyanov, S.V., Fabozzi, F.J.: The Methods of Distances in the Theory of Probability and Statistics. Springer, Heidelberg (2013). https://doi.org/10.1007/978-1-4614-4869-3CrossRefMATH

34.

Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA, USA (1995)

35.

Skorokhod, A.V.: Limit theorems for stochastic processes. Theory Probab. Appl. 1, 261–290 (1956)MathSciNetCrossRef

36.

Sriperumbudur, B.K., Fukumizu, K., Gretton, A., Schölkopf, B., Lanckriet, G.R.G.: On the empirical estimation of integral probability metrics. Electron. J. Stat. 6, 1550–1599 (2021)MathSciNetMATH

37.

Thorsley, D., Klavins, E.: Approximating stochastic biochemical processes with Wasserstein pseudometrics. IET Syst. Biol. 4(3), 193–211 (2010)CrossRef

38.

Tolstikhin, I.O., Bousquet, O., Gelly, S., Schölkopf, B.: Wasserstein auto-encoders. In: Proceedings of ICLR 2018 (2018)

39.

Vaserstein, L.N.: Markovian processes on countable space product describing large systems of automata. Probl. Peredachi Inf. 5(3), 64–72 (1969)MATH

40.

Villani, C.: Optimal Transport: Old and New, vol. 338. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71050-9CrossRefMATH

41.

Virágh, C., Nagy, M., Gershenson, C., Vásárhelyi, G.: Self-organized UAV traffic in realistic environments. In: Proceedings of IROS 2016, pp. 1645–1652. IEEE (2016)

Titel: How Adaptive and Reliable is Your Program?
verfasst von: Valentina Castiglioni
Michele Loreti
Simone Tini
Verlag: Springer International Publishing
Buch: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-78088-3

Electronic ISBN: 978-3-030-78089-0

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-78089-0_4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"