Definition
Timed Automata is a formalism for modelling and verification of time-critical systems. It has been proven to be a formalism that is well adapted to the expression of the timing constraints appearing in interactive scores and video games, because it is a powerful model for describing both the logical ordering of the events in such scenario and also the duration of events and the timing between them.
Introduction
As coined by Espen Aarseth in his very first editorial launching the “game studies” journal (considered as one of the core events establishing “game studies” as an academic field), games are “both object and process [which] must be played. Playing is integral, not coincidental […]. The complex nature of simulations is such that a result cannot be predicted beforehand; it can vary greatly depending on the players luck, skill and creativity.” (Aarseth 2001). Activating a video...
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Aarseth, E.: Computer game studies, year one. Game Stud. 1(1), (2001). http://gamestudies.org/0101/editorial.html
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8
Arias, J., Desainte-Catherine, M., Rueda, C.: Modelling data processing for interactive scores using coloured petri nets. In: 14th International Conference on Application of Concurrency to System Design, ACSD 2014, Tunis La Marsa, Tunisia, June 23–27, 2014, pp. 186–195. IEEE Computer Society (2014). https://doi.org/10.1109/ACSD.2014.23
Arias, J., Desainte-Catherine, M., Olarte, C., Rueda, C.: Foundations for reliable and flexible interactive multimedia scores. In: Collins, T., Meredith, D., Volk, A. (eds.) Mathematics and Computation in Music – 5th International Conference, MCM 2015, London, UK, June 22–25, 2015, Proceedings, volume 9110 of Lecture Notes in Computer Science, pp. 29–41. Springer (2015a). https://doi.org/10.1007/978-3-319-20603-5_3
Arias, J., Desainte-Catherine, M., Rueda, C.: A Framework for Composition, Verification and Real-Time Performance of Multimedia Interactive Scenarios, pp. 140–151. IEEE (2015b). https://doi.org/10.1109/ACSD.2015.8
Arias, J., Desainte-Catherine, M., Dubnov, S.: Automatic construction of interactive machine improvisation scenarios from audio recordings. In: 4th International Workshop on Musical Metacreation, MUME 2016, Paris (2016). ISBN 978-0-86491-397-5. http://musicalmetacreation.org/buddydrive/file/arias_automatic_construction/
Arias, J., Celerier, J.-M., Desainte-Catherine, M.: Authoring and automatic verification of interactive multimedia scores. J. New Music Res. 46(1), 15–33 (2017). https://doi.org/10.1080/09298215.2016.1248444
Calleja, G.: In-Game: From Immersion to Incorporation, 1st edn. The MIT Press (2011). ISBN 0262015463, 9780262015462
Celerier, J.-M., Baltazar, P., Bossut, C., Vuaille, N., Couturier, J.-M., Desainte-Catherine, M.: OSSIA: Towards a unified interface for scoring time and interaction. In: Proceedings of the First International Conference on Technologies for Music Notation and Representation, TENOR 2015, pp. 81–90, Paris (2015). ISBN 978-2-9552905-0-7. http://tenor2015.tenor-conference.org/papers/13-Celerier-OSSIA.pdf
Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8
David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT. 17(4), 397–415 (2015). https://doi.org/10.1007/s10009-014-0361-y
Desainte-Catherine, M., Allombert, A., Assayag, G.: Towards a hybrid temporal paradigm for musical composition and performance: The case of musical interpretation. Comput. Music. J. 37(2), 61–72 (2013). https://doi.org/10.1162/COMJ_a_00179
Drachen, A., Canossa, A.: Towards gameplay analysis via gameplay metrics. In: Proceedings of the 13th International MindTrek Conference: Everyday Life in the Ubiquitous Era, MindTrek ’09, pp. 202–209. ACM. ISBN 978-1-60558-633-5, New York (2009). https://doi.org/10.1145/1621841.1621878
Dulaurans, M., Marczak, R.: Quand le jeu vido devient affaire de clan: un clash royale entre incitation et inhibition. Revue Franaise des Sciences de l’Information et de la Communication. 13, (2018). https://journals.openedition.org/rfsic/3610
Echeveste, J., Cont, A., Giavitto, J.-L., Jacquemard, F.: Operational semantics of a domain specific language for real time musiciancomputer interaction. Discrete Event Dyn. Syst. 23(4), 343–383 (2013). https://doi.org/10.1007/s10626-013-0166-2
Fahrenberg, U., Larsen, K.G., Thrane, C.R.: Verification, performance analysis and controller synthesis for real-time systems. In: Fundamentals of Software Engineering, vol. 5961, pp. 34–61. Springer, Berlin/Heidelberg (2010). https://doi.org/10.1007/978-3-642-11623-02
Jacquemard, F., Poncelet, C.: An automatic test framework for interactive music systems. J. New Music Res. 45(2), 87–100 (2016). https://doi.org/10.1080/09298215.2016.1173707
Marczak R.: Feedback-Based Gameplay Metrics and Gameplay Performance Segmentation: An audio-visual approach for assessing player experience. PhD thesis, University of Waikato, Faculty of Arts and Social Sciences, 2014
Marczak, R., Schott, G., Hanna, P.: Postprocessing gameplay metrics for gameplay performance segmentation based on audiovisual analysis. IEEE Trans. Comput. Intell. AI Games. 7(3), 279–291 (2015). https://doi.org/10.1109/TCIAIG.2014.2382718
Olarte, C., Rueda, C.: A declarative language for dynamic multimedia interaction systems. In: Chew, E., Childs, A., Chuan, C.-H. (eds.) Mathematics and Computation in Music, pp. 218–227. Springer, Berlin/Heidelberg (2009). ISBN 978-3-642-02394-1
Sanchez, C.P., Jacquemard, F.: Model-based testing for building reliable realtime interactive music systems. Sci. Comput. Program. 132, 143–172 (2016). https://doi.org/10.1016/j.scico.2016.08.002
Toro, M., Desainte-Catherine, M., Rueda, C.: Formal semantics for interactive music scores: a framework to design, specify properties and execute interactive scenarios. J. Math. Music. 8(1), 93–112 (2014). https://doi.org/10.1080/17459737.2013.870610
Wang, C.-i., Dubnov, S.: The variable markov oracle: Algorithms for human gesture applications. IEEE MultiMedia. 22(4), 52–67 (2015). https://doi.org/10.1109/MMUL.2015.76
Wang, G., Cook, P.R., Salazar, S.: Chuc K: A strongly timed computer music language. Comput. Music. J. 39(4), 10–29 (2015). https://doi.org/10.1162/COMJa00324
Zagal, J., Mateas, M., Fernandez-Vara, C., Hochhalter, B., Lichti, N.: Towards an ontological language for game analysis. In: DiGRA ’05 – Proceedings of the 2005 DiGRA International Conference: Changing Views: Worlds in Play, Vancouver (2005). http://www.digra.org/digital-library/publications/towards-an-ontological-language-for-game-analysis/?doing_wp_cron=1531064778.6737051010131835937500
Zagal, J., Fernandez-Vara, C., Mateas, M.: Rounds, levels, and waves: The early evolution of gameplay segmentation. Games Cult. 3(2), 175–198 (2008). https://doi.org/10.1177/1555412008314129
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 Springer Nature Switzerland AG
About this entry
Cite this entry
Arias, J., Marczak, R., Desainte-Catherine, M. (2024). Timed Automata for Video Games and Interaction. In: Lee, N. (eds) Encyclopedia of Computer Graphics and Games. Springer, Cham. https://doi.org/10.1007/978-3-031-23161-2_298
Download citation
DOI: https://doi.org/10.1007/978-3-031-23161-2_298
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-23159-9
Online ISBN: 978-3-031-23161-2
eBook Packages: Computer ScienceReference Module Computer Science and Engineering