Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-11-28T03:03:37.690Z Has data issue: false hasContentIssue false
  • English
  • Français

Monoidal-closed categories of tree automata

Published online by Cambridge University Press:  25 February 2020

Colin Riba
Colin Riba*
Affiliation:
Université de Lyon, EnsL, UCBL, LIP, F-69342, LYON Cedex 07, France
*
Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Keywords

Automata on infinite treesmonadic second-order logiclinear logiccurry-Howard correspondencecategorical logic
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 30 , Issue 1 , January 2020 , pp. 62 - 117
Copyright
© Cambridge University Press 2020 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

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.Google Scholar
Amadio, R. M. and Curien, P.-L. (1998). Domains and Lambda-Calculi, Cambridge Tracts in Theoretical Computer Science, Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Arnold, A. and Niwinski, D. (2007). Continuous Separation of Game Languages. Fundamenta Informaticae 81 (1–3) 19–28.Google Scholar
Arnold, A. (1999). The μ-calculus alternation-depth hierarchy is strict on binary trees. ITA 33 (4/5) 329–340.Google Scholar
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.CrossRefGoogle Scholar
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 Science 8 (4) 1–45.CrossRefGoogle Scholar
Blackburn, P., de Rijke, M. and Venema, Y. (2002). Modal Logic, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press.Google Scholar
Blumensath, A. (2013). An algebraic proof of Rabin’s Tree Theorem. Theoretical Computer Science 478 1–21.CrossRefGoogle Scholar
Börger, E., Grädel, E. and Gurevich, Y. (1997). The Classical Decision Problem, Perspectives in Mathematical Logic, Springer.CrossRefGoogle Scholar
Bucciarelli, A. and Ehrhard, T. (1993). A Theory of Sequentiality. Theoretical Computer Science 113 (2) 273–291.CrossRefGoogle Scholar
Büchi, J. R. and Landweber, L. H. (1969). Solving sequential conditions by finite-state strategies. Transaction of the American Mathematical Society 138 367–378.CrossRefGoogle Scholar
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.Google Scholar
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 Mathematics 8 (4) 662–682.Google Scholar
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.Google Scholar
de Paiva, V. (1991) The Dialectica categories. Technical Report 213, University of Cambridge Computer Laboratory.Google Scholar
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.Google Scholar
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.Google Scholar
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50 1–102.CrossRefGoogle Scholar
Girard, J.-Y., Lafont, Y. and Taylor, P. (1989). Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge, Cambridge University Press.Google Scholar
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.CrossRefGoogle Scholar
Gurevich, Y. and Harrington, L. (1982). Trees, automata, and games. In: STOC, ACM, 60–65.Google Scholar
Gurevich, Y. and Shelah, S. (1983). Rabin’s Uniformization Problem. Journal of Symbolic Logic 48 (4) 1105–1119.CrossRefGoogle Scholar
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.Google Scholar
Hirschowitz, T. and Pous, D. (2012). Innocent strategies as presheaves and interactive equivalences for CCS. Scientific Annals of Computer Science 22 (1) 147–199.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
Hyland, J. M. E. (2002). Proof theory in the abstract. Annals of Pure and Applied Logic 114 (1–3) 43–78.CrossRefGoogle Scholar
Hyland, J. M. E. and Ong, C.-H. (2000). On full abstraction for PCF: I, II, and III. Information and Computation 163 (2) 285–408.CrossRefGoogle Scholar
Hyland, J. M. E. and Schalk, A. (1999). Abstract games for linear logic. Electronic Notes in Theoretical Computer Science 29 127–150.CrossRefGoogle Scholar
Hyland, J. M. E. and Schalk, A. (2003). Glueing and orthogonality for models of linear logic. Theoretical Computer Science 294 (1/2) 183–231.CrossRefGoogle Scholar
Jacobs, B. (2001). Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics. Amsterdam, Elsevier.Google Scholar
Johnstone, P. T. (1986). Stone Spaces, Cambridge Studies in Advanced Mathematics, Cambridge, Cambridge University Press.Google Scholar
Jutla, C. S. (1997). Determinization and memoryless winning strategies. Information and Computation 133 (2) 117–134.CrossRefGoogle Scholar
Klarlund, N. (1994). Progress measures, immediate determinacy, and a subset construction for tree automata. Annals of Pure and Applied Logic 69 (2–3) 243–268.CrossRefGoogle Scholar
Klarlund, N. and Kozen, D. (1995). Rabin measures. Chicago Journal of Theoretical Computer Science. http://cjtcs.cs.uchicago.edu/articles/1995/3/selfcitation.bib.Google Scholar
Kohlenbach, U. (2008). Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer Monographs in Mathematics, Berlin, Heidelberg, Springer-Verlag.Google Scholar
Kupferman, O. and Vardi, M. Y. (2005). Safraless decision procedures. In: Proceedings of FOCS’05, Washington, DC, USA, 2005, IEEE Computer Society, 531–542.Google Scholar
Lambek, J. and Scott, P. J. (1986). Introduction to Higher Order Categorical Logic, Cambridge, CUP.Google Scholar
Mac Lane, S. (1998). Categories for the Working Mathematician, 2nd edn., New York, Springer-Verlag.Google Scholar
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.Google Scholar
McNaughton, R. (1966). Testing and generating infinite sequences by a finite automaton. Information and Control 9 (5) 521–530.CrossRefGoogle Scholar
Melliès, P.-A. (2004). Comparing hierarchies of types in models of linear logic. Information and Computation 189 (2) 202–234.CrossRefGoogle Scholar
Melliès, P.-A. (2005). Sequential algorithms and strongly stable functions. Theoretical Computer Science 343 (1–2) 237–281.CrossRefGoogle Scholar
Melliès, P.-A. (2006). Asynchronous games 2: the true concurrency of innocence. Theoretical Computer Science 358 (2–3) 200–228.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
Möllerfeld, M. (2002). Generalized Inductive Definitions - The μ-Calculus and Π12-Comprehension. PhD thesis, Westfälischen Wilhelms-Universität Münster. https://miami.uni-muenster.de/Record/9dfa74b6-186b-4e95-a51f-9965d7e1e508.Google Scholar
Muller, D. E. and Schupp, P. E. (1987). Alternating automata on infinite trees. Theoretical Computer Science 54 267–276.CrossRefGoogle Scholar
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 Science 141 (1&2) 69–107.CrossRefGoogle Scholar
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.Google Scholar
Perrin, D. and Pin, J.-É. (2004). Infinite Words: Automata, Semigroups, Logic and Games, Pure and Applied Mathematics, Amsterdam, Elsevier.Google Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
Pradic, P. and Riba, C. (2019). A Dialectica-like interpretation of a linear MSO on infinite words. In FoSSaCS, Cham, Springer.Google Scholar
Rabin, M. O. (1969). Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 141 1–35.Google Scholar
Rabin, M. O. (1972). Automata on Infinite Objects and Church’s Problem, American Mathematical Society.Google Scholar
Riba, C. (2015). Fibrations of tree automata. In: TLCA, LIPIcs, vol. 38, Dagstuhl, Germany, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 302–316.Google Scholar
Riba, C. (2018). Monoidal-Closed Categories of Tree Automata. Available on HAL (hal-01261183) https://hal.archives-ouvertes.fr/hal-01261183.Google Scholar
Santocanale, L. and Arnold, A. (2005). Ambiguous classes in mu-calculi hierarchies. Theoretical Computer Science 333(1–2) 265–296.CrossRefGoogle Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
Walukiewicz, I. (2002). Monadic second-order logic on tree-like structures. Theoretical Computer Science 275(1–2) 311–346.CrossRefGoogle Scholar
Zielonka, Z. (1998). Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1–2) 135–183.CrossRefGoogle Scholar