Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
Special Issue on Distributed Hybrid Systems

Higher-Dimensional Timed and Hybrid Automata

PDF
  • Uli Fahrenberg
Uli Fahrenberg
EPITA Research and Development Laboratory (LRDE), France
DOI: https://doi.org/10.4230/LITES.8.2.3

Published 2022-12-07

Keywords

  • timed automaton,
  • higher-dimensional automaton,
  • precubical set,
  • real time,
  • non-interleaving concurrency,
  • hybrid automaton
    • ...More
    Less

How to Cite

[1]
Fahrenberg, U. 2022. Higher-Dimensional Timed and Hybrid Automata. Leibniz Transactions on Embedded Systems. 8, 2 (Dec. 2022), 03:1–03:16. DOI:https://doi.org/10.4230/LITES.8.2.3.

Copyright (c) 2022 Uli Fahrenberg

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Abstract

We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek’s higher-dimensional automata and Alur and Dill’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata.
The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.

PDF

References

  1. Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, and Jiří Srba. Reactive Systems. Cambridge University Press, 2007.
  2. Luca Aceto and François Laroussinie. Is your model checker on time? On the complexity of model checking for timed modal logics. Journal of Logic and Algebraic Methods in Programming, 52-53:7-51, 2002.
  3. Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3-34, 1995.
  4. Rajeev Alur and David L. Dill. Automata for modeling real-time systems. In Mike Paterson, editor, ICALP, volume 443 of Lecture Notes in Computer Science, pages 322-335. Springer, 1990.
  5. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
  6. Youssef Arbach, David Karcher, Kirstin Peters, and Uwe Nestmann. Dynamic causality in event structures. In Susanne Graf and Mahesh Viswanathan, editors, FORTE, volume 9039 of Lecture Notes in Computer Science, pages 83-97. Springer, 2015.
  7. Tuomas Aura and Johan Lilius. Time processes for time Petri-nets. In Pierre Azéma and Gianfranco Balbo, editors, ICATPN, volume 1248 of Lecture Notes in Computer Science, pages 136-155. Springer, 1997.
  8. Marek A. Bednarczyk. Categories of asynchronous systems. PhD thesis, University of Sussex, UK, 1987.
  9. Gerd Behrmann, Alexandre David, and Kim Guldstrand Larsen. A tutorial on uppaal. In Marco Bernardo and Flavio Corradini, editors, SFM-RT, volume 3185 of Lecture Notes in Computer Science, pages 200-236. Springer, 2004.
  10. Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In Lectures on Concurrency and Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 87-124. Springer, 2003.
  11. Béatrice Bérard, Antoine Petit, Volker Diekert, and Paul Gastin. Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae, 36(2-3):145-182, 1998.
  12. Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, Joël Ouaknine, and James Worrell. Model checking real-time systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking., pages 1001-1046. Springer, 2018.
  13. Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. Kronos: A model-checking tool for real-time systems. In Alan J. Hu and Moshe Y. Vardi, editors, CAV, volume 1427 of Lecture Notes in Computer Science, pages 546-550. Springer, 1998.
  14. Luca Cardelli. Real time agents. In Mogens Nielsen and Erik Meineche Schmidt, editors, ICALP, volume 140 of Lecture Notes in Computer Science, pages 94-106. Springer, 1982.
  15. Franck Cassez, Thomas Chatain, and Claude Jard. Symbolic unfoldings for networks of timed automata. In Susanne Graf and Wenhui Zhang, editors, ATVA, volume 4218 of Lecture Notes in Computer Science, pages 307-321. Springer, 2006.
  16. Giovanni Casu and G. Michele Pinna. Petri nets and dynamic causality for service-oriented computations. In Ahmed Seffah, Birgit Penzenstadler, Carina Alves, and Xin Peng, editors, SAC, pages 1326-1333. ACM, 2017.
  17. Thomas Chatain and Claude Jard. Complete finite prefixes of symbolic unfoldings of safe time Petri nets. In Susanna Donatelli and P. S. Thiagarajan, editors, ICATPN, volume 4024 of Lecture Notes in Computer Science, pages 125-145. Springer, 2006.
  18. Thomas Chatain and Claude Jard. Back in time Petri nets. In Víctor A. Braberman and Laurent Fribourg, editors, FORMATS, volume 8053 of Lecture Notes in Computer Science, pages 91-105. Springer, 2013.
  19. Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Louis-Marie Traonouez, and Andrzej Wasowski. Real-time specifications. Int. J. Software Tools for Technology Transfer, 17(1):17-45, 2015.
  20. Jérémy Dubut. Trees in partial higher dimensional automata. In Mikołaj Bojańczyk and Alex Simpson, editors, FOSSACS, volume 11425 of Lecture Notes in Computer Science, pages 224-241. Springer, 2019.
  21. Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata, and David Sprunger. Quantitative bisimulations using coreflections and open morphisms. CoRR, abs/1809.09278, 2018.
  22. Javier Esparza. A false history of true concurrency: From Petri to tools (invited talk). In Jaco van de Pol and Michael Weber, editors, SPIN, volume 6349 of Lecture Notes in Computer Science, pages 180-186. Springer, 2010.
  23. Javier Esparza and Keijo Heljanko. Unfoldings - A Partial-Order Approach to Model Checking. Monographs Theor. Comput. Sci. Springer, 2008.
  24. Uli Fahrenberg. A category of higher-dimensional automata. In Vladimiro Sassone, editor, FoSSaCS, volume 3441 of Lecture Notes in Computer Science, pages 187-201. Springer, 2005.
  25. Uli Fahrenberg. Higher-Dimensional Automata from a Topological Viewpoint. PhD thesis, Aalborg University, Denmark, 2005.
  26. Uli Fahrenberg. How to pull back open maps along semantics functors. In Jochen Pfalzgraf, editor, ACCAT, 2008.
  27. Uli Fahrenberg. Higher-dimensional timed automata. In Alessandro Abate, Antoine Girard, and Maurice Heemels, editors, ADHS, volume 51 of IFAC-PapersOnLine, pages 109-114. Elsevier, 2018.
  28. Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemiański. Languages of higher-dimensional automata. Mathematical Structures in Computer Science, pages 1-39, 2021.
  29. Uli Fahrenberg and Axel Legay. Partial higher-dimensional automata. In Lawrence S. Moss and Pawel Sobocinski, editors, CALCO, volume 35 of LIPIcs, pages 101-115, 2015.
  30. Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, and Martin Raussen. Directed Algebraic Topology and Concurrency. Springer, 2016.
  31. Lisbeth Fajstrup, Martin Raussen, and Éric Goubault. Algebraic topology and concurrency. Theoretical Computer Science, 357(1-3):241-278, 2006.
  32. Hans Fleischhack and Christian Stehno. Computing a finite prefix of a time Petri net. In Javier Esparza and Charles Lakos, editors, ICATPN, volume 2360 of Lecture Notes in Computer Science, pages 163-181. Springer, 2002.
  33. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems, volume 1032 of Lecture Notes in Computer Science. Springer, 1996.
  34. Ursula Goltz and Wolfgang Reisig. The non-sequential behavior of Petri nets. Information and Control, 57(2/3):125-147, 1983.
  35. Eric Goubault. Durations for truly-concurrent transitions. In Hanne Riis Nielson, editor, ESOP, volume 1058 of Lecture Notes in Computer Science, pages 173-187. Springer, 1996.
  36. Eric Goubault. Labelled cubical sets and asynchronous transition systems: an adjunction. In Preliminary Proceedings CMCIM'02, 2002.
  37. Marco Grandis. Directed algebraic topology: models of non-reversible worlds. New mathematical monographs. Cambridge University Press, 2009.
  38. Hans-Michael Hanisch. Analysis of place/transition nets with timed arcs and its application to batch process control. In Marco Ajmone Marsan, editor, ATPN, volume 691 of Lecture Notes in Computer Science, pages 282-299. Springer, 1993.
  39. Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, and Jun Sun. Partial order reduction for timed automata with abstractions. In Armin Biere and Roderick Bloem, editors, CAV, volume 8559 of Lecture Notes in Computer Science, pages 391-406. Springer, 2014.
  40. Karl Henrik Johansson, Magnus Egerstedt, John Lygeros, and Shankar Sastry. On the regularization of Zeno hybrid automata. Systems & Control Letters, 38(3):141-150, 1999.
  41. Kim G. Larsen, Uli Fahrenberg, and Axel Legay. From timed automata to stochastic hybrid games. In Dependable Software Systems Engineering, pages 60-103. IOS Press, 2017.
  42. Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a nutshell. Int. J. Software Tools for Technology Transfer, 1(1-2):134-152, 1997.
  43. Philip M. Merlin and David J. Farber. Recoverability of communication protocols-implications of a theoretical study. IEEE Transactions on Communications, 24(9):1036-1043, 1976.
  44. Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
  45. Mogens Nielsen and Thomas Hune. Bisimulation and open maps for timed transition systems. Fundamenta Informaticae, 38(1-2):61-77, 1999.
  46. Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. Petri nets, event structures and domains, part I. Theoretical Computer Science, 13:85-108, 1981.
  47. Carl A. Petri. Kommunikation mit Automaten. Bonn: Institut für Instrumentelle Mathematik, Schriften des IIM Nr. 2, 1962.
  48. Vaughan R. Pratt. Modeling concurrency with geometry. In David S. Wise, editor, POPL, pages 311-322. ACM Press, 1991.
  49. Vaughan R. Pratt. Higher dimensional automata revisited. Mathematical Structures in Computer Science, 10(4):525-548, 2000.
  50. Mike W. Shields. Concurrent machines. The Computer Journal, 28(5):449-465, 1985.
  51. Joseph Sifakis. Use of Petri nets for performance evaluation. In Measuring, Modelling and Evaluating Computer Systems, pages 75-93. North-Holland, 1977.
  52. Joseph Sifakis and Sergio Yovine. Compositional specification of timed systems. In Claude Puech and Rüdiger Reischuk, editors, STACS, volume 1046 of Lecture Notes in Computer Science, pages 347-359. Springer, 1996.
  53. Jiří Srba. Comparing the expressiveness of timed automata and timed extensions of Petri nets. In Franck Cassez and Claude Jard, editors, FORMATS, volume 5215 of Lecture Notes in Computer Science, pages 15-32. Springer, 2008.
  54. Rob J. van Glabbeek. Bisimulations for higher dimensional automata. Email message, June 1991.
  55. Rob J. van Glabbeek. afirstOn the expressiveness of higher dimensional automata. Theoretical Computer Science, 356(3):265-290, 2006.
  56. Rob J. van Glabbeek. Erratum to "On the expressiveness of higher dimensional automata". Theoretical Computer Science, 368(1-2):168-194, 2006.
  57. Rob J. van Glabbeek and Gordon D. Plotkin. Configuration structures. In LICS, pages 199-209. IEEE Computer Society, 1995.
  58. Rob J. van Glabbeek and Gordon D. Plotkin. Configuration structures, event structures and Petri nets. Theoretical Computer Science, 410(41):4111-4159, 2009.
  59. Farn Wang, Aloysius K. Mok, and E. Allen Emerson. Symbolic model checking for distributed real-time systems. In Jim Woodcock and Peter Gorm Larsen, editors, FME, volume 670 of Lecture Notes in Computer Science, pages 632-651. Springer, 1993.
  60. Glynn Winskel and Mogens Nielsen. Models for concurrency. In Handbook of Logic in Computer Science, volume 4. Clarendon Press, Oxford, 1995.