Document Open Access Logo

Higher-Dimensional Timed and Hybrid Automata

Author Uli Fahrenberg

PDF
Thumbnail PDF

File

LITES.8.2.3.pdf
  • Filesize: 0.64 MB
  • 16 pages

Document Identifiers

Author Details

Uli Fahrenberg
  • EPITA Research and Development Laboratory (LRDE), France

Cite AsGet BibTex

Uli Fahrenberg. Higher-Dimensional Timed and Hybrid Automata. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 03:1-03:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LITES.8.2.3

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Timed and hybrid models
Keywords
  • timed automaton
  • higher-dimensional automaton
  • precubical set
  • real time
  • non-interleaving concurrency
  • hybrid automaton

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen, and Jiří Srba. Reactive Systems. Cambridge University Press, 2007. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  5. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  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. Google Scholar
  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. Google Scholar
  8. Marek A. Bednarczyk. Categories of asynchronous systems. PhD thesis, University of Sussex, UK, 1987. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  23. Javier Esparza and Keijo Heljanko. Unfoldings - A Partial-Order Approach to Model Checking. Monographs Theor. Comput. Sci. Springer, 2008. Google Scholar
  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. Google Scholar
  25. Uli Fahrenberg. Higher-Dimensional Automata from a Topological Viewpoint. PhD thesis, Aalborg University, Denmark, 2005. Google Scholar
  26. Uli Fahrenberg. How to pull back open maps along semantics functors. In Jochen Pfalzgraf, editor, ACCAT, 2008. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  30. Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, and Martin Raussen. Directed Algebraic Topology and Concurrency. Springer, 2016. Google Scholar
  31. Lisbeth Fajstrup, Martin Raussen, and Éric Goubault. Algebraic topology and concurrency. Theoretical Computer Science, 357(1-3):241-278, 2006. Google Scholar
  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. Google Scholar
  33. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems, volume 1032 of Lecture Notes in Computer Science. Springer, 1996. Google Scholar
  34. Ursula Goltz and Wolfgang Reisig. The non-sequential behavior of Petri nets. Information and Control, 57(2/3):125-147, 1983. Google Scholar
  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. Google Scholar
  36. Eric Goubault. Labelled cubical sets and asynchronous transition systems: an adjunction. In Preliminary Proceedings CMCIM'02, 2002. Google Scholar
  37. Marco Grandis. Directed algebraic topology: models of non-reversible worlds. New mathematical monographs. Cambridge University Press, 2009. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  44. Robin Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  45. Mogens Nielsen and Thomas Hune. Bisimulation and open maps for timed transition systems. Fundamenta Informaticae, 38(1-2):61-77, 1999. Google Scholar
  46. Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. Petri nets, event structures and domains, part I. Theoretical Computer Science, 13:85-108, 1981. Google Scholar
  47. Carl A. Petri. Kommunikation mit Automaten. Bonn: Institut für Instrumentelle Mathematik, Schriften des IIM Nr. 2, 1962. Google Scholar
  48. Vaughan R. Pratt. Modeling concurrency with geometry. In David S. Wise, editor, POPL, pages 311-322. ACM Press, 1991. Google Scholar
  49. Vaughan R. Pratt. Higher dimensional automata revisited. Mathematical Structures in Computer Science, 10(4):525-548, 2000. Google Scholar
  50. Mike W. Shields. Concurrent machines. The Computer Journal, 28(5):449-465, 1985. Google Scholar
  51. Joseph Sifakis. Use of Petri nets for performance evaluation. In Measuring, Modelling and Evaluating Computer Systems, pages 75-93. North-Holland, 1977. Google Scholar
  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. Google Scholar
  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. Google Scholar
  54. Rob J. van Glabbeek. Bisimulations for higher dimensional automata. Email message, June 1991. Google Scholar
  55. Rob J. van Glabbeek. afirstOn the expressiveness of higher dimensional automata. Theoretical Computer Science, 356(3):265-290, 2006. Google Scholar
  56. Rob J. van Glabbeek. Erratum to "On the expressiveness of higher dimensional automata". Theoretical Computer Science, 368(1-2):168-194, 2006. Google Scholar
  57. Rob J. van Glabbeek and Gordon D. Plotkin. Configuration structures. In LICS, pages 199-209. IEEE Computer Society, 1995. Google Scholar
  58. Rob J. van Glabbeek and Gordon D. Plotkin. Configuration structures, event structures and Petri nets. Theoretical Computer Science, 410(41):4111-4159, 2009. Google Scholar
  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. Google Scholar
  60. Glynn Winskel and Mogens Nielsen. Models for concurrency. In Handbook of Logic in Computer Science, volume 4. Clarendon Press, Oxford, 1995. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact