Skip to main content

Distributed Adaptive Systems

Theory, Specification, Reasoning

  • Conference paper
  • First Online:
Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10817))

Abstract

A distributed system can be characterised by autonomously acting agents, where each agent executes its own program, uses shared resources and communicates with the others, but otherwise is totally oblivious to the behaviour of the other agents. In a distributed adaptive system agents may change their programs, and enter or leave the collection at any time thereby changing the behaviour of the overall system. This article first develops a language-independent axiomatic definition of distributed adaptive systems and then presents concurrent reflective Abstract State Machines (crASMs), an abstract machine model for their specification. It can be proven that any distributed adaptive system as stipulated by the axiomatisation can be step-by-step simulated by a crASM. Proofs about crASMs can be grounded in a multiple-step logic, which extends known complete one-step logics for deterministic and non-deterministic ASMs.

The research reported in this paper was partially supported by the Austrian Science Fund (FWF)[I2420-N31] for the project: Higher-Order Logics and Structures.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

References

  1. Blass, A., Gurevich, Y.: Abstract State Machines capture parallel algorithms. ACM Trans. Comput. Log. 4(4), 578–651 (2003)

    Article  MathSciNet  Google Scholar 

  2. Blass, A., Gurevich, Y.: Abstract State Machines capture parallel algorithms: correction and extension. ACM Trans. Comput. Log. 9(3), 19:1–19:32 (2008)

    MathSciNet  MATH  Google Scholar 

  3. Blass, A., Gurevich, Y.: Background of computation. Bull. EATCS 92, 82–114 (2007)

    MathSciNet  MATH  Google Scholar 

  4. Börger, E., Schewe, K.D.: Concurrent Abstract State Machines. Acta Informatica 53(5), 469–492 (2016)

    Article  MathSciNet  Google Scholar 

  5. Börger, E.: The ASM refinement method. Formal Asp. Comp. 15(2–3), 237–257 (2003)

    Article  Google Scholar 

  6. Börger, E., Schewe, K.D.: Communication in Abstract State Machines. J. Univ. Comp. Sci. 23(2), 129–145 (2017)

    MathSciNet  Google Scholar 

  7. Börger, E., Stärk, R.: Abstract State Machines. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-642-18216-7

    Book  MATH  Google Scholar 

  8. Ferrarotti, F., Schewe, K.D., Tec, L., Wang, Q.: A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis. Theor. Comput. Sci. 649, 25–53 (2016)

    Article  MathSciNet  Google Scholar 

  9. Ferrarotti, F., Schewe, K.-D., Tec, L.: A behavioural theory for reflective sequential algorithms. In: Petrenko, A.K., Voronkov, A. (eds.) PSI 2017. LNCS, vol. 10742, pp. 117–131. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74313-4_10

    Chapter  Google Scholar 

  10. Ferrarotti, F., Schewe, K.D., Tec, L., Wang, Q.: A complete logic for database Abstract State Machines. Log. J. IGPL 25(5), 700–740 (2017)

    Google Scholar 

  11. Ferrarotti, F., Schewe, K.D., Tec, L., Wang, Q.: A unifying logic for non-deterministic, parallel and concurrent Abstract State Machines. Ann. Math. Artif. Intell. (2018, to appear)

    Google Scholar 

  12. Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Specification and Validation Methods, pp. 9–36. Oxford University Press (1995)

    Google Scholar 

  13. Gurevich, Y.: Sequential Abstract State Machines capture sequential algorithms. ACM Trans. Comput. Log. 1(1), 77–111 (2000)

    Article  MathSciNet  Google Scholar 

  14. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  15. Hewitt, C.: What is computation? Actor model versus Turing’s model. In: Zenil, H. (ed.) A Computable Universe: Understanding Computation and Exploring Nature as Computation. World Scientific Publishing, Singapore (2012)

    Google Scholar 

  16. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  17. Kröger, F., Merz, S.: Temporal Logic and State Systems. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68635-4

    Book  MATH  Google Scholar 

  18. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)

    Article  Google Scholar 

  19. Lynch, N.: Distributed Algorithms. Morgan Kaufmann, Burlington (1996)

    MATH  Google Scholar 

  20. Mazurkiewicz, A.: Introduction to trace theory. In: Diekert, V., Rozenberg, G. (eds.) The Book of Traces, pp. 3–67. World Scientific, Singapore (1995)

    Chapter  Google Scholar 

  21. Merz, S.: On the logic of TLA\(^+\). Comput. Artif. Intell. 22(3–4), 351–379 (2003)

    MathSciNet  MATH  Google Scholar 

  22. Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10235-3

    Book  MATH  Google Scholar 

  23. Milner, R.: Communicating and Mobile Systems – The Pi-Calculus. Cambridge University Press (1999). ISBN 978-0-521-65869-0

    Google Scholar 

  24. Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice-Hall, Upper Saddle River (1981)

    MATH  Google Scholar 

  25. Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Institut für Instrumentelle Mathematik der Universität Bonn (1962). schriften des IIM Nr. 2

    Google Scholar 

  26. Riccobene, E., Scandurra, P.: Towards ASM-based formal specification of self-adaptive systems. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 204–209. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43652-3_17

    Chapter  Google Scholar 

  27. Roscoe, A.: The Theory and Practice of Concurrency. Prentice-Hall, Upper Saddle River (1997)

    Google Scholar 

  28. Schellhorn, G., Tofan, B., Ernst, G., Pfähler, J., Reif, W.: RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. 71, 1–44 (2014)

    Article  MathSciNet  Google Scholar 

  29. Schewe, K.D., Wang, Q.: A customised ASM thesis for database transformations. Acta Cybern. 19(4), 765–805 (2010)

    MathSciNet  MATH  Google Scholar 

  30. Schewe, K.D., Wang, Q.: Partial updates in complex-value databases. In: Heimbürger, A., et al. (eds.) Information and Knowledge Bases XXII, Frontiers in Artificial Intelligence and Applications, vol. 225, pp. 37–56. IOS Press (2011)

    Google Scholar 

  31. Schewe, K.D.: Concurrent reflective Abstract State Machines. In: Jebelean, T., et al. (eds.) 19th Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017). IEEE (2018, to appear)

    Google Scholar 

  32. Schewe, K.D., Ferrarotti, F., Tec, L., Wang, Q.: Towards a behavioural theory for random parallel computing. In: Beierle, C., Brewka, G., Thimm, M. (eds.) Computational Models of Rationality - Essays Dedicated to Gabriele Kern-Isberner on the Occasion of Her 60th Birthday, Tributes, vol. 29, pp. 365–373. College Publications (2016)

    Google Scholar 

  33. Schewe, K.D., Ferrarotti, F., Tec, L., Wang, Q., An, W.: Evolving concurrent systems: behavioural theory and logic. In: Proceedings of the Australasian Computer Science Week Multiconference, (ACSW 2017), pp. 77:1–77:10. ACM (2017)

    Google Scholar 

  34. Schewe, K.D., Wang, Q.: XML database transformations. J. UCS 16(20), 3043–3072 (2010)

    MATH  Google Scholar 

  35. Schmalz, M.: Formalizing the Logic of Event-B. Ph.D. thesis, ETH Zürich (2012)

    Google Scholar 

  36. Seebach, H., Nafz, F., Steghöfer, J.P., Reif, W.: How to design and implement self-organising resource-flow systems. In: Müller-Schloer, C., Schmeck, H., Ungerer, T. (eds.) Organic Computing - A Paradigm Shift for Complex Systems. ASYS, vol. 1, pp. 145–161. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-0348-0130-0_9

    Chapter  Google Scholar 

  37. Stärk, R.F., Nanchen, S.: A logic for Abstract State Machines. J. Univ. Comput. Sci. 7(11), 980–1005 (2001)

    MathSciNet  MATH  Google Scholar 

  38. Steghöfer, J.P.: Large-scale open self-organising systems: managing complexity with hierarchies, monitoring, adaptation, and principled design. Ph.D. thesis, University of Augsburg (2014)

    Google Scholar 

  39. Steghöfer, J.P., et al.: Combining PosoMAS method content with Scrum: agile software engineering for open self-organising systems. Scalable Comput.: Pract. Exp. 16(4), 333–354 (2015)

    Google Scholar 

  40. The Petri nets bibliography, University of Hamburg. http://www.informatik.uni-hamburg.de/TGI/pnbib/index.html

  41. Winskel, G., Nielsen, M.: Models for concurrency. In: Abramsky, S., Gabbay, D., Maibaum, T.S.E. (eds.) Handbook of Logic and the Foundations of Computer Science: Semantic Modelling, vol. 4, pp. 1–148. Oxford University Press, Oxford (1995)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Klaus-Dieter Schewe .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Schewe, KD., Ferrarotti, F., Tec, L., Wang, Q. (2018). Distributed Adaptive Systems. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-91271-4_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-91270-7

  • Online ISBN: 978-3-319-91271-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics