Cost Automata, Safe Schemes, and Downward Closures

• Autorzy: Barozzini, David , Clemente, Lorenzo , Colcombet, Thomas , Parys, Paweł
• Języki publikacji: EN

Abstrakty

EN

In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes. Higher-order recursion schemes are an expressive formalism used to define languages of finite and infinite ranked trees by means of fixed points of lambda terms. They extend regular and context-free grammars, and are equivalent in expressive power to the simply typed λY-calculus and collapsible pushdown automata. Safety in a syntactic restriction which limits their expressive power. The class of alternating B-automata is an extension of alternating parity automata over infinite trees; it enhances them with counting features that can be used to describe boundedness properties

Słowa kluczowe

EN

cost logics; cost automata; downward closures; higher-order recursion schemes; safe recursion schemes

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 188, nr 3
• Strony: 127--178
• Opis fizyczny: Bibliogr. 65 poz., rys.

Twórcy

autor

Barozzini, David

• Institute of Informatics University of Warsaw Warsaw, Poland,

autor

Clemente, Lorenzo

• Institute of Informatics University of Warsaw Warsaw, Poland,

autor

Colcombet, Thomas

• IRIF-CNRS-Universit´e de Paris Paris, France,

autor

Parys, Paweł

• Institute of Informatics University of Warsaw Warsaw, Poland,

Bibliografia

• [1] Kobayashi N. Model Checking Higher-Order Programs. J. ACM, 2013. 60(3):20:1-20:62. doi:10.1145/2487241.2487246.
• [2] Salvati S, Walukiewicz I. Simply Typed Fixpoint Calculus and Collapsible Pushdown Automata. Math. Struct. Comput. Sci., 2016. 26(7):1304-1350. doi:10.1017/S0960129514000590.
• [3] Hague M, Murawski AS, Ong CL, Serre O. Collapsible Pushdown Automata and Recursion Schemes. ACM Trans. Comput. Log., 2017. 18(3):25:1-25:42. doi:10.1145/3091122.
• [4] Clemente L, Parys P, Salvati S, Walukiewicz I. Ordered Tree-Pushdown Systems. In: Harsha P, Ramalingam G (eds.), 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. Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2015 pp. 163-177. doi:10.4230/LIPIcs.FSTTCS. 2015.163.
• [5] Damm W. The IO- and OI-Hierarchies. Theor. Comput. Sci., 1982. 20:95-207. doi:10.1016/0304-3975(82)90009-3.
• [6] Kobele GM, Salvati S. The IO and OI Hierarchies Revisited. Inf. Comput., 2015. 243:205-221. doi:10.1016/j.ic.2014.12.015.
• [7] Aho AV. Indexed Grammars—An Extension of Context-Free Grammars. J. ACM, 1968. 15(4):647-671. doi:10.1145/321479.321488.
• [8] Breveglieri L, Cherubini A, Citrini C, Crespi-Reghizzi S. Multi-push-down Languages and Grammars. Int. J. Found. Comput. Sci., 1996. 7(3):253-292. doi:10.1142/S0129054196000191.
• [9] Ong CL. 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. IEEE Computer Society, 2006 pp. 81-90. doi:10.1109/LICS.2006.38.
• [10] Hague M, Murawski AS, Ong CL, Serre O. 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. IEEE Computer Society, 2008 pp. 452-461. doi:10.1109/LICS. 2008.34.
• [11] Kobayashi N, Ong CL. 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. IEEE Computer Society, 2009 pp. 179-188. doi:10.1109/LICS.2009.29.
• [12] Salvati S, Walukiewicz I. Krivine Machines and Higher-Order Schemes. Inf. Comput., 2014. 239:340-355. doi:10.1016/j.ic.2014.07.012.
• [13] Parys P. Higher-Order Model Checking Step by Step. In: Bansal N, Merelli E, Worrell J (eds.), 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021 pp. 140:1-140:16. doi:10.4230/LIPIcs.ICALP.2021.140.
• [14] Broadbent CH, Ong CL. On Global Model Checking Trees Generated by Higher-Order Recursion Schemes. In: de Alfaro L (ed.), 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. Springer, 2009 pp. 107-121. doi:10.1007/978-3-642-00596-1 9.
• [15] Broadbent CH, Carayol A, Ong CL, Serre O. 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. IEEE Computer Society, 2010 pp. 120-129. doi:10.1109/LICS.2010.40.
• [16] Carayol A, Serre O. 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. IEEE Computer Society, 2012 pp. 165-174. doi:10.1109/LICS.2012.73.
• [17] Salvati S, Walukiewicz I. A Model for Behavioural Properties of Higher-Order Programs. In: Kreutzer S (ed.), 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7–10, 2015, Berlin, Germany, volume 41 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2015 pp. 229-243. doi:10.4230/LIPIcs.CSL.2015.229.
• [18] Stockmeyer LJ. The Complexity of Decision Problems in Automata Theory and Logic. Ph.D. thesis, MIT, 1974.
• [19] Broadbent CH, Kobayashi N. Saturation-Based Model Checking of Higher-Order Recursion Schemes. In: Rocca SRD (ed.), Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2–5, 2013, Torino, Italy, volume 23 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2013 pp. 129-148. doi:10.4230/LIPIcs.CSL.2013.129.
• [20] Kobayashi N. A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes. In: Hofmann M (ed.), 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. Springer, 2011 pp. 260-274. doi:10.1007/978-3-642-19805-2 18.
• [21] Neatherway RP, Ong CL. TravMC2: Higher-Order Model Checking for Alternating Parity Tree Automata. In: Rungta N, Tkachuk O (eds.), 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21–23, 2014. ACM, 2014 pp. 129-132. doi:10.1145/2632362.2632381.
• [22] Ramsay SJ, Neatherway RP, Ong CL. A Type-Directed Abstraction Refinement Approach to Higher-Order Model Checking. In: Jagannathan S, Sewell P (eds.), The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20–21, 2014. ACM, 2014 pp. 61-72. doi:10.1145/2535838.2535873.
• [23] Clemente L, Parys P, Salvati S, Walukiewicz I. The Diagonal Problem for Higher-Order Recursion Schemes is Decidable. In: Grohe M, Koskinen E, Shankar N (eds.), Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5–8, 2016. ACM, 2016 pp. 96-105. doi:10.1145/2933575.2934527.
• [24] Hague M, Kochems J, Ong CL. Unboundedness and Downward Closures of Higher-Order Pushdown Automata. In: Bod´ık R, Majumdar R (eds.), Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20–22, 2016. ACM, 2016 pp. 151-163. doi:10.1145/2837614.2837627.
• [25] Parys P. A Type System Describing Unboundedness. Discret. Math. Theor. Comput. Sci., 2020. 22(4). doi:10.23638/DMTCS-22-4-2.
• [26] Zetzsche G. An Approach to Computing Downward Closures. In: Halld´orsson MM, Iwama K, Kobayashi N, Speckmann B (eds.), Automata, Languages, and Programming – 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6–10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science. Springer, 2015 pp. 440-451. doi:10.1007/978-3-662-47666-6 35.
• [27] Czerwiński W, Martens W, van Rooijen L, Zeitoun M, Zetzsche G. A Characterization for Decidable Separability by Piecewise Testable Languages. Discret. Math. Theor. Comput. Sci., 2017. 19(4). doi:10.23638/DMTCS-19-4-1.
• [28] Czerwi´nski W, Martens W, van Rooijen L, Zeitoun M. A Note on Decidable Separability by Piecewise Testable Languages. In: Kosowski A, Walukiewicz I (eds.), Fundamentals of Computation Theory – 20th International Symposium, FCT 2015, Gda´nsk, Poland, August 17–19, 2015, Proceedings, volume 9210 of Lecture Notes in Computer Science. Springer, 2015 pp. 173-185. doi:10.1007/978-3-319-22177-9 14.
• [29] Higman G. Ordering by Divisibility in Abstract Algebras. Proc. London Math. Soc., 1952. s3-2(1):326-336. doi:10.1112/plms/s3-2.1.326.
• [30] Bachmeier G, Luttenberger M, Schlund M. Finite Automata for the Sub- and Superword Closure of CFLs: Descriptional and Computational Complexity. In: Dediu A, Formenti E, Mart´ın-Vide C, Truthe B (eds.), 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. Springer, 2015 pp. 473-485. doi:10.1007/978-3-319-15579-1 37.
• [31] Courcelle B. On Constructing Obstruction Sets of Words. Bull. EATCS, 1991. 44:178-186.
• [32] van Leeuwen J. Effective Constructions in Well-Partially-Ordered Free Monoids. Discret. Math., 1978. 21(3):237-252. doi:10.1016/0012-365X(78)90156-5.
• [33] Habermehl P, Meyer R, Wimmel H. The Downward-Closure of Petri Net Languages. In: Abramsky S, Gavoille C, Kirchner C, auf der Heide FM, Spirakis PG (eds.), 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. Springer, 2010 pp. 466-477. doi:10.1007/978-3-642-14162-1 39.
• [34] Zetzsche G. Computing Downward Closures for Stacked Counter Automata. In: Mayr EW, Ollinger N (eds.), 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4–7, 2015, Garching, Germany, volume 30 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015 pp. 743-756. doi:10.4230/LIPIcs.STACS.2015.743.
• [35] Abdulla PA, Boasson L, Bouajjani A. Effective Lossy Queue Languages. In: Orejas F, Spirakis PG, van Leeuwen J (eds.), Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8–12, 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science. Springer, 2001 pp. 639-651. doi:10.1007/3-540-48224-5 53.
• [36] Goubault-Larrecq J, Schmitz S. Deciding Piecewise Testable Separability for Regular Tree Languages. In: Chatzigiannakis I, Mitzenmacher M, Rabani Y, Sangiorgi D (eds.), 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11–15, 2016, Rome, Italy, volume 55 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016 pp. 97:1-97:15. doi:10.4230/LIPIcs. ICALP.2016.97.
• [37] Bojańczyk M, Colcombet T. Bounds in ω-Regularity. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12–15 August 2006, Seattle, WA, USA, Proceedings. IEEE Computer Society, 2006 pp. 285-296. doi:10.1109/LICS.2006.17.
• [38] Colcombet T. The Theory of Stabilisation Monoids and Regular Cost Functions. In: Albers S, Marchetti-Spaccamela A, Matias Y, Nikoletseas SE, Thomas W (eds.), Automata, Languages and Programming, 36th Internatilonal Colloquium, ICALP 2009, Rhodes, Greece, July 5–12, 2009, Proceedings, Part II, volume 5556 of Lecture Notes in Computer Science. Springer, 2009 pp. 139-150. doi:10.1007/978-3-642-02930-1 12.
• [39] Colcombet T, L¨oding C. 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. IEEE Computer Society, 2010 pp. 70-79. doi:10.1109/LICS.2010.36.
• [40] Kuperberg D, Vanden Boom M. On the Expressive Power of Cost Logics Over Infinite Words. In:Czumaj A, Mehlhorn K, Pitts AM, Wattenhofer R (eds.), Automata, Languages, and Programming – 39th International Colloquium, ICALP 2012, Warwick, UK, July 9–13, 2012, Proceedings, Part II, volume 7392 of Lecture Notes in Computer Science. Springer, 2012 pp. 287-298. doi:10.1007/978-3-642-31585-5 28.
• [41] Vanden Boom M. Weak Cost Monadic Logic Over Infinite Trees. In: Murlak F, Sankowski P (eds.), 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. Springer, 2011 pp. 580-591. doi:10.1007/978-3-642-22993-0 52.
• [42] Kuperberg D, Vanden Boom M. Quasi-Weak Cost Automata: A New Variant of Weakness. In: Chakraborty S, Kumar A (eds.), IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12–14, 2011, Mumbai, India, volume 13 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2011 pp. 66-77. doi:10.4230/LIPIcs. FSTTCS.2011.66.
• [43] Grӓdel E, Thomas W, Wilke T (eds.). 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. ISBN 3-540-00388-6. doi:10.1007/3-540-36387-4.
• [44] Colcombet T, L¨oding C. The Non-deterministic Mostowski Hierarchy and Distance-Parity Automata. In:Aceto L, Damg˚ard I, Goldberg LA, Halld´orsson MM, Ingӧlfsdӧttir A, Walukiewicz I (eds.), 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. Springer, 2008 pp. 398-409. doi:10.1007/978-3-540-70583-3 33.
• [45] Bojańczyk M. A Bounding Quantifier. In: Marcinkowski J, Tarlecki A (eds.), 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. Springer, 2004 pp. 41-55. doi:10.1007/978-3-540-30124-0 7.
• [46] Parys P. Recursion Schemes, the MSO Logic, and the U Quantifier. Log. Methods Comput. Sci., 2020. 16(1). doi:10.23638/LMCS-16(1:20)2020.
• [47] Knapik T, Niwi´nski D, Urzyczyn P. Higher-Order Pushdown Trees Are Easy. In: Nielsen M, Engberg U (eds.), Foundations of Software Science and Computation Structures, 5th International Conference, FOS-SACS 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. Springer, 2002 pp. 205-222. doi:10.1007/3-540-45931-6 15.
• [48] Parys P. On the Expressive Power of Higher-Order Pushdown Systems. Log. Methods Comput. Sci., 2020. 16(3). doi:10.23638/LMCS-16(3:11)2020.
• [49] Blumensath A, Colcombet T, Kuperberg D, Parys P, Vanden Boom M. Two-Way Cost Automata and Cost Logics Over Infinite Trees. In: Henzinger TA, Miller D (eds.), 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. ACM, 2014 pp. 16:1-16:9. doi:10.1145/2603088.2603104.
• [50] Finkel A, Goubault-Larrecq J. Forward Analysis for WSTS, Part I: Completions. In: Albers S, Marion J (eds.), 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings, volume 3 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Germany, 2009 pp. 433-444. doi:10.4230/LIPIcs.STACS.2009.1844.
• [51] Barozzini D, Clemente L, Colcombet T, Parys P. Cost Automata, Safe Schemes, and Downward Closures. In: Czumaj A, Dawar A, Merelli E (eds.), 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8–11, 2020, Saarbr¨ucken, Germany (Virtual Conference), volume 168 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2020 pp. 109:1-109:18. doi:10.4230/LIPIcs. ICALP.2020.109. (Best paper award for Track B).
• [52] Berarducci A, Dezani-Ciancaglini M. Infinite Lambda-Calculus and Types. Theor. Comput. Sci., 1999. 212(1-2):29-75. doi:10.1016/S0304-3975(98)00135-2.
• [53] Kennaway R, Klop JW, Sleep MR, de Vries F. Infinitary Lambda Calculus. Theor. Comput. Sci., 1997. 175(1):93-125. doi:10.1016/S0304-3975(96)00171-5.
• [54] Blum W, Ong CL. The Safe Lambda Calculus. Log. Methods Comput. Sci., 2009. 5(1). doi:10.2168/LMCS-5(1:3)2009.
• [55] Haddad A. IO vs OI in Higher-Order Recursion Schemes. In: Miller D, Esik Z (eds.), Proceedings 8th Workshop on Fixed Points in Computer Science, FICS 2012, Tallinn, Estonia, 24th March 2012, volume 77 of EPTCS. 2012 pp. 23-30. doi:10.4204/EPTCS.77.4.
• [56] Colcombet T, G¨oller S. Games With Bound Guess Actions. In: Grohe M, Koskinen E, Shankar N (eds.), Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. ACM, 2016 pp. 257-266. doi:10.1145/2933575.2934502.
• [57] Knapik T, Niwi´nski D, Urzyczyn P. Deciding Monadic Theories of Hyperalgebraic Trees. In: Abramsky S (ed.), 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. Springer, 2001 pp. 253-267. doi:10.1007/3-540-45413-6 21.
• [58] Comon H, Dauchet M, Gilleron R, Jacquemard F, Lugiez D, Lӧding C, Tison S, Tommasi M. Tree Automata Techniques and Applications, 2007. URL http://tata.gforge.inria.fr/.
• [59] Colcombet T. Regular Cost Functions, Part I: Logic and Algebra Over Words. Log. Methods Comput. Sci., 2013. 9(3). doi:10.2168/LMCS-9(3:3)2013.
• [60] Clemente L, Parys P, Salvati S, Walukiewicz I. The Diagonal Problem for Higher-Order Recursion Schemes is Decidable. CoRR, 2016. abs/1605.00371.
• [61] Carayol A, W¨ohrle S. The Caucal Hierarchy of Infinite Graphs in Terms of Logic and Higher-Order Pushdown Automata. In: Pandya PK, Radhakrishnan J (eds.), FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 23rd Conference, Mumbai, India, December 15-17, 2003, Proceedings, volume 2914 of Lecture Notes in Computer Science. Springer, 2003 pp. 112-123. doi:10.1007/978-3-540-24597-1 10.
• [62] Zetzsche G. The Complexity of Downward Closure Comparisons. In: Chatzigiannakis I, Mitzenmacher M, Rabani Y, Sangiorgi D (eds.), 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016 pp. 123:1-123:14. doi:10.4230/LIPIcs.ICALP.2016.123
• [63] Parys P. Homogeneity Without Loss of Generality. In: Kirchner H (ed.), 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2018 pp. 27:1-27:15. doi:10.4230/LIPIcs.FSCD.2018.27.
• [64] Barendregt H. The Lambda Calculus - Its Syntax and Semantics. Elsevier Science Publishers Ltd., 1984.
• [65] Curry H, Feys R. Combinatory Logic - Volume I. North-Holland Publishing Company, 1958

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2024).

Identyfikatory

DOI

10.3233/FI-222145