Document Open Access Logo

Complementing Emerson-Lei Elevator Automata

Authors Ondrej Alexaj , Vojtěch Havlena , Ondřej Lengál , Yong Li , Nicolas Mazzocchi

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.8.pdf
  • Filesize: 1.47 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Emerson-Lei elevator automata
  • complementation
  • elevator automata
  • omega automata
  • infinite words
  • omega-regular languages

Metrics

Abstract

Büchi elevator automata naturally appear in several areas of formal methods as a structural expressibly-equivalent subclass of Büchi automata where every strongly connected component is either deterministic or inherently weak. It was shown that this class contains the majority of Büchi automata generated in practical applications, including LTL model-checking and verification of hyperproperties. Moreover, the elevator subclass enables more efficient complementation and determinization algorithms than unrestricted Büchi automata. In this paper, we introduce Emerson-Lei elevator automata, which is a generalization of Büchi elevator automata to richer acceptance conditions. We provide a complementation algorithm with a significantly better asymptotic complexity than the best known algorithm for unrestricted Emerson-Lei automata. The practical efficiency of our algorithm is demonstrated by an experimental comparison with the popular state-of-the-art tool Spot. Our work is, to the best of our knowledge, the first step towards practical algorithms for complementing, determinizing, and testing universality and inclusion of Emerson-Lei automata with rich acceptance conditions.

Cite As Get BibTex

Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, and Nicolas Mazzocchi. Complementing Emerson-Lei Elevator Automata. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.8

Author Details

Ondrej Alexaj
  • Brno University of Technology, Czech Republic
Vojtěch Havlena
  • Brno University of Technology, Czech Republic
Ondřej Lengál
  • Brno University of Technology, Czech Republic
Yong Li
  • Key Laboratory of System Software (Chinese Academy of Sciences), ISCAS, Beijing, China
Nicolas Mazzocchi
  • Slovak University of Technology in Bratislava, Slovakia

Funding

This work was supported in part by the CAS Project for Young Scientists in Basic Research (Grant No. YSBR-040), the National Natural Science Foundation of China (Grant No. 62102407), the Beijing Natural Science Foundation (Grant No. IS26039), the Czech Science Foundation project 26-22640S, and the FIT BUT internal project FIT-S-26-9011.

Supplementary Materials

References

  1. Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, and Nicolas Mazzocchi. VeriFIT/kofola. Software, (visited on 2026-08-12). URL: https://github.com/VeriFIT/kofola
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.27641
  2. Ondrej Alexaj, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Yong Li, and Nicolas Mazzocchi. Kofola 1.0: A modular approach to ω-regular complementation and inclusion checking. In CAV'26 (to appear), 2026. Google Scholar
  3. Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, and Nicolas Mazzocchi. Complementing Emerson-Lei elevator automata (technical report). CoRR, abs/2606.26768, 2026. URL: https://arxiv.org/abs/2606.26768.
  4. Joël D. Allred and Ulrich Ultes-Nitsche. A simple and optimal complementation algorithm for Büchi automata. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 46-55. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209138.
  5. František Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejček, and Ming-Hsien Tsai. Complementing semi-deterministic Büchi automata. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 770-787. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_49.
  6. Udi Boker. Why these automata types? In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018, volume 57 of EPiC Series in Computing, pages 143-163. EasyChair, 2018. URL: https://doi.org/10.29007/C3BJ.
  7. Stefan Breuers, Christof Löding, and Jörg Olschewski. Improved Ramsey-based Büchi complementation. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, Lecture Notes in Computer Science, pages 150-164. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28729-9_10.
  8. J. Richard Büchi. On a decision method in restricted second order arithmetic. In Proc. of International Congress on Logic, Method, and Philosophy of Science 1960. Stanford Univ. Press, Stanford, 1962. Google Scholar
  9. Yang Cai and Ting Zhang. A tight lower bound for Streett complementation. In Supratik Chakraborty and Amit Kumar, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India, volume 13 of LIPIcs, pages 339-350. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2011.339.
  10. Yang Cai and Ting Zhang. Tight upper bounds for Streett and parity complementation. In Marc Bezem, editor, Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings, volume 12 of LIPIcs, pages 112-128. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.CSL.2011.112.
  11. Krishnendu Chatterjee, Andreas Gaiser, and Jan Křetínský. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, pages 559-575. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_37.
  12. Yu-Fang Chen, Vojtěch Havlena, and Ondřej Lengál. Simulations in rank-based Büchi automata complementation. In Anthony Widjaja Lin, editor, Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, volume 11893 of Lecture Notes in Computer Science, pages 447-467. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34175-6_23.
  13. Yu-Fang Chen, Matthias Heizmann, Ondřej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, and Lijun Zhang. Advanced automata-based algorithms for program termination checking. In Jeffrey S. Foster and Dan Grossman, editors, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 135-150. ACM, 2018. URL: https://doi.org/10.1145/3192366.3192405.
  14. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Martín Abadi and Steve Kremer, editors, Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, Lecture Notes in Computer Science, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  15. Costas Courcoubetis and Mihalis Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, pages 338-345. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/SFCS.1988.21950.
  16. David Dokoupil. Efficient complementation of generalized Büchi automata. Master’s thesis, Faculty of Informatics, Masaryk University, 2026. URL: https://is.muni.cz/th/xu3iz/.
  17. Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. From Spot 2.0 to Spot 2.10: What’s new? In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 174-187. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_9.
  18. E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program., 8(3):275-306, 1987. URL: https://doi.org/10.1016/0167-6423(87)90036-0.
  19. Javier Esparza, Jan Křetínský, and Salomon Sickert. From LTL to deterministic automata - A safraless compositional approach. Formal Methods Syst. Des., 49(3):219-271, 2016. URL: https://doi.org/10.1007/S10703-016-0259-2.
  20. Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi, and Lijun Zhang. On the power of finite ambiguity in Büchi complementation. Inf. Comput., 292:105032, 2023. URL: https://doi.org/10.1016/J.IC.2023.105032.
  21. Vojtěch Havlena and Ondřej Lengál. Reducing (to) the ranks: Efficient rank-based Büchi automata complementation. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 2:1-2:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.2.
  22. Vojtěch Havlena, Ondřej Lengál, Yong Li, Barbora Šmahlíková, and Andrea Turrini. Modular mix-and-match complementation of Büchi automata. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pages 249-270. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_13.
  23. Vojtěch Havlena, Ondřej Lengál, and Barbora Šmahlíková. Complementing Büchi automata with Ranker. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 188-201. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_10.
  24. Vojtěch Havlena, Ondřej Lengál, and Barbora Šmahlíková. Sky is not the limit: Tighter rank bounds for elevator automata in Büchi automata complementation. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, volume 13244 of Lecture Notes in Computer Science, pages 118-136. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99527-0_7.
  25. Vojtěch Havlena, Ondřej Lengál, and Barbora Šmahlíková. Complementation of Emerson-Lei automata. In Parosh Aziz Abdulla and Delia Kesner, editors, Foundations of Software Science and Computation Structures - 28th International Conference, FoSSaCS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, volume 15691 of Lecture Notes in Computer Science, pages 88-110. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90897-2_5.
  26. Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, and Andreas Podelski. Ultimate Automizer and the search for perfect interpolants (competition contribution). In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II, Lecture Notes in Computer Science, pages 447-451. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89963-3_30.
  27. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Software model checking for people who love automata. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, pages 36-52. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_2.
  28. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Termination analysis by learning terminating programs. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science, pages 797-813. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_53.
  29. Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey O. Shallit. Decidability for Sturmian words. Log. Methods Comput. Sci., 20(3), 2024. URL: https://doi.org/10.46298/LMCS-20(3:12)2024.
  30. Tobias John, Simon Jantsch, Christel Baier, and Sascha Klüppelholz. Determinization and limit-determinization of Emerson-Lei automata. In Zhe Hou and Vijay Ganesh, editors, Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings, Lecture Notes in Computer Science, pages 15-31. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88885-5_2.
  31. Detlef Kähler and Thomas Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games, Lecture Notes in Computer Science, pages 724-735. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70575-8_59.
  32. Yonit Kesten and Amir Pnueli. A complete proof systems for QPTL. In Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995, pages 2-12. IEEE Computer Society, 1995. URL: https://doi.org/10.1109/LICS.1995.523239.
  33. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata are not that weak. ACM Trans. Comput. Log., 2(3):408-429, 2001. URL: https://doi.org/10.1145/377978.377993.
  34. Orna Kupferman and Moshe Y. Vardi. Complementation constructions for nondeterministic automata on infinite words. In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer Science, pages 206-221. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31980-1_14.
  35. Orna Kupferman and Moshe Y. Vardi. From complementation to certification. Theor. Comput. Sci., 345(1):83-100, 2005. URL: https://doi.org/10.1016/j.tcs.2005.07.021.
  36. Robert P. Kurshan. Complementing deterministic Büchi automata in polynomial time. J. Comput. Syst. Sci., 35(1):59-71, 1987. URL: https://doi.org/10.1016/0022-0000(87)90036-5.
  37. Jan Křetínský and Javier Esparza. Deterministic automata for the (F, G)-fragment of LTL. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, Lecture Notes in Computer Science, pages 7-22. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31424-7_7.
  38. Ondřej Lengál et al. Automata benchmarks. https://github.com/ondrik/automata-benchmarks, 2026.
  39. Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi, and Lijun Zhang. Divide-and-conquer determinization of Büchi automata based on SCC decomposition. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 152-173. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_8.
  40. Yong Li, Andrea Turrini, Lijun Zhang, and Sven Schewe. Learning to complement Büchi automata. In Isil Dillig and Jens Palsberg, editors, Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, Lecture Notes in Computer Science, pages 313-335. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-73721-8_15.
  41. Yong Li, Moshe Y. Vardi, and Lijun Zhang. On the power of unambiguity in Büchi complementation. In Jean-François Raskin and Davide Bresolin, editors, Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020, EPTCS, pages 182-198, 2020. URL: https://doi.org/10.4204/EPTCS.326.12.
  42. Juraj Major. LTL3TELA benchmark formulae. https://github.com/jurajmajor/ltl3tela/tree/master/Experiments/formulae, 2019. Commit 02092adca492678407bd74b5d3bbe103d8 c2b400.
  43. Juraj Major, František Blahoudek, Jan Strejček, Miriama Sasaráková, and Tatiana Zbončáková. ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, Lecture Notes in Computer Science, pages 357-365. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_21.
  44. Max Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 15, 1988. Google Scholar
  45. Satoru Miyano and Takeshi Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32(3):321-330, 1984. URL: https://doi.org/10.1016/0304-3975(84)90049-5.
  46. Reed Oei, Dun Ma, Christian Schulz, and Philipp Hieronymi. Pecan: An automated theorem prover for automatic sequences using Büchi automata. CoRR, abs/2102.01727, 2021. URL: https://arxiv.org/abs/2102.01727.
  47. Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci., 3(3), 2007. URL: https://doi.org/10.2168/LMCS-3(3:5)2007.
  48. Shmuel Safra. On the complexity of ω-automata. In 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, pages 319-327. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
  49. Shmuel Safra and Moshe Y. Vardi. On ω-automata and temporal logic (preliminary report). In David S. Johnson, editor, Proceedings of the 21st Annual ACM Symposium on Theory of Computing, May 14-17, 1989, Seattle, Washington, USA, pages 127-137. ACM, 1989. URL: https://doi.org/10.1145/73007.73019.
  50. Sven Schewe. Büchi complementation made tight. In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings, volume 3 of LIPIcs, pages 661-672. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2009. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1854.
  51. A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic. Theoretical Computer Science, 49(2-3):217-237, 1987. URL: https://doi.org/10.1016/0304-3975(87)90008-9.
  52. Moshe Y. Vardi. The Büchi complementation saga. In Wolfgang Thomas and Pascal Weil, editors, STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Aachen, Germany, February 22-24, 2007, Proceedings, Lecture Notes in Computer Science, pages 12-22. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-70918-3_2.
  53. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings of the Symposium on Logic in Computer Science (LICS '86), Cambridge, Massachusetts, USA, June 16-18, 1986, pages 332-344. IEEE Computer Society, 1986. Google Scholar
  54. Qiqi Yan. Lower bounds for complementation of ω-automata via the full automata technique. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, pages 589-600, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11787006_50.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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