Document Open Access Logo

Cost Automata, Safe Schemes, and Downward Closures

Authors David Barozzini, Lorenzo Clemente , Thomas Colcombet , Paweł Parys

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2020.109.pdf
  • Filesize: 0.56 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Rewrite systems
Keywords
  • Cost logics
  • cost automata
  • downward closures
  • higher-order recursion schemes
  • safe recursion schemes

Metrics

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

Abstract

Higher-order recursion schemes are an expressive formalism used to define languages of possibly infinite ranked trees. They extend regular and context-free grammars, and are equivalent to simply typed λY-calculus and collapsible pushdown automata. In this work we prove, under a syntactical constraint called safety, decidability of the model-checking problem for recursion schemes against properties defined by alternating B-automata, an extension of alternating parity automata for infinite trees with a boundedness acceptance condition. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes.

Cite As Get BibTex

David Barozzini, Lorenzo Clemente, Thomas Colcombet, and Paweł Parys. Cost Automata, Safe Schemes, and Downward Closures. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 109:1-109:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ICALP.2020.109

Author Details

David Barozzini
  • Institute of Informatics, University of Warsaw, Poland
Lorenzo Clemente
  • Institute of Informatics, University of Warsaw, Poland
Thomas Colcombet
  • IRIF-CNRS-Université de Paris, France
Paweł Parys
  • Institute of Informatics, University of Warsaw, Poland

Funding

  • Barozzini, David: Author supported by the National Science Centre, Poland (grant no. 2016/22/E/ST6/00041).
  • Clemente, Lorenzo: Author supported by the National Science Centre, Poland (grant no. 2016/22/E/ST6/00041).
  • Colcombet, Thomas: Supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No.670624), and the DeLTA ANR project (ANR-16-CE40-0007).
  • Parys, Paweł: Author supported by the National Science Centre, Poland (grant no. 2016/22/E/ST6/00041).

References

  1. Parosh Aziz Abdulla, Luc Boasson, and Ahmed Bouajjani. Effective lossy queue languages. In Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen, editors, Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science, pages 639-651. Springer, 2001. URL: https://doi.org/10.1007/3-540-48224-5_53.
  2. Alfred V. Aho. Indexed grammars - an extension of context-free grammars. J. ACM, 15(4):647-671, 1968. URL: https://doi.org/10.1145/321479.321488.
  3. Georg Bachmeier, Michael Luttenberger, and Maximilian Schlund. Finite automata for the sub- and superword closure of CFLs: Descriptional and computational complexity. In Adrian-Horia Dediu, Enrico Formenti, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications - 9th International Conference, LATA 2015, Nice, France, March 2-6, 2015, Proceedings, volume 8977 of Lecture Notes in Computer Science, pages 473-485. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-15579-1_37.
  4. David Barozzini, Lorenzo Clemente, Thomas Colcombet, and Paweł Parys. Cost Automata, Safe Schemes, and Downward Closures. arXiv e-prints, page arXiv:2004.12187, April 2020. URL: http://arxiv.org/abs/2004.12187.
  5. Alessandro Berarducci and Mariangiola Dezani-Ciancaglini. Infinite lambda-calculus and types. Theor. Comput. Sci., 212(1-2):29-75, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00135-2.
  6. Achim Blumensath, Thomas Colcombet, Denis Kuperberg, Paweł Parys, and Michael Vanden Boom. Two-way cost automata and cost logics over infinite trees. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 16:1-16:9. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603104.
  7. Mikołaj Bojańczyk. A bounding quantifier. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 41-55. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30124-0_7.
  8. Luca Breveglieri, Alessandra Cherubini, Claudio Citrini, and Stefano Crespi-Reghizzi. Multi-push-down languages and grammars. Int. J. Found. Comput. Sci., 7(3):253-292, 1996. URL: https://doi.org/10.1142/S0129054196000191.
  9. Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, and Olivier Serre. Recursion schemes and logical reflection. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 120-129. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/LICS.2010.40.
  10. Christopher H. Broadbent and Naoki Kobayashi. Saturation-based model checking of higher-order recursion schemes. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 129-148. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.129.
  11. Christopher H. Broadbent and C.-H. Luke Ong. On global model checking trees generated by higher-order recursion schemes. In Luca de Alfaro, editor, Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5504 of Lecture Notes in Computer Science, pages 107-121. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00596-1_9.
  12. Arnaud Carayol and Olivier Serre. Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 165-174. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.73.
  13. Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. Ordered tree-pushdown systems. In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India, volume 45 of LIPIcs, pages 163-177. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.163.
  14. Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. The diagonal problem for higher-order recursion schemes is decidable. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 96-105. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934527.
  15. Thomas Colcombet. Regular cost functions, part I: Logic and algebra over words. Logical Methods in Computer Science, 9(3), 2013. URL: https://doi.org/10.2168/LMCS-9(3:3)2013.
  16. Thomas Colcombet and Stefan Göller. Games with bound guess actions. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 257-266. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934502.
  17. Thomas Colcombet and Christof Löding. The non-deterministic Mostowski hierarchy and distance-parity automata. 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 II - Track B: Logic, Semantics, and Theory of Programming & Track C: Security and Cryptography Foundations, volume 5126 of Lecture Notes in Computer Science, pages 398-409. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_33.
  18. Thomas Colcombet and Christof Löding. Regular cost functions over finite trees. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 70-79. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/LICS.2010.36.
  19. Hubert Comon, Max Dauchet, Remi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications, 2007. URL: http://tata.gforge.inria.fr/.
  20. Bruno Courcelle. On constructing obstruction sets of words. Bulletin of EATCS, 1991. Google Scholar
  21. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, and Marc Zeitoun. A note on decidable separability by piecewise testable languages. In Adrian Kosowski and Igor Walukiewicz, editors, Fundamentals of Computation Theory - 20th International Symposium, FCT 2015, Gdańsk, Poland, August 17-19, 2015, Proceedings, volume 9210 of Lecture Notes in Computer Science, pages 173-185. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22177-9_14.
  22. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, Marc Zeitoun, and Georg Zetzsche. A Characterization for Decidable Separability by Piecewise Testable Languages. Discrete Mathematics & Theoretical Computer Science, Vol. 19 no. 4, FCT '15, December 2017. URL: https://doi.org/10.23638/DMTCS-19-4-1.
  23. Werner Damm. The IO- and OI-hierarchies. Theor. Comput. Sci., 20:95-207, 1982. URL: https://doi.org/10.1016/0304-3975(82)90009-3.
  24. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part I: Completions. 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 433-444. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2009. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1844.
  25. Jean Goubault-Larrecq and Sylvain Schmitz. Deciding piecewise testable separability for regular tree languages. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 97:1-97:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.97.
  26. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  27. Peter Habermehl, Roland Meyer, and Harro Wimmel. The downward-closure of Petri net languages. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 466-477. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_39.
  28. Axel Haddad. IO vs OI in higher-order recursion schemes. In Dale Miller and Zoltán Ésik, editors, Proceedings 8th Workshop on Fixed Points in Computer Science, FICS 2012, Tallinn, Estonia, 24th March 2012., volume 77 of EPTCS, pages 23-30, 2012. URL: https://doi.org/10.4204/EPTCS.77.4.
  29. Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 151-163. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837627.
  30. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 452-461. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/LICS.2008.34.
  31. Graham Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc., s3-2(1):326-336, January 1952. URL: https://doi.org/10.1112/plms/s3-2.1.326.
  32. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. Theor. Comput. Sci., 175(1):93-125, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00171-5.
  33. Teodor Knapik, Damian Niwiński, and Paweł Urzyczyn. Deciding monadic theories of hyperalgebraic trees. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Kraków, Poland, May 2-5, 2001, Proceedings, volume 2044 of Lecture Notes in Computer Science, pages 253-267. Springer, 2001. URL: https://doi.org/10.1007/3-540-45413-6_21.
  34. Teodor Knapik, Damian Niwiński, and Paweł Urzyczyn. Higher-order pushdown trees are easy. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205-222. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_15.
  35. Naoki Kobayashi. A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 260-274. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_18.
  36. Naoki Kobayashi. Model checking higher-order programs. J. ACM, 60(3):20:1-20:62, 2013. URL: https://doi.org/10.1145/2487241.2487246.
  37. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 179-188. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.29.
  38. Gregory M. Kobele and Sylvain Salvati. The IO and OI hierarchies revisited. Inf. Comput., 243:205-221, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.015.
  39. Denis Kuperberg and Michael Vanden Boom. Quasi-weak cost automata: A new variant of weakness. 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 66-77. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
  40. Denis Kuperberg and Michael Vanden Boom. Quasi-weak cost automata: A new variant of weakness. 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 66-77. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2011.66.
  41. Jan van Leeuwen. Effective constructions in well-partially- ordered free monoids. Discrete Mathematics, 21(3):237-252, 1978. URL: https://doi.org/10.1016/0012-365X(78)90156-5.
  42. Robin P. Neatherway and C.-H. Luke Ong. TravMC2: Higher-order model checking for alternating parity tree automata. In Neha Rungta and Oksana Tkachuk, editors, 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21-23, 2014, pages 129-132. ACM, 2014. URL: https://doi.org/10.1145/2632362.2632381.
  43. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81-90. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.38.
  44. Paweł Parys. On the significance of the collapse operation. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 521-530. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.62.
  45. Paweł Parys. The complexity of the diagonal problem for recursion schemes. In Satya Lokam and R. Ramanujam, editors, Proc. of FSTTCS'17, volume 93 of Leibniz International Proceedings in Informatics (LIPIcs), pages 45:1-45:14, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2017.45.
  46. Paweł Parys. Recursion schemes and the WMSO+U logic. In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, volume 96 of LIPIcs, pages 53:1-53:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.53.
  47. Steven J. Ramsay, Robin P. Neatherway, and C.-H. Luke Ong. A type-directed abstraction refinement approach to higher-order model checking. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 61-72. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535873.
  48. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Inf. Comput., 239:340-355, 2014. URL: https://doi.org/10.1016/j.ic.2014.07.012.
  49. Sylvain Salvati and Igor Walukiewicz. A model for behavioural properties of higher-order programs. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 229-243. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.229.
  50. Sylvain Salvati and Igor Walukiewicz. Simply typed fixpoint calculus and collapsible pushdown automata. Mathematical Structures in Computer Science, 26(7):1304-1350, 2016. URL: https://doi.org/10.1017/S0960129514000590.
  51. Larry J. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, MIT, 1974. Google Scholar
  52. Michael Vanden Boom. Weak cost monadic logic over infinite trees. In Filip Murlak and Piotr Sankowski, editors, Mathematical Foundations of Computer Science 2011 - 36th International Symposium, MFCS 2011, Warsaw, Poland, August 22-26, 2011. Proceedings, volume 6907 of Lecture Notes in Computer Science, pages 580-591. Springer, 2011. Google Scholar
  53. Michael Vanden Boom. Weak cost monadic logic over infinite trees. In Filip Murlak and Piotr Sankowski, editors, Mathematical Foundations of Computer Science 2011 - 36th International Symposium, MFCS 2011, Warsaw, Poland, August 22-26, 2011. Proceedings, volume 6907 of Lecture Notes in Computer Science, pages 580-591. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22993-0_52.
  54. Georg Zetzsche. An approach to computing downward closures. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Proc. of ICALP'15, volume 9135 of LNCS, pages 440-451. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_35.
  55. Georg Zetzsche. Computing downward closures for stacked counter automata. In Ernst W. Mayr and Nicolas Ollinger, editors, 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, volume 30 of LIPIcs, pages 743-756. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.STACS.2015.743.
  56. Georg Zetzsche. The complexity of downward closure comparisons. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 123:1-123:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.123.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact