×

Monoidal-closed categories of tree automata. (English) Zbl 1435.68183

Summary: This paper surveys a new perspective on tree automata and Monadic second-order logic (MSO) on infinite trees. We show that the operations on tree automata used in the translations of MSO-formulae to automata underlying Rabin’s Tree Theorem (the decidability of MSO) correspond to the connectives of Intuitionistic Multiplicative Exponential Linear Logic (IMELL). Namely, we equip a variant of usual alternating tree automata (that we call uniform tree automata) with a fibered monoidal-closed structure which in particular handles a linear complementation of alternating automata. Moreover, this monoidal structure is actually Cartesian on non-deterministic automata, and an adaptation of a usual construction for the simulation of alternating automata by non-deterministic ones satisfies the deduction rules of the \(!(-)\) exponential modality of IMELL. (But this operation is unfortunately not a functor because it does not preserve composition.) Our model of IMLL consists in categories of games which are based on usual categories of two-player linear sequential games called simple games, and which generalize usual acceptance games of tree automata. This model provides a realizability semantics, along the lines of Curry-Howard proofs-as-programs correspondence, of a linear constructive deduction system for tree automata. This realizability semantics, which can be summarized with the slogan “automata as objects, strategies as morphisms,” satisfies an expected property of witness extraction from proofs of existential statements. Moreover, it makes it possible to combine realizers produced as interpretations of proofs with strategies witnessing (non-)emptiness of tree automata.

MSC:

68Q45 Formal languages and automata
03B70 Logic in computer science
03D05 Automata and formal grammars in connection with logical questions
03G30 Categorical logic, topoi
18B20 Categories of machines, automata
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
18M45 Categorical aspects of linear logic
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S. (1997). Semantics of interaction. In: Pitts, A. M. and Dybjer, P. (eds.) Semantics and Logics of Computation, Publications of the Newton Institute, vol. 14, Cambridge, Cambridge University Press, 1. · Zbl 0938.91500
[2] Amadio, R. M. and Curien, P.-L. (1998). Domains and Lambda-Calculi, Cambridge Tracts in Theoretical Computer Science, Cambridge, Cambridge University Press. · Zbl 0962.03001
[3] Arnold, A. and Niwinski, D. (2007). Continuous Separation of Game Languages. Fundamenta Informaticae81 (1-3) 19-28. · Zbl 1213.03051
[4] Arnold, A. (1999). The μ-calculus alternation-depth hierarchy is strict on binary trees. ITA33 (4/5) 329-340. · Zbl 0945.68118
[5] Avigad, J. and Feferman, S. (1998). Gödel’s functional (“Dialectica”) interpretation. In: Buss, S. (ed.) Handbook Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 137, Amsterdam, Elsevier, 337-405. · Zbl 0913.03053
[6] Birkedal, L., Møgelberg, R. E., Schwinghammer, J. and Støvring, K. (2012). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science8 (4) 1-45. · Zbl 1269.03035
[7] Blackburn, P., De Rijke, M. and Venema, Y. (2002). Modal Logic, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press.
[8] Blumensath, A. (2013). An algebraic proof of Rabin’s Tree Theorem. Theoretical Computer Science4781-21. · Zbl 1283.68222
[9] Börger, E., Grädel, E. and Gurevich, Y. (1997). The Classical Decision Problem, Perspectives in Mathematical Logic, Springer. · Zbl 0865.03004
[10] Bucciarelli, A. and Ehrhard, T. (1993). A Theory of Sequentiality. Theoretical Computer Science113 (2) 273-291. · Zbl 0779.68056
[11] Büchi, J. R. and Landweber, L. H. (1969). Solving sequential conditions by finite-state strategies. Transaction of the American Mathematical Society138367-378.
[12] Carayol, A. and Löding, C. (2007). MSO on the infinite binary tree: choice and order. In CSL, Lecture Notes in Computer Science, vol. 4646, Berlin, Heidelberg, Springer, 161-176. · Zbl 1179.03016
[13] Carayol, A., Löding, C., Niwinski, D. and Walukiewicz, I. (2010) Choice functions and well-orderings over the infinite binary tree. Central European Journal of Mathematics8 (4) 662-682. · Zbl 1215.03054
[14] Colcombet, T. and Löding, C. (2008). The non-deterministic Mostowski Hierarchy and distance-parity automata. In ICALP 2008, Lecture Notes in Computer Science, vol. 5126, Berlin, Heidelberg, Springer, 398-409. · Zbl 1165.68038
[15] De Paiva, V. (1991) The Dialectica categories. Technical Report 213, University of Cambridge Computer Laboratory. · Zbl 0675.03039
[16] Emerson, E. A. and Jutla, C. S. (1991) Tree automata, Mu-Calculus and determinacy (extended abstract). In FOCS, Washington, DC, IEEE Computer Society, 368-377.
[17] Facchini, A., Murlak, F. and Skrzypczak, M. (2013) Rabin-Mostowski index problem: a step beyond deterministic automata. In LICS, Washington, DC, IEEE Computer Society, 499-508. · Zbl 1366.68142
[18] Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science501-102.
[19] Girard, J.-Y., Lafont, Y. and Taylor, P. (1989). Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge, Cambridge University Press. · Zbl 0671.68002
[20] Grädel, E., Thomas, W. and Wilke, T. (eds.) (2002). Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science, vol. 2500, Berlin, Heidelberg, Springer-Verlag. · Zbl 1011.00037
[21] Gurevich, Y. and Harrington, L. (1982). Trees, automata, and games. In: STOC, ACM, 60-65.
[22] Gurevich, Y. and Shelah, S. (1983). Rabin’s Uniformization Problem. Journal of Symbolic Logic48 (4) 1105-1119. · Zbl 0537.03007
[23] Harmer, R., Hyland, M. and Melliès, P.-A. (2007). Categorical combinatorics for innocent strategies. In LICS 2007, Washington, DC, IEEE Computer Society, 379-388.
[24] Hirschowitz, T. and Pous, D. (2012). Innocent strategies as presheaves and interactive equivalences for CCS. Scientific Annals of Computer Science22 (1) 147-199. · Zbl 1424.68103
[25] Hofstra, P. J. W. (2011) The dialectica monad and its cousins. In: Makkai, M. and Hart, B.T. (eds.) Models, Logics, and Higher-dimensional Categories: A Tribute to the Work of Mihály Makkai, CRM Proceedings & Lecture Notes, Providence, RI, American Mathematical Society. · Zbl 1243.03074
[26] Hyland, J. M. E. (1997). Game semantics. In: Pitts, A. M. and Dybjer, P. (eds.) Semantics and Logics of Computation, Publications of the Newton Institute, vol. 14, Cambridge, Cambridge University Press, 131. · Zbl 0919.68084
[27] Hyland, J. M. E. (2002). Proof theory in the abstract. Annals of Pure and Applied Logic114 (1-3) 43-78. · Zbl 1007.03056
[28] Hyland, J. M. E. and Ong, C.-H. (2000). On full abstraction for PCF: I, II, and III. Information and Computation163 (2) 285-408. · Zbl 1006.68027
[29] Hyland, J. M. E. and Schalk, A. (1999). Abstract games for linear logic. Electronic Notes in Theoretical Computer Science29127-150. · Zbl 0959.03507
[30] Hyland, J. M. E. and Schalk, A. (2003). Glueing and orthogonality for models of linear logic. Theoretical Computer Science294 (1/2) 183-231. · Zbl 1029.03051
[31] Jacobs, B. (2001). Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics. Amsterdam, Elsevier. · Zbl 0911.03001
[32] Johnstone, P. T. (1986). Stone Spaces, Cambridge Studies in Advanced Mathematics, Cambridge, Cambridge University Press.
[33] Jutla, C. S. (1997). Determinization and memoryless winning strategies. Information and Computation133 (2) 117-134. · Zbl 0887.68071
[34] Klarlund, N. (1994). Progress measures, immediate determinacy, and a subset construction for tree automata. Annals of Pure and Applied Logic69 (2-3) 243-268. · Zbl 0821.68084
[35] Klarlund, N. and Kozen, D. (1995). Rabin measures. Chicago Journal of Theoretical Computer Science. http://cjtcs.cs.uchicago.edu/articles/1995/3/selfcitation.bib. · Zbl 0924.68142
[36] Kohlenbach, U. (2008). Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer Monographs in Mathematics, Berlin, Heidelberg, Springer-Verlag. · Zbl 1158.03002
[37] Kupferman, O. and Vardi, M. Y. (2005). Safraless decision procedures. In: Proceedings of FOCS’05, Washington, DC, USA, 2005, IEEE Computer Society, 531-542.
[38] Lambek, J. and Scott, P. J. (1986). Introduction to Higher Order Categorical Logic, Cambridge, CUP. · Zbl 0596.03002
[39] Mac Lane, S. (1998). Categories for the Working Mathematician, 2nd edn., New York, Springer-Verlag. · Zbl 0906.18001
[40] Maillard, K. and Melliès, P.-A. (2015). A fibrational account of local states. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, Computer Society, 402-413. · Zbl 1395.18003
[41] Mcnaughton, R. (1966). Testing and generating infinite sequences by a finite automaton. Information and Control9 (5) 521-530. · Zbl 0212.33902
[42] Melliès, P.-A. (2004). Comparing hierarchies of types in models of linear logic. Information and Computation189 (2) 202-234. · Zbl 1052.03038
[43] Melliès, P.-A. (2005). Sequential algorithms and strongly stable functions. Theoretical Computer Science343 (1-2) 237-281. · Zbl 1121.68024
[44] Melliès, P.-A. (2006). Asynchronous games 2: the true concurrency of innocence. Theoretical Computer Science358 (2-3) 200-228. · Zbl 1099.68072
[45] Melliès, P.-A. (2009). Categorical semantics of linear logic. In: Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses, vol. 27, SMF. · Zbl 1206.03052
[46] Melliès, P.-A. (2013). On dialogue games and coherent strategies. In: CSL, LIPIcs, vol. 23, Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 540-562. · Zbl 1356.03075
[47] Melliès, P.-A. (2017). Higher-order parity automata. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, Washington, DC, IEEE Computer Society, 1-12. · Zbl 1457.68145
[48] Melliès, P.-A., Tabareau, N. and Tasson, C. (2009). An explicit formula for the free exponential modality of linear logic. In: Proceedings of ICALP’09, Lecture Notes in Computer Science, vol. 5556, Berlin, Heidelberg, Springer, 247-260. · Zbl 1248.03080
[49] Möllerfeld, M. (2002). Generalized Inductive Definitions - The μ-Calculus and Π_1^2-Comprehension. PhD thesis, Westfälischen Wilhelms-Universität Münster. https://miami.uni-muenster.de/Record/9dfa74b6-186b-4e95-a51f-9965d7e1e508. · Zbl 1050.03040
[50] Muller, D. E. and Schupp, P. E. (1987). Alternating automata on infinite trees. Theoretical Computer Science54267-276. · Zbl 0636.68108
[51] Muller, D. E. and Schupp, P. E. (1995). Simulating alternating tree automata by nondeterministic automata: new results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science141 (1&2) 69-107. · Zbl 0873.68135
[52] Ong, C.-H. L. (2006). On model-checking trees generated by higher-order recursion schemes. In: Proceedings of LICS’06, Washington, DC, IEEE Computer Society, 81-90.
[53] Perrin, D. and Pin, J.-É. (2004). Infinite Words: Automata, Semigroups, Logic and Games, Pure and Applied Mathematics, Amsterdam, Elsevier. · Zbl 1094.68052
[54] Pradic, P. and Riba, C. (2017). A Curry-Howard approach to Church’s synthesis. In: Proceedings of FSCD’17, LIPIcs, vol. 84, Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 30:1-30:16. · Zbl 1509.03121
[55] Pradic, P. and Riba, C. (2018). LMSO: a Curry-Howard approach to Church’s synthesis via linear logic. In LICS, New York, NY, ACM, 849-858. · Zbl 1453.03070
[56] Pradic, P. and Riba, C. (2019). A Dialectica-like interpretation of a linear MSO on infinite words. In FoSSaCS, Cham, Springer. · Zbl 1429.03214
[57] Rabin, M. O. (1969). Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society1411-35.
[58] Rabin, M. O. (1972). Automata on Infinite Objects and Church’s Problem, American Mathematical Society. · Zbl 0315.02037
[59] Riba, C. (2015). Fibrations of tree automata. In: TLCA, LIPIcs, vol. 38, Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 302-316. · Zbl 1367.68206
[60] Riba, C. (2018). Monoidal-Closed Categories of Tree Automata. Available on HAL (hal-01261183) https://hal.archives-ouvertes.fr/hal-01261183. · Zbl 1435.68183
[61] Santocanale, L. and Arnold, A. (2005). Ambiguous classes in mu-calculi hierarchies. Theoretical Computer Science333(1-2) 265-296. · Zbl 1070.68077
[62] Sørensen, M. H. and Urzyczyn, P. (2006). Lectures on the Curry-Howard Isomorphism, Studies in Logic and the Foundations of Mathematics, vol. 149, Amsterdam, Elsevier Science Inc. · Zbl 1183.03004
[63] Thomas, W. (1997). Languages, automata, and logic. In: Rozenberg, G. and Salomaa, A. (eds.) Handbook of Formal Languages, vol. III, Berlin, Heidelberg, Springer-Verlag, 389-455.
[64] Tsukada, T. and Ong, C.-H. L. (2015). Nondeterminism in game semantics via sheaves. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, Washington, DC, IEEE Computer Society, 220-231. · Zbl 1401.68177
[65] Vardi, M. Y. and Wilke, T. (2008). Automata: from logics to algorithms. In: Logic and Automata, Texts in Logic and Games, vol. 2, Amsterdam, Amsterdam University Press, 629-736. · Zbl 1234.03026
[66] Walukiewicz, I. (2002). Monadic second-order logic on tree-like structures. Theoretical Computer Science275(1-2) 311-346. · Zbl 1026.68087
[67] Zielonka, Z. (1998). Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science200(1-2) 135-183. · Zbl 0915.68120
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.