[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Emerging Synchrony in Applauding Audiences: Formal Analysis and Specification

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola (ISoLA 2024)

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

Included in the following conference series:

  • 168 Accesses

Abstract

Applause is an ancient, widespread collective behaviour by which an audience expresses appreciation at the conclusion of a collective event such as an artistic performance or a public ceremony. In some cultures, it is possible to observe a spontaneous transition from an initially incoherent to a surprisingly synchronised form of applause. Such kind of emergent behaviour has long since fascinated researchers from different disciplines. This paper shows a possible application of formal methods to study similar phenomena. The key idea is to model the audience as a concurrent system, where each person is a separate process that follows the same, simple behaviour. The model can then be automatically analysed to study the possible evolutions of the system as a whole, and in particular to assess the likelihood of emerging synchronisation.

This work is dedicated to Rocco De Nicola on the occasion of his 70th birthday. Luca is very thankful for having been supervised by Rocco during his doctoral studies and for the enduring collaboration. Omar would like to express his gratitude to Rocco for the opportunities of joint work (including Luca’s supervision) and the precious advice. Rocco’s work and vision are a continuing source of inspiration for both authors.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Similar content being viewed by others

Notes

  1. 1.

    Throughout the paper, \(\div \) denotes integer division with rounding.

  2. 2.

    https://github.com/labs-lang/sliver.

  3. 3.

    https://doi.org/10.5281/zenodo.11374365.

References

  1. Abd Alrahman, Y., Azzopardi, S., Di Stefano, L., Piterman, N.: Language support for verifying reconfigurable interacting systems. Int. J. Softw. Tools Technol. Transfer 25(5), 765–784 (2023). https://doi.org/10/gs4rg6

  2. Abd Alrahman, Y., De Nicola, R., Loreti, M.: Programming interactions in collective adaptive systems by relying on attribute-based communication. Sci. Comput. Program. 192, 102428 (2020). https://doi.org/10.1016/j.scico.2020.102428

  3. Abd Alrahman, Y., De Nicola, R., Loreti, M., Tiezzi, F., Vigo, R.: A calculus for attribute-based communication. In: SAC. ACM (2015). https://doi.org/gf4vn6

  4. Bartocci, E., Liò, P.: Computational modeling, formal analysis, and tools for systems biology. PLoS Comput. Biol. 12, e1004591 (2016). https://doi.org/10/f8knqc

  5. Bergstra, J.A., Klop, J.W., Tucker, J.V.: Algebraic tools for system construction. In: Clarke, E., Kozen, D. (eds.) Workshop on Logics of Programs. LNCS, vol. 164. Springer, Cham (1983). https://doi.org/10.1007/3-540-12896-4_353

  6. Boemo, M.A., Cardelli, L., Nieduszynski, C.A.: The Beacon Calculus: a formal method for the flexible and concise modelling of biological systems. PLOS Comput. Biol. 16, e1007651 (2020). https://doi.org/10.1371/journal.pcbi.1007651

  7. Cavada, R., et al.: The NUXMV symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22

  8. Chopard, B., Droz, M.: Cellular Automata Modeling of Physical Systems. Cambridge University Press, Cambridge (1998). https://doi.org/10.1017/CBO9780511549755

  9. Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS. LNCS, vol. 2988, pp. 168–176. Springer, Cham (2004). https://doi.org/10/cfm9ks

  10. Crawley, A.: Clap, clap, clap - unsystematic review essay on clapping and applause. Integr. Psychol. Behav. Sci. 57, 1354–1382 (2023). https://doi.org/10/gt5mb5

  11. De Nicola, R.: A gentle introduction to Process Algebras. IMT School for Advanced Studies, Lucca, Italy (2011). https://doi.org/10.5281/zenodo.11065174

  12. De Nicola, R., Di Stefano, L., Inverso, O.: Multi-agent systems with virtual stigmergy. Sci. Comput. Program. 187, 102345 (2020). https://doi.org/10/h3kv

  13. De Nicola, R., Di Stefano, L., Inverso, O., Valiani, S.: Intuitive modelling and formal analysis of collective behaviour in foraging ants. In: Pang, J., Niehren, J. (eds.) CMSB. LNCS, vol. 14137, pp. 44–61. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-42697-1_4

  14. De Nicola, R., Di Stefano, L., Inverso, O., Valiani, S.: Modelling flocks of birds and colonies of ants from the bottom up. Int. J. Softw. Tools Technol. Transf. 25, 675–691 (2023). https://doi.org/10.1007/s10009-023-00731-0

  15. De Nicola, R., Duong, T., Inverso, O., Trubiani, C.: AErlang: empowering Erlang with attribute-based communication. Sci. Comput. Program. 168, 71–93 (2018). https://doi.org/10.1016/j.scico.2018.08.006

  16. De Nicola, R., Duong, T., Loreti, M.: ABEL - a domain specific framework for programming with attribute-based communication. In: Riis Nielson, H., Tuosto, E. (eds.) COORDINATION. LNCS, vol. 11533, pp. 111–128. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-22397-7_7

  17. De Nicola, R., Ferrari, G.L., Pugliese, R.: KLAIM: a kernel language for agents interaction and mobility. IEEE Trans. Softw. Eng. 24, 315–330 (1998). https://doi.org/10.1109/32.685256

  18. De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A formal approach to autonomic systems programming: the SCEL language. ACM Trans. Auton. Adapt. Syst. 9, 1–29 (2014). https://doi.org/10.1145/2619998

  19. Di Stefano, L., De Nicola, R., Inverso, O.: Verification of distributed systems via sequential emulation. ACM Trans. Softw. Eng. Methodol. 31, 1–41 (2022). https://doi.org/10.1145/3490387

  20. Di Stefano, L., Lang, F.: Verifying temporal properties of stigmergic collective systems using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA. LNCS, vol. 13036, pp. 473–489. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-89159-6_29

  21. Di Stefano, L., Lang, F.: Compositional verification of stigmergic collective systems. In: Dragoi, C., Emmi, M., Wang, J. (eds.) VMCAI. LNCS, vol. 13881, pp. 155–176. Springer, Cham (2023). https://doi.org/10/jxwd, https://doi.org/10.1007/978-3-031-24950-1_8

  22. Fleury, M., Biere, A.: Mining definitions in Kissat with Kittens. Form. Methods Syst. Des. 60, 381–404 (2022). https://doi.org/10.1007/s10703-023-00421-2

  23. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985). http://www.usingcsp.com/cspbook.pdf

  24. Horni, A., Montini, L.: A glimpse at emergence in agent-based simulations. In: STRC. ETH Zürich (2013). https://doi.org/10/m94g

  25. Kauffman, S.: Homeostasis and differentiation in random genetic control networks. Nature 224(5215), 177–178 (1969). https://doi.org/10.1038/224177a0

  26. Kermack, W.O., McKendrick, A.G.: Contributions to the mathematical theory of epidemics–I. Bull. Math. Biol. 53, 33–55 (1991). https://doi.org/10.1007/BF02464423, reprinted from Proc. R. Soc. A 115 (1927)

  27. Kuramoto, Y., Nishikawa, I.: Statistical macrodynamics of large dynamical systems. Case of a phase transition in oscillator communities. J. Stat. Phys. 49, 569–605 (1987). https://doi.org/10.1007/BF01009349

  28. Li, D., Liu, K., Sun, Y., Han, M.: Emerging clapping synchronization from a complex multiagent network with local information via local control. IEEE Trans. Circ. Syst. II Express Briefs 56-II, 504–508 (2009). https://doi.org/10.1109/TCSII.2009.2020931

  29. Mann, R.P., Faria, J., Sumpter, D.J.T., Krause, J.: The dynamics of audience applause. J. R. Soc. Interface 10, 20130466 (2013). https://doi.org/10/f2zmr6

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

  31. Milner, R.: Elements of interaction - turing award lecture. Commun. ACM 36, 78–89 (1993). https://doi.org/10.1145/151233.151240

  32. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inf. Comput. 100, 1–40 (1992). https://doi.org/10.1016/0890-5401(92)90008-4

  33. Néda, Z., Ravasz, E., Brechet, Y., Vicsek, T., Barabási, A.L.: The sound of many hands clapping. Nature 403, 849–850 (2000). https://doi.org/10.1038/35002660

  34. Néda, Z., Ravasz, E., Vicsek, T., Brechet, Y., Barabási, A.L.: Physics of the rhythmic applause. Phys. Rev. E 61, 6987–6992 (2000). https://doi.org/10.1103/PhysRevE.61.6987

  35. Pnueli, A.: The temporal logic of programs. In: 18th Symposium on Foundations of Computer Science (FOCS), pp. 46–57. IEEE (1977). https://doi.org/10/dn8cpn

  36. Sumpter, D.J., Blanchard, G.B., Broomhead, D.S.: Ants and agents: a process algebra approach to modelling ant colony behaviour. Bull. Math. Biol. 63, 951–980 (2001). https://doi.org/10.1006/bulm.2001.0252

  37. Thomson, M., Murphy, K., Lukeman, R.: Groups clapping in unison undergo size-dependent error-induced frequency increase. Sci. Rep. 8, 808 (2018). https://doi.org/10.1038/s41598-017-18539-9

  38. Tofts, C.M.N.: Describing social insect behaviour using process algebra. Trans. Soc. Comput. Simul. 9, 227 (1992)

    Google Scholar 

  39. Winfree, A.T.: Biological rhythms and the behavior of populations of coupled oscillators. J. Theoret. Biol. 16, 15–42 (1967). https://doi.org/10/bhr4xf

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Engineering, TU Wien, Treitlstraße 3, 1040, Vienna, Austria

    Luca Di Stefano

  2. Gran Sasso Science Institute (GSSI), L’Aquila, Italy

    Omar Inverso

Authors
  1. Luca Di Stefano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Omar Inverso
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luca Di Stefano .

Editor information

Editors and Affiliations

  1. University of Limerick, CSIS and Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund University, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Di Stefano, L., Inverso, O. (2025). Emerging Synchrony in Applauding Audiences: Formal Analysis and Specification. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola. ISoLA 2024. Lecture Notes in Computer Science, vol 15219. Springer, Cham. https://doi.org/10.1007/978-3-031-73709-1_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-73709-1_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-73708-4

  • Online ISBN: 978-3-031-73709-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation